From 9f00207bb768895b937221be56f5b0dab18cc155 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 24 Jan 2024 16:39:45 +0000 Subject: [PATCH] NewLemma -> NewTheorem (global) and "x" -> /-- x -/ (in tutorial and addition) --- Game/Levels/Addition/L01zero_add.lean | 11 +++++++---- Game/Levels/Addition/L02succ_add.lean | 4 +++- Game/Levels/Addition/L03add_comm.lean | 2 +- Game/Levels/Addition/L04add_assoc.lean | 7 +++++-- Game/Levels/Addition/L05add_right_comm.lean | 7 ++++--- Game/Levels/Algorithm/L05pred.lean | 2 +- Game/Levels/Algorithm/L06is_zero.lean | 2 +- Game/Levels/Implication/L04succ_inj.lean | 2 +- Game/Levels/Implication/L09zero_ne_succ.lean | 2 +- Game/Levels/LessOrEqual/Level_1.lean | 2 +- Game/Levels/Multiplication/L01mul_one.lean | 2 +- Game/Levels/Power/L01zero_pow_zero.lean | 2 +- Game/Levels/Power/L02zero_pow_succ.lean | 2 +- Game/Levels/Tutorial/L03two_eq_ss0.lean | 2 +- Game/Levels/Tutorial/L05add_zero.lean | 15 +++++++++------ Game/Levels/Tutorial/L07add_succ.lean | 4 ++-- 16 files changed, 40 insertions(+), 28 deletions(-) diff --git a/Game/Levels/Addition/L01zero_add.lean b/Game/Levels/Addition/L01zero_add.lean index a4ac6b6..1ebda52 100644 --- a/Game/Levels/Addition/L01zero_add.lean +++ b/Game/Levels/Addition/L01zero_add.lean @@ -30,11 +30,13 @@ will ask us to show that if `0 + d = d` then `0 + succ d = succ d`. Because See if you can do your first induction proof in Lean. " -TheoremDoc MyNat.zero_add as "zero_add" in "+" " +/-- `zero_add x` is the proof of `0 + x = x`. `zero_add` is a `simp` lemma, because replacing `0 + x` by `x` -is almost always what you want to do if you're simplifying an expression." +is almost always what you want to do if you're simplifying an expression. +-/ +TheoremDoc MyNat.zero_add as "zero_add" in "+" /-- For all natural numbers $n$, we have $0 + n = n$. -/ Statement zero_add (n : ℕ) : 0 + n = n := by @@ -61,7 +63,7 @@ Statement zero_add (n : ℕ) : 0 + n = n := by attribute [simp] zero_add -TacticDoc induction " +/-- ## Summary If `n : ℕ` is an object, and the goal mentions `n`, then `induction n with d hd` @@ -96,4 +98,5 @@ Conclusion `add_zero` and `zero_add`! Let's continue on our journey to `add_comm`, the proof of `x + y = y + x`. -" +-/ +TacticDoc induction diff --git a/Game/Levels/Addition/L02succ_add.lean b/Game/Levels/Addition/L02succ_add.lean index 09066bc..8a51965 100644 --- a/Game/Levels/Addition/L02succ_add.lean +++ b/Game/Levels/Addition/L02succ_add.lean @@ -16,8 +16,10 @@ we have the problem that we are adding `b` to things, so we need to use induction to split into the cases where `b = 0` and `b` is a successor. " +/-- +`succ_add a b` is a proof that `succ a + b = succ (a + b)`. +-/ TheoremDoc MyNat.succ_add as "succ_add" in "+" -"`succ_add a b` is a proof that `succ a + b = succ (a + b)`." /-- For all natural numbers $a, b$, we have diff --git a/Game/Levels/Addition/L03add_comm.lean b/Game/Levels/Addition/L03add_comm.lean index 65dfea0..c1122de 100644 --- a/Game/Levels/Addition/L03add_comm.lean +++ b/Game/Levels/Addition/L03add_comm.lean @@ -15,8 +15,8 @@ Look in your inventory to see the proofs you have available. These should be enough. " +/-- `add_comm x y` is a proof of `x + y = y + x`. -/ TheoremDoc MyNat.add_comm as "add_comm" in "+" -"`add_comm x y` is a proof of `x + y = y + x`." /-- On the set of natural numbers, addition is commutative. In other words, if `a` and `b` are arbitrary natural numbers, then diff --git a/Game/Levels/Addition/L04add_assoc.lean b/Game/Levels/Addition/L04add_assoc.lean index 154d908..027e31b 100644 --- a/Game/Levels/Addition/L04add_assoc.lean +++ b/Game/Levels/Addition/L04add_assoc.lean @@ -19,10 +19,13 @@ Introduction That's true, but we didn't prove it yet. Let's prove it now by induction. " -TheoremDoc MyNat.add_assoc as "add_assoc" in "+" "`add_assoc a b c` is a proof +/-- +`add_assoc a b c` is a proof that `(a + b) + c = a + (b + c)`. Note that in Lean `(a + b) + c` prints as `a + b + c`, because the notation for addition is defined to be left -associative. " +associative. +-/ +TheoremDoc MyNat.add_assoc as "add_assoc" in "+" /-- On the set of natural numbers, addition is associative. In other words, if $a, b$ and $c$ are arbitrary natural numbers, we have diff --git a/Game/Levels/Addition/L05add_right_comm.lean b/Game/Levels/Addition/L05add_right_comm.lean index fca65fe..a520787 100644 --- a/Game/Levels/Addition/L05add_right_comm.lean +++ b/Game/Levels/Addition/L05add_right_comm.lean @@ -23,11 +23,12 @@ will only do rewrites of the form `b + ? = ? + b`, and `rw [add_comm b c]` will only do rewrites of the form `b + c = c + b`. " -TheoremDoc MyNat.add_right_comm as "add_right_comm" in "+" -"`add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b`. +/-- `add_right_comm a b c` is a proof that `(a + b) + c = (a + c) + b` In Lean, `a + b + c` means `(a + b) + c`, so this result gets displayed -as `a + b + c = a + c + b`." +as `a + b + c = a + c + b`. +-/ +TheoremDoc MyNat.add_right_comm as "add_right_comm" in "+" /-- If $a, b$ and $c$ are arbitrary natural numbers, we have $(a + b) + c = (a + c) + b$. -/ diff --git a/Game/Levels/Algorithm/L05pred.lean b/Game/Levels/Algorithm/L05pred.lean index f7345ce..f5671be 100644 --- a/Game/Levels/Algorithm/L05pred.lean +++ b/Game/Levels/Algorithm/L05pred.lean @@ -35,7 +35,7 @@ TheoremDoc MyNat.pred_succ as "pred_succ" in "Peano" `pred_succ n` is a proof of `pred (succ n) = n`. " -NewLemma MyNat.pred_succ +NewTheorem MyNat.pred_succ /-- If $\operatorname{succ}(a)=\operatorname{succ}(b)$ then $a=b$. -/ Statement (a b : ℕ) (h : succ a = succ b) : a = b := by diff --git a/Game/Levels/Algorithm/L06is_zero.lean b/Game/Levels/Algorithm/L06is_zero.lean index a5b50aa..0726ce1 100644 --- a/Game/Levels/Algorithm/L06is_zero.lean +++ b/Game/Levels/Algorithm/L06is_zero.lean @@ -42,7 +42,7 @@ TheoremDoc MyNat.succ_ne_zero as "succ_ne_zero" in "Peano" `succ_ne_zero a` is a proof of `succ a ≠ 0`. " -NewLemma MyNat.is_zero_zero MyNat.is_zero_succ +NewTheorem MyNat.is_zero_zero MyNat.is_zero_succ TacticDoc triv " # Summary diff --git a/Game/Levels/Implication/L04succ_inj.lean b/Game/Levels/Implication/L04succ_inj.lean index 6733ef5..c184da9 100644 --- a/Game/Levels/Implication/L04succ_inj.lean +++ b/Game/Levels/Implication/L04succ_inj.lean @@ -47,7 +47,7 @@ in Lean it can be proved using `pred`, a mathematically pathological function. " -NewLemma MyNat.succ_inj +NewTheorem MyNat.succ_inj /-- If $x+1=4$ then $x=3$. -/ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by diff --git a/Game/Levels/Implication/L09zero_ne_succ.lean b/Game/Levels/Implication/L09zero_ne_succ.lean index d0a6a2a..1c77752 100644 --- a/Game/Levels/Implication/L09zero_ne_succ.lean +++ b/Game/Levels/Implication/L09zero_ne_succ.lean @@ -18,7 +18,7 @@ Here `False` is a generic false statement. This means that you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`. " -NewLemma MyNat.zero_ne_succ +NewTheorem MyNat.zero_ne_succ Introduction " As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to diff --git a/Game/Levels/LessOrEqual/Level_1.lean b/Game/Levels/LessOrEqual/Level_1.lean index 21163d4..57de2ee 100644 --- a/Game/Levels/LessOrEqual/Level_1.lean +++ b/Game/Levels/LessOrEqual/Level_1.lean @@ -67,7 +67,7 @@ Statement --one_add_le_self rfl NewTactic use -- ring -NewLemma MyNat.le_iff_exists_add +NewTheorem MyNat.le_iff_exists_add TheoremTab "Inequality" Conclusion "Now look at your proof. We're going to remove a line. diff --git a/Game/Levels/Multiplication/L01mul_one.lean b/Game/Levels/Multiplication/L01mul_one.lean index 9df96a6..f6832a3 100644 --- a/Game/Levels/Multiplication/L01mul_one.lean +++ b/Game/Levels/Multiplication/L01mul_one.lean @@ -42,7 +42,7 @@ TheoremDoc MyNat.mul_succ as "mul_succ" in "*" `mul_succ a b` is the proof that `a * succ b = a * b + a`. " -NewLemma MyNat.mul_zero MyNat.mul_succ +NewTheorem MyNat.mul_zero MyNat.mul_succ TheoremDoc MyNat.mul_one as "mul_one" in "*" " `mul_one m` is the proof that `m * 1 = m`. diff --git a/Game/Levels/Power/L01zero_pow_zero.lean b/Game/Levels/Power/L01zero_pow_zero.lean index 911ceea..0ab0164 100644 --- a/Game/Levels/Power/L01zero_pow_zero.lean +++ b/Game/Levels/Power/L01zero_pow_zero.lean @@ -34,7 +34,7 @@ TheoremDoc MyNat.pow_zero as "pow_zero" in "^" " defining exponentiation in this game. " -NewLemma MyNat.pow_zero +NewTheorem MyNat.pow_zero TheoremDoc MyNat.zero_pow_zero as "zero_pow_zero" in "^" " Mathematicians sometimes argue that `0 ^ 0 = 0` is also diff --git a/Game/Levels/Power/L02zero_pow_succ.lean b/Game/Levels/Power/L02zero_pow_succ.lean index 7d409d5..7bb411b 100644 --- a/Game/Levels/Power/L02zero_pow_succ.lean +++ b/Game/Levels/Power/L02zero_pow_succ.lean @@ -14,7 +14,7 @@ TheoremDoc MyNat.pow_succ as "pow_succ" in "^" " two axioms defining exponentiation in this game. " -NewLemma MyNat.pow_succ +NewTheorem MyNat.pow_succ TheoremDoc MyNat.zero_pow_succ as "zero_pow_succ" in "^" " Although $0^0=1$ in this game, $0^n=0$ if $n>0$, i.e., if diff --git a/Game/Levels/Tutorial/L03two_eq_ss0.lean b/Game/Levels/Tutorial/L03two_eq_ss0.lean index 24ae9aa..344c410 100644 --- a/Game/Levels/Tutorial/L03two_eq_ss0.lean +++ b/Game/Levels/Tutorial/L03two_eq_ss0.lean @@ -36,7 +36,7 @@ TheoremDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "012" "`four_eq_succ_three` is a proof of `4 = succ 3`." NewDefinition MyNat -NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two +NewTheorem MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two MyNat.four_eq_succ_three Introduction diff --git a/Game/Levels/Tutorial/L05add_zero.lean b/Game/Levels/Tutorial/L05add_zero.lean index 4facda6..7ce849b 100644 --- a/Game/Levels/Tutorial/L05add_zero.lean +++ b/Game/Levels/Tutorial/L05add_zero.lean @@ -24,8 +24,8 @@ NewDefinition Add TheoremTab "+" -TheoremDoc MyNat.add_zero as "add_zero" in "+" -"`add_zero a` is a proof that `a + 0 = a`. +/-- +`add_zero a` is a proof that `a + 0 = a`. ## Summary @@ -43,10 +43,12 @@ to input. A mathematician sometimes thinks of `add_zero` as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$. This is just another way of saying that it's a function which -can eat any number n and will return a proof that `n + 0 = n`." +can eat any number n and will return a proof that `n + 0 = n`. +-/ +TheoremDoc MyNat.add_zero as "add_zero" in "+" -TacticDoc «repeat» " +/-- ## Summary `repeat t` repeatedly applies the tactic `t` @@ -59,9 +61,10 @@ tactic, it just speeds things up sometimes. `a + 0 + (0 + (0 + 0)) = b + 0 + 0` into the goal `a = b`. -" +-/ +TacticDoc «repeat» -NewLemma MyNat.add_zero +NewTheorem MyNat.add_zero Introduction " diff --git a/Game/Levels/Tutorial/L07add_succ.lean b/Game/Levels/Tutorial/L07add_succ.lean index 167bf60..db13546 100644 --- a/Game/Levels/Tutorial/L07add_succ.lean +++ b/Game/Levels/Tutorial/L07add_succ.lean @@ -10,10 +10,10 @@ TheoremTab "012" namespace MyNat +/-- `add_succ a b` is the proof of `a + succ b = succ (a + b)`. -/ TheoremDoc MyNat.add_succ as "add_succ" in "+" -"`add_succ a b` is the proof of `a + succ b = succ (a + b)`." -NewLemma MyNat.add_succ +NewTheorem MyNat.add_succ TheoremDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "+" "`succ_eq_add_one n` is the proof that `succ n = n + 1`."