lvl updates

Game.lean

@@ -129,9 +129,7 @@ Info "
 
 This game is currently in its initial development phase, designed to be largely self-contained and accessible without requiring a programming or math background to navigate. Feedback about meeting that goal is welcome!
 
-While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writing proof terms — rather than using tactics. In fact, logic proof automation is such that if you use the tactic **`tauto`**, you can prove any propositional logic theorem.
-
-Constructive propositional logic is effectively decidable, in the sense that a finite constructive process applies uniformly to every propositional formula, either producing a proof of the formula or demonstrating that no such proof can exist. The fun is in thinking your way through a puzzle with the tools made available to you.
+While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writing proof terms — rather than using tactics.
 
 Please feel encouraged to visit the game's GitHub repository and initiate a discussion on any topic regarding this game. Just open a new issue or comment on an existing one.
 Github: [A Lean Intro to Logic](https://github.com/Trequetrum/lean4game-logic)

Game/Doc/Definitions.lean

@@ -1,8 +1,10 @@
 import GameServer.Commands
 
+namespace GameLogic
+
 def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
 
-DefinitionDoc and_left as "∧-e left" "
+DefinitionDoc GameLogic.and_left as "∧ elim left" "
 # ∧ Elimination Left
 ### and_left : P ∧ Q -> P`
 
@@ -13,7 +15,7 @@ If `h` is a term with a type like `AP∧ Q`
 
 def and_right {P Q : Prop} (h : P ∧ Q) : Q := And.right h
 
-DefinitionDoc and_right as "∧-e right" "
+DefinitionDoc GameLogic.and_right as "∧ elim right" "
 # ∧ Elimination Right
 ### and_right : P ∧ Q -> Q`
 
@@ -24,7 +26,7 @@ If `h` is a term with a type like `P ∧ Q`
 
 def and_intro {P Q : Prop} (left : P) (right : Q) : P ∧ Q := And.intro left right
 
-DefinitionDoc and_intro as "∧ intro" "
+DefinitionDoc GameLogic.and_intro as "∧ intro" "
 # and_intro
 ### `and_intro : P -> Q -> P ∧ Q`
 `and_intro` is a function with two parameters. It takes two disparate pieces of evidence and combines them into a single piece of evidence. If `(e₁ : P)` and `(e₂ : Q)` are evidence, then
@@ -52,7 +54,7 @@ have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
 "
 
-DefinitionDoc FunElim as "→ elim" "
+DefinitionDoc GameLogic.FunElim as "→ elim" "
 # Function Application/Implication Elimination
 `P → Q` is propostion given to functions from evidence of `P` to evidence of `Q`.
 # Juxtaposition
@@ -86,7 +88,7 @@ exact (h₁ a)
 Takes `h₁` and applies `a` to it.
 "
 
-DefinitionDoc FunIntro as "→ intro" "
+DefinitionDoc GameLogic.FunIntro as "→ intro" "
 # `fun _ => _`
 You can create evidence for an implication by defining the appropriate function.
 - `have h₁ : P → P := fun p : P => p`
@@ -101,7 +103,7 @@ Generally, you don't need to repeat the types when they're obvious from the cont
 - `=>` can be written as `↦`
 "
 
-DefinitionDoc AsciiTable as "Symbol Table" "
+DefinitionDoc GameLogic.AsciiTable as "Symbol Table" "
 ### **Logic Constants & Operators**
 | $Name~~~$ | $Ascii~~~$ | $Unicode$ | $Unicode Cmd$ |
 | --- | :---: | :---: | --- |
@@ -136,7 +138,7 @@ fun h : P ∧ Q => and_intro (and_right h) (and_left h)
 | Subscript Numbers | ₁ ₂ ₃ ... | `\\1` `\\2` `\\3` ... |
 "
 
-DefinitionDoc Precedence as "Precedence" "
+DefinitionDoc GameLogic.Precedence as "Precedence" "
 # Remembering Algebra
 In math class, you may have learned an acronym like BEDMAS or PEMDAS to remember the precedence of operators in your math expressions:
 1. Brackets (or Parentheses)
@@ -152,15 +154,22 @@ Brackets group or disambiguate expressions. You can think of precedence rules as
 - non-associative: `P ↔ Q ↔ R` is an error
 # High to low Precedence
 Function application doesn't have an operator, it's just `function <space> argument`. It has max precedence and is left associative (meaning `and_intro p q` ≡ `(and_intro p) q`).
+### Propositional Operators
 | $Operator$ | $~~~Precedence$ | |
 | :---: | :---: | --- |
 | ¬ | max | |
 | ∧ | 35 | right-associative |
 | ∨ | 30 | right-associative |
 | → | 25 | right-associative |
 | ↔ | 20 | non-associative |
-| ∃ | _10_ | |
-| ∀ | _05_ | |
+| ∃ | __ | |
+| ∀ | __ | |
+### Expression Operators
+| $Operator$ | $~~~Precedence$ | |
+| :---: | :---: | --- |
+| ≫ | 85 | left-associative |
+| |> | min + 1 | right-associative |
+| <| | min | left-associative |
 ### Example:
 ```
 ¬P ∨ Q ∧ P → Q ↔ Q ∨ R ∨ ¬S
@@ -189,7 +198,7 @@ Here's a version where you can see it aligned
 
 def false_elim {P : Prop} (h : False) : P := h.rec
 
-DefinitionDoc false_elim as "false_elim" "
+DefinitionDoc GameLogic.false_elim as "False elim" "
 If
 ```
 -- Assumptions
@@ -204,7 +213,7 @@ will allow you to write any well formed proposition in place of `T`. This makes
 
 def or_inl {P Q : Prop} (p : P) : Or P Q := Or.inl p
 
-DefinitionDoc or_inl as "or_inl" "
+DefinitionDoc GameLogic.or_inl as "∨ intro left" "
 # Or Introduction Left
 Turns evidence for the lefthand of an `∨` proposition into a disjunction. The context must supply what the righthand side of the disjunction is.
 ```
@@ -223,7 +232,7 @@ have h := show P ∨ Q from or_inl p
 
 def or_inr {P Q : Prop} (q : Q) : Or P Q := Or.inr q
 
-DefinitionDoc or_inr as "or_inr" "
+DefinitionDoc GameLogic.or_inr as "∨ intro right" "
 # Or Introduction Right
 Turns evidence for the righthand of an `∨` proposition into a disjunction. The context must supply what the lefthand side of the disjunction is.
 ```
@@ -247,7 +256,7 @@ def or_elim
   (right : Q → R) : R :=
     Or.elim h left right
 
-DefinitionDoc or_elim as "or_elim" "
+DefinitionDoc GameLogic.or_elim as "∨ elim" "
 # Or Elimination
 If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
 
@@ -269,3 +278,25 @@ qr : Q → R
 have r : R := or_elim pvq pr qr
 ```
 "
+
+def iff_intro
+  {P Q : Prop}
+  (hpq: P → Q)
+  (hqp: Q → P) : P ↔ Q :=
+    Iff.intro hpq hqp
+
+DefinitionDoc GameLogic.iff_intro as "↔ intro" "
+  TODO 8888
+"
+
+def iff_mp {P Q : Prop} (h : P ↔ Q) : P → Q := h.mp
+
+DefinitionDoc GameLogic.iff_mp as "↔ elim mp" "
+  TODO 1234
+"
+
+def iff_mpr {P Q : Prop} (h : P ↔ Q) : Q → P := h.mpr
+
+DefinitionDoc GameLogic.iff_mpr as "↔ elim mpr" "
+  TODO 4321
+"

Game/Doc/Lemmas.lean

@@ -1,8 +1,14 @@
 import GameServer.Commands
 
+namespace GameLogic
+
+def foo_bar(h : α) : α := h
+
+LemmaDoc GameLogic.foo_bar as "fb" in "∩" "TODO"
+
 def modus_ponens {P Q : Prop} (hpq: P → Q) (p: P) : Q := hpq p
 
-LemmaDoc modus_ponens as "modus_ponens" in "→" "
+LemmaDoc GameLogic.modus_ponens as "modus_ponens" in "→" "
 In this game, the deductive rule *modus_ponens* is just function application.
 ```
 intro h : A ∧ B
@@ -37,7 +43,7 @@ def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
     λ⟨l,r⟩ ↦ ⟨r,l⟩
   ⟩
 
-LemmaDoc and_comm as "and_comm" in "↔" "
+LemmaDoc GameLogic.and_comm as "and_comm" in "↔" "
 # ∧ is commutative
 
 `and_comm` is evidence that `P ∧ Q ↔ Q ∧ P`
@@ -53,7 +59,7 @@ def or_comm {P Q : Prop}: P ∨ Q ↔ Q ∨ P :=
     (Or.elim · Or.inr Or.inl)
   ⟩
 
-LemmaDoc or_comm as "or_comm" in "↔" "
+LemmaDoc GameLogic.or_comm as "or_comm" in "↔" "
 # ∨ is commutative
 
 `or_comm` is evidence that `P ∨ Q ↔ Q ∨ P`
@@ -94,7 +100,7 @@ example {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R := by
 
 def imp_trans {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) (p : P): R := hqr (hpq p)
 
-LemmaDoc imp_trans as "imp_trans" in "→" "
+LemmaDoc GameLogic.imp_trans as "imp_trans" in "→" "
 # → is transitive
 `P → Q` and `Q → R` implies `P → R`
 ```
@@ -110,23 +116,24 @@ Of course, because of `and_comm`, you know you can flip this around too.
 For the math-inclined, because the expression for an implication is a function, you can also use function composition for the same purpose (`∘` is written as “`\\o`”). Just remember that `∘` has the parameters swapped from the way `imp_trans` is defined.
 "
 
-infixl:85 " ≫ " => λa b ↦ Function.comp b a -- type as \gg
-
+infixl:85 " ≫ " => λa b ↦ Function.comp b a  -- type as \gg
 
 def not_not_not {P : Prop}: ¬¬¬P ↔ ¬P := ⟨
   (λh p ↦ h (λnp ↦ np p)),
-  (λh np ↦ np h)
+  (λnp nnp ↦ nnp $ np)
 ⟩
 
-LemmaDoc not_not_not as "not_not_not" in "↔" "
+LemmaDoc GameLogic.not_not_not as "not_not_not" in "↔" "
 # Negation is stable
 A nice result of this theorem is that any more than 2 negations can be simplified down to 1 or 2 negations.
 ```
 not_not_not : ¬¬¬P ↔ ¬P
 ```
 "
 
-LemmaDoc mt as "mt" in "→" "
+def mt {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
+
+LemmaDoc GameLogic.mt as "mt" in "→" "
 # Modus Tollens
 Denying the consequent. We've given this theorem an extra short name because it appears so often.
 
@@ -143,7 +150,7 @@ mt : (P → Q) → ¬Q → ¬P
 
 def identity {P : Prop}(p : P) : P := p
 
-LemmaDoc identity as "identity" in "→" "
+LemmaDoc GameLogic.identity as "identity" in "→" "
 # Propositional Identity
 This is the \"I think therefore I am\" of propositional logic. Like `True` it is a simple tautology whose truth requires no premises or assumptions — only reason alone.
 ```

Game/Doc/Tactics.lean

@@ -90,3 +90,54 @@ Goal:
 ¬P
 ```
 "
+
+TacticDoc rw "
+## Summary
+
+If `h` is a proof of an equality `X = Y`, then `rw [h]` will change
+all `X`s in the goal to `Y`s. It's the way to \"substitute in\".
+
+## Variants
+
+* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)
+
+* `rw [h1, h2]` (a sequence of rewrites)
+
+* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)
+
+* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;
+get the `⊢` symbol with `\\|-`.)
+
+* `repeat rw [add_zero]` will keep changing `? + 0` to `?`
+until there are no more matches for `? + 0`.
+
+* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.
+"
+
+TacticDoc «repeat» "
+## Summary
+
+`repeat t` repeatedly applies the tactic `t`
+to the goal. You don't need to use this
+tactic, it just speeds things up sometimes.
+
+## Example
+
+`repeat rw [add_zero]` will turn the goal
+`a + 0 + (0 + (0 + 0)) = b + 0 + 0`
+into the goal
+`a = b`.
+"
+
+TacticDoc nth_rewrite "
+## Summary
+
+If `h : X = Y` and there are several `X`s in the goal, then
+`nth_rewrite 3 [h]` will just change the third `X` to a `Y`.
+
+## Example
+
+If the goal is `2 + 2 = 4` then `nth_rewrite 2 [two_eq_succ_one]`
+will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
+will change the goal to `succ 1 + succ 1 = 4`.
+"

Game/Levels/AndIntro/L01.lean

@@ -1,12 +1,13 @@
-
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 1
 Title "Exactly! It's in the premise"
 
 NewTactic exact
-NewDefinition AsciiTable
+NewDefinition GameLogic.AsciiTable
 
 Introduction "
 # Introduction

Game/Levels/AndIntro/L02.lean

@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 2
 Title "And Introduction"
 
-NewDefinition and_intro
+NewDefinition GameLogic.and_intro
 
 Introduction "
 # Sending Invitations in a Single Package
@@ -37,6 +39,7 @@ Statement (P S : Prop)(p: P)(s : S) : P ∧ S := by
   Hint (hidden := true) "exact and_intro p s"
   exact and_intro (left := p) (right := s)
 
+
 Conclusion "
 You've got evidence that Paul and Sarah are invited to the party.\\
 \\

Game/Levels/AndIntro/L03.lean

@@ -1,10 +1,13 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 3
 Title "The Have Tactic"
 
-NewDefinition Precedence
+NewDefinition GameLogic.Precedence
+NewTactic «have»
 
 Introduction "
 # Too Many Invites
@@ -44,8 +47,6 @@ ou: O ∧ U
 Finally, now you can place these two boxes — `ai` and `ou` — into a third box and submit your answer using the `exact` tactic.
 "
 
-NewTactic «have»
-
 /-- Three × and_intro. -/
 Statement (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by
   have ai := and_intro a i

Game/Levels/AndIntro/L04.lean

@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 4
 Title "And Elimination"
 
-NewDefinition and_left
+NewDefinition GameLogic.and_left
 
 Introduction "
 # Using Only What Is Needed

Game/Levels/AndIntro/L05.lean

@@ -1,10 +1,12 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 5
 Title "And Elimination 2"
 
-NewDefinition and_right
+NewDefinition GameLogic.and_right
 
 Introduction "
 # Another Unlock

Game/Levels/AndIntro/L06.lean

@@ -1,5 +1,7 @@
 import Game.Metadata
 
+open GameLogic
+
 World "AndIntro"
 Level 6
 Title "Mix and Match"