split off test game
still need to adapt the call to the lean binary to provide two arguments
This commit is contained in:
Alexander Bentkamp
@@ -0,0 +1,2 @@
|
||||
import GameServer.Commands
|
||||
import GameServer.Server
|
||||
@@ -1,7 +1,7 @@
|
||||
import Lean
|
||||
|
||||
import NNG.GameServer.Utils
|
||||
import NNG.GameServer.EnvExtensions
|
||||
import GameServer.Utils
|
||||
import GameServer.EnvExtensions
|
||||
|
||||
open Lean Meta
|
||||
|
||||
@@ -1,5 +1,5 @@
|
||||
import NNG.GameServer.HashMapExtension
|
||||
import NNG.GameServer.SingleValPersistentEnvExtension
|
||||
import GameServer.HashMapExtension
|
||||
import GameServer.SingleValPersistentEnvExtension
|
||||
|
||||
/-! # Environment extensions
|
||||
|
||||
@@ -6,8 +6,8 @@ It is based on lean-gym by Daniel Selsam.
|
||||
-/
|
||||
import Lean.Data.Json.Basic
|
||||
|
||||
import NNG.GameServer.Utils
|
||||
import NNG.GameServer.EnvExtensions
|
||||
import GameServer.Utils
|
||||
import GameServer.EnvExtensions
|
||||
|
||||
open Lean Meta Elab Tactic Std
|
||||
|
||||
@@ -223,7 +223,7 @@ where
|
||||
open System Lean Std in
|
||||
partial def runGame (GameName : Name) (paths : List FilePath): IO Unit := do
|
||||
searchPathRef.set paths
|
||||
let env ← importModules [{ module := `Init : Import }, { module := GameName ++ GameName : Import }] {} 0
|
||||
let env ← importModules [{ module := `Init : Import }, { module := GameName : Import }] {} 0
|
||||
let termElabM : TermElabM Unit := do
|
||||
let levels := levelsExt.getState env
|
||||
let game := {← gameExt.get with nb_levels := levels.size }
|
||||
+14
-11
@@ -1,13 +1,16 @@
|
||||
import NNG.GameServer.Server
|
||||
import NNG.NNG
|
||||
import GameServer.Server
|
||||
|
||||
def System.FilePath.parent! (fp : System.FilePath) : System.FilePath :=
|
||||
match fp.parent with
|
||||
| some path => path
|
||||
| none => panic! "Couldn't find parent folder"
|
||||
unsafe def main (args : List String) : IO Unit := do
|
||||
|
||||
unsafe def main : IO Unit := do
|
||||
let build_folder := (← IO.appPath).parent!.parent!
|
||||
let paths : List System.FilePath := [build_folder/"lib",
|
||||
(← Lean.findSysroot) / "lib" / "lean"]
|
||||
Server.runGame `NNG paths
|
||||
if args.length != 2 then
|
||||
throw (IO.userError "Expected two arguments: The name of the game module and the path to the game project.")
|
||||
|
||||
let out ← IO.Process.output { cwd := args[1]!, cmd := "lake", args := #["env","printenv","LEAN_PATH"] }
|
||||
|
||||
if out.exitCode != 0 then
|
||||
IO.eprintln out.stderr
|
||||
else
|
||||
let paths : List System.FilePath := System.SearchPath.parse out.stdout.trim
|
||||
let currentDir ← IO.currentDir
|
||||
let paths := paths.map fun p => currentDir / (args[1]! : System.FilePath) / p
|
||||
Server.runGame (Lean.Name.mkSimple args[0]!) paths
|
||||
|
||||
@@ -1,14 +0,0 @@
|
||||
import NNG.GameServer.Commands
|
||||
import NNG.MyNat
|
||||
|
||||
LemmaDoc zero_add as zero_add in "Addition"
|
||||
"This lemma says `∀ a : ℕ, 0 + a = a`."
|
||||
|
||||
LemmaDoc add_zero as add_zero in "Addition"
|
||||
"This lemma says `∀ a : ℕ, a + 0 = a`."
|
||||
|
||||
LemmaDoc add_succ as add_succ in "Addition"
|
||||
"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
|
||||
|
||||
LemmaSet addition : "Addition lemmas" :=
|
||||
zero_add add_zero
|
||||
@@ -1,26 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Level 1
|
||||
|
||||
Title "The reflexivity spell"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Let's learn a first spell: the `rfl` spell. `rfl` stands for \"reflexivity\", which is a fancy
|
||||
way of saying that it will prove any goal of the form `A = A`. It doesn't matter how
|
||||
complicated `A` is, all that matters is that the left hand side is *exactly equal* to the
|
||||
right hand side (a computer scientist would say \"definitionally equal\"). I really mean
|
||||
\"press the same buttons on your computer in the same order\" equal.
|
||||
For example, `x * y + z = x * y + z` can be proved by `rfl`, but `x + y = y + x` cannot.
|
||||
This is a very low level spell, but you need to start somewhere.
|
||||
|
||||
After closing this message, type rfl in the invocation zone and hit Enter or click
|
||||
the \"Cast spell\" button.
|
||||
"
|
||||
|
||||
Statement (x y z : ℕ) : x * y + z = x * y + z := by
|
||||
rfl
|
||||
|
||||
Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button."
|
||||
|
||||
Tactics rfl
|
||||
@@ -1,36 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Level 2
|
||||
|
||||
Title "The rewriting spell"
|
||||
|
||||
Introduction
|
||||
"
|
||||
The rewrite spell is the way to \"substitute in\" the value
|
||||
of an expression. In general, if you have a hypothesis of the form `A = B`, and your
|
||||
goal mentions the left hand side `A` somewhere, then
|
||||
the `rewrite` tactic will replace the `A` in your goal with a `B`.
|
||||
|
||||
The documentation for `rewrite` just appeared in your spell book.
|
||||
Play around with the menus and see what is there currently.
|
||||
More information will appear as you progress.
|
||||
|
||||
Take a look in the top right box at what we have.
|
||||
The variables $x$ and $y$ are natural numbers, and we have
|
||||
an assumption `h` that $y = x + 7$. Our goal
|
||||
is to prove that $2y=2(x+7)$. This goal is obvious -- we just
|
||||
substitute in $y = x+7$ and we're done. In Lean, we do
|
||||
this substitution using the `rewrite` spell. This spell takes a list of equalities
|
||||
or equivalences so you can cast `rewrite [h]`.
|
||||
"
|
||||
|
||||
Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by
|
||||
rewrite [h]
|
||||
rfl
|
||||
|
||||
Message (x : ℕ) (y : ℕ) (h : y = x + 7) : 2*(x + 7) = 2*(x + 7) =>
|
||||
"Great! Now the goal should be easy to reach using the `rfl` spell."
|
||||
|
||||
Conclusion "Congratulations for completing your second level!"
|
||||
|
||||
Tactics rfl rewrite
|
||||
@@ -1,81 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Level 3
|
||||
|
||||
Title "Peano's axioms"
|
||||
|
||||
Introduction
|
||||
"
|
||||
The team that salvaged the type `ℕ` of natural numbers actually got us three things:
|
||||
|
||||
* a term `0 : ℕ`, interpreted as the number zero.
|
||||
* a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after $n$\".
|
||||
* The principle of mathematical induction.
|
||||
|
||||
These are essentially the axioms isolated by Peano which uniquely characterise
|
||||
the natural numbers (we also need recursion, but we can ignore it for now).
|
||||
The first axiom says that $0$ is a natural number. The second says that there
|
||||
is a `succ` function which eats a number and spits out the number after it,
|
||||
so $\\operatorname{succ}(0)=1$, $\\operatorname{succ}(1)=2$ and so on.
|
||||
|
||||
Peano's last axiom is the principle of mathematical induction. This is a deeper
|
||||
fact. It says that if we have infinitely many true/false statements $P(0)$, $P(1)$,
|
||||
$P(2)$ and so on, and if $P(0)$ is true, and if for every natural number $d$
|
||||
we know that $P(d)$ implies $P(\\operatorname{succ}(d))$, then $P(n)$ must be true for every
|
||||
natural number $n$. It's like saying that if you have a long line of dominoes, and if
|
||||
you knock the first one down, and if you know that if a domino falls down then the one
|
||||
after it will fall down too, then you can deduce that all the dominos will fall down.
|
||||
One can also think of it as saying that every natural number
|
||||
can be built by starting at `0` and then applying `succ` a finite number of times.
|
||||
|
||||
Peano's insights were firstly that these axioms completely characterise
|
||||
the natural numbers, and secondly that these axioms alone can be used to build
|
||||
a whole bunch of other structure on the natural numbers, for example
|
||||
addition, multiplication and so on.
|
||||
|
||||
This game is all about seeing how far these axioms of Peano can take us.
|
||||
|
||||
Let's practice our use of the `rewrite` tactic in the following example.
|
||||
Our hypothesis `h` is a proof that `succ(a) = b` and we want to prove that
|
||||
`succ(succ(a))=succ(b)`. In words, we're going to prove that if
|
||||
`b` is the number after `a` then `succ(b)` is the number after `succ(a)`.
|
||||
Note that the system drops brackets when they're not
|
||||
necessary, so `succ b` just means `succ(b)`.
|
||||
|
||||
Now here's a tricky question. Knowing that our goal is `succ (succ a) = succ b`,
|
||||
and our assumption is `h : succ a = b`, then what will the goal change
|
||||
to when we type
|
||||
|
||||
`rewrite [h]`
|
||||
|
||||
and hit enter? Remember that `rewrite [h]` will
|
||||
look for the *left* hand side of `h` in the goal, and will replace it with
|
||||
the *right* hand side. Try and figure out how the goal will change, and
|
||||
then try it.
|
||||
"
|
||||
|
||||
Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by
|
||||
rewrite [h]
|
||||
rfl
|
||||
|
||||
Message (a : ℕ) (b : ℕ) (h : succ a = b) : succ b = succ b =>
|
||||
"
|
||||
Look: Lean changed `succ a` into `b`, so the goal became `succ b = succ b`.
|
||||
That goal is of the form `X = X`, so you know what to do.
|
||||
"
|
||||
|
||||
|
||||
Conclusion "Congratulations for completing the third level!
|
||||
You may be wondering whether we could have just substituted in the definition of `b`
|
||||
and proved the goal that way. To do that, we would want to replace the right hand
|
||||
side of `h` with the left hand side. You do this in Lean by writing `rewrite [<- h]`. You get the
|
||||
left-arrow by typing `\\l` and then a space; note that this is a small letter L,
|
||||
not a number 1. You can just edit your proof and try it.
|
||||
|
||||
You may also be wondering why we keep writing `succ(b)` instead of `b+1`. This
|
||||
is because we haven't defined addition yet! On the next level, the final level
|
||||
of the tutorial, we will introduce addition, and then
|
||||
we'll be ready to enter Addition World.
|
||||
"
|
||||
|
||||
Tactics rfl rewrite
|
||||
@@ -1,62 +0,0 @@
|
||||
import NNG.Metadata
|
||||
|
||||
Level 4
|
||||
|
||||
Title "Addition"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Peano defined addition `a + b` by induction on `b`, or,
|
||||
more precisely, by *recursion* on `b`. He first explained how to add 0 to a number:
|
||||
this is the base case.
|
||||
|
||||
* `add_zero (a : ℕ) : a + 0 = a`
|
||||
|
||||
We will call this theorem `add_zero`. It has just appeared in your inventory!
|
||||
Mathematicians sometimes call it \"Lemma 2.1\" or \"Hypothesis P6\" or something. But
|
||||
computer scientists call it `add_zero` because it tells you
|
||||
what the answer to \"$x$ add zero\" is. It's a *much* better name than \"Lemma 2.1\".
|
||||
Even better, we can use the rewrite tactic with `add_zero`.
|
||||
If you ever see `x + 0` in your goal, `rewrite [add_zero]` will simplify it to `x`.
|
||||
This is because `add_zero` is a proof that `x + 0 = x` (more precisely,
|
||||
`add_zero x` is a proof that `x + 0 = x` but Lean can figure out the `x` from the context).
|
||||
|
||||
Now here's the inductive step. If you know how to add `d` to `a`, then
|
||||
Peano tells you how to add `succ(d)` to `a`. It looks like this:
|
||||
|
||||
* `add_succ (a d : ℕ) : a + succ(d) = succ (a + d)`
|
||||
|
||||
What's going on here is that we assume `a + d` is already
|
||||
defined, and we define `a + succ(d)` to be the number after it.
|
||||
This is also in your inventory now -- `add_succ` tells you
|
||||
how to add a successor to something. If you ever see `... + succ ...`
|
||||
in your goal, you should be able to use `rewrite [add_succ]` to make
|
||||
progress. Here is a simple example where we shall see both. Let's prove
|
||||
that $x$ add the number after $0$ is the number after $x$.
|
||||
|
||||
Observe that the goal mentions `... + succ ...`. So type
|
||||
|
||||
`rewrite [add_succ]`
|
||||
|
||||
and hit enter; see the goal change.
|
||||
"
|
||||
|
||||
Statement (a : ℕ ) : a + succ 0 = succ a := by
|
||||
rewrite [add_succ]
|
||||
rewrite [add_zero]
|
||||
rfl
|
||||
|
||||
Message (a : ℕ) : succ (a + 0) = succ a => "
|
||||
Do you see that the goal now mentions ` ... + 0 ...`? So type
|
||||
|
||||
`rewrite [add_zero]`
|
||||
|
||||
and try to finish the level alone from there.
|
||||
"
|
||||
|
||||
Conclusion "Congratulations for completing your fourth level! This is the end of the tutorial part
|
||||
of the game. Serious things start in the next level."
|
||||
|
||||
Tactics rfl rewrite
|
||||
|
||||
Lemmas add_succ add_zero
|
||||
@@ -1,125 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.Tactics
|
||||
|
||||
Level 5
|
||||
|
||||
Title "The induction_on spell"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Welcome to Addition World. If you've done all four levels in tutorial world
|
||||
and know about `rewrite` and `rfl`, then you're in the right place. Here's
|
||||
a reminder of the things you're now equipped with which we'll need in this world.
|
||||
|
||||
## Data:
|
||||
|
||||
* a type called `ℕ`
|
||||
* a term `0 : ℕ`, interpreted as the number zero.
|
||||
* a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\".
|
||||
* Usual numerical notation 0,1,2 etc (although 2 onwards will be of no use to us until much later ;-) ).
|
||||
* Addition (with notation `a + b`).
|
||||
|
||||
## Theorems:
|
||||
|
||||
* `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`.
|
||||
* `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`.
|
||||
* The principle of mathematical induction. Use with `induction_on` (see below)
|
||||
|
||||
|
||||
## Spells:
|
||||
|
||||
* `rfl` : proves goals of the form `X = X`
|
||||
* `rewrite [h]` : if h is a proof of `A = B`, changes all A's in the goal to B's.
|
||||
* `induction_on n with d hd` : we're going to learn this right now.
|
||||
|
||||
# Important thing:
|
||||
|
||||
This is a *really* good time to check you understand about the spell book and the inventory on
|
||||
the left. Eveything you need is collected in those lists. They
|
||||
will prove invaluable as the number of theorems we prove gets bigger. On the other hand,
|
||||
we only need to learn one more spell to really start going places, so let's learn about
|
||||
that spell right now.
|
||||
|
||||
OK so let's see induction in action. We're going to prove
|
||||
|
||||
`zero_add (n : ℕ) : 0 + n = n`.
|
||||
|
||||
That is: for all natural numbers $n$, $0+n=n$. Wait $-$ what is going on here?
|
||||
Didn't we already prove that adding zero to $n$ gave us $n$?
|
||||
No we didn't! We proved $n + 0 = n$, and that proof was called `add_zero`. We're now
|
||||
trying to establish `zero_add`, the proof that $0 + n = n$. But aren't these two theorems
|
||||
the same? No they're not! It is *true* that `x + y = y + x`, but we haven't
|
||||
*proved* it yet, and in fact we will need both `add_zero` and `zero_add` in order
|
||||
to prove this. In fact `x + y = y + x` is the boss level for addition world,
|
||||
and `induction_on` is the only other spell you'll need to beat it.
|
||||
|
||||
Now `add_zero` is one of Peano's axioms, so we don't need to prove it, we already have it
|
||||
(indeed, if you've opened the Addition World theorem statements on the left, you can even see it).
|
||||
To prove `0 + n = n` we need to use induction on $n$. While we're here,
|
||||
note that `zero_add` is about zero add something, and `add_zero` is about something add zero.
|
||||
The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`.
|
||||
|
||||
Start by casting `induction_on n`.
|
||||
"
|
||||
|
||||
Statement (n : ℕ) : 0 + n = n := by
|
||||
induction_on n
|
||||
rewrite [add_zero]
|
||||
rfl
|
||||
rewrite [add_succ]
|
||||
rewrite [ind_hyp]
|
||||
rfl
|
||||
|
||||
Message : (0 : ℕ) + 0 = 0 => "
|
||||
We now have *two goals!* The
|
||||
induction spell has generated for us a base case with `n = 0` (the goal at the top)
|
||||
and an inductive step (the goal underneath). The golden rule: **spells operate on the current goal** --
|
||||
the goal at the top. So let's just worry about that top goal now, the base case `0 + 0 = 0`.
|
||||
|
||||
Remember that `add_zero` (the proof we have already) is the proof of `x + 0 = x`
|
||||
(for any $x$) so we can try
|
||||
|
||||
`rewrite [add_zero]`
|
||||
|
||||
What do you think the goal will change to? Remember to just keep
|
||||
focussing on the top goal, ignore the other one for now, it's not changing
|
||||
and we're not working on it.
|
||||
"
|
||||
|
||||
Message (n : ℕ) (ind_hyp: 0 + n = n) : 0 + succ n = succ n =>
|
||||
"
|
||||
Great! You solved the base case. We are now be back down
|
||||
to one goal -- the inductive step.
|
||||
|
||||
We have a fixed natural number `n`, and the inductive hypothesis `ind_hyp : 0 + n = n`
|
||||
saying that we have a proof of `0 + n = n`.
|
||||
Our goal is to prove `0 + succ n = succ n`. In words, we're showing that
|
||||
if the lemma is true for `n`, then it's also true for the number after `n`.
|
||||
That's the inductive step. Once we've proved this inductive step, we will have proved
|
||||
`zero_add` by the principle of mathematical induction.
|
||||
|
||||
To prove our goal, we need to use `add_succ`. We know that `add_succ 0 n`
|
||||
is the result that `0 + succ n = succ (0 + n)`, so the first thing
|
||||
we need to do is to replace the left hand side `0 + succ n` of our
|
||||
goal with the right hand side. We do this with the `rewrite` spell. You can write
|
||||
|
||||
`rewrite [add_succ]`
|
||||
|
||||
(or even `rewrite [add_succ 0 n]` if you want to give Lean all the inputs instead of making it
|
||||
figure them out itself).
|
||||
"
|
||||
|
||||
Message (n : ℕ) (ind_hyp: 0 + n = n) : succ (0 + n) = succ n =>
|
||||
"Well-done! We're almost there. It's time to use our induction hypothesis.
|
||||
Cast
|
||||
|
||||
`rewrite [ind_hyp]`
|
||||
|
||||
and finish by yourself.
|
||||
"
|
||||
|
||||
Conclusion "Congratulations for completing your first inductive proof!"
|
||||
|
||||
Tactics rfl rewrite induction_on
|
||||
|
||||
Lemmas add_succ add_zero
|
||||
@@ -1,21 +0,0 @@
|
||||
import NNG.GameServer.Commands
|
||||
import NNG.MyNat
|
||||
import NNG.TacticDocs
|
||||
import NNG.LemmaDocs
|
||||
|
||||
Game "NNG"
|
||||
|
||||
Title "The Natural Number Game"
|
||||
|
||||
Introduction
|
||||
"This is a sad day for mathematics. While trying to find glorious new foundations for mathematics,
|
||||
someone removed the law of excluded middle and the axiom of choice. Unsurprisingly,
|
||||
everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage
|
||||
but now we need to rebuild all of mathematics from scratch.
|
||||
|
||||
As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from
|
||||
the axioms that Giuseppe Peano found under the collapsed tower of number theory. You've been equipped
|
||||
with a level 1 spell book. Good luck."
|
||||
|
||||
Conclusion
|
||||
"There is nothing else so far. Thanks for rescuing natural numbers!"
|
||||
@@ -1,20 +0,0 @@
|
||||
axiom MyNat : Type
|
||||
|
||||
notation "ℕ" => MyNat
|
||||
|
||||
--axiom zero : ℕ
|
||||
|
||||
axiom succ : ℕ → ℕ
|
||||
|
||||
@[instance] axiom MyOfNat (n : Nat) : OfNat ℕ n
|
||||
|
||||
@[instance] axiom myAddition : HAdd ℕ ℕ ℕ
|
||||
|
||||
@[instance] axiom myMultiplication : HMul ℕ ℕ ℕ
|
||||
|
||||
axiom add_zero : ∀ a : ℕ, a + 0 = a
|
||||
|
||||
axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)
|
||||
|
||||
@[elabAsElim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
|
||||
|
||||
@@ -1,7 +0,0 @@
|
||||
import NNG.Metadata
|
||||
import NNG.Levels.Level1
|
||||
import NNG.Levels.Level2
|
||||
import NNG.Levels.Level3
|
||||
import NNG.Levels.Level4
|
||||
import NNG.Levels.Level5
|
||||
|
||||
@@ -1,148 +0,0 @@
|
||||
import NNG.GameServer.Commands
|
||||
|
||||
import NNG.Tactics
|
||||
|
||||
TacticDoc rfl
|
||||
"
|
||||
## Summary
|
||||
|
||||
`rfl` proves goals of the form `X = X`.
|
||||
|
||||
## Details
|
||||
|
||||
The `rfl` tactic will close any goal of the form `A = B`
|
||||
where `A` and `B` are *exactly the same thing*.
|
||||
|
||||
### Example:
|
||||
If it looks like this in the top right hand box:
|
||||
```
|
||||
Objects
|
||||
a b c d : ℕ
|
||||
Prove:
|
||||
(a + b) * (c + d) = (a + b) * (c + d)
|
||||
```
|
||||
|
||||
then
|
||||
|
||||
`rfl`
|
||||
|
||||
will close the goal and solve the level."
|
||||
|
||||
TacticDoc induction_on
|
||||
"
|
||||
## Summary
|
||||
|
||||
If `n : ℕ` is in our objects list, then `induction_on n`
|
||||
attempts to prove the current goal by induction on `n`, with the inductive
|
||||
assumption in the `succ` case being `ind_hyp`.
|
||||
|
||||
### Example:
|
||||
If your current goal is:
|
||||
```
|
||||
Objects
|
||||
n : ℕ
|
||||
Prove:
|
||||
2 * n = n + n
|
||||
```
|
||||
|
||||
then
|
||||
|
||||
`induction_on n`
|
||||
|
||||
will give us two goals:
|
||||
|
||||
```
|
||||
Prove:
|
||||
2 * 0 = 0 + 0
|
||||
```
|
||||
|
||||
and
|
||||
```
|
||||
Objects
|
||||
n : ℕ,
|
||||
Assumptions
|
||||
ind_hyp : 2 * n = n + n
|
||||
Prove:
|
||||
2 * succ n = succ n + succ n
|
||||
```
|
||||
"
|
||||
|
||||
TacticDoc rewrite
|
||||
"
|
||||
## Summary
|
||||
|
||||
If `h` is a proof of `X = Y`, then `rewrite [h],` will change
|
||||
all `X`s in the goal to `Y`s. Variants: `rewrite [<- h]` (changes
|
||||
`Y` to `X`) and
|
||||
`rewrite [h] at h2` (changes `X` to `Y` in hypothesis `h2` instead
|
||||
of the goal).
|
||||
|
||||
## Details
|
||||
|
||||
The `rewrite` tactic is a way to do \"substituting in\". There
|
||||
are two distinct situations where use this tactics.
|
||||
|
||||
1) If `h : A = B` is a hypothesis (i.e., a proof of `A = B`)
|
||||
in your local context (the box in the top right)
|
||||
and if your goal contains one or more `A`s, then `rewrite h`
|
||||
will change them all to `B`'s.
|
||||
|
||||
2) The `rewrite` tactic will also work with proofs of theorems
|
||||
which are equalities (look for them in the inventory).
|
||||
For example, if your inventory contains `add_zero x : x + 0 = x`,
|
||||
then `rewrite [add_zero]` will change `x + 0` into `x` in your goal
|
||||
(or fail with an error if Lean cannot find `x + 0` in the goal).
|
||||
|
||||
Important note: if `h` is not a proof of the form `A = B`
|
||||
or `A ↔ B` (for example if `h` is a function, an implication,
|
||||
or perhaps even a proposition itself rather than its proof),
|
||||
then `rewrite` is not the tactic you want to use. For example,
|
||||
`rewrite [P = Q]` is never correct: `P = Q` is the true-false
|
||||
statement itself, not the proof.
|
||||
If `h : P = Q` is its proof, then `rewrite [h]` will work.
|
||||
|
||||
Pro tip 1: If `h : A = B` and you want to change
|
||||
`B`s to `A`s instead, try `rewrite [<- h]` (get the arrow with `\\l` and
|
||||
note that this is a small letter L, not a number 1).
|
||||
|
||||
### Example:
|
||||
If it looks like this in the top right hand box:
|
||||
```
|
||||
Objects
|
||||
x y : ℕ
|
||||
Assumptions
|
||||
h : x = y + y
|
||||
Prove:
|
||||
succ (x + 0) = succ (y + y)
|
||||
```
|
||||
|
||||
then
|
||||
|
||||
`rewrite [add_zero]`
|
||||
|
||||
will change the goal into `succ x = succ (y + y)`, and then
|
||||
|
||||
`rewrite [h]`
|
||||
|
||||
will change the goal into `succ (y + y) = succ (y + y)`, which
|
||||
can be solved with `rfl,`.
|
||||
|
||||
### Example:
|
||||
You can use `rewrite` to change a hypothesis as well.
|
||||
For example, if your local context looks like this:
|
||||
```
|
||||
Objects
|
||||
x y : ℕ
|
||||
Assumptions
|
||||
h1 : x = y + 3
|
||||
h2 : 2 * y = x
|
||||
Prove:
|
||||
y = 3
|
||||
```
|
||||
then `rewrite [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
|
||||
"
|
||||
|
||||
TacticDoc intro
|
||||
"Useful to introduce stuff"
|
||||
|
||||
TacticSet basics := rfl induction_on intro rewrite
|
||||
@@ -1,12 +0,0 @@
|
||||
import Lean
|
||||
import NNG.MyNat
|
||||
|
||||
open Lean Elab Tactic
|
||||
|
||||
elab "swap" : tactic => do
|
||||
match ← getGoals with
|
||||
| g₁::g₂::t => setGoals (g₂::g₁::t)
|
||||
| _ => pure ()
|
||||
|
||||
macro "induction_on" n:ident : tactic =>
|
||||
`(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
|
||||
+3
-11
@@ -1,20 +1,12 @@
|
||||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
package nng {
|
||||
-- add package configuration options here
|
||||
}
|
||||
package GameServer
|
||||
|
||||
lean_lib NNG {
|
||||
-- add library configuration options here
|
||||
}
|
||||
|
||||
lean_lib NNG.levels {
|
||||
-- add library configuration options here
|
||||
}
|
||||
lean_lib GameServer
|
||||
|
||||
@[defaultTarget]
|
||||
lean_exe nng {
|
||||
lean_exe gameserver {
|
||||
root := `Main
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user