-
Notifications
You must be signed in to change notification settings - Fork 30
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
5 changed files
with
144 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,39 @@ | ||
import Game.Levels.LessOrEqual.L08le_total | ||
|
||
World "LessOrEqual" | ||
Level 9 | ||
Title "succ x ≤ succ y → x ≤ y" | ||
|
||
LemmaTab "≤" | ||
|
||
namespace MyNat | ||
|
||
LemmaDoc MyNat.le_of_succ_le_succ as "le_of_succ_le_succ" in "≤" " | ||
`le_of_succ_le_succ x y` is a proof that if `succ x ≤ succ y` then `x ≤ y`. | ||
" | ||
|
||
Introduction " | ||
The last goal in this world is to prove which numbers are `≤ 2`. | ||
This lemma will be helpful for that. | ||
" | ||
|
||
/-- If $\operatorname{succ}(x) \leq \operatorname{succ}(y)$ then $x \leq y$. -/ | ||
Statement le_of_succ_le_succ (x y : ℕ) (hx : succ x ≤ succ y) : x ≤ y := by | ||
cases hx with d hd | ||
use d | ||
rw [succ_add] at hd | ||
apply succ_inj at hd | ||
exact hd | ||
|
||
Conclusion " | ||
Here's my proof: | ||
``` | ||
cases hx with d hd | ||
use d | ||
rw [succ_add] at hd | ||
apply succ_inj at hd | ||
exact hd | ||
``` | ||
This lemma can be helpful for the next two levels. | ||
" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,46 @@ | ||
import Game.Levels.LessOrEqual.L09le_of_succ_le_succ | ||
World "LessOrEqual" | ||
Level 10 | ||
Title "x ≤ 1" | ||
|
||
LemmaTab "≤" | ||
|
||
namespace MyNat | ||
|
||
LemmaDoc MyNat.le_one as "le_one" in "≤" " | ||
`le_one x` is a proof that if `x ≤ 1` then `x = 0` or `x = 1`. | ||
" | ||
|
||
Introduction " | ||
We've seen `le_zero`, the proof that if `x ≤ 0` then `x = 0`. | ||
Now we'll prove that if `x ≤ 1` then `x = 0` or `x = 1`. | ||
" | ||
|
||
/-- If $x \leq 1$ then either $x = 0$ or $x = 1$. -/ | ||
Statement le_one (x : ℕ) (hx : x ≤ 1) : x = 0 ∨ x = 1 := by | ||
cases x with y | ||
left | ||
rfl | ||
rw [one_eq_succ_zero] at hx ⊢ | ||
apply le_of_succ_le_succ at hx | ||
apply le_zero at hx | ||
rw [hx] | ||
right | ||
rfl | ||
|
||
Conclusion " | ||
Here's my proof: | ||
``` | ||
cases x with y | ||
left | ||
rfl | ||
rw [one_eq_succ_zero] at hx ⊢ | ||
apply le_of_succ_le_succ at hx | ||
apply le_zero at hx | ||
rw [hx] | ||
right | ||
rfl | ||
``` | ||
If you solved this level then you should be fine with the next level! | ||
" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,48 @@ | ||
import Game.Levels.LessOrEqual.L10le_one | ||
World "LessOrEqual" | ||
Level 11 | ||
Title "le_two" | ||
|
||
namespace MyNat | ||
|
||
LemmaTab "012" | ||
|
||
LemmaDoc MyNat.le_two as "le_two" in "≤" " | ||
`le_two x` is a proof that if `x ≤ 2` then `x = 0` or `x = 1` or `x = 2`. | ||
" | ||
|
||
Introduction " | ||
We'll need this lemma to prove that two is prime! | ||
You'll need to know that `∨` is right associative. This means that | ||
`x = 0 ∨ x = 1 ∨ x = 2` actually means `x = 0 ∨ (x = 1 ∨ x = 2)`. | ||
" | ||
|
||
/-- If $x \leq 2$ then $x = 0$ or $1$ or $2$. -/ | ||
Statement le_two (x : ℕ) (hx : x ≤ 2) : x = 0 ∨ x = 1 ∨ x = 2 := by | ||
cases x with y | ||
left | ||
rfl | ||
cases y with z | ||
right | ||
left | ||
rw [one_eq_succ_zero] | ||
rfl | ||
rw [two_eq_succ_one, one_eq_succ_zero] at hx ⊢ | ||
apply le_of_succ_le_succ at hx | ||
apply le_of_succ_le_succ at hx | ||
apply le_zero at hx | ||
rw [hx] | ||
right | ||
right | ||
rfl | ||
|
||
|
||
Conclusion " | ||
Nice! | ||
The next step in the development of order theory is to develop | ||
the theory of the interplay between `≤` and multiplication. | ||
If you've already done Multiplication World, step into | ||
Advanced Multiplication World (once I've written it...) | ||
" |