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

tinkering

Browse Source
This commit is contained in:
Kevin Buzzard
2023-10-22 15:50:20 +01:00
parent c1addcbe86
commit d80a520359
19 changed files with 276 additions and 225 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game.lean
View File

@@ -46,7 +46,7 @@ Other brand new worlds will also be appearing during October 2023.
## More
Open \"Game Info\" in the burger menu on the top right for resources,
Click on the three lines in the top right and select \"Game Info\" for resources,
links, and ways to interact with the Lean community.
"

6
Game/Levels/AdvAddition/L06eq_zero_of_add_right_eq_zero.lean
View File

@@ -10,7 +10,7 @@ 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
" We have still not proved that if `a + b = 0` then `a = 0` and also `b = 0`. Let's finish this
world by proving one of these in this level, and the other in the next.
## Two new tactics
@@ -66,8 +66,8 @@ LemmaDoc MyNat.eq_zero_of_add_right_eq_zero as "eq_zero_of_add_right_eq_zero" in
/-- If $a+b=0$ then $a=0$. -/
Statement eq_zero_of_add_right_eq_zero (a b : ℕ) : a + b = 0 → a = 0 := by
Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately, but so start with `induction b with d hd`
but just ignore the inductive hypothesis in the `succ d` case :-)"
Hint "We want to deal with the cases `b = 0` and `b ≠ 0` separately,
so start with `cases b with d`."
cases b with d
intro h
rw [add_zero] at h

4
Game/Levels/LessOrEqual.lean
View File

@@ -2,8 +2,8 @@ import GameServer.Commands
import Game.Levels.LessOrEqual.L01le_refl
import Game.Levels.LessOrEqual.L02zero_le
import Game.Levels.LessOrEqual.L03le_succ_self
import Game.Levels.LessOrEqual.L04le_zero
import Game.Levels.LessOrEqual.L05le_trans
import Game.Levels.LessOrEqual.L04le_trans
import Game.Levels.LessOrEqual.L05le_zero
import Game.Levels.LessOrEqual.L06le_antisymm
import Game.Levels.LessOrEqual.L07le_total

2
Game/Levels/LessOrEqual/L01le_refl.lean
View File

@@ -42,7 +42,7 @@ The reason for the name is that this lemma is \"reflexivity of $\\le$\"
NewLemma MyNat.le_refl
/-- If $x$ is a number, then $x \\le x$. -/
/-- If $x$ is a number, then $x \le x$. -/
Statement le_refl (x : ℕ) : x ≤ x := by
Hint "The reason `x ≤ x` is because `x = x + 0`.
So you should start this proof with `use 0`."

5
Game/Levels/LessOrEqual/L02zero_le.lean
View File

@@ -8,10 +8,7 @@ namespace MyNat
Introduction
"
Although subtraction doesn't make sense for general numbers in this game
(because there are no negative numbers in this game), one way of thinking about
how to prove `a ≤ b` is to `use b - a`. See how you get on with this level,
which proves that every number in the game is at least 0.
To solve this level, you need to `use` a number `c` such that `x = 0 + c`.
"
LemmaDoc MyNat.zero_le as "zero_le" in "≤" "

3
Game/Levels/LessOrEqual/L03le_succ_self.lean
View File

@@ -12,6 +12,9 @@ LemmaDoc MyNat.le_succ_self as "le_succ_self" in "≤" "
NewLemma MyNat.le_succ_self
Introduction "If you `use` the wrong number, you get stuck with a goal you can't prove.
What number will you `use` here?"
/-- If $x$ is a number, then $x \le \operatorname{succ}(x)$. -/
Statement le_succ_self (x : ℕ) : x ≤ succ x := by
use 1

42
Game/Levels/LessOrEqual/L05le_trans.lean → Game/Levels/LessOrEqual/L04le_trans.lean
View File

