brozek/website
1
0
Fork 0
mirror of https://github.com/Brandon-Rozek/website.git synced 2024-11-25 09:36:31 -05:00
Code Issues Projects Releases Packages Wiki Activity

Mentions Classical.em

Browse source
This commit is contained in:
Brandon Rozek 2024-03-17 23:31:59 -04:00
parent 09b75a543b
commit 16f621fa0f
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
1 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
content/blog/lean4-tutorial.md
View file

@ -128,9 +128,14 @@ This allows them to export proofs as programs in OCaml.
Lean places less of an emphasis on this approach and instead supports the proof by contradiction style Lean places less of an emphasis on this approach and instead supports the proof by contradiction style
you see in classical theorem proving. you see in classical theorem proving.
During the tutorial, I decided to make this distinction explicit by making use of the law of excluded middle. By default, Lean uses the axiom of choice which can then be used to derive the law of excluded middle, but I cut that part out for brevity. For this tutorial, I decided to make this distinction
explicit by declaring a new axiom for the law of
excluded middle.
By default, Lean has the axiom of choice which
they use to prove the law of excluded middle
through the proof `Classical.em`.
In other words, if you want to perform a proof by contradiction, don't use the techniques shown in this section and instead use the `by_contra` tactic. In other words, if you want to perform a proof by contradiction, don't use the techniques shown in this section and instead use the `by_contra` tactic or directly use `Classical.em`.
Declare the axiom of law of excluded middle: Declare the axiom of law of excluded middle: