Timeline for In Lean, why is it possible to prove $\text{succ}\; x \neq 0$ without adding it as an axiom?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 14, 2023 at 11:00 | comment | added | It'sNotALie. |
In lean4, you can use fun h => nomatch h or (some Std extensions) fun h => match h with./fun. to achieve what . did in Lean3
|
|
| Dec 13, 2023 at 6:59 | comment | added | Andrej Bauer | Ok, I think this is a good 'user perspective" answer. The mathematician in me wants to see the proof done with bare hands, so I posted one. | |
| Dec 13, 2023 at 4:55 | history | edited | Jason Rute | CC BY-SA 4.0 |
added 336 characters in body
|
| Dec 13, 2023 at 4:41 | comment | added | Jason Rute | @AndrejBauer better now? The proof goes through noConfusion, but the reader can read the proof of noConfusion themselves or read the blog post on it. | |
| Dec 13, 2023 at 4:41 | history | edited | Jason Rute | CC BY-SA 4.0 |
Major rewrite for Lean 4
|
| Dec 13, 2023 at 3:52 | comment | added | Jason Rute |
It'sNotALie posted the proof, and I answered the question behind the question which is what is going on underneath the surface in Lean. I assume that is what the OP intended to ask. But since It'sNotALie's one-character proof only works for Lean 3, I'll update my answer with some Lean 4 specific stuff including what is probably the "right" proof now: by simp.
|
|
| Dec 12, 2023 at 23:27 | comment | added | Andrej Bauer | Why is this answer accepted? I do not see a proof that $0 \neq 1$ follows from the induction principle. | |
| Aug 22, 2022 at 13:09 | vote | accept | Craig Gidney | ||
| S Aug 22, 2022 at 2:29 | history | suggested | François G. Dorais | CC BY-SA 4.0 |
fix second constructor
|
| Aug 22, 2022 at 2:25 | review | Suggested edits | |||
| S Aug 22, 2022 at 2:29 | |||||
| Aug 21, 2022 at 22:30 | history | answered | Jason Rute | CC BY-SA 4.0 |