From 16f621fa0f93e6ed81126a12b74c08393c1511b6 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 17 Mar 2024 23:31:59 -0400 Subject: [PATCH] Mentions Classical.em --- content/blog/lean4-tutorial.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/content/blog/lean4-tutorial.md b/content/blog/lean4-tutorial.md index 741ba85..8cd2de9 100644 --- a/content/blog/lean4-tutorial.md +++ b/content/blog/lean4-tutorial.md @@ -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 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: