Skip to content

Commit

Permalink
start on <= world
Browse files Browse the repository at this point in the history
  • Loading branch information
kbuzzard committed Oct 13, 2023
1 parent 39a9c26 commit 7e4226e
Show file tree
Hide file tree
Showing 26 changed files with 165 additions and 38 deletions.
4 changes: 2 additions & 2 deletions Game.lean
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,9 @@ import Game.Levels.Multiplication
import Game.Levels.Power
import Game.Levels.Implication
import Game.Levels.AdvAddition
import Game.Levels.LessOrEqual
--import Game.Levels.AdvMultiplication
--import Game.Levels.EvenOdd
--import Game.Levels.Inequality
--import Game.Levels.Prime
--import Game.Levels.StrongInduction
--import Game.Levels.Hard
Expand Down Expand Up @@ -102,5 +102,5 @@ Dependency Addition → Multiplication → Power
--Dependency Addition → AdvAddition → AdvMultiplication → Inequality → Prime → Hard
--Dependency Multiplication → AdvMultiplication
--Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
Dependency Addition → Implication → AdvAddition
Dependency Addition → Implication → AdvAddition → LessOrEqual
MakeGame
35 changes: 0 additions & 35 deletions Game/Levels/Inequality.lean

This file was deleted.

21 changes: 21 additions & 0 deletions Game/Levels/LessOrEqual.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
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

World "LessOrEqual"
Title "≤ World"

Introduction
"
In this world we define `a ≤ b` and prove standard facts
about it, such as \"if `a ≤ b` and `b ≤ c` then `a ≤ c`.\"
The definition of `a ≤ b` is \"there exists a number `c`
such that `b = a + c`. \" So we're going to have to learn
a tactic to prove \"exists\" theorems, and another one
to use \"exists\" hypotheses.
Click on \"Start\" to proceed.
"
53 changes: 53 additions & 0 deletions Game/Levels/LessOrEqual/L01le_refl.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
import Game.Metadata
import Game.MyNat.LE
import Game.Tactic.Use
import Game.Levels.AdvAddition

World "LessOrEqual"
Level 1
Title "The `use` tactic"

namespace MyNat

TacticDoc use "
## Summary
The `use` tactic makes progress with goals which claim something *exists*.
If the goal claims that some `x` exists with some property, and you know
that `x = 37` will work, then `use 37` will make progress.
Because `a ≤ b` is notation for \"there exists `c` such that `b = a + c`\",
you can make progress on goals of the form `a ≤ b` by `use`ing the
number which is morally `b - a`.
"

NewTactic use

Introduction
"
`a ≤ b` is *notation* for `∃ c, b = a + c`. This \"backwards E\"
means \"there exists\". So `a ≤ b` means that there exists
a number `c` such that `b = a + c`. This definition works
because there are no negative numbers in this game.
To *prove* an \"exists\" statement, use the `use` tactic.
Let's see an example.
"

LemmaDoc MyNat.le_refl as "le_refl" in "≤" "
`le_refl x` is a proof of `x ≤ x`.
The reason for the name is that this lemma is \"reflexivity of $\\le$\"
"

/-- 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`."
use 0
Hint "You can probably take it from here."
rw [add_zero]
rfl


LemmaTab "≤"
23 changes: 23 additions & 0 deletions Game/Levels/LessOrEqual/L02zero_le.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
import Game.Levels.LessOrEqual.L01le_refl

World "LessOrEqual"
Level 2
Title "0 ≤ x"

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.
"

/-- If $x$ is a number, then $0 \\le x$. -/
Statement le_refl (x : ℕ) : 0 ≤ x := by
use x
rw [zero_add]
rfl

LemmaTab "≤"
26 changes: 26 additions & 0 deletions Game/Levels/LessOrEqual/L03le_succ_self.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
import Game.Levels.LessOrEqual.L02zero_le

World "LessOrEqual"
Level 3
Title "x ≤ succ x"

namespace MyNat

/-- If $x$ is a number, then $x \\le \\mathoperator{succ}(x)$. -/
Statement le_succ_self (x : ℕ) : x ≤ succ x := by
use 1
rw [succ_eq_add_one]
rfl

LemmaTab "≤"

/-
Introduction
"
Because constanly rewriting `zero_add` and `add_zero` is a bit dull,
let's unlock the `ring` tactic. This will prove any goal which is \"true
in the language of ring theory\", for example `a + b + c = c + b + a`.
It doesn't understand `succ` though, so use `succ_eq_add_one` in this
level to get rid of it.
"
-/
31 changes: 31 additions & 0 deletions Game/Levels/LessOrEqual/L04le_zero.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
import Game.Levels.LessOrEqual.L03le_succ_self

World "LessOrEqual"
Level 4
Title "x ≤ 0 → x = 0"

namespace MyNat

Introduction "
In this level, our inequality is a *hypothesis*. We have not seen this before.
"
/-- If $x \leq 0$, then $x=0$. -/
Statement le_zero (x : ℕ) (hx : x ≤ 0) : x = 0 := by
cases' hx with y hy
symm at hy
apply eq_zero_of_add_right_eq_zero at hy
exact hy

LemmaTab "≤"

/-
Introduction
"
Because constanly rewriting `zero_add` and `add_zero` is a bit dull,
let's unlock the `ring` tactic. This will prove any goal which is \"true
in the language of ring theory\", for example `a + b + c = c + b + a`.
It doesn't understand `succ` though, so use `succ_eq_add_one` in this
level to get rid of it.
"
-/
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,19 @@ leevl 8 not P = P -> false (no explanation of false?)
Advanced Prop world ;
level 1 split
level 2 rcases
(for and)
(for and)
(note that level 1 is now consructor)
level 6 left and right
level 9 exfalso (because \not is involved)
level 10 by_cases

Advanced addition world: start with level 0 exact
level 1 apply

TODO in this game:
have
split
rcases
left
right
by_cases? exfalso?

0 comments on commit 7e4226e

Please sign in to comment.