Created
January 31, 2025 08:14
-
-
Save illusory0x0/703bad1fd5098c1fc01785e655717d8a to your computer and use it in GitHub Desktop.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* | |
| 用 Gallina 重写的一个版本 | |
| ref: Tactics Version | |
| Coq里的排中律 - 遇到困难睡大觉的文章 - 知乎 | |
| https://zhuanlan.zhihu.com/p/361454504 | |
| *) | |
| Definition excluded_middle_irrefutable : | |
| forall P : Prop, (P \/ (P -> False) -> False) -> False | |
| := | |
| fun A H => | |
| let H' : A -> False := | |
| fun x => H (or_introl x) | |
| in | |
| H (or_intror H'). | |
| Definition excluded_middle_irrefutable' : | |
| forall (P:Prop), | |
| ~ ~ (P \/ ~ P) | |
| := | |
| fun A H => | |
| let H' : A -> False := | |
| fun x => H (or_introl x) | |
| in | |
| H (or_intror H'). |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment