greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

break off implication world

Browse Source
This commit is contained in:
Kevin Buzzard
2023-10-11 17:53:51 +01:00
parent 2b431544d8
commit a01eb1bd00
32 changed files with 452 additions and 465 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
Game.lean
View File

@@ -8,6 +8,7 @@ import Game.Levels.Tutorial
import Game.Levels.Addition
import Game.Levels.Multiplication
import Game.Levels.Power
import Game.Levels.Implication
import Game.Levels.AdvAddition
--import Game.Levels.AdvMultiplication
--import Game.Levels.EvenOdd
@@ -93,5 +94,5 @@ Dependency Addition → Multiplication → Power
--Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard
--Dependency Multiplication → AdvMultiplication
--Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
Dependency Addition → AdvAddition
Dependency Addition → Implication → AdvAddition
MakeGame

34
Game/Levels/AdvAddition.lean
View File

@@ -1,32 +1,20 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition -- `zero_ne_succ` and `succ_inj`
import Game.Levels.AdvAddition.L01assumption
import Game.Levels.AdvAddition.L02assumption2
import Game.Levels.AdvAddition.L03apply
import Game.Levels.AdvAddition.L04succ_inj
import Game.Levels.AdvAddition.L05succ_inj2
import Game.Levels.AdvAddition.L06intro
import Game.Levels.AdvAddition.L07intro2
import Game.Levels.AdvAddition.L08add_right_cancel
import Game.Levels.AdvAddition.L09add_left_cancel
import Game.Levels.AdvAddition.L10add_left_eq_self
import Game.Levels.AdvAddition.L11add_right_eq_self
import Game.Levels.Implication
import Game.Levels.AdvAddition.L01ne_succ_self
import Game.Levels.AdvAddition.L02add_right_cancel
import Game.Levels.AdvAddition.L03add_left_cancel
import Game.Levels.AdvAddition.L04add_left_eq_self
import Game.Levels.AdvAddition.L05add_right_eq_self
import Game.Levels.AdvAddition.L06eq_zero_of_add_right_eq_zero
import Game.Levels.AdvAddition.L07eq_zero_of_add_left_eq_zero
World "AdvAddition"
Title "Advanced Addition World"
Introduction
"
We've proved that $2+2=4$; in Advanced Addition World we'll learn
how to prove that $2+2\\neq 5$.
In Addition World we proved *equalities* like `x + y = y + x`.
In this world we'll learn how to prove *implications*
like $x+n=y+n \\implies x=y$. We'll have to learn three new
tactics to do this: `assumption`, `apply` and `intro`.
We'll also learn two new fundamental facts about
natural numbers, which Peano introduced as axioms.
In Advanced Addition World we will prove some basic
addition facts such as $x+y=x\implies y=0$. They will
all involve implications.
Click on \"Start\" to proceed.
"

36
Game/Levels/AdvAddition/L01assumption.lean
View File

@@ -1,36 +0,0 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
World "AdvAddition"
Level 1
Title "The `assumption` tactic"
namespace MyNat
TacticDoc assumption "
## Summary
This tactic closes the goal if the goal is *identically* one
of the assumptions.
### Example
If the goal is `x = 37` and you have a hypothesis `main_result_2 : x = 37`
then `assumption` will solve the goal.
"
NewTactic assumption
Introduction
"
In this world we'll learn how to prove theorems of the form $P\\implies Q$.
To do that we need to learn some more tactics.
The `assumption` tactic closes a goal if it is identical to
one of our hypotheses.
"
/-- Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$. -/
Statement (x y z : ℕ) (h1 : x + y = 37) (h2 : 3 * x + z = 42) : x + y = 37 := by
Hint "The goal is one of our hypotheses. Solve the goal by casting `assumption`."
assumption

41
Game/Levels/AdvAddition/L01ne_succ_self.lean Normal file
View File

@@ -0,0 +1,41 @@
import Game.Levels.Implication.L11two_add_two_ne_five
World "AdvAddition"
Level 1
Title "ne_succ_self"
LemmaTab "Peano"
namespace MyNat
Introduction
"In this world I will mostly leave you on your own.
However I'll give you a couple of hints for this first level,
which is a warm-up to see if you remember `zero_ne_succ`
and `succ_inj`, and how to use the `apply` tactic.
"
/-- $n\neq\operatorname{succ}(n)$. -/
Statement ne_succ_self (n : ℕ) : n ≠ succ n := by
Hint "Start with `induction`."
induction n with d hd
Hint (hidden := true) "Now you can do `intro, apply, exact`, but `exact zero_ne_succ 0` will work."
exact zero_ne_succ 0
intro h
apply succ_inj at h
apply hd at h
exact h
Conclusion "How about this for a proof:
```
induction n with d hd
-- base case can be done in one line
exact zero_ne_succ 0
-- inductive step
intro h
apply succ_inj at h
apply hd at h -- remember `hd : d = succ d → False`
exact h
```
"

13
Game/Levels/AdvAddition/L08add_right_cancel.lean → Game/Levels/AdvAddition/L02add_right_cancel.lean
View File

@@ -1,8 +1,7 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.AdvAddition.L01ne_succ_self
World "AdvAddition"
Level 8
Level 2
Title "add_right_cancel"
namespace MyNat
@@ -18,19 +17,19 @@ NewLemma MyNat.add_right_cancel
Introduction
"`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.
Start with `induction n with d hd` and see if you can take it from there.
"
/-- $a+n=b+n\\implies a=b$. -/
/-- $a+n=b+n\implies a=b$. -/
Statement add_right_cancel (a b n : ℕ) : a + n = b + n → a = b := by
Hint (hidden := true) "Start with induction on `n`."
induction n with d hd
intro h
repeat rw [add_zero] at h
assumption
exact h
intro h
repeat rw [add_succ] at h
apply succ_inj at h
apply hd at h
assumption
exact h
Conclusion "Nice!"

8
Game/Levels/AdvAddition/L09add_left_cancel.lean → Game/Levels/AdvAddition/L03add_left_cancel.lean
View File

@@ -1,7 +1,7 @@
import Game.Levels.AdvAddition.L08add_right_cancel
import Game.Levels.AdvAddition.L02add_right_cancel
World "AdvAddition"
Level 9
Level 3
Title "add_left_cancel"
namespace MyNat
@@ -17,7 +17,7 @@ NewLemma MyNat.add_left_cancel
Introduction
"`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.
You can prove it by induction on `n` or you can deduce it from `add_left_cancel`.
You can prove it by induction on `n` or you can deduce it from `add_right_cancel`.
"
/-- $a+n=b+n\implies a=b$. -/
@@ -25,4 +25,4 @@ Statement add_left_cancel (a b n : ℕ) : n + a = n + b → a = b := by
repeat rw [add_comm n]
intro h
apply add_right_cancel at h
assumption
exact h

11
Game/Levels/AdvAddition/L10add_left_eq_self.lean → Game/Levels/AdvAddition/L04add_left_eq_self.lean
View File

@@ -1,7 +1,7 @@
import Game.Levels.AdvAddition.L09add_left_cancel
import Game.Levels.AdvAddition.L03add_left_cancel
World "AdvAddition"
Level 10
Level 4
Title "add_left_eq_self"
namespace MyNat
@@ -25,18 +25,19 @@ Statement add_left_eq_self (x y : ℕ) : x + y = y → x = 0 := by
intro h
nth_rewrite 2 [← zero_add y] at h
apply add_right_cancel at h
assumption
exact h
Conclusion "Did you use induction on `y`?
Here's a proof of `add_left_eq_self` which uses `add_right_cancel`.
If you want to inspect it, you can go into editor mode by clicking `</>` in the top right
and then just cut and paste the proof and move your cursor around it
(although you'll lose your own proof this way if you're not careful). Click `>_` to get
to see the hypotheses and goal at any given point
(although you'll lose your own proof this way). Click `>_` to get
back to command line mode.
```
intro h
nth_rewrite 2 [← zero_add y] at h
apply add_right_cancel at h
assumption
exact h
```
"

27
Game/Levels/AdvAddition/L11add_right_eq_self.lean → Game/Levels/AdvAddition/L05add_right_eq_self.lean
View File

@@ -1,7 +1,7 @@
import Game.Levels.AdvAddition.L10add_left_eq_self
import Game.Levels.AdvAddition.L04add_left_eq_self
World "AdvAddition"
Level 11
Level 5
Title "add_right_eq_self"
LemmaTab "Add"
@@ -17,20 +17,37 @@ NewLemma MyNat.add_right_eq_self
Introduction
"`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
Two ways to do it spring to mind; I'll mention them when you've solved it.
"
/-- $a+n=b+n\implies a=b$. -/
/-- $x+y=x\implies y=0$. -/
Statement add_right_eq_self (x y : ℕ) : x + y = x → y = 0 := by
rw [add_comm]
intro h
apply add_left_eq_self at h
assumption
exact h
Conclusion "Here's a proof using `add_left_eq_self`:
```
rw [add_comm]
intro h
apply add_left_eq_self at h
assumption
exact h
```
Alternatively you can just prove it by induction on `x`
(the dots in the proof just indicate the two goals and
can be omitted):
```
induction x with d hd
· intro h
rw [zero_add] at h
assumption
· intro h
rw [succ_add] at h
apply succ_inj at h
apply hd at h
assumption
```
"

46
Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean Normal file
View File

@@ -0,0 +1,46 @@
import Game.Levels.AdvAddition.L05add_right_eq_self
World "AdvAddition"
Level 6
Title "eq_zero_of_add_right_eq_zero"
LemmaTab "Peano"
namespace MyNat
Introduction
" We have still not proved that if `a + b = 0` then `a = 0` and `b = 0`. Let's finish this
world by proving one of these in this level, and the other in the next.
If you have a hypothesis `h : False` then you are done, because a false statement implies
any statement. You can use the `contradiction` tactic to finish your proof.
"
TacticDoc contradiction "
The `contradiction` tactic will solve any goal, if you have a hypothesis `h : False`.
"
NewTactic contradiction
LemmaDoc MyNat.eq_zero_of_add_eq_zero_right as "eq_zero_of_add_eq_zero_right" in "Add" "
A proof that $a+b=0 \\implies a=0$.
"
-- **TODO** `symm` tactic
-- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
-- https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/eq_zero_of_add_eq_zero_right/near/395716874
/-- If $a+b=0$ then $a=0$. -/
Statement eq_zero_of_add_eq_zero_right (a b : ℕ) : a + b = 0 → a = 0 := by
Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately, so start with `induction b with d hd`
but just ignore the inductive hypothesis in the `succ d` case :-)"
induction b with d _ -- don't even both naming inductive hypo
intro h
rw [add_zero] at h
exact h
intro h
-- clear hd -- **TODO** remove after `cases`
rw [add_succ] at h
symm at h
apply zero_ne_succ at h
contradiction

35
Game/Levels/AdvAddition/L07eq_zero_of_add_left_eq_zero.lean Normal file
View File

@@ -0,0 +1,35 @@
import Game.Levels.AdvAddition.L06eq_zero_of_add_right_eq_zero
World "AdvAddition"
Level 7
Title "eq_zero_of_add_left_eq_zero"
LemmaTab "Peano"
namespace MyNat
Introduction
"You can just mimic the previous proof to do this one -- or you can figure out a way
of using it.
"
LemmaDoc MyNat.eq_zero_of_add_eq_zero_left as "eq_zero_of_add_eq_zero_left" in "Add" "
A proof that $a+b=0 \\implies b=0$.
"
-- **TODO** why `add_eq_zero_right` and not `add_right_eq_zero`?
/-- If $a+b=0$ then $b=0$. -/
Statement eq_zero_of_add_eq_zero_left (a b : ℕ) : a + b = 0 → b = 0 := by
rw [add_comm]
exact eq_zero_of_add_eq_zero_right b a
Conclusion "How about this for a proof:
```
rw [add_comm]
exact eq_zero_of_add_eq_zero_right b a
```
You're now ready for LessThanOrEqual World.
"

77
Game/Levels/AdvAddition/Level_10.lean
View File

@@ -1,77 +0,0 @@
import Game.Levels.AdvAddition.Level_9
import Std.Tactic.RCases
World "AdvAddition"
Level 10
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.
"
/-- If $a$ and $b$ are natural numbers such that
$$ a + b = 0, $$
then $b = 0$. -/
Statement MyNat.add_left_eq_zero
{a b : ℕ} (h : a + b = 0) : b = 0 := by
Hint "
You want to start of by making a distinction `b = 0` or `b = succ d` for some
`d`. You can do this with
```
induction b
```
even if you are never going to use the induction hypothesis.
"
-- TODO: induction vs rcases
Branch
rcases b
-- TODO: `⊢ zero = 0` :(
induction b with d
· rfl
· Hint "This goal seems impossible! 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
```
"
rw [add_succ] at h
Hint "
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.
"
Branch
have j := succ_ne_zero (a + d) h
exfalso
exact j
exfalso
apply succ_ne_zero (a + d)
exact h
LemmaTab "Add"
Conclusion
"
"

30
Game/Levels/AdvAddition/Level_11.lean
View File

@@ -1,30 +0,0 @@
import Game.Levels.AdvAddition.Level_10
World "AdvAddition"
Level 11
Title "add_right_eq_zero"
open MyNat
Introduction
"
We just proved `add_left_eq_zero (a b : ℕ) : a + b = 0 → b = 0`.
Hopefully `add_right_eq_zero` shouldn't be too hard now.
"
/-- If $a$ and $b$ are natural numbers such that
$$ a + b = 0, $$
then $a = 0$. -/
Statement MyNat.add_right_eq_zero
{a b : ℕ} : a + b = 0 → a = 0 := by
intro h
rw [add_comm] at h
exact add_left_eq_zero h
LemmaTab "Add"
Conclusion
"
"

34
Game/Levels/AdvAddition/Level_12.lean
View File

@@ -1,34 +0,0 @@
import Game.Levels.AdvAddition.Level_11
World "AdvAddition"
Level 12
Title "add_one_eq_succ"
open MyNat
Introduction
"
We have
```
succ_eq_add_one (n : ℕ) : succ n = n + 1
```
but sometimes the other way is also convenient.
"
/-- For any natural number $d$, we have
$$ d+1 = \\operatorname{succ}(d). $$ -/
Statement MyNat.add_one_eq_succ
(d : ℕ) : d + 1 = succ d := by
rw [succ_eq_add_one]
rfl
LemmaTab "Add"
Conclusion
"
"

38
Game/Levels/AdvAddition/Level_13.lean
View File

@@ -1,38 +0,0 @@
import Game.Levels.AdvAddition.Level_12
World "AdvAddition"
Level 13
Title "ne_succ_self"
open MyNat
Introduction
"
The last level in Advanced Addition World is the statement
that $n\\not=\\operatorname{succ}(n)$.
"
/-- For any natural number $n$, we have
$$ n \\neq \\operatorname{succ}(n). $$ -/
Statement --ne_succ_self
(n : ℕ) : n ≠ succ n := by
Hint (hidden := true) "I would start a proof by induction on `n`."
induction n with d hd
· apply zero_ne_succ
· Hint (hidden := true) "If you have no clue, you could start with `rw [Ne, Not]`."
Branch
rw [Ne, Not]
intro hs
apply hd
apply succ_inj
exact hs
LemmaTab "Nat"
Conclusion
"
Congratulations. 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).
"

35
Game/Levels/AdvAddition/Level_7.lean
View File

@@ -1,35 +0,0 @@
import Game.Levels.AdvAddition.Level_6
World "AdvAddition"
Level 7
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 `constructor`
to split an `↔` goal into the `→` goal and the `←` goal.
"
/-- For all naturals $a$, $b$ and $t$,
$$ a + t = b + t\\iff a=b. $$
-/
Statement MyNat.add_right_cancel_iff
(t a b : ℕ) : a + t = b + t ↔ a = b := by
Branch
induction t
· simp
· simp
exact n_ih
constructor
· Hint "Pro tip: `exact add_right_cancel _ _ _` means \"let Lean figure out the missing inputs\"."
exact add_right_cancel _ _ _
· intro H
rw [H]
rfl
LemmaTab "Add"
DisabledTactic simp

36
Game/Levels/AdvAddition/Level_8.lean
View File

@@ -1,36 +0,0 @@
import Game.Levels.AdvAddition.Level_7
World "AdvAddition"
Level 8
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.
"
/-- If $a$ and $b$ are natural numbers such that
$$ a + b = a, $$
then $b = 0$. -/
Statement MyNat.eq_zero_of_add_right_eq_self
{a b : ℕ} : a + b = a → b = 0 := by
intro h
Hint (hidden := true) "Look at `add_left_cancel`."
apply add_left_cancel a
rw [h]
rw [add_zero]
rfl
LemmaTab "Add"
-- Note: if you find a way to use `simp`, honestly go for it :)
Conclusion
"
"

59
Game/Levels/AdvAddition/Level_9.lean
View File

@@ -1,59 +0,0 @@
import Game.Levels.AdvAddition.Level_8
World "AdvAddition"
Level 9
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 : ¬) : 0 ≠ succ a
```
$X\\ne Y$ is *defined to mean* $X = Y\\implies{\\tt False}$, similar to how `¬A` was defined.
"
-- TODO: I dont think there is a `symmetry` tactic anymore.
-- 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`.
/-- Zero is not the successor of any natural number. -/
Statement MyNat.succ_ne_zero
(a : ℕ) : succ a ≠ 0 := by
Hint "You have several options how to start. One would be to recall that `≠` is defined as
`(· = ·) → False` and start with `intro`. Or do `rw [Ne, Not]` to explicitely remove the
`≠`. Or you could use the lemma `Ne.symm (a b : ℕ) : a ≠ b → b ≠ a` which I just added to your
inventory."
Branch
simp?
Branch
rw [Ne] -- same as `simp` or `rw [ne_eq]`
rw[Not]
intro h
apply zero_ne_succ a
Branch
apply Eq.symm
exact h
rw [h]
rfl
Branch
exact (zero_ne_succ a).symm
apply Ne.symm
exact zero_ne_succ a
NewLemma MyNat.zero_ne_succ Ne.symm Eq.symm Iff.symm
NewDefinition Ne
LemmaTab "Nat"
Conclusion
"
"

37
Game/Levels/AdvAddition/levels
View File

@@ -1,39 +1,4 @@
-- **TODO** more levels! Put them elsewhere.
-- next: intro intro level.
theorem add_right_cancel (x y t : ℕ) : x + t = y + t → x = y := by
induction t with d hd
intro h
rw [add_zero, add_zero] at h
assumption
intro h
rw [add_succ, add_succ] at h
apply succ_inj at h
apply hd at h
assumption
example (x y : ℕ) : x + t = t → x = 0 := by
intro h
nth_rewrite 2 [← zero_add t] at h
apply add_right_cancel at h
assumption
axiom succ_ne_zero (x : ℕ) : succ x ≠ 0
example (x y : ℕ) : x + y = 0 → x = 0 := by
induction y with d hd
intro h
rw [add_zero] at h
assumption
clear hd
rw [add_succ]
intro h
apply succ_ne_zero at h
contradiction
What about levels like:
What about levels like:
h1 : 3x+4y=7
h2 : x+5y=6
⊢ x=1

32
Game/Levels/Implication.lean Normal file
View File

@@ -0,0 +1,32 @@
import Game.Levels.Addition
import Game.MyNat.PeanoAxioms -- `zero_ne_succ` and `succ_inj`
import Game.Levels.Implication.L01exact
import Game.Levels.Implication.L02exact2
import Game.Levels.Implication.L03apply
import Game.Levels.Implication.L04succ_inj
import Game.Levels.Implication.L05succ_inj2
import Game.Levels.Implication.L06intro
import Game.Levels.Implication.L07intro2
import Game.Levels.Implication.L08ne
import Game.Levels.Implication.L09zero_ne_succ
import Game.Levels.Implication.L10one_ne_zero
import Game.Levels.Implication.L11two_add_two_ne_five
World "Implication"
Title "Implication World"
Introduction
"
We've proved that $2+2=4$; in Implication World we'll learn
how to prove $2+2\\neq 5$.
In Addition World we proved *equalities* like `x + y = y + x`.
In this second tutorial world we'll learn some new tactics,
enabling us to prove *implications*
like $x+1=4 \\implies x=3.
We'll also learn two new fundamental facts about
natural numbers, which Peano introduced as axioms.
Click on \"Start\" to proceed.
"

43
Game/Levels/Implication/L01exact.lean Normal file
View File

@@ -0,0 +1,43 @@
import Game.Levels.Addition
import Game.MyNat.PeanoAxioms
World "Implication"
Level 1
Title "The `exact` tactic"
namespace MyNat
TacticDoc exact "
## Summary
If the goal is a statement `P`, then `exact h` will close the goal if `h` is a proof of `P`.
### Example
If the goal is `x = 37` and you have a hypothesis `h : x = 37`
then `exact h` will solve the goal.
### Example
If the goal is `x + 0 = x` then `exact add_zero x` will close the goal.
Note that `exact add_zero` will *not work*; the proof has to be exactly
a proof of the goal. `add_zero` is a proof of `∀ n, n + 0 = n` or, if you like,
a proof of `? + 0 = ?` where `?` is yet to be supplied.
"
NewTactic exact
Introduction
"
In this world we'll learn how to prove theorems of the form $P\\implies Q$.
To do that we need to learn some more tactics.
The `exact` tactic can be used to close a goal which is exactly one of
the hypotheses.
"
/-- Assuming $x+y=37$ and $3x+z=42$, we have $x+y=37$. -/
Statement (x y z : ℕ) (h1 : x + y = 37) (h2 : 3 * x + z = 42) : x + y = 37 := by
Hint "The goal is one of our hypotheses. Solve the goal by executing `exact h1`."
exact h1

18
Game/Levels/AdvAddition/L02assumption2.lean → Game/Levels/Implication/L02exact2.lean
View File

@@ -1,9 +1,8 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L01exact
World "AdvAddition"
World "Implication"
Level 2
Title "`assumption` practice."
Title "`exact` practice."
namespace MyNat
@@ -14,6 +13,13 @@ use rewrites to fix things up."
Statement (x : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
Hint "Rewrite `zero_add` at `h` twice, to change `h` into the goal."
repeat rw [zero_add] at h
Hint "Now you could finish with `rw [h]` then `rfl`, but `assumption`
Hint "Now you could finish with `rw [h]` then `rfl`, but `exact h`
does it in one line."
assumption
exact h
Conclusion "Here's a two-line proof:
```
repeat rw [zero_add] at h
exact h
```
"

9
Game/Levels/AdvAddition/L03apply.lean → Game/Levels/Implication/L03apply.lean
View File

@@ -1,7 +1,6 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L02exact2
World "AdvAddition"
World "Implication"
Level 3
Title "The `apply` tactic."
@@ -46,5 +45,5 @@ hypothesis with the `apply` tactic.
Statement (x y : ℕ) (h : x = 37) (imp : x = 37 → y = 42) : y = 42 := by
Hint "Start with `apply imp at h`. This will change `h` to `y = 42`."
apply imp at h
Hint "Now finish with `assumption`."
assumption
Hint "Now finish using `exact`."
exact h

9
Game/Levels/AdvAddition/L04succ_inj.lean → Game/Levels/Implication/L04succ_inj.lean
View File

@@ -1,7 +1,6 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L03apply
World "AdvAddition"
World "Implication"
Level 4
Title "succ_inj : the successor function is injective"
@@ -66,7 +65,7 @@ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
apply succ_inj at h
Hint "Now finish in one line."
Hint (hidden := true) "And now we've deduced what we wanted to prove: the goal is one of our assumptions.
Finish the level with `assumption`."
assumption
Finish the level with `exact h`."
exact h
Conclusion "In the next level, we'll do the same proof but backwards."

16
Game/Levels/AdvAddition/L05succ_inj2.lean → Game/Levels/Implication/L05succ_inj2.lean
View File

@@ -1,10 +1,11 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L04succ_inj
World "AdvAddition"
World "Implication"
Level 5
Title "Arguing backwards"
LemmaTab "Peano"
namespace MyNat
Introduction
@@ -27,8 +28,11 @@ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
Hint "Now rewrite `four_eq_succ_three` backwards to make the goal
equal to the hypothesis."
rw [← four_eq_succ_three]
Hint "You can now finish with `assumption`."
assumption
Hint "You can now finish with `exact h`."
exact h
Conclusion "Many people find `apply t at h` easy, but some find `apply t` confusing.
If you find it confusing, then just argue forwards."
If you find it confusing, then just argue forwards.
You can read more about the `apply` tactic in its documentation, which you can view by
clicking on the tactic in the list on the right."

12
Game/Levels/AdvAddition/L06intro.lean → Game/Levels/Implication/L06intro.lean
View File

@@ -1,7 +1,6 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L05succ_inj2
World "AdvAddition"
World "Implication"
Level 6
Title "intro"
@@ -27,13 +26,12 @@ Introduction
"We have seen how to `apply` theorems and assumptions of
of the form `P → Q`. But what if our *goal* is of the form `P → Q`?
To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"
in Lean. We do this with the `intro` tactic, the last tactic you need
to learn to solve all the levels in this world.
in Lean. We do this with the `intro` tactic.
"
/-- $x=37\implies x=37$. -/
Statement (x : ℕ) : x = 37 → x = 37 := by
Hint "Start with `intro h` to assume the hypothesis and call its proof `h`."
intro h
Hint (hidden := true) "Now `assumption` finishes the job."
assumption
Hint (hidden := true) "Now `exact h` finishes the job."
exact h

12
Game/Levels/AdvAddition/L07intro2.lean → Game/Levels/Implication/L07intro2.lean
View File

@@ -1,7 +1,6 @@
import Game.Levels.Addition
import Game.MyNat.AdvAddition
import Game.Levels.Implication.L06intro
World "AdvAddition"
World "Implication"
Level 7
Title "intro practice"
@@ -21,8 +20,5 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
repeat rw [← succ_eq_add_one] at h
Hint (hidden := true) "Now `apply succ_inj at h` to cancel the `succ`s."
apply succ_inj at h
Hint (hidden := true) "Now `rw [h]` then `rfl` works, but `assumption` is quicker."
assumption
Conclusion "These worlds have been a tutorial on our new tactics. Now let's use them
to prove some more fundamental facts about the naturals which we will need in later worlds."
Hint (hidden := true) "Now `rw [h]` then `rfl` works, but `exact h` is quicker."
exact h

31
Game/Levels/Implication/L08ne.lean Normal file
View File

@@ -0,0 +1,31 @@
import Game.Levels.Implication.L07intro2
World "Implication"
Level 8
Title "≠"
LemmaTab "Peano"
namespace MyNat
Introduction
"We still can't prove `2 + 2 ≠ 5` because we have not talked about the
definition of `≠`. In Lean, `a ≠ b` is *defined* to mean `a = b → False`.
Here `False` is a generic false proposition, and this definition works
because `True → False` is false, but `False → False` is true.
Even though `a ≠ b` does not look like an implication,
you should treat it as an implication. The next two levels will show you how.
`False` is a goal which you cannot deduce from a consistent set of assumptions!
So if your goal is `False` then you had better hope that your hypotheses
are contradictory, which they are in this level.
"
/-- If $x=y$ and $x \neq y$ then we can deduce a contradiction. -/
Statement (x y : ℕ) (h1 : x = y) (h2 : x ≠ y) : False := by
Hint "Try `apply`ing `h2` either `at h1` or directly to the goal."
apply h2 at h1
exact h1
Conclusion "Remember, `x ≠ y` is *notation* for `x = y → False`"

41
Game/Levels/Implication/L09zero_ne_succ.lean Normal file
View File

@@ -0,0 +1,41 @@
import Game.Levels.Implication.L08ne
World "Implication"
Level 9
Title "zero_ne_succ"
LemmaTab "Peano"
namespace MyNat
LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Peano" "
`zero_ne_succ n` is the proof that `0 ≠ succ n`.
In Lean, `a ≠ b` is *defined to mean* `a = b → False`. Hence
`zero_ne_succ n` is really a proof of `0 = succ n → False`.
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`.
"
Introduction "
As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to
introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.
To learn about this result, click on it in the list of lemmas on the right.
"
LemmaDoc MyNat.zero_ne_one as "zero_ne_one" in "numerals" "
`zero_ne_one` is a proof of `0 ≠ 1`.
"
NewLemma MyNat.zero_ne_succ MyNat.zero_ne_one
/-- $0\neq1$. -/
Statement zero_ne_one : (0 : ℕ) ≠ 1 := by
Hint "Start with `intro h`."
intro h
rw [one_eq_succ_zero] at h -- **TODO** this line is not needed :-/
apply zero_ne_succ at h -- **TODO** cripple `apply`.
exact h
Conclusion "Remember, `x ≠ y` is *notation* for `x = y → false`"

51
Game/Levels/Implication/L10one_ne_zero.lean Normal file
View File

@@ -0,0 +1,51 @@
import Game.Levels.Implication.L09zero_ne_succ
World "Implication"
Level 10
Title "1 ≠ 0"
LemmaTab "Peano"
namespace MyNat
Introduction "
We know `succ_ne_zero n` is a proof of `0 = succ n → false` -- but what
if we have a hypothesis `succ n = 0`? It's the wrong way around!
The `symm` tactic changes a goal `x = y` to `y = x`, and a goal `x ≠ y`
to `y ≠ x`. And `symm at h`
does the same for a hypothesis `h`. We've proved $0 \\neq 1$; now try
proving $1 \\neq 0$.
"
TacticDoc symm "
## Summary
The `symm` tactic will change a goal or hypothesis of
the form `X = Y` to `Y = X`. It will also work on `X ≠ Y`
and on `X ↔ Y`.
### Example
If the goal is `2 + 2 = 4` then `symm` will change it to `4 = 2 + 2`.
### Example
If `h : 2 + 2 ≠ 5` then `symm at h` will change `h` to `5 ≠ 2 + 2`.
"
NewTactic symm
/-- $0\neq1$. -/
Statement : (1 : ℕ) ≠ 0 := by
symm
exact zero_ne_one
Conclusion "What do you think of this two-liner:
```
symm
exact zero_ne_one
```
`exact` doesn't just take hypotheses, it will eat any proof which exists
in the system.
"

37
Game/Levels/Implication/L11two_add_two_ne_five.lean Normal file
View File

@@ -0,0 +1,37 @@
import Game.Levels.Implication.L10one_ne_zero
World "Implication"
Level 11
Title "2 + 2 ≠ 5"
LemmaTab "Peano"
namespace MyNat
Introduction
" 2 + 2 ≠ 5 is really boring to prove, given the tools we have. To make it a lot less
painful, I have unfolded all of the numerals. See if you can use `zero_ne_succ` and
`succ_inj` to prove this.
"
/-- $2+2≠5$. -/
Statement : succ (succ 0) + succ (succ 0) ≠ succ (succ (succ (succ (succ 0)))) := by
intro h
rw [add_succ, add_succ, add_zero] at h
repeat apply succ_inj at h
apply zero_ne_succ at h
exact h
Conclusion "Here's my proof:
```
intro h
rw [add_succ, add_succ, add_zero] at h
repeat apply succ_inj at h
apply zero_ne_succ at h
exact h
```
Right now we have not developed enough material to make Lean an adequate calculator.
In the forthcoming algorithm and functional programming worlds we will develop machinery
which makes questions like this much easier, and questions like 20 + 20 ≠ 41 feasible.
Until I've written them, why not press on to Advanced Addition World."

4
Game/Levels/map.txt
View File

@@ -9,13 +9,15 @@ c) If x + z = y + z then x = y and comm version
## Algorithm world
Optional. Learn about automating proofs with `simp` and/or `ac_rfl`.
Note : `add_add_add_comm` is needed for isEven_add_isEven
and also in power world with pow_add I think it was,
and also if you choose a lousy variable
to induct on in one of mul_add/add_mul (the
one you don't prove via comm)
But we should make `ac_rfl`.
Where does a reduction tactic which turns all numerals
into succ succ succ 0 live? Here or functional program world?
**TODO** Aesop levels. Tutorial about how to get aesop proving...something.

2
Game/MyNat/AdvAddition.lean → Game/MyNat/PeanoAxioms.lean
View File

@@ -1,4 +1,4 @@
import Game.MyNat.Addition
import Game.MyNat.Definition
import Mathlib.Tactic
namespace MyNat