From fec40054766cd55eae5b3ee03260e728fc5c9969 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 13 Apr 2023 16:43:45 +0200 Subject: [PATCH] nng levels --- server/nng/NNG.lean | 8 +-- .../nng/NNG/Levels/AdvAddition/Level_1.lean | 40 ++++++++--- .../nng/NNG/Levels/AdvAddition/Level_10.lean | 64 ++++++++++++++++-- .../nng/NNG/Levels/AdvAddition/Level_11.lean | 19 ++++-- .../nng/NNG/Levels/AdvAddition/Level_12.lean | 18 +++-- .../nng/NNG/Levels/AdvAddition/Level_13.lean | 24 +++++-- .../nng/NNG/Levels/AdvAddition/Level_2.lean | 41 ++++++++++-- .../nng/NNG/Levels/AdvAddition/Level_3.lean | 18 +++-- .../nng/NNG/Levels/AdvAddition/Level_4.lean | 28 ++++++-- .../nng/NNG/Levels/AdvAddition/Level_5.lean | 26 +++++-- .../nng/NNG/Levels/AdvAddition/Level_6.lean | 20 ++++-- .../nng/NNG/Levels/AdvAddition/Level_7.lean | 25 +++++-- .../nng/NNG/Levels/AdvAddition/Level_8.lean | 21 ++++-- .../nng/NNG/Levels/AdvAddition/Level_9.lean | 22 ++++-- .../NNG/Levels/AdvMultiplication/Level_1.lean | 43 ++++++++++-- .../NNG/Levels/AdvMultiplication/Level_2.lean | 26 +++++-- .../NNG/Levels/AdvMultiplication/Level_3.lean | 29 ++++++-- .../NNG/Levels/AdvMultiplication/Level_4.lean | 51 ++++++++++++-- .../NNG/Levels/AdvProposition/Level_1.lean | 17 ++++- .../NNG/Levels/AdvProposition/Level_10.lean | 47 ++++++++++++- .../NNG/Levels/AdvProposition/Level_2.lean | 19 +++++- .../NNG/Levels/AdvProposition/Level_3.lean | 5 +- .../NNG/Levels/AdvProposition/Level_4.lean | 7 +- .../NNG/Levels/AdvProposition/Level_5.lean | 29 +++++++- .../NNG/Levels/AdvProposition/Level_6.lean | 14 +++- .../NNG/Levels/AdvProposition/Level_7.lean | 14 +++- .../NNG/Levels/AdvProposition/Level_8.lean | 18 ++++- .../NNG/Levels/AdvProposition/Level_9.lean | 39 ++++++++++- server/nng/NNG/Levels/Function/Level_9.lean | 10 ++- server/nng/NNG/Levels/Inequality.lean | 25 +++++++ server/nng/NNG/Levels/Inequality/Level_1.lean | 50 ++++++++++++-- .../nng/NNG/Levels/Inequality/Level_10.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_11.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_12.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_13.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_14.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_15.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_16.lean | 3 +- .../nng/NNG/Levels/Inequality/Level_17.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_2.lean | 16 +++-- server/nng/NNG/Levels/Inequality/Level_3.lean | 45 +++++++++++-- server/nng/NNG/Levels/Inequality/Level_4.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_5.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_6.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_7.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_8.lean | 3 +- server/nng/NNG/Levels/Inequality/Level_9.lean | 3 +- server/nng/NNG/Levels/Power.lean | 22 ++++++ server/nng/NNG/Levels/Power/Level_1.lean | 4 +- server/nng/NNG/Levels/Power/Level_4.lean | 1 + .../nng/NNG/Levels/Proposition/Level_1.lean | 58 +++++++++++++++- .../nng/NNG/Levels/Proposition/Level_2.lean | 46 ++++++++++++- .../nng/NNG/Levels/Proposition/Level_3.lean | 67 ++++++++++++++++++- .../nng/NNG/Levels/Proposition/Level_4.lean | 27 +++++++- .../nng/NNG/Levels/Proposition/Level_5.lean | 58 +++++++++++++++- .../nng/NNG/Levels/Proposition/Level_6.lean | 19 +++++- .../nng/NNG/Levels/Proposition/Level_7.lean | 15 ++++- .../nng/NNG/Levels/Proposition/Level_8.lean | 19 +++++- .../nng/NNG/Levels/Proposition/Level_9.lean | 14 +++- server/nng/NNG/Modifications/Tactics.lean | 4 +- server/nng/NNG/MyNat/AdvAddition.lean | 13 ++++ server/nng/NNG/MyNat/LE.lean | 18 +++++ server/nng/NNG/MyNat/Multiplication.lean | 2 + 63 files changed, 1121 insertions(+), 186 deletions(-) create mode 100644 server/nng/NNG/MyNat/AdvAddition.lean create mode 100644 server/nng/NNG/MyNat/LE.lean diff --git a/server/nng/NNG.lean b/server/nng/NNG.lean index f9dbac0..84d07b5 100644 --- a/server/nng/NNG.lean +++ b/server/nng/NNG.lean @@ -3,13 +3,13 @@ import GameServer.Commands import NNG.Levels.Tutorial import NNG.Levels.Addition import NNG.Levels.Multiplication -import NNG.Levels.Power +-- import NNG.Levels.Power import NNG.Levels.Function import NNG.Levels.Proposition import NNG.Levels.AdvProposition import NNG.Levels.AdvAddition import NNG.Levels.AdvMultiplication -import NNG.Levels.Inequality +-- import NNG.Levels.Inequality Game "NNG" Title "Natural Number Game" @@ -57,8 +57,8 @@ If you delete it, your progress will be lost! " Path Tutorial → Addition → Function → Proposition → AdvProposition → AdvAddition -Path AdvAddition → AdvMultiplication → Inequality +Path AdvAddition → AdvMultiplication -- → Inequality Path Addition → Multiplication → AdvMultiplication -Path Multiplication → Power +-- Path Multiplication → Power MakeGame diff --git a/server/nng/NNG/Levels/AdvAddition/Level_1.lean b/server/nng/NNG/Levels/AdvAddition/Level_1.lean index 411fd7b..622fcc9 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_1.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_1.lean @@ -1,24 +1,42 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 1 -Title "" +Title "`succ_inj`. A function." open MyNat Introduction " - +Peano's original collection of axioms for the natural numbers contained two further +assumptions, which have not yet been mentioned in the game: + +``` +succ_inj {a b : mynat} : + succ(a) = succ(b) → a = b + +zero_ne_succ (a : mynat) : + zero ≠ succ(a) + ``` + +The reason they have not been used yet is that they are both implications, +that is, +of the form $P\\implies Q$. This is clear for `succ_inj a b`, which +says that for all $a$ and $b$ we have $succ(a)=succ(b)\\implies a=b$. +For `zero_ne_succ` the trick is that $X\ne Y$ is *defined to mean* +$X = Y\\implies{\\tt false}$. If you have played through Proposition world, +you now have the required Lean skills (i.e., you know the required +tactics) to work with these implications. +Let's finally learn how to use `succ_inj`. You should know a couple +of ways to prove the below -- one directly using an `exact`, +and one which uses an `apply` first. But either way you'll need to use `succ_inj`. " -theorem MyNat.succ_inj {a b : ℕ} : succ a = succ b → a = b := by simp only [succ.injEq, imp_self] - -theorem MyNat.zero_ne_succ (a : ℕ) : zero ≠ succ a := by simp only [ne_eq, not_false_iff] - Statement -- MyNat.succ_inj' -"" +"For all naturals $a$ and $b$, if we assume $succ(a)=succ(b)$, then we can +deduce $a=b$." {a b : ℕ} (hs : succ a = succ b) : a = b := by exact succ_inj hs @@ -26,5 +44,11 @@ NewLemma MyNat.succ_inj MyNat.zero_ne_succ Conclusion " +## Important thing. +You can rewrite proofs of *equalities*. If `h : A = B` then `rw h` changes `A`s to `B`s. +But you *cannot rewrite proofs of implications*. `rw succ_inj` will *never work* +because `succ_inj` isn't of the form $A = B$, it's of the form $A\\implies B$. This is one +of the most common mistakes I see from beginners. $\\implies$ and $=$ are *two different things* +and you need to be clear about which one you are using. " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_10.lean b/server/nng/NNG/Levels/AdvAddition/Level_10.lean index f9f01c7..e591844 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_10.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_10.lean @@ -1,22 +1,74 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition +import NNG.MyNat.Multiplication Game "NNG" World "AdvAddition" Level 10 -Title "" +Title "add_left_eq_zero" open MyNat Introduction " +In Lean, `a ≠ b` is *defined to mean* `(a = b) → false`. +This means that if you see `a ≠ b` you can *literally treat +it as saying* `(a = b) → false`. Computer scientists would +say that these two terms are *definitionally equal*. +The following lemma, $a+b=0\\implies b=0$, will be useful in inequality world. +Let me go through the proof, because it introduces several new +concepts: + +* `cases b`, where `b : mynat` +* `exfalso` +* `apply succ_ne_zero` + +We're going to prove $a+b=0\\implies b=0$. Here is the +strategy. Each natural number is either `0` or `succ(d)` for +some other natural number `d`. So we can start the proof +with + +`cases b with d,` + +and then we have two goals, the case `b = 0` (which you can solve easily) +and the case `b = succ(d)`, which looks like this: + +``` +a d : mynat, +H : a + succ d = 0 +⊢ succ d = 0 +``` + +Our goal is impossible to prove. However our hypothesis `H` +is also impossible, meaning that we still have a chance! +First let's see why `H` is impossible. We can + +`rw add_succ at H,` + +to turn `H` into `H : succ (a + d) = 0`. Because +`succ_ne_zero (a + d)` is a proof that `succ (a + d) ≠ 0`, +it is also a proof of the implication `succ (a + d) = 0 → false`. +Hence `succ_ne_zero (a + d) H` is a proof of `false`! +Unfortunately our goal is not `false`, it's a generic +false statement. + +Recall however that the `exfalso` command turns any goal into `false` +(it's logically OK because `false` implies every proposition, true or false). +You can probably take it from here. " -Statement -"" - : true := by - trivial +Statement -- add_left_eq_zero +"If $a$ and $b$ are natural numbers such that +$$ a + b = 0, $$ +then $b = 0$." + {{a b : ℕ}} (H : a + b = 0) : b = 0 := by + induction b with d + rfl + rw [add_succ] at H + exfalso + apply succ_ne_zero (a + d) + exact H Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_11.lean b/server/nng/NNG/Levels/AdvAddition/Level_11.lean index b4d244e..526f92c 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_11.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_11.lean @@ -1,22 +1,29 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 11 -Title "" +Title "add_right_eq_zero" open MyNat +theorem MyNat.add_left_eq_zero {{a b : ℕ}} (H : a + b = 0) : b = 0 := by sorry + Introduction " - +We just proved `add_left_eq_zero (a b : mynat) : a + b = 0 → b = 0`. +Hopefully `add_right_eq_zero` shouldn't be too hard now. " Statement -"" - : true := by - trivial +"If $a$ and $b$ are natural numbers such that +$$ a + b = 0, $$ +then $a = 0$." + {a b : ℕ} : a + b = 0 → a = 0 := by + intro H + rw [add_comm] at H + exact add_left_eq_zero H Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_12.lean b/server/nng/NNG/Levels/AdvAddition/Level_12.lean index ddc0e06..a6df33c 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_12.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_12.lean @@ -1,22 +1,30 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 12 -Title "" +Title "add_one_eq_succ" open MyNat Introduction " +We have + * `succ_eq_add_one (n : mynat) : succ n = n + 1` + +but sometimes the other way is also convenient. " +theorem succ_eq_add_one (d : ℕ) : succ d = d + 1 := by sorry + Statement -"" - : true := by - trivial +"For any natural number $d$, we have +$$ d+1 = \\operatorname{succ}(d). $$" + (d : ℕ) : d + 1 = succ d := by + rw [succ_eq_add_one] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_13.lean b/server/nng/NNG/Levels/AdvAddition/Level_13.lean index 13250ec..663a292 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_13.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_13.lean @@ -1,22 +1,32 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 13 -Title "" +Title "ne_succ_self" open MyNat Introduction " - +The last level in Advanced Addition World is the statement +that $n\\not=\\operatorname{succ}(n)$. When you've done this +you've completed Advanced Addition World and can move on +to Advanced Multiplication World (after first doing +Multiplication World, if you didn't do it already). " -Statement -"" - : true := by - trivial +Statement --ne_succ_self +"For any natural number $n$, we have +$$ n \\neq \\operatorname{succ}(n). $$" + (n : ℕ) : n ≠ succ n := by + induction n with d hd + apply zero_ne_succ + intro hs + apply hd + apply succ_inj + assumption Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_2.lean b/server/nng/NNG/Levels/AdvAddition/Level_2.lean index 1d22594..dceae92 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_2.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_2.lean @@ -1,24 +1,53 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 2 -Title "" +Title "succ_succ_inj" open MyNat Introduction " - +In the below theorem, we need to apply `succ_inj` twice. Once to prove +$succ(succ(a))=succ(succ(b))\\implies succ(a)=succ(b)$, and then again +to prove $succ(a)=succ(b)\\implies a=b$. However `succ(a)=succ(b)` is +nowhere to be found, it's neither an assumption or a goal when we start +this level. You can make it with `have` or you can use `apply`. " Statement -"" - : true := by - trivial +"For all naturals $a$ and $b$, if we assume $succ(succ(a))=succ(succ(b))$, then we can +deduce $a=b$. " + {a b : ℕ} (h : succ (succ a) = succ ( succ b )) : a = b := by + apply succ_inj + apply succ_inj + assumption Conclusion " +## Sample solutions to this level. + +Make sure you understand them all. And remember that `rw` should not be used +with `succ_inj` -- `rw` works only with equalities or `↔` statements, +not implications or functions. + +example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) : a = b := +begin + apply succ_inj, + apply succ_inj, + exact h +end + +example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) : a = b := +begin + apply succ_inj, + exact succ_inj(h), +end +example {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) : a = b := +begin + exact succ_inj(succ_inj(h)), +end " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_3.lean b/server/nng/NNG/Levels/AdvAddition/Level_3.lean index 09185a8..8d8cc21 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_3.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_3.lean @@ -1,22 +1,28 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 3 -Title "" +Title "succ_eq_succ_of_eq" open MyNat Introduction " - +We are going to prove something completely obvious: if $a=b$ then +$succ(a)=succ(b)$. This is *not* `succ_inj`! +This is trivial -- we can just rewrite our proof of `a=b`. +But how do we get to that proof? Use the `intro` tactic. " Statement -"" - : true := by - trivial +"For all naturals $a$ and $b$, $a=b\\implies succ(a)=succ(b)$. +" + {a b : ℕ} : a = b → succ a = succ b := by + intro h + rw [h] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_4.lean b/server/nng/NNG/Levels/AdvAddition/Level_4.lean index 6973471..5fdad86 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_4.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_4.lean @@ -1,22 +1,40 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 4 -Title "" +Title "eq_iff_succ_eq_succ" open MyNat Introduction " +Here is an `iff` goal. You can split it into two goals (the implications in both +directions) using the `split` tactic, which is how you're going to have to start. +`split,` + +Now you have two goals. The first is exactly `succ_inj` so you can close +it with + +`exact succ_inj,` + +and the second one you could solve by looking up the name of the theorem +you proved in the last level and doing `exact `, or alternatively +you could get some more `intro` practice and seeing if you can prove it +using `intro`, `rw` and `refl`. " Statement -"" - : true := by - trivial +"Two natural numbers are equal if and only if their successors are equal. +" + (a b : ℕ) : succ a = succ b ↔ a = b := by + constructor + exact succ_inj + intro H + rw [H] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_5.lean b/server/nng/NNG/Levels/AdvAddition/Level_5.lean index c3b8b6f..d46fcba 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_5.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_5.lean @@ -1,22 +1,36 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 5 -Title "" +Title "add_right_cancel" open MyNat Introduction " - +The theorem `add_right_cancel` is the theorem that you can cancel on the right +when you're doing addition -- if `a + t = b + t` then `a = b`. After `intro h` +I'd recommend induction on `t`. Don't forget that `rw add_zero at h` can be used +to do rewriting of hypotheses rather than the goal. " Statement -"" - : true := by - trivial +"On the set of natural numbers, addition has the right cancellation property. +In other words, if there are natural numbers $a, b$ and $c$ such that +$$ a + t = b + t, $$ +then we have $a = b$." + (a t b : ℕ) : a + t = b + t → a = b := by + intro h + induction t with d hd + rw [add_zero] at h + rw [add_zero] at h + exact h + apply hd + rw [add_succ] at h + rw [add_succ] at h + exact succ_inj h Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_6.lean b/server/nng/NNG/Levels/AdvAddition/Level_6.lean index 72623d1..47f6332 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_6.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_6.lean @@ -1,22 +1,32 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 6 -Title "" +Title "add_left_cancel" open MyNat Introduction " +The theorem `add_left_cancel` is the theorem that you can cancel on the left +when you're doing addition -- if `t + a = t + b` then `a = b`. +There is a three-line proof which ends in `exact add_right_cancel a t b` (or even +`exact add_right_cancel _ _ _`); this +strategy involves changing the goal to the statement of `add_right_cancel` somehow. " Statement -"" - : true := by - trivial +"On the set of natural numbers, addition has the left cancellation property. +In other words, if there are natural numbers $a, b$ and $t$ such that +$$ t + a = t + b, $$ +then we have $a = b$." + (t a b : ℕ) : t + a = t + b → a = b := by + rw [add_comm] + rw [add_comm t] + exact add_right_cancel a t b Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_7.lean b/server/nng/NNG/Levels/AdvAddition/Level_7.lean index 1ef04a2..d17bdf1 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_7.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_7.lean @@ -1,23 +1,34 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 7 -Title "" +Title "add_right_cancel_iff" open MyNat Introduction " +It's sometimes convenient to have the \"if and only if\" version +of theorems like `add_right_cancel`. Remember that you can use `split` +to split an `↔` goal into the `→` goal and the `←` goal. -" +## Pro tip: -Statement -"" - : true := by - trivial +`exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\" +" +Statement --add_right_cancel_iff +"For all naturals $a$, $b$ and $t$, +$$ a + t = b + t\\iff a=b. $$ +" + (t a b : ℕ) : a + t = b + t ↔ a = b := by + constructor + exact add_right_cancel _ _ _ -- done that way already, + intro H -- H : a = b, + rw [H] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_8.lean b/server/nng/NNG/Levels/AdvAddition/Level_8.lean index 09a2200..ff5ffad 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_8.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_8.lean @@ -1,22 +1,29 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 8 -Title "" +Title "eq_zero_of_add_right_eq_self" open MyNat Introduction " - +The lemma you're about to prove will be useful when we want to prove that $\\leq$ is antisymmetric. +There are some wrong paths that you can take with this one. " -Statement -"" - : true := by - trivial +Statement --eq_zero_of_add_right_eq_self +"If $a$ and $b$ are natural numbers such that +$$ a + b = a, $$ +then $b = 0$." + {a b : ℕ} : a + b = a → b = 0 := by + intro h + apply add_left_cancel a + rw [h] + rw [add_zero] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/AdvAddition/Level_9.lean b/server/nng/NNG/Levels/AdvAddition/Level_9.lean index 6acbb8b..1563958 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_9.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_9.lean @@ -1,22 +1,32 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.AdvAddition Game "NNG" World "AdvAddition" Level 9 -Title "" +Title "succ_ne_zero" open MyNat Introduction " +Levels 9 to 13 introduce the last axiom of Peano, namely +that $0\\not=\\operatorname{succ}(a)$. The proof of this is called `zero_ne_succ a`. +`zero_ne_succ (a : mynat) : 0 ≠ succ(a)` + +The `symmetry` tactic will turn any goal of the form `R x y` into `R y x`, +if `R` is a symmetric binary relation (for example `=` or `≠`). +In particular, you can prove `succ_ne_zero` below by first using +`symmetry` and then `exact zero_ne_succ a`. " -Statement -"" - : true := by - trivial +Statement -- succ_ne_zero +"Zero is not the successor of any natural number." + (a : ℕ) : succ a ≠ 0 := by + apply Ne.symm + exact zero_ne_succ a + Conclusion " diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean index bb1d6fc..1efa887 100644 --- a/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_1.lean @@ -1,22 +1,55 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.Multiplication +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight Game "NNG" World "AdvMultiplication" Level 1 -Title "" +Title "mul_pos" open MyNat Introduction " +Welcome to Advanced Multiplication World! Before attempting this +world you should have completed seven other worlds, including +Multiplication World and Advanced Addition World. There are four +levels in this world. + +Recall that if `b : mynat` is a hypothesis and you do `cases b with n`, +your one goal will split into two goals, +namely the cases `b = 0` and `b = succ(n)`. So `cases` here is like +a weaker version of induction (you don't get the inductive hypothesis). + +## Tricks + +1) if your goal is `⊢ X ≠ Y` then `intro h` will give you `h : X = Y` and +a goal of `⊢ false`. This is because `X ≠ Y` *means* `(X = Y) → false`. +Conversely if your goal is `false` and you have `h : X ≠ Y` as a hypothesis +then `apply h` will turn the goal into `X = Y`. + +2) if `hab : succ (3 * x + 2 * y + 1) = 0` is a hypothesis and your goal is `⊢ false`, +then `exact succ_ne_zero _ hab` will solve the goal, because Lean will figure +out that `_` is supposed to be `3 * x + 2 * y + 1`. " Statement -"" - : true := by - trivial +"The product of two non-zero natural numbers is non-zero." + (a b : ℕ) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 := by + intro ha hb + intro hab + induction b with b + apply hb + rfl + rw [mul_succ] at hab + apply ha + induction a with a + rfl + rw [add_succ] at hab + exfalso + exact succ_ne_zero _ hab Conclusion " diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean index f1afe1b..1d78a7b 100644 --- a/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_2.lean @@ -1,22 +1,34 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.Multiplication +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight Game "NNG" World "AdvMultiplication" Level 2 -Title "" +Title "eq_zero_or_eq_zero_of_mul_eq_zero" open MyNat Introduction " - +A variant on the previous level. " -Statement -"" - : true := by - trivial +Statement -- eq_zero_or_eq_zero_of_mul_eq_zero +"If $ab = 0$, then at least one of $a$ or $b$ is equal to zero." + (a b : ℕ) (h : a * b = 0) : + a = 0 ∨ b = 0 := by + induction a with d + left + rfl + induction b with e he + right + rfl + exfalso + rw [mul_succ] at h + rw [add_succ] at h + exact succ_ne_zero _ h Conclusion " diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean index 33413e4..4f67dca 100644 --- a/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_3.lean @@ -1,22 +1,39 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.Multiplication +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight Game "NNG" World "AdvMultiplication" Level 3 -Title "" +Title "mul_eq_zero_iff" open MyNat Introduction " - +Now you have `eq_zero_or_eq_zero_of_mul_eq_zero` this is pretty straightforward. " +axiom eq_zero_or_eq_zero_of_mul_eq_zero (a b : ℕ) (h : a * b = 0) : a = 0 ∨ b = 0 +axiom zero_mul (a : ℕ) : 0 * a = 0 + Statement -"" - : true := by - trivial +"$ab = 0$, if and only if at least one of $a$ or $b$ is equal to zero. +" + (a b : ℕ): a * b = 0 ↔ a = 0 ∨ b = 0 := by + constructor + intro h + exact eq_zero_or_eq_zero_of_mul_eq_zero a b h + intro hab + rcases hab with hab | hab + rw [hab] + rw [zero_mul] + rfl + rw [hab] + rw [mul_zero] + rfl + Conclusion " diff --git a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean index fa3a204..0f8068f 100644 --- a/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean +++ b/server/nng/NNG/Levels/AdvMultiplication/Level_4.lean @@ -1,22 +1,63 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.Multiplication +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight Game "NNG" World "AdvMultiplication" Level 4 -Title "" +Title "mul_left_cancel" open MyNat Introduction " +This is the last of the bonus multiplication levels. +`mul_left_cancel` will be useful in inequality world. +People find this level hard. I have probably had more questions about this +level than all the other levels put together, in fact. Many levels in this +game can just be solved by \"running at it\" -- do induction on one of the +variables, keep your head, and you're done. In fact, if you like a challenge, +it might be instructive if you stop reading after the end of this paragraph and try solving this level now by induction, +seeing the trouble you run into, and reading the rest of these comments afterwards. This level +has a sting in the tail. If you are a competent mathematician, try +and figure out what is going on. Write down a maths proof of the +theorem in this level. Exactly what statement do you want to prove +by induction? It is subtle. + +Ok so here are some spoilers. The problem with naively running at it, is that if you try induction on, +say, $c$, then you are imagining a and b as fixed, and your inductive +hypothesis $P(c)$ is $ab=ac \\implies b=c$. So for your inductive step +you will be able to assume $ab=ad \\implies b=d$ and your goal will +be to show $ab=a(d+1) \\implies b=d+1$. When you also assume $ab=a(d+1)$ +you will realise that your inductive hypothesis is *useless*, because +$ab=ad$ is not true! The statement $P(c)$ (with $a$ and $b$ regarded +as constants) is not provable by induction. + +What you *can* prove by induction is the following *stronger* statement. +Imagine $a\not=0$ as fixed, and then prove \"for all $b$, if $ab=ac$ then $b=c$\" +by induction on $c$. This gives us the extra flexibility we require. +Note that we are quantifying over all $b$ in the inductive hypothesis -- it +is essential that $b$ is not fixed. + +You can do this in two ways in Lean -- before you start the induction +you can write `revert b,`. The `revert` tactic is the opposite of the `intro` +tactic; it replaces the `b` in the hypotheses with \"for all $b$\" in the goal. + +Alternatively, you can write `induction c with d hd +generalizing b` as the first line of the proof. + +If you do not modify your technique in this way, then this level seems +to be impossible (judging by the comments I've had about it!) " Statement -"" - : true := by - trivial +"If $a \\neq 0$, $b$ and $c$ are natural numbers such that +$ ab = ac, $ +then $b = c$." + (a b c : ℕ) (ha : a ≠ 0) : a * b = a * c → b = c := by + sorry Conclusion " diff --git a/server/nng/NNG/Levels/AdvProposition/Level_1.lean b/server/nng/NNG/Levels/AdvProposition/Level_1.lean index 10868a8..b3989db 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_1.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_1.lean @@ -4,17 +4,28 @@ import NNG.MyNat.Addition Game "NNG" World "AdvProposition" Level 1 -Title "" +Title "the `split` tactic" open MyNat Introduction " - +In this world we will learn five key tactics needed to solve all the +levels of the Natural Number Game, namely `split`, `cases`, `left`, `right`, and `exfalso`. +These, and `use` (which we'll get to in Inequality World) are all the +tactics you will need to beat all the levels of the game. + +## Level 1: the `split` tactic. + +The logical symbol `∧` means \"and\". If $P$ and $Q$ are propositions, then +$P\\land Q$ is the proposition \"$P$ and $Q$\". If your *goal* is `P ∧ Q` then +you can make progress with the `split` tactic, which turns one goal `⊢ P ∧ Q` +into two goals, namely `⊢ P` and `⊢ Q`. In the level below, after a `split`, +you will be able to finish off the goals with the `exact` tactic. " Statement -"" +"If $P$ and $Q$ are true, then $P\\land Q$ is true." (P Q : Prop) (p : P) (q : Q) : P ∧ Q := by constructor exact p diff --git a/server/nng/NNG/Levels/AdvProposition/Level_10.lean b/server/nng/NNG/Levels/AdvProposition/Level_10.lean index 1622db4..b83c69d 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_10.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_10.lean @@ -5,17 +5,54 @@ import Std.Tactic.RCases Game "NNG" World "AdvProposition" Level 10 -Title "" +Title "Level 10: the law of the excluded middle." open MyNat Introduction " +We proved earlier that `(P → Q) → (¬ Q → ¬ P)`. The converse, +that `(¬ Q → ¬ P) → (P → Q)` is certainly true, but trying to prove +it using what we've learnt so far is impossible (because it is not provable in +constructive logic). For example, after +``` +intro h, +intro p, +repeat {rw not_iff_imp_false at h}, +``` + +in the below, you are left with +``` +P Q : Prop, +h : (Q → false) → P → false +p : P +⊢ Q +``` + +The tools you have are not sufficient to continue. But you can just +prove this, and any other basic lemmas of this form like `¬ ¬ P → P`, +using the `by_cases` tactic. Instead of starting with all the `intro`s, +try this instead: + +`by_cases p : P; by_cases q : Q,` + +**Note the semicolon**! It means \"do the next tactic to all the goals, not just the top one\". +After it, there are four goals, one for each of the four possibilities PQ=TT, TF, FT, FF. +You can see that `p` is a proof of `P` in some of the goals, and a proof of `¬ P` in others. +Similar comments apply to `q`. + +`repeat {cc}` then finishes the job. + +This approach assumed that `P ∨ ¬ P` was true; the `by_cases` tactic just does `cases` on +this result. This is called the law of the excluded middle, and it cannot be proved just +using tactics such as `intro` and `apply`. " Statement -"" +"If $P$ and $Q$ are true/false statements, then +$$(\\lnot Q\\implies \\lnot P)\\implies(P\\implies Q).$$ +" (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by by_cases p : P · by_cases q : Q @@ -32,5 +69,11 @@ Statement Conclusion " +OK that's enough logic -- now perhaps it's time to go on to Advanced Addition World! +Get to it via the main menu. + +## Pro tip + +In fact the tactic `tauto!` just kills this goal (and many other logic goals) immediately. " diff --git a/server/nng/NNG/Levels/AdvProposition/Level_2.lean b/server/nng/NNG/Levels/AdvProposition/Level_2.lean index 86b3fb5..0e95056 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_2.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_2.lean @@ -5,19 +5,34 @@ import Std.Tactic.RCases Game "NNG" World "AdvProposition" Level 2 -Title "" +Title "the `cases` tactic" open MyNat Introduction " +If `P ∧ Q` is in the goal, then we can make progress with `split`. +But what if `P ∧ Q` is a hypothesis? In this case, the `cases` tactic will enable +us to extract proofs of `P` and `Q` from this hypothesis. +The lemma below asks us to prove `P ∧ Q → Q ∧ P`, that is, +symmetry of the \"and\" relation. The obvious first move is + +`intro h,` + +because the goal is an implication and this tactic is guaranteed +to make progress. Now `h : P ∧ Q` is a hypothesis, and + +`cases h with p q,` + +will change `h`, the proof of `P ∧ Q`, into two proofs `p : P` +and `q : Q`. From there, `split` and `exact` will get you home. " set_option tactic.hygienic false Statement --and_symm -"" +"If $P$ and $Q$ are true/false statements, then $P\\land Q\\implies Q\\land P$. " (P Q : Prop) : P ∧ Q → Q ∧ P := by intro h rcases h with ⟨p, q⟩ diff --git a/server/nng/NNG/Levels/AdvProposition/Level_3.lean b/server/nng/NNG/Levels/AdvProposition/Level_3.lean index 93336c1..05955ff 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_3.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_3.lean @@ -5,7 +5,7 @@ import Std.Tactic.RCases Game "NNG" World "AdvProposition" Level 3 -Title "" +Title "and_trans" open MyNat @@ -15,7 +15,8 @@ Introduction " Statement --and_trans -"" +"If $P$, $Q$ and $R$ are true/false statements, then $P\\land Q$ and +$Q\\land R$ together imply $P\\land R$." (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by intro hpq intro hqr diff --git a/server/nng/NNG/Levels/AdvProposition/Level_4.lean b/server/nng/NNG/Levels/AdvProposition/Level_4.lean index 01a84dd..efa59ed 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_4.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_4.lean @@ -11,11 +11,16 @@ open MyNat Introduction " +The mathematical statement $P\\iff Q$ is equivalent to $(P\\implies Q)\\land(Q\\implies P)$. The `cases` +and `split` tactics work on hypotheses and goals (respectively) of the form `P ↔ Q`. If you need +to write an `↔` arrow you can do so by typing `\\iff`, but you shouldn't need to. After an initial +`intro h,` you can type `cases h with hpq hqp` to break `h : P ↔ Q` into its constituent parts. " Statement --iff_trans -"" +"If $P$, $Q$ and $R$ are true/false statements, then +$P\\iff Q$ and $Q\\iff R$ together imply $P\\iff R$." (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by intro hpq intro hqr diff --git a/server/nng/NNG/Levels/AdvProposition/Level_5.lean b/server/nng/NNG/Levels/AdvProposition/Level_5.lean index 19e7421..fe11353 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_5.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_5.lean @@ -5,17 +5,42 @@ import Std.Tactic.RCases Game "NNG" World "AdvProposition" Level 5 -Title "" +Title "`iff_trans` easter eggs." open MyNat Introduction " +Let's try `iff_trans` again. Try proving it in other ways. +### A trick. + +Instead of using `cases` on `h : P ↔ Q` you can just access the proofs of `P → Q` and `Q → P` +directly with `h.1` and `h.2`. So you can solve this level with + +``` +intros hpq hqr, +split, +intro p, +apply hqr.1, +... +``` + +### Another trick + +Instead of using `cases` on `h : P ↔ Q`, you can just `rw h`, and this will change all `P`s to `Q`s +in the goal. You can use this to create a much shorter proof. Note that +this is an argument for *not* running the `cases` tactic on an iff statement; +you cannot rewrite one-way implications, but you can rewrite two-way implications. + +### Another trick + +`cc` works on this sort of goal too. " Statement --iff_trans -"" +"If $P$, $Q$ and $R$ are true/false statements, then `P ↔ Q` and `Q ↔ R` together imply `P ↔ R`. +" (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by intro hpq hqr constructor diff --git a/server/nng/NNG/Levels/AdvProposition/Level_6.lean b/server/nng/NNG/Levels/AdvProposition/Level_6.lean index 01ee698..7fda5db 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_6.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_6.lean @@ -7,17 +7,25 @@ import Mathlib.Tactic.LeftRight Game "NNG" World "AdvProposition" Level 6 -Title "" +Title "Or, and the `left` and `right` tactics." open MyNat Introduction " - +`P ∨ Q` means \"$P$ or $Q$\". So to prove it, you +need to choose one of `P` or `Q`, and prove that one. +If `⊢ P ∨ Q` is your goal, then `left` changes this +goal to `⊢ P`, and `right` changes it to `⊢ Q`. +Note that you can take a wrong turn here. Let's +start with trying to prove $Q\\implies (P\\lor Q)$. +After the `intro`, one of `left` and `right` leads +to an impossible goal, the other to an easy finish. " Statement -"" +"If $P$ and $Q$ are true/false statements, then +$$Q\\implies(P\\lor Q).$$ " (P Q : Prop) : Q → (P ∨ Q) := by intro q right diff --git a/server/nng/NNG/Levels/AdvProposition/Level_7.lean b/server/nng/NNG/Levels/AdvProposition/Level_7.lean index d6c77b4..250c2cc 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_7.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_7.lean @@ -6,17 +6,25 @@ import Mathlib.Tactic.LeftRight Game "NNG" World "AdvProposition" Level 7 -Title "" +Title "`or_symm`" open MyNat Introduction " - +Proving that $(P\\lor Q)\\implies(Q\\lor P)$ involves an element of danger. +`intro h,` is the obvious start. But now, +even though the goal is an `∨` statement, both `left` and `right` put +you in a situation with an impossible goal. Fortunately, after `intro h,` +you can do `cases h with p q`. Then something new happens: because +there are two ways to prove `P ∨ Q` (namely, proving `P` or proving `Q`), +the `cases` tactic turns one goal into two, one for each case. You should +be able to make it home from there. " Statement --or_symm -"" +"If $P$ and $Q$ are true/false statements, then +$$P\\lor Q\\implies Q\\lor P.$$ " (P Q : Prop) : P ∨ Q → Q ∨ P := by intro h rcases h with p | q diff --git a/server/nng/NNG/Levels/AdvProposition/Level_8.lean b/server/nng/NNG/Levels/AdvProposition/Level_8.lean index 983f507..b44f820 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_8.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_8.lean @@ -6,17 +6,21 @@ import Mathlib.Tactic.LeftRight Game "NNG" World "AdvProposition" Level 8 -Title "" +Title "`and_or_distrib_left`" open MyNat Introduction " - +We know that `x(y+z)=xy+xz` for numbers, and this +is called distributivity of multiplication over addition. +The same is true for `∧` and `∨` -- in fact `∧` distributes +over `∨` and `∨` distributes over `∧`. Let's prove one of these. " Statement --and_or_distrib_left -"" +"If $P$. $Q$ and $R$ are true/false statements, then +$$P\\land(Q\\lor R)\\iff(P\\land Q)\\lor (P\\land R).$$ " (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by constructor intro h @@ -45,5 +49,13 @@ Statement --and_or_distrib_left Conclusion " +## Pro tip + +Did you spot the import? What do you think it does? + +If you follow the instructions at +the mathlib github page +you will be able to install Lean and mathlib on your own system, and then you can create a new project +and experiment with such imports yourself. " diff --git a/server/nng/NNG/Levels/AdvProposition/Level_9.lean b/server/nng/NNG/Levels/AdvProposition/Level_9.lean index eb13d75..6ffa620 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_9.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_9.lean @@ -8,17 +8,30 @@ import NNG.MyNat.Theorems.Proposition Game "NNG" World "AdvProposition" Level 9 -Title "" +Title "`exfalso` and proof by contradiction. " open MyNat Introduction " +You already know enough to embark on advanced addition world. But here are just a couple +more things. + +## Level 9: `exfalso` and proof by contradiction. + +It's certainly true that $P\\land(\\lnot P)\\implies Q$ for any propositions $P$ +and $Q$, because the left hand side of the implication is false. But how do +we prove that `false` implies any proposition $Q$? A cheap way of doing it in +Lean is using the `exfalso` tactic, which changes any goal at all to `false`. +You might think this is a step backwards, but if you have a hypothesis `h : ¬ P` +then after `rw not_iff_imp_false at h,` you can `apply h,` to make progress. +Try solving this level without using `cc` or `tauto`, but using `exfalso` instead. " Statement --contra -"" +"If $P$ and $Q$ are true/false statements, then +$$(P\\land(\\lnot P))\\implies Q.$$" (P Q : Prop) : (P ∧ ¬ P) → Q := by intro h rcases h with ⟨p, np ⟩ @@ -32,5 +45,27 @@ NewTactic exfalso contradiction Conclusion " +## Pro tip. + +`¬ P` is actually `P → false` *by definition*. Try +commenting out `rw not_iff_imp_false at ...` by putting two minus signs `--` +before the `rw`. Does it still compile? +-/ + +/- Tactic : exfalso + +## Summary + +`exfalso` changes your goal to `false`. + +## Details + +We know that `false` implies `P` for any proposition `P`, and so if your goal is `P` +then you should be able to `apply` `false → P` and reduce your goal to `false`. This +is what the `exfalso` tactic does. The theorem that `false → P` is called `false.elim` +so one can achieve the same effect with `apply false.elim`. +This tactic can be used in a proof by contradiction, where the hypotheses are enough +to deduce a contradiction and the goal happens to be some random statement (possibly +a false one) which you just want to simplify to `false`. " diff --git a/server/nng/NNG/Levels/Function/Level_9.lean b/server/nng/NNG/Levels/Function/Level_9.lean index f612d41..18eed2f 100644 --- a/server/nng/NNG/Levels/Function/Level_9.lean +++ b/server/nng/NNG/Levels/Function/Level_9.lean @@ -10,11 +10,16 @@ open MyNat Introduction " +I asked around on Zulip and apparently there is not a tactic for this, perhaps because +this level is rather artificial. In world 6 we will see a variant of this example +which can be solved by a tactic. It would be an interesting project to make a tactic +which could solve this sort of level in Lean. +You can of course work both forwards and backwards, or you could crack and draw a picture. " Statement -"" +"Given a bunch of functions, we can define another one." (A B C D E F G H I J K L : Type) (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) @@ -32,5 +37,6 @@ Statement Conclusion " - +That's the end of Function World! Next it's Proposition world, and the tactics you've learnt in Function World are enough +to solve all nine levels! In fact, the levels in Proposition world might look strangely familiar$\\ldots$. " diff --git a/server/nng/NNG/Levels/Inequality.lean b/server/nng/NNG/Levels/Inequality.lean index 87a1766..4ffeb5c 100644 --- a/server/nng/NNG/Levels/Inequality.lean +++ b/server/nng/NNG/Levels/Inequality.lean @@ -22,4 +22,29 @@ Title "Inequality World" Introduction " +A new import, giving us a new definition. If `a` and `b` are naturals, +`a ≤ b` is *defined* to mean + +`∃ (c : mynat), b = a + c` + +The upside-down E means \"there exists\". So in words, $a\\le b$ +if and only if there exists a natural $c$ such that $b=a+c$. + +If you really want to change an `a ≤ b` to `∃ c, b = a + c` then +you can do so with `rw le_iff_exists_add`: + +``` +le_iff_exists_add (a b : mynat) : + a ≤ b ↔ ∃ (c : mynat), b = a + c +``` + +But because `a ≤ b` is *defined as* `∃ (c : mynat), b = a + c`, you +do not need to `rw le_iff_exists_add`, you can just pretend when you see `a ≤ b` +that it says `∃ (c : mynat), b = a + c`. You will see a concrete +example of this below. + +A new construction like `∃` means that we need to learn how to manipulate it. +There are two situations. Firstly we need to know how to solve a goal +of the form `⊢ ∃ c, ...`, and secondly we need to know how to use a hypothesis +of the form `∃ c, ...`. " \ No newline at end of file diff --git a/server/nng/NNG/Levels/Inequality/Level_1.lean b/server/nng/NNG/Levels/Inequality/Level_1.lean index 0995685..5779955 100644 --- a/server/nng/NNG/Levels/Inequality/Level_1.lean +++ b/server/nng/NNG/Levels/Inequality/Level_1.lean @@ -1,23 +1,61 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use +--import Mathlib.Tactic.Ring Game "NNG" World "Inequality" Level 1 -Title "" +Title "the `use` tactic" open MyNat Introduction " +The goal below is to prove $x\\le 1+x$ for any natural number $x$. +First let's turn the goal explicitly into an existence problem with +`rw le_iff_exists_add,` + +and now the goal has become `∃ c : mynat, 1 + x = x + c`. Clearly +this statement is true, and the proof is that $c=1$ will work (we also +need the fact that addition is commutative, but we proved that a long +time ago). How do we make progress with this goal? + +The `use` tactic can be used on goals of the form `∃ c, ...`. The idea +is that we choose which natural number we want to use, and then we use it. +So try + +`use 1,` + +and now the goal becomes `⊢ 1 + x = x + 1`. You can solve this by +`exact add_comm 1 x`, or if you are lazy you can just use the `ring` tactic, +which is a powerful AI which will solve any equality in algebra which can +be proved using the standard rules of addition and multiplication. Now +look at your proof. We're going to remove a line. + +## Important + +An important time-saver here is to note that because `a ≤ b` is *defined* +as `∃ c : mynat, b = a + c`, you *do not need to write* `rw le_iff_exists_add`. +The `use` tactic will work directly on a goal of the form `a ≤ b`. Just +use the difference `b - a` (note that we have not defined subtraction so +this does not formally make sense, but you can do the calculation in your head). +If you have written `rw le_iff_exists_add` below, then just put two minus signs `--` +before it and comment it out. See that the proof still compiles. " -Statement -"" - : true := by - trivial +axiom add_comm (a b : ℕ) : a + b = b + a +Statement --one_add_le_self +"If $x$ is a natural number, then $x\\le 1+x$. +" + (x : ℕ) : x ≤ 1 + x := by + rw [le_iff_exists_add] + use 1 + rw [add_comm] + rfl + Conclusion " diff --git a/server/nng/NNG/Levels/Inequality/Level_10.lean b/server/nng/NNG/Levels/Inequality/Level_10.lean index a08569a..f2441f8 100644 --- a/server/nng/NNG/Levels/Inequality/Level_10.lean +++ b/server/nng/NNG/Levels/Inequality/Level_10.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_11.lean b/server/nng/NNG/Levels/Inequality/Level_11.lean index b141e0f..95252b5 100644 --- a/server/nng/NNG/Levels/Inequality/Level_11.lean +++ b/server/nng/NNG/Levels/Inequality/Level_11.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_12.lean b/server/nng/NNG/Levels/Inequality/Level_12.lean index 9ef7d0e..7bccf47 100644 --- a/server/nng/NNG/Levels/Inequality/Level_12.lean +++ b/server/nng/NNG/Levels/Inequality/Level_12.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_13.lean b/server/nng/NNG/Levels/Inequality/Level_13.lean index 5308b97..501a5ca 100644 --- a/server/nng/NNG/Levels/Inequality/Level_13.lean +++ b/server/nng/NNG/Levels/Inequality/Level_13.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_14.lean b/server/nng/NNG/Levels/Inequality/Level_14.lean index 4fd5211..28edd11 100644 --- a/server/nng/NNG/Levels/Inequality/Level_14.lean +++ b/server/nng/NNG/Levels/Inequality/Level_14.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_15.lean b/server/nng/NNG/Levels/Inequality/Level_15.lean index 74ff4aa..b05b988 100644 --- a/server/nng/NNG/Levels/Inequality/Level_15.lean +++ b/server/nng/NNG/Levels/Inequality/Level_15.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_16.lean b/server/nng/NNG/Levels/Inequality/Level_16.lean index 25d25fc..1cc96a6 100644 --- a/server/nng/NNG/Levels/Inequality/Level_16.lean +++ b/server/nng/NNG/Levels/Inequality/Level_16.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_17.lean b/server/nng/NNG/Levels/Inequality/Level_17.lean index f42a282..3dfc86e 100644 --- a/server/nng/NNG/Levels/Inequality/Level_17.lean +++ b/server/nng/NNG/Levels/Inequality/Level_17.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_2.lean b/server/nng/NNG/Levels/Inequality/Level_2.lean index 597f6bd..bcee184 100644 --- a/server/nng/NNG/Levels/Inequality/Level_2.lean +++ b/server/nng/NNG/Levels/Inequality/Level_2.lean @@ -1,22 +1,26 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" Level 2 -Title "" +Title "le_rfl" open MyNat Introduction " - +Here's a nice easy one. " Statement -"" - : true := by - trivial +"The $\\le$ relation is reflexive. In other words, if $x$ is a natural number, +then $x\\le x$." + (x : ℕ) : x ≤ x := by + use 0 + rw [add_zero] + rfl Conclusion " diff --git a/server/nng/NNG/Levels/Inequality/Level_3.lean b/server/nng/NNG/Levels/Inequality/Level_3.lean index 21d9865..32adff5 100644 --- a/server/nng/NNG/Levels/Inequality/Level_3.lean +++ b/server/nng/NNG/Levels/Inequality/Level_3.lean @@ -1,22 +1,57 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use +import Std.Tactic.RCases Game "NNG" World "Inequality" Level 3 -Title "" +Title "le_succ_of_le" open MyNat Introduction " +We have seen how the `use` tactic makes progress on goals of the form `⊢ ∃ c, ...`. +But what do we do when we have a *hypothesis* of the form `h : ∃ c, ...`? +The hypothesis claims that there exists some natural number `c` with some +property. How are we going to get to that natural number `c`? It turns out +that the `cases` tactic can be used (just like it was used to extract +information from `∧` and `∨` and `↔` hypotheses). Let me talk you through +the proof of $a\\le b\\implies a\\le\\operatorname{succ}(b)$. + +The goal is an implication so we clearly want to start with + +`intro h,` + +. After this, if you *want*, you can do something like + +`rw le_iff_exists_add at h ⊢,` + +(get the sideways T with `\\|-` then space). This changes the `≤` into +its `∃` form in `h` and the goal -- but if you are happy with just +*imagining* the `∃` whenever you read a `≤` then you don't need to do this line. + +Our hypothesis `h` is now `∃ (c : mynat), b = a + c` (or `a ≤ b` if you +elected not to do the definitional rewriting) so + +`cases h with c hc,` + +gives you the natural number `c` and the hypothesis `hc : b = a + c`. +Now use `use` wisely and you're home. " Statement -"" - : true := by - trivial +"For all naturals $a$, $b$, if $a\\leq b$ then $a\\leq \\operatorname{succ}(b)$. +" + (a b : ℕ) : a ≤ b → a ≤ (succ b) := by + intro h + rcases h with ⟨c, hc⟩ + rw [hc] + use c + 1 + sorry + --rfl Conclusion " diff --git a/server/nng/NNG/Levels/Inequality/Level_4.lean b/server/nng/NNG/Levels/Inequality/Level_4.lean index 788af62..a3a34cb 100644 --- a/server/nng/NNG/Levels/Inequality/Level_4.lean +++ b/server/nng/NNG/Levels/Inequality/Level_4.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_5.lean b/server/nng/NNG/Levels/Inequality/Level_5.lean index 3cf1b1b..59159c1 100644 --- a/server/nng/NNG/Levels/Inequality/Level_5.lean +++ b/server/nng/NNG/Levels/Inequality/Level_5.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_6.lean b/server/nng/NNG/Levels/Inequality/Level_6.lean index 5b28efe..86f83a1 100644 --- a/server/nng/NNG/Levels/Inequality/Level_6.lean +++ b/server/nng/NNG/Levels/Inequality/Level_6.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_7.lean b/server/nng/NNG/Levels/Inequality/Level_7.lean index bc22434..8ff4d8d 100644 --- a/server/nng/NNG/Levels/Inequality/Level_7.lean +++ b/server/nng/NNG/Levels/Inequality/Level_7.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_8.lean b/server/nng/NNG/Levels/Inequality/Level_8.lean index 8cc9b70..4d6f744 100644 --- a/server/nng/NNG/Levels/Inequality/Level_8.lean +++ b/server/nng/NNG/Levels/Inequality/Level_8.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Inequality/Level_9.lean b/server/nng/NNG/Levels/Inequality/Level_9.lean index 4c2afa4..185f626 100644 --- a/server/nng/NNG/Levels/Inequality/Level_9.lean +++ b/server/nng/NNG/Levels/Inequality/Level_9.lean @@ -1,5 +1,6 @@ import NNG.Metadata -import NNG.MyNat.Addition +import NNG.MyNat.LE +import Mathlib.Tactic.Use Game "NNG" World "Inequality" diff --git a/server/nng/NNG/Levels/Power.lean b/server/nng/NNG/Levels/Power.lean index 54910cb..1199c78 100644 --- a/server/nng/NNG/Levels/Power.lean +++ b/server/nng/NNG/Levels/Power.lean @@ -13,4 +13,26 @@ Title "Power World" Introduction " +A new world with seven levels. And a new import! +This import gives you the power to make powers of your +natural numbers. It is defined by recursion, just like addition and multiplication. +Here are the two new axioms: + + * `pow_zero (a : mynat) : a ^ 0 = 1` + * `pow_succ (a b : mynat) : a ^ succ(b) = a ^ b * a` + +The power function has various relations to addition and multiplication. +If you have gone through levels 1--6 of addition world and levels 1--9 of +multiplication world, you should have no trouble with this world: +The usual tactics `induction`, `rw` and `refl` should see you through. +You might want to fiddle with the +drop-down menus on the left so you can see which theorems of Power World +you have proved at any given time. Addition and multiplication -- we +have a solid API for them now, i.e. if you need something about addition +or multiplication, it's probably already in the library we have built. +Collectibles are indication that we are proving the right things. + +The levels in this world were designed by Sian Carey, a UROP student +at Imperial College London, funded by a Mary Lister McCammon Fellowship, +in the summer of 2019. Thanks Sian! " \ No newline at end of file diff --git a/server/nng/NNG/Levels/Power/Level_1.lean b/server/nng/NNG/Levels/Power/Level_1.lean index c6729a0..b75c7d5 100644 --- a/server/nng/NNG/Levels/Power/Level_1.lean +++ b/server/nng/NNG/Levels/Power/Level_1.lean @@ -4,7 +4,7 @@ import NNG.Metadata Game "NNG" World "Power" Level 1 -Title "" +Title "zero_pow_zero" open MyNat @@ -15,7 +15,7 @@ Introduction Statement "$0 ^ 0 = 1$" - : true := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by + : (0 : ℕ) ^ 0 = (1 : ℕ) := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by trivial Conclusion diff --git a/server/nng/NNG/Levels/Power/Level_4.lean b/server/nng/NNG/Levels/Power/Level_4.lean index 635fd22..812dca0 100644 --- a/server/nng/NNG/Levels/Power/Level_4.lean +++ b/server/nng/NNG/Levels/Power/Level_4.lean @@ -22,3 +22,4 @@ Conclusion " " + \ No newline at end of file diff --git a/server/nng/NNG/Levels/Proposition/Level_1.lean b/server/nng/NNG/Levels/Proposition/Level_1.lean index 179f73a..09dfcc1 100644 --- a/server/nng/NNG/Levels/Proposition/Level_1.lean +++ b/server/nng/NNG/Levels/Proposition/Level_1.lean @@ -4,18 +4,72 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 1 -Title "" +Title "the `exact` tactic" open MyNat Introduction " +A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`. +Just like we can have concrete sets in Lean like `ℕ`, and abstract +sets called things like `X`, we can also have concrete propositions like +`2 + 2 = 5` and abstract propositions called things like `P`. +Mathematicians are very good at conflating a theorem with its proof. +They might say \"now use theorem 12 and we're done\". What they really +mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved +it already). Particularly problematic is the fact that mathematicians +use the word Proposition to mean \"a relatively straightforward statement +which is true\" and computer scientists use it to mean \"a statement of +arbitrary complexity, which might be true or false\". Computer scientists +are far more careful about distinguishing between a proposition and a proof. +For example: `x + 0 = x` is a proposition, and `add_zero x` +is its proof. The convention we'll use is capital letters for propositions +and small letters for proofs. " Statement -"" +"If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true." (P Q : Prop) (p : P) (h : P → Q) : Q := by +Hint +" +Here `P` is the true/false statement (the statement of proposition), and `p` is its proof. +It's like `P` being the set and `p` being the element. In fact computer scientists +sometimes think about the following analogy: propositions are like sets, +and their proofs are like their elements. + +## What's going on in this world? + +We're going to learn about manipulating propositions and proofs. +Fortunately, we don't need to learn a bunch of new tactics -- the +ones we just learnt (`exact`, `intro`, `have`, `apply`) will be perfect. + +The levels in proposition world are \"back to normal\", we're proving +theorems, not constructing elements of sets. Or are we? + +If you delete the sorry below then your local context will look like this: + +In this situation, we have true/false statements $P$ and $Q$, +a proof $p$ of $P$, and $h$ is the hypothesis that $P\\implies Q$. +Our goal is to construct a proof of $Q$. It's clear what to do +*mathematically* to solve this goal, $P$ is true and $P$ implies $Q$ +so $Q$ is true. But how to do it in Lean? + +Adopting a point of view wholly unfamiliar to many mathematicians, +Lean interprets the hypothesis $h$ as a function from proofs +of $P$ to proofs of $Q$, so the rather surprising approach + +`exact h p` + +works to close the goal. + +Note that `exact h P` (with a capital P) won't work; +this is a common error I see from beginners. \"We're trying to solve `P` +so it's exactly `P`\". The goal states the *theorem*, your job is to +construct the *proof*. $P$ is not a proof of $P$, it's $p$ that is a proof of $P$. + +In Lean, Propositions, like sets, are types, and proofs, like elements of sets, are terms. +" exact h p Conclusion diff --git a/server/nng/NNG/Levels/Proposition/Level_2.lean b/server/nng/NNG/Levels/Proposition/Level_2.lean index d4165df..bfca35b 100644 --- a/server/nng/NNG/Levels/Proposition/Level_2.lean +++ b/server/nng/NNG/Levels/Proposition/Level_2.lean @@ -4,19 +4,61 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 2 -Title "" +Title "intro" open MyNat Introduction " +Let's prove an implication. Let $P$ be a true/false statement, +and let's prove that $P\\implies P$. You can see that the goal of this level is +`P → P`. Constructing a term +of type `P → P` (which is what solving this goal *means*) in this +case amounts to proving that $P\\implies P$, and computer scientists +think of this as coming up with a function which sends proofs of $P$ +to proofs of $P$. + +To define an implication $P\\implies Q$ we need to choose an arbitrary +proof $p : P$ of $P$ and then, perhaps using $p$, construct a proof +of $Q$. The Lean way to say \"let's assume $P$ is true\" is `intro p`, +i.e., \"let's assume we have a proof of $P$\". + +## Note for worriers. + +Those of you who know +something about the subtle differences between truth and provability +discovered by Goedel -- these are not relevant here. Imagine we are +working in a fixed model of mathematics, and when I say \"proof\" +I actually mean \"truth in the model\", or \"proof in the metatheory\". + +## Rule of thumb: + +If your goal is to prove `P → Q` (i.e. that $P\\implies Q$) +then `intro p`, meaning \"assume $p$ is a proof of $P$\", will make progress. " Statement -"" +"If $P$ is a proposition then $P\\implies P$." {P : Prop} : P → P := by + Hint " + To solve this goal, you have to come up with a function from + `P` (thought of as the set of proofs of $P$!) to itself. Start with + + `intro p` + " intro p + Hint " + Our job now is to construct a proof of $P$. But $p$ is a proof of $P$. + So + + `exact p` + + will close the goal. Note that `exact P` will not work -- don't + confuse a true/false statement (which could be false!) with a proof. + We will stick with the convention of capital letters for propositions + and small letters for proofs. + " exact p Conclusion diff --git a/server/nng/NNG/Levels/Proposition/Level_3.lean b/server/nng/NNG/Levels/Proposition/Level_3.lean index 707f571..29008b0 100644 --- a/server/nng/NNG/Levels/Proposition/Level_3.lean +++ b/server/nng/NNG/Levels/Proposition/Level_3.lean @@ -4,17 +4,58 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 3 -Title "" +Title "have" open MyNat Introduction " +Say you have a whole bunch of propositions and implications between them, +and your goal is to build a certain proof of a certain proposition. +If it helps, you can build intermediate proofs of other propositions +along the way, using the `have` command. `have q : Q := ...` is the Lean analogue +of saying \"We now see that we can prove $Q$, because...\" +in the middle of a proof. +It is often not logically necessary, but on the other hand +it is very convenient, for example it can save on notation, or +it can break proofs up into smaller steps. +In the level below, we have a proof of $P$ and we want a proof +of $U$; during the proof we will construct proofs of +of some of the other propositions involved. The diagram of +propositions and implications looks like this pictorially: + +![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg) + +and so it's clear how to deduce $U$ from $P$. +Indeed, we could solve this level in one move by typing + +`exact l(j(h(p))),` + +But let us instead stroll more lazily through the level. +We can start by using the `have` tactic to make a proof of $Q$: + +`have q := h(p),` + +and then we note that $j(q)$ is a proof of $T$: + +`have t : T := j(q),` + +(note how we explicitly told Lean what proposition we thought $t$ was +a proof of, with that `: T` thing before the `:=`) +and we could even define $u$ to be $l(t)$: + +`have u : U := l(t),` + +and then finish the level with + +`exact u,` + +. " Statement -"" +"In the maze of logical implications above, if $P$ is true then so is $U$." (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) : U := by have q := h p @@ -26,5 +67,27 @@ DisabledTactic apply Conclusion " +If you solved the level using `have`, then click on the last line of your proof +(you do know you can move your cursor around with the arrow keys +and explore your proof, right?) and note that the local context at that point +is in something like the following mess: + +``` +P Q R S T U : Prop, +p : P, +h : P → Q, +i : Q → R, +j : Q → T, +k : S → T, +l : T → U, +q : Q, +t : T, +u : U +⊢ U +``` +It was already bad enough to start with, and we added three more +terms to it. In level 4 we will learn about the `apply` tactic +which solves the level using another technique, without leaving +so much junk behind. " diff --git a/server/nng/NNG/Levels/Proposition/Level_4.lean b/server/nng/NNG/Levels/Proposition/Level_4.lean index e81b416..45f0197 100644 --- a/server/nng/NNG/Levels/Proposition/Level_4.lean +++ b/server/nng/NNG/Levels/Proposition/Level_4.lean @@ -4,17 +4,40 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 4 -Title "" +Title "apply" open MyNat Introduction " +Let's do the same level again: +![diagram](https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game_images/implies_diag.jpg) + +We are given a proof $p$ of $P$ and our goal is to find a proof of $U$, or +in other words to find a path through the maze that links $P$ to $U$. +In level 3 we solved this by using `have`s to move forward, from $P$ +to $Q$ to $T$ to $U$. Using the `apply` tactic we can instead construct +the path backwards, moving from $U$ to $T$ to $Q$ to $P$. + +Our goal is to prove $U$. But $l:T\\implies U$ is +an implication which we are assuming, so it would suffice to prove $T$. +Tell Lean this by starting the proof below with + +`apply l,` + +and notice that our assumptions don't change but *the goal changes* +from `⊢ U` to `⊢ T`. + +Keep `apply`ing implications until your goal is `P`, and try not +to get lost! Now solve this goal +with `exact p`. Note: you will need to learn the difference between +`exact p` (which works) and `exact P` (which doesn't, because $P$ is +not a proof of $P$). " Statement -"" +"We can solve a maze." (P Q R S T U: Prop) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) : U := by apply l diff --git a/server/nng/NNG/Levels/Proposition/Level_5.lean b/server/nng/NNG/Levels/Proposition/Level_5.lean index 30c6832..e2418e0 100644 --- a/server/nng/NNG/Levels/Proposition/Level_5.lean +++ b/server/nng/NNG/Levels/Proposition/Level_5.lean @@ -4,17 +4,53 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 5 -Title "" +Title "P → (Q → P)" open MyNat Introduction " +In this level, our goal is to construct an implication, like in level 2. +``` +⊢ P → (Q → P) +``` + +So $P$ and $Q$ are propositions, and our goal is to prove +that $P\\implies(Q\\implies P)$. +We don't know whether $P$, $Q$ are true or false, so initially +this seems like a bit of a tall order. But let's give it a go. Delete +the `sorry` and let's think about how to proceed. + +Our goal is `P → X` for some true/false statement $X$, and if our +goal is to construct an implication then we almost always want to use the +`intro` tactic from level 2, Lean's version of \"assume $P$\", or more precisely +\"assume $p$ is a proof of $P$\". So let's start with + +`intro p,` + +and we then find ourselves in this state: + +``` +P Q : Prop, +p : P +⊢ Q → P +``` + +We now have a proof $p$ of $P$ and we are supposed to be constructing +a proof of $Q\\implies P$. So let's assume that $Q$ is true and try +and prove that $P$ is true. We assume $Q$ like this: + +`intro q,` + +and now we have to prove $P$, but have a proof handy: + +`exact p,` " Statement -"" +"For any propositions $P$ and $Q$, we always have +$P\\implies(Q\\implies P)$." (P Q : Prop) : P → (Q → P) := by intro p intro q @@ -22,5 +58,23 @@ Statement Conclusion " +A mathematician would treat the proposition $P\\implies(Q\\implies P)$ +as the same as the proposition $P\\land Q\\implies P$, +because to give a proof of either of these is just to give a method which takes +a proof of $P$ and a proof of $Q$, and returns a proof of $P$. Thinking of the +goal as $P\\land Q\\implies P$ we see why it is provable. + +## Did you notice? + +I wrote `P → (Q → P)` but Lean just writes `P → Q → P`. This is because +computer scientists adopt the convention that `→` is *right associative*, +which is a fancy way of saying \"when we write `P → Q → R`, we mean `P → (Q → R)`. +Mathematicians would never dream of writing something as ambiguous as +$P\\implies Q\\implies R$ (they are not really interested in proving abstract +propositions, they would rather work with concrete ones such as Fermat's Last Theorem), +so they do not have a convention for where the brackets go. It's important to +remember Lean's convention though, or else you will get confused. If your goal +is `P → Q → R` then you need to know whether `intro h` will create `h : P` or `h : P → Q`. +Make sure you understand which one. " diff --git a/server/nng/NNG/Levels/Proposition/Level_6.lean b/server/nng/NNG/Levels/Proposition/Level_6.lean index 2d71058..c824303 100644 --- a/server/nng/NNG/Levels/Proposition/Level_6.lean +++ b/server/nng/NNG/Levels/Proposition/Level_6.lean @@ -4,12 +4,29 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 6 -Title "" +Title "(P → (Q → R)) → ((P → Q) → (P → R))" open MyNat Introduction " +You can solve this level completely just using `intro`, `apply` and `exact`, +but if you want to argue forwards instead of backwards then don't forget +that you can do things like `have j : Q → R := f p` if `f : P → (Q → R)` +and `p : P`. I recommend that you start with `intro f` rather than `intro p` +because even though the goal starts `P → ...`, the brackets mean that +the goal is not the statement that `P` implies anything, it's the statement that +$P\\implies (Q\\implies R)$ implies something. In fact I'd recommend that you started +with `intros f h p`, which introduces three variables at once. +You then find that your your goal is `⊢ R`. If you try `have j : Q → R := f p` +now then you can `apply j`. Alternatively you can `apply (f p)` directly. +What happens if you just try `apply f`? Can you figure out what just happened? This is a little +`apply` easter egg. Why is it mathematically valid? +-/ + +/- Lemma : no-side-bar +If $P$ and $Q$ and $R$ are true/false statements, then +$$(P\\implies(Q\\implies R))\\implies((P\\implies Q)\\implies(P\\implies R)).$$ " diff --git a/server/nng/NNG/Levels/Proposition/Level_7.lean b/server/nng/NNG/Levels/Proposition/Level_7.lean index 5caa3a3..8637a15 100644 --- a/server/nng/NNG/Levels/Proposition/Level_7.lean +++ b/server/nng/NNG/Levels/Proposition/Level_7.lean @@ -4,17 +4,26 @@ import NNG.MyNat.Addition Game "NNG" World "Proposition" Level 7 -Title "" +Title "(P → Q) → ((Q → R) → (P → R))" open MyNat Introduction " - +If you start with `intro hpq` and then `intro hqr` +the dust will clear a bit and the level will look like this: +``` +P Q R : Prop, +hpq : P → Q, +hqr : Q → R +⊢ P → R +``` +So this level is really about showing transitivity of $\\implies$, +if you like that sort of language. " Statement -"" +"From $P\\implies Q$ and $Q\\implies R$ we can deduce $P\\implies R$." (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) := by intro hpq hqr intro p diff --git a/server/nng/NNG/Levels/Proposition/Level_8.lean b/server/nng/NNG/Levels/Proposition/Level_8.lean index 566034c..8235534 100644 --- a/server/nng/NNG/Levels/Proposition/Level_8.lean +++ b/server/nng/NNG/Levels/Proposition/Level_8.lean @@ -6,17 +6,32 @@ import NNG.MyNat.Theorems.Proposition Game "NNG" World "Proposition" Level 8 -Title "" +Title "(P → Q) → (¬ Q → ¬ P)" open MyNat Introduction " +There is a false proposition `false`, with no proof. It is +easy to check that $\\lnot Q$ is equivalent to $Q\\implies {\tt false}$, +and in the natural number game we call this +`not_iff_imp_false (P : Prop) : ¬ P ↔ (P → false)` + +So you can start the proof of the contrapositive below with + +`repeat {rw not_iff_imp_false},` + +to get rid of the two occurences of `¬`, and I'm sure you can +take it from there (note that we just added `not_iff_imp_false` to the +theorem statements in the menu on the left). At some point your goal might be to prove `false`. +At that point I guess you must be proving something by contradiction. +Or are you? " Statement -"" +"If $P$ and $Q$ are propositions, and $P\\implies Q$, then +$\\lnot Q\\implies \\lnot P$. " (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) := by rw [not_iff_imp_false] rw [not_iff_imp_false] diff --git a/server/nng/NNG/Levels/Proposition/Level_9.lean b/server/nng/NNG/Levels/Proposition/Level_9.lean index 3f83050..64d4e96 100644 --- a/server/nng/NNG/Levels/Proposition/Level_9.lean +++ b/server/nng/NNG/Levels/Proposition/Level_9.lean @@ -5,17 +5,25 @@ import NNG.MyNat.Theorems.Proposition Game "NNG" World "Proposition" Level 9 -Title "" +Title "a big maze." open MyNat Introduction " - +Now move onto advanced proposition world, where you will see +how to prove goals such as `P ∧ Q` ($P$ and $Q$), `P ∨ Q` ($P$ or $Q$), +`P ↔ Q` ($P\\iff Q$). +You will need to learn five more tactics: `split`, `cases`, +`left`, `right`, and `exfalso`, +but they are all straightforward, and furthermore they are +essentially the last tactics you +need to learn in order to complete all the levels of the Natural Number Game, +including all the 17 levels of Inequality World. " Statement -"" +"There is a way through the following maze." (A B C D E F G H I J K L : Prop) (f1 : A → B) (f2 : B → E) (f3 : E → D) (f4 : D → A) (f5 : E → F) (f6 : F → C) (f7 : B → C) (f8 : F → G) (f9 : G → J) (f10 : I → J) diff --git a/server/nng/NNG/Modifications/Tactics.lean b/server/nng/NNG/Modifications/Tactics.lean index ba0aff7..72be45b 100644 --- a/server/nng/NNG/Modifications/Tactics.lean +++ b/server/nng/NNG/Modifications/Tactics.lean @@ -51,7 +51,7 @@ namespace Lean.Parser.Tactic open Meta Elab Elab.Tactic open private getAltNumFields in evalCases ElimApp.evalAlts.go in -def ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax) +def ElimApp.evalNames.MyNat (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax) (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) : TermElabM (Array MVarId) := do let mut names : List Syntax := withArg[1].getArgs |>.toList @@ -96,7 +96,7 @@ elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+) let elimArgs := result.elimApp.getAppArgs ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds g.assign result.elimApp - let subgoals ← ElimApp.evalNames elimInfo result.alts withArg + let subgoals ← ElimApp.evalNames.MyNat elimInfo result.alts withArg (numGeneralized := fvarIds.size) (toClear := targetFVarIds) setGoals <| (subgoals ++ result.others).toList ++ gs diff --git a/server/nng/NNG/MyNat/AdvAddition.lean b/server/nng/NNG/MyNat/AdvAddition.lean new file mode 100644 index 0000000..25251b5 --- /dev/null +++ b/server/nng/NNG/MyNat/AdvAddition.lean @@ -0,0 +1,13 @@ +import NNG.MyNat.Theorems.Addition + +namespace MyNat +open MyNat + +axiom succ_inj {a b : ℕ} : succ a = succ b → a = b + +axiom zero_ne_succ (a : ℕ) : zero ≠ succ a + +axiom add_right_cancel (a t b : ℕ) : a + t = b + t → a = b + +axiom add_left_cancel (a b c : ℕ) : a + b = a + c → b = c + diff --git a/server/nng/NNG/MyNat/LE.lean b/server/nng/NNG/MyNat/LE.lean new file mode 100644 index 0000000..0e30011 --- /dev/null +++ b/server/nng/NNG/MyNat/LE.lean @@ -0,0 +1,18 @@ +import NNG.MyNat.Multiplication + +namespace MyNat + +def le (a b : ℕ) := ∃ (c : ℕ), b = a + c + +-- Another choice is to define it recursively: +-- | le 0 _ +-- | le (succ a) (succ b) = le ab + +-- notation +instance : LE MyNat := ⟨MyNat.le⟩ + +--@[leakage] theorem le_def' : MyNat.le = (≤) := rfl + +theorem le_iff_exists_add (a b : ℕ) : a ≤ b ↔ ∃ (c : ℕ), b = a + c := Iff.rfl + +end MyNat \ No newline at end of file diff --git a/server/nng/NNG/MyNat/Multiplication.lean b/server/nng/NNG/MyNat/Multiplication.lean index 53dd6b3..d92ac54 100644 --- a/server/nng/NNG/MyNat/Multiplication.lean +++ b/server/nng/NNG/MyNat/Multiplication.lean @@ -15,3 +15,5 @@ axiom mul_zero (a : MyNat) : a * 0 = 0 axiom mul_succ (a b : MyNat) : a * (succ b) = a * b + a +-- ToDO +axiom succ_ne_zero (a : ℕ) : succ a ≠ 0