import GameServer.Commands

import TestGame.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