[%] Lean 고수 구합니다

[익명(223.39)]

section open classical example : ¬ (A ↔ ¬ A) := have hn : (A ∨ ¬ A), from sorry, assume h : (A ↔ ¬ A), show false, from or.elim hn (assume h1 : A, h.mp h1 h1) (assume h2 : ¬ A, h2 (h.mpr h2)) end

이거 증명 도와주실 수 있으신 분 있나요?ㅠㅠ 

언어는 Lean 입니다

배중률 관련 문제고, 문제에서는 by_contradiction을 쓰라고 하는데 감이 안잡히네요

[익명(220.70)]

exclusive middle -> double negation elimination 검색

[익명(223.39)]

¬¬A랑 A를 다른걸로 치던데요...

[익명(223.39)]

아 그걸 증명하란 소린가요? 시도해 보겠습니다

[익명(223.39)]

모르겠으면 일단 library_search, suggest

[익명(223.39)]

배중률 자체가 공리로 되어 있으니 검색하는게 빠름

[익명(223.39)]

또 다른 편법은 simp 쓰고 바깥쪽에다 set_option trace.simplify true 먹이기

[익명(223.39)]

sorry 부분에 by_contradiction 써서도 가능하긴 한데 증명이 좀 길어질거임