@@ -1,15 +1,12 @@
import Game.Levels.LessOrEqual.L04le_zero
import Game.Levels.LessOrEqual.L03le_succ_self
World "LessOrEqual"
Level 5
Level 4
Title "x ≤ y and y ≤ z implies x ≤ z"
namespace MyNat
LemmaTab "≤"
Introduction "
We have already proved that `x ≤ x`, i.e. that `≤` is *reflexive*. Now let's
prove that it's *transitive*, i.e., that if `x ≤ y` and `y ≤ z` then `x ≤ z`.
"
namespace MyNat
LemmaDoc MyNat.le_trans as "le_trans" in "≤" "
`le_trans x y z` is a proof that if `x ≤ y` and `y ≤ z` then `x ≤ z`.
@@ -19,31 +16,32 @@ If $x \\le y$ then (pause) if $y \\le z$ then $x \\le z$.
## A note on associativity
In Lean, `a + b + c` means `(a + b) + c`, because `+` is left associative. However
`→` is right associative, meaning that `x ≤ y → y ≤ z → x ≤ z` means
exactly that `≤` is transitive.
`→` is right associative. This means that `x ≤ y → y ≤ z → x ≤ z` in Lean means
exactly that `≤` is transitive. This is different to how mathematicians use
$P\\implies Q\\implies R$; for them, this usually means that $P\\implies Q$
and $Q\\implies R$.
"
Introduction "
In this level, we inequalities as *hypotheses*. We have not seen this before.
The `cases` tactic can be used to take `hxy` apart.
"
/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
Statement le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
Hint "If you start with `rcases hxy with ⟨a, ha⟩` then `ha` will be a proof that `y = x + a`.
If you want to instead *define* `y` to be `x + a` then you can do `rcases hxy with ⟨a, rfl⟩`.
This is a time-saving trick. "
rcases hxy with ⟨a, rfl⟩
rcases hyz with ⟨b, rfl⟩
Hint "Start with `cases hxy with a ha`."
cases hxy with a ha
Hint "Now `ha` is a proof that `y = x + a`, and `hxy` has vanished. Similarly, you can destruct
`hyz` into its parts with `cases hyz with b hb`."
cases hyz with b hb
Hint "Now you need to figure out which number to `use`. See if you can take it from here."
use a + b
rw [hb, ha]
exact add_assoc x a b
LemmaTab "≤"
Conclusion "
Here's a four line proof:
```
rcases hxy with ⟨a, rfl⟩
rcases hyz with ⟨b, rfl⟩
use a + b
exact add_assoc x a b
```
A passing mathematician remarks that with reflexivity and transitivity out of the way,
you have proved that `≤` is a *preorder* on `ℕ`.
"

11
Game/Levels/LessOrEqual/L04le_zero.lean → Game/Levels/LessOrEqual/L05le_zero.lean
View File

@@ -1,7 +1,7 @@
import Game.Levels.LessOrEqual.L03le_succ_self
import Game.Levels.LessOrEqual.L04le_trans
World "LessOrEqual"
Level 4
Level 5
Title "x ≤ 0 → x = 0"
namespace MyNat
@@ -11,8 +11,9 @@ LemmaDoc MyNat.le_zero as "le_zero" in "≤" "
"
Introduction "
In this level, our inequality is a *hypothesis*. We have not seen this before.
The `rcases` tactic can be used to take `hx` apart.
It's \"intuitively obvious\" that there are no numbers less than zero,
but to prove it you will need a result which you showed in advanced
addition world.
"
LemmaDoc MyNat.le_zero as "le_zero" in "≤"
@@ -20,8 +21,6 @@ LemmaDoc MyNat.le_zero as "le_zero" in "≤"
/-- If $x \leq 0$, then $x=0$. -/
Statement le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
Hint "Start with `cases hx with y hy`. You can get the funny pointy brackets with `\\<` and
`\\>`, or `\\<>` will give you both at once."
cases hx with y hy
Hint "Now `y` is what you have to add to `x` to get `0`, and `hy` is the proof of this."
Hint (hidden := true) "You want to use `eq_zero_of_add_right_eq_zero`, which you already

16
Game/Levels/LessOrEqual/L06le_antisymm.lean
View File

@@ -1,4 +1,4 @@
import Game.Levels.LessOrEqual.L05le_trans
import Game.Levels.LessOrEqual.L05le_zero
World "LessOrEqual"
Level 6
@@ -18,9 +18,10 @@ It's the trickiest one so far. Good luck!
/-- If $x \leq y$ and $y \leq x$, then $x = y$. -/
Statement le_antisymm (x y : ℕ) (hxy : x ≤ y) (hyx : y ≤ x) : x = y := by
rcases hxy with ⟨a, rfl⟩
rcases hyx with ⟨b, hb⟩
rw [add_assoc] at hb
cases hxy with a ha
cases hyx with b hb
rw [ha]
rw [ha, add_assoc] at hb
symm at hb
apply add_right_eq_self at hb
apply eq_zero_of_add_right_eq_zero at hb
@@ -32,9 +33,10 @@ LemmaTab "≤"
Conclusion "
Here's my proof:
```
rcases hxy with ⟨a, rfl⟩
rcases hyx with ⟨b, hb⟩
rw [add_assoc] at hb
cases hxy with a ha
cases hyx with b hb
rw [ha]
rw [ha, add_assoc] at hb
symm at hb
apply add_right_eq_self at hb
apply eq_zero_of_add_right_eq_zero at hb

25
Game/Levels/LessOrEqual/L07le_total.lean
View File

@@ -6,6 +6,12 @@ Title "x ≤ y or y ≤ x"
namespace MyNat
LemmaDoc MyNat.le_total as "le_total" in "≤" "
`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.
"
NewLemma MyNat.le_total
Introduction "
This is I think the toughest level yet. We haven't talked about \"or\" at all,
but here's everything you need to know.
@@ -18,31 +24,26 @@ progress: `left` and `right`. But don't choose a direction unless your
hypotheses guarantee that it's the right one.
3) If you have an \"or\" statement as a *hypothesis* `h`, then
`rcases h with (h1 | h2)` will create two goals, one where you went left,
`cases h with h1 h2` will create two goals, one where you went left,
and the other where you went right.
"
LemmaDoc MyNat.le_total as "le_total" in "≤" "
`le_total x y` is a proof that `x ≤ y` or `y ≤ x`.
"
NewLemma MyNat.le_total
/-- If $x \leq y$ and $y \leq z$, then $x \leq z$. -/
Statement le_total (x y : ℕ) : x ≤ y ∨ y ≤ x := by
induction y with d hd
right
exact zero_le x
rcases hd with (h1 | h2)
cases hd with h1 h2
left
rcases h1 with ⟨e, rfl⟩
cases h1 with e h1
rw [h1]
use e + 1
rw [succ_eq_add_one, add_assoc]
rfl
rcases h2 with ⟨e, rfl⟩
rcases e with ⟨f⟩
cases h2 with e h2
rw [h2]
cases e with a
left
change d + 0 ≤ succ d
rw [add_zero]
use 1
exact succ_eq_add_one d

11
Game/Levels/Tutorial.lean
View File

@@ -1,10 +1,11 @@
import Game.Levels.Tutorial.L01rfl
import Game.Levels.Tutorial.L02rw
import Game.Levels.Tutorial.L03three_eq_sss0
import Game.Levels.Tutorial.L04add_zero
import Game.Levels.Tutorial.L05add_zero2
import Game.Levels.Tutorial.L06add_succ
import Game.Levels.Tutorial.L07twoaddtwo
import Game.Levels.Tutorial.L03two_eq_ss0
import Game.Levels.Tutorial.L04rw_backwards
import Game.Levels.Tutorial.L05add_zero
import Game.Levels.Tutorial.L06add_zero2
import Game.Levels.Tutorial.L07add_succ
import Game.Levels.Tutorial.L08twoaddtwo
/-!
# Tutorial world

52
Game/Levels/Tutorial/L01rfl.lean
View File

@@ -6,31 +6,9 @@ World "Tutorial"
Level 1
Title "The rfl tactic"
Introduction
"
# Read this first
LemmaTab "numerals"
Each level in this game involves proving a mathematical theorem (the \"Goal\").
The goal will be a statement about *numbers*. Some numbers in this game have known values.
Those numbers have names like $37$. Other numbers will be secret. They're called things
like $x$ and $q$. We know $x$ is a number, we just don't know which one.
In this first level we're going to prove the theorem that $37x + q = 37x + q$.
You can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`
are numbers.
We solve goals in Lean using *Tactics*, and the first tactic we're
going to learn is called `rfl`, which proves all theorems of the form $X = X$.
Prove that $37x+q=37x+q$ by casting the `rfl` tactic.
"
/-- If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$ -/
Statement
(x q : ℕ) : 37 * x + q = 37 * x + q := by
Hint "In order to use the tactic `rfl` you can enter it in the text box
under the goal and hit \"Execute\"."
rfl
namespace MyNat
TacticDoc rfl
"
@@ -70,6 +48,32 @@ as mathematicians are concerned, and who cares what the definition of addition i
NewTactic rfl
Introduction
"
# Read this first
Each level in this game involves proving a mathematical theorem (the \"Goal\").
The goal will be a statement about *numbers*. Some numbers in this game have known values.
Those numbers have names like $37$. Other numbers will be secret. They're called things
like $x$ and $q$. We know $x$ is a number, we just don't know which one.
In this first level we're going to prove the theorem that $37x + q = 37x + q$.
You can see `x q : ℕ` in the *Objects* below, which means that `x` and `q`
are numbers.
We solve goals in Lean using *Tactics*, and the first tactic we're
going to learn is called `rfl`, which proves all theorems of the form $X = X$.
Prove that $37x+q=37x+q$ by executing the `rfl` tactic.
"
/-- If $x$ and $q$ are arbitrary natural numbers, then $37x+q=37x+q.$ -/
Statement
(x q : ℕ) : 37 * x + q = 37 * x + q := by
Hint "In order to use the tactic `rfl` you can enter it in the text box
under the goal and hit \"Execute\"."
rfl
Conclusion
"
Congratulations! You completed your first verified proof!

45
Game/Levels/Tutorial/L02rw.lean
View File

@@ -6,26 +6,9 @@ World "Tutorial"
Level 2
Title "the rw tactic"
Introduction
"
In this level the *goal* is $2y=2(x+7)$ but to help us we
have an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in
your list of assumptions. Lean thinks of `h` as being a secret proof of the
assumption, rather like `x` is a secret number.
LemmaTab "numerals"
Before we can use `rfl`, we have to \"substitute in for $y$\".
We do this in Lean by *rewriting* the proof `h`,
using the `rw` tactic.
"
/-- If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$. -/
Statement
(x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
Hint "First execute `rw [h]` to replace the `y` with `x + 7`."
rw [h]
Hint "Can you take it from here? Click on \"Show more help!\" if you need a hint."
Hint (hidden := true) "Now `rfl` will work."
rfl
namespace MyNat
TacticDoc rw "
## Summary
@@ -160,10 +143,34 @@ will change the goal to `succ 1 + succ 1 = 4`.
NewHiddenTactic nth_rewrite
Introduction
"
In this level the *goal* is $2y=2(x+7)$ but to help us we
have an *assumption* `h` saying that $y = x + 7$. Check that you can see `h` in
your list of assumptions. Lean thinks of `h` as being a secret proof of the
assumption, rather like `x` is a secret number.
Before we can use `rfl`, we have to \"substitute in for $y$\".
We do this in Lean by *rewriting* the proof `h`,
using the `rw` tactic.
"
/-- If $x$ and $y$ are natural numbers, and $y = x + 7$, then $2y = 2(x + 7)$. -/
Statement
(x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
Hint "First execute `rw [h]` to replace the `y` with `x + 7`."
rw [h]
Hint "Can you take it from here? Click on \"Show more help!\" if you need a hint."
Hint (hidden := true) "Now `rfl` will work."
rfl
Conclusion
"You now know enough tactics to prove `2 + 2 = 4`! Let's begin the journey.
"
/-
**TODO** where to put this? Not this early.
You can now press on by clicking \"Next\", but if you want to inspect the
proof you just created, toggle \"Editor mode\" by clicking
on the `</>` button in the top right. In editor mode,

72
Game/Levels/Tutorial/L03three_eq_sss0.lean → Game/Levels/Tutorial/L03two_eq_ss0.lean
View File

@@ -8,38 +8,6 @@ Title "Numbers"
namespace MyNat
Introduction
"
## The birth of number.
Numbers in Lean are defined by two rules.
* `0` is a number.
* If `n` is a number, then the *successor* `succ n` of `n` is a number.
The successor of `n` means the number after `n`. Let's learn to
count, and name a few small numbers.
## Counting to four.
`0` is a number, so `succ 0` is a number. Let's call this new number `1`.
Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.
This gives us plenty of numbers to be getting along with.
The *proof* that `3 = succ 2` is called `three_eq_succ_two`.
Check out the \"numerals\" tab in the list of lemmas on the right.
"
/-- $3$ is the number after the number after the number after $0$. -/
Statement
: 3 = succ (succ (succ 0)) := by
Hint "Start with `rw [three_eq_succ_two]` to begin to break `3` down."
rw [three_eq_succ_two]
Hint (hidden := true) "If you're in a hurry, try `rw [two_eq_succ_one, one_eq_succ_zero]`."
rw [two_eq_succ_one]
rw [one_eq_succ_zero]
Hint (hidden := true) "Now finish the job with `rfl`."
rfl
DefinitionDoc MyNat as "ℕ"
"
`ℕ` is the natural numbers, just called \"numbers\" in this game. It's
@@ -71,14 +39,44 @@ LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals"
NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
MyNat.four_eq_succ_three
Introduction
"
## The birth of number.
Numbers in Lean are defined by two rules.
* `0` is a number.
* If `n` is a number, then the *successor* `succ n` of `n` is a number.
The successor of `n` means the number after `n`. Let's learn to
count, and name a few small numbers.
## Counting to four.
`0` is a number, so `succ 0` is a number. Let's call this new number `1`.
Similarly let's define `2 = succ 1`, `3 = succ 2` and `4 = succ 3`.
This gives us plenty of numbers to be getting along with.
The *proof* that `2 = succ 1` is called `two_eq_succ_one`.
Check out the \"numerals\" tab in the list of lemmas on the right.
Let's prove that $2$ is the number after the number after zero.
"
/-- $2$ is the number after the number after $0$. -/
Statement
: 2 = succ (succ 0) := by
Hint "Start with `rw [two_eq_succ_one]` to begin to break `2` down into its definition."
rw [two_eq_succ_one]
Hint "Can you take it from here?"
Hint (hidden := true) "Next turn `1` into `succ 0` with `rw [one_eq_succ_zero]`."
rw [one_eq_succ_zero]
Hint (hidden := true) "Now finish the job with `rfl`."
rfl
LemmaTab "numerals"
Conclusion
"
Note that you can do
`rw [three_eq_succ_two, two_eq_succ_one, one_eq_succ_zero]`
Note that you can do `rw [two_eq_succ_one, one_eq_succ_zero]`
and then `rfl` to solve this level in two lines.
Why did we not just define `succ n` to be `n + 1`? Because we have not
even *defined* addition yet! We'll do that in the next level.
"

37
Game/Levels/Tutorial/L04rw_backwards.lean Normal file
View File

@@ -0,0 +1,37 @@
import Game.Metadata
import Game.MyNat.TutorialLemmas
World "Tutorial"
Level 4
Title "rewriting backwards"
LemmaTab "numerals"
namespace MyNat
Introduction
"
If `h` is a proof of `X = Y` then `rw [h]` will
turn `X`s into `Y`s. But what if we want to
turn `Y`s into `X`s? To tell the `rw` tactic
we want this, we use a left arrow `←`. Type
`\\l` and then hit the space bar to get this arrow.
Let's prove that $2$ is the number after the number
after $0$ again, this time by changing `succ (succ 0)`
into `2`.
"
/-- $2$ is the number after the number after $0$. -/
Statement : 2 = succ (succ 0) := by
Hint "Try `rw [← one_eq_succ_zero]` to change `succ 0` into `1`."
rw [← one_eq_succ_zero]
Hint "What next?"
Hint (hidden := true) "Now `rw [← two_eq_succ_one]` will change `succ 1` into `2`."
rw [← two_eq_succ_one]
rfl
Conclusion "
Why did we not just define `succ n` to be `n + 1`? Because we have not
even *defined* addition yet! We'll do that in the next level.
"

72
Game/Levels/Tutorial/L04add_zero.lean → Game/Levels/Tutorial/L05add_zero.lean
View File

@@ -2,46 +2,11 @@ import Game.Metadata
import Game.MyNat.Addition
World "Tutorial"
Level 4
Level 5
Title "Adding zero"
Introduction
"
We'd like to prove `2 + 2 = 4` but right now
we can't even *state* it
because we haven't yet defined addition.
## Defining addition.
How are we going to add $37$ to an arbitrary number $x$? Well,
there are only two ways to make numbers in this game: $0$
and successors. So to define `37 + x` we will need
to know what `37 + 0` is and what `37 + succ x` is.
Let's start with adding `0`.
### Adding 0
To make addition agree with our intuition, we should *define* `37 + 0`
to be `37`. More generally, we should define `a + 0` to be `a` for
any number `a`. The name of this proof in Lean is `add_zero a`.
* `add_zero 37 : 37 + 0 = 37`
* `add_zero a : a + 0 = a`
*` add_zero : ? + 0 = ?`
"
namespace MyNat
/-- $a+(b+0)+(c+0)=a+b+c.$ -/
Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
Hint "`rw [add_zero]` will change `b + 0` into `b`."
rw [add_zero b]
Hint "Now `rw [add_zero]` will change `c + 0` into `c`."
rw [add_zero]
rfl
DefinitionDoc Add as "+" "`Add a b`, with notation `a + b`, is
the usual sum of natural numbers. Internally it is defined
via the following two hypotheses:
@@ -97,6 +62,41 @@ into the goal
NewHiddenTactic «repeat»
Introduction
"
We'd like to prove `2 + 2 = 4` but right now
we can't even *state* it
because we haven't yet defined addition.
## Defining addition.
How are we going to add $37$ to an arbitrary number $x$? Well,
there are only two ways to make numbers in this game: $0$
and successors. So to define `37 + x` we will need
to know what `37 + 0` is and what `37 + succ x` is.
Let's start with adding `0`.
### Adding 0
To make addition agree with our intuition, we should *define* `37 + 0`
to be `37`. More generally, we should define `a + 0` to be `a` for
any number `a`. The name of this proof in Lean is `add_zero a`.
* `add_zero 37 : 37 + 0 = 37`
* `add_zero a : a + 0 = a`
*` add_zero : ? + 0 = ?`
"
/-- $a+(b+0)+(c+0)=a+b+c.$ -/
Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
Hint "`rw [add_zero]` will change `b + 0` into `b`."
rw [add_zero]
Hint "Now `rw [add_zero]` will change `c + 0` into `c`."
rw [add_zero]
rfl
Conclusion "Those of you interested in speedrunning the game may want to know
that `repeat rw [add_zero]` will do both rewrites at once.
"

7
Game/Levels/Tutorial/L05add_zero2.lean → Game/Levels/Tutorial/L06add_zero2.lean
View File

@@ -3,7 +3,7 @@ import Game.MyNat.Addition
World "Tutorial"
Level 5
Level 6
Title "Precision rewriting"
Introduction
@@ -23,8 +23,9 @@ namespace MyNat
Statement (a b c : ℕ) : a + (b + 0) + (c + 0) = a + b + c := by
Hint "Try `rw [add_zero c]`."
rw [add_zero c]
Hint "You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. It's
usually easiest to stick to `add_zero` if it works though."
Hint "`add_zero c` is a proof of `c + 0 = c` so that was what got rewritten.
You can now change `b + 0` to `b` with `rw [add_zero]` or `rw [add_zero b]`. You
can usually stick to `add_zero` unless you need real precision."
rw [add_zero]
rfl

27
Game/Levels/Tutorial/L06add_succ.lean → Game/Levels/Tutorial/L07add_succ.lean
View File

@@ -1,11 +1,21 @@
import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L03three_eq_sss0
import Game.Levels.Tutorial.L03two_eq_ss0
World "Tutorial"
Level 6
Level 7
Title "add_succ"
namespace MyNat
LemmaDoc MyNat.add_succ as "add_succ" in "Add"
"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
"`succ_eq_add_one n` is the proof that `succ n = n + 1`."
NewLemma MyNat.add_succ MyNat.succ_eq_add_one
Introduction
"
Every number in Lean is either 0 or a successor. We know how to add $0$,
@@ -24,15 +34,6 @@ Let's now prove that `succ n = n + 1`. Figure out how to get `+ succ` into
the picture, and then `rw [add_succ]`. Use the Add and Numerals tabs to
switch between lemmas so you can see which proofs you can rewrite.
"
namespace MyNat
LemmaDoc MyNat.add_succ as "add_succ" in "Add"
"`add_succ a b` is the proof of `a + succ b = succ (a + b)`."
NewLemma MyNat.add_succ
LemmaDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "Add"
"`succ_eq_add_one n` is the proof that `succ n = n + 1`."
/-- For all natural numbers $a$, we have $\operatorname{succ}(a) = a+1$. -/
Statement succ_eq_add_one n : succ n = n + 1 := by
@@ -45,7 +46,9 @@ Statement succ_eq_add_one n : succ n = n + 1 := by
Hint (hidden := true) "And finally `rfl`."
rfl
LemmaTab "Add"
NewLemma MyNat.succ_eq_add_one
LemmaTab "numerals"
Conclusion
"[dramatic music]. Now are you ready to face the first boss of the game?"

62
Game/Levels/Tutorial/L07twoaddtwo.lean → Game/Levels/Tutorial/L08twoaddtwo.lean
View File

@@ -1,35 +1,15 @@
import Game.Metadata
import Game.MyNat.Addition
import Game.Levels.Tutorial.L06add_succ
import Game.Levels.Tutorial.L07add_succ
World "Tutorial"
Level 7
Level 8
Title "2+2=4"
LemmaTab "numerals"
Introduction
" Good luck!
One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.
If you only want to change one of them, say the 3rd one, then use
`nth_rewrite 3 [h]`.
"
namespace MyNat
/-- $2+2=4$. -/
Statement : (2 : ℕ) + 2 = 4 := by
Hint (hidden := true) "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
nth_rewrite 2 [two_eq_succ_one]
Hint (hidden := true) "Now you can `rw [add_succ]`"
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rw [four_eq_succ_three]
rw [three_eq_succ_two]
rfl
TacticDoc nth_rewrite "
## Summary
@@ -45,19 +25,39 @@ will change the goal to `succ 1 + succ 1 = 4`.
NewHiddenTactic nth_rewrite
Conclusion
Introduction
" Good luck!
One last hint. If `h : X = Y` then `rw [h]` will change *all* `X`s into `Y`s.
If you only want to change one of them, say the 3rd one, then use
`nth_rewrite 3 [h]`.
"
Here is an example proof showing off various techniques. You can copy
and paste it directly into Lean if you switch into editor mode, and then
you can inspect it by clicking around within the proof or moving your cursor
down the lines.
Click on `</>` and `>_` in the top right to switch between editor mode
and command line mode. Switch back to command line mode
when you've finished, if you prefer to see hints.
/-- $2+2=4$. -/
Statement : (2 : ℕ) + 2 = 4 := by
Hint (hidden := true) "`nth_rewrite 2 [two_eq_succ_one]` is I think quicker than `rw [two_eq_succ_one]`."
nth_rewrite 2 [two_eq_succ_one]
Hint (hidden := true) "Now you can `rw [add_succ]`"
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]
rw [four_eq_succ_three]
rw [three_eq_succ_two]
rfl
Conclusion
"
Below is an example proof showing off various techniques. You can copy
and paste it directly into Lean if you switch into editor mode, and then
you can inspect it by clicking around within the proof or moving your cursor
down the lines.
Click on `</>` and `>_` in the top right to switch between editor mode
and command line mode. Switch back to command line mode
when you've finished, if you prefer to see hints.
```lean
nth_rewrite 2 [two_eq_succ_one]
nth_rewrite 2 [two_eq_succ_one] -- only change the second `2` to `succ 1`.
rw [add_succ]
rw [one_eq_succ_zero]
rw [add_succ, add_zero] -- two rewrites at once