lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=
induction c with d hd,
rw add_zero, rw add_zero, refl,
rw add_succ, rw add_succ, rw add_succ, rw hd, refl,
이거 이케 풀었는데 걍 될때까지 rw rw rw 해도 되는거임..? proof complete 되긴했는데 솔직히 머릿속으로 그려가며 한게 아니고 될때까지 해본거라 제대로 하고 있는건지 모르겟음
왜 ⊢ a + b + 0 = a + (b + 0) 에서 rw add_zero 하면 a + b = a + (b + 0) 되는거야 "If h is a proof of X = Y, then rw h, will change all Xs in the goal to Ys." 면 바로 a + b = a + (b + 0) 되야 되는거 아냐? 내가 뭐 놓치는건가
*바로 a + b = a + (b) = a + b 되야
(a + b) + 0 = a + (b + 0) 에서 좌변은 add_zero (a+b) 고 우변은 add_zero b 임
우와! 나 theorem에 인자 줄 수있는지몰랏어
저게 원래는 add_zero m 같이 인자가 뭔지 명시해줘야 하는데, 매번 그러면 너무 귀찮으니까 인자 생략하면 expression 보고 추론해줌
쩐다 ㅎㄷㄷ
이....이기머노
유전 알고리즘으로 풀고있노...
induction c with d hd, rw add_zero, rw add_zero, refl, rw add_succ, rw add_succ, rw add_succ, rw hd, refl, 나이렇게함
나랑똑같단뜻
예아
근데 refl 할 때 normalization 할것 같은데. 첫번째 케이스 그냥 refl 만 하면 안됨?
되네... 여기서 normalization이라는게 정확히 머야
계산을 수행하는거. n + 0 은 '+'의 정의에 의해서 n으로 계산됨. 마찬가지로 m + suc n 은 +의 정의를 따라서 suc (m + n) 으로 계산됨
refl tactic은 좌변과 우변 각각을 normalize한 후에 같은지 비교하기 때문에 add_zero, add_succ 은 사실 필요 없음.
n + 0이 n 되는것도 add_zero 덕분에 그런거 아냐? add_zero니 zero_add니 한땀 한땀 구현할땐 언제고 갑자기 당연한거 아님? 해버리니까 당황스럽네..
게임 초반에 +는 ㅁㅁ이다 라고 정의한걸 내가 놓쳣나..
이전에 구한 theorem들은 자동으로 계산되는건감
게임은 안해봐서 모르겠는데, 만든 사람이 의도한건 add_zero theorem 써서 증명하는것일 수는 있어
n + 0 는 n으로 normalization 되지만, 0 + n 은 n으로 normalization 되지 않음. 왜냐면 +의 정의가 두번째 인자에 대헤서 재귀적으로 정의되어 있거든
와 근데 게임 해보지도 않고 normalization 될거라곤 어캐 안거임.. 통찰인가? 멋지다
통찰은 아니고 증명언어들끼리 다 비슷해서 그럼
그거 게임 내부 구현인줄 알았는데 + 설정 국룰 같은거라서 그렇게 유추된거임? ㅎㄷ
m + n 을 m에 대한 재귀로 정의하는지, n에 대한 재귀로 정의하는지에 따라서 사소한 차이가 있긴 한데, 그거 외로는 대부분 똑같은 정의 씀
멋있다 주딱