Fix some spelling

Author: Trequetrum

Game/Doc/Definitions.lean

@@ -2,7 +2,7 @@ import GameServer.Commands
 
 namespace GameLogic
 
-DefinitionDoc GameLogic.and_def as "∧" "
+/--
 # Conjunction
 ## Introduction
 An “And” can be introduced with the `and_intro` theorem. Conjunctions and biconditionals can both be constructed using the angle bracket notation as well.
@@ -24,9 +24,10 @@ have h₇ := (⟨p,q⟩ : P ∧ Q)
 An “And” like `h : P ∧ Q` can be reduced in two ways:
 1. Aquire evidence for `P` using `and_left h` or `h.left`
 2. Aquire evidence for `Q` using `and_right` or `h.right`
-"
+-/
+DefinitionDoc GameLogic.and_def as "∧"
 
-DefinitionDoc GameLogic.or_def as "∨" "
+/--
 # Disjunction
 ## Introduction
 An “Or” like `h : P ∨ Q` can be introduced in two ways:
@@ -44,14 +45,16 @@ qr : Q → R
 -- Goal: R
 exact or_elim pvq pr qr
 ```
-"
+-/
+DefinitionDoc GameLogic.or_def as "∨"
 
-DefinitionDoc GameLogic.false_def as "False" "
+/--
 # False
 This is a proposition for which there can never be any evidence. If your assumptions lead you to evidence for `False`, then your assumptions are inconsitent and you can use `false_elim` to deduce any proposition you like.
-"
+-/
+DefinitionDoc GameLogic.false_def as "False"
 
-DefinitionDoc GameLogic.iff_def as "↔" "
+/--
 # Biconditional
 ## Introduction
 An “If and only if” can be introduced with the `iff_intro` theorem. Biconditionals and conjunctions can both be constructed using the angle bracket notation as well.
@@ -75,9 +78,10 @@ An “If and only if” like `h : P ↔ Q` can be reduced in two ways:
 2. Aquire evidence for `Q → P` using `iff_mpr h` or `h.mpr`
 ## Rewrite
 Biconditionals let you use the `rewrite` tactic to change goals or assumptions.
-"
+-/
+DefinitionDoc GameLogic.iff_def as "↔"
 
-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
@@ -107,9 +111,10 @@ B
 exact (h₁ a)
 ```
 Takes `h₁` and applies `a` to it.
-"
+-/
+DefinitionDoc GameLogic.FunElim as "→ elim"
 
-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`
@@ -125,9 +130,10 @@ Generally, you don't need to repeat the types when they're obvious from the cont
 ----
 - `have h₁ : P → P := λp ↦ p`
 - `have h₂ : P ∧ Q → P := λh ↦ h.left`
-"
+-/
+DefinitionDoc GameLogic.FunIntro as "→ intro"
 
-DefinitionDoc GameLogic.AsciiTable as "Unicode Table" "
+/--
 ### **Logic Constants & Operators**
 | $Name~~~$ | $Ascii~~~$ | $Unicode$ | $Unicode Cmd$ |
 | --- | :---: | :---: | --- |
@@ -162,9 +168,10 @@ fun h : P ∧ Q => and_intro (and_right h) (and_left h)
 | Subscript Numbers | ₁ ₂ ₃ ... | `\\1` `\\2` `\\3` ... |
 | Left Arrow | ← | `\\l` `\\leftarrow` `\\gets` `\\<-` |
 | Turnstyle | ⊢ | `\\│-` `\\entails` `\\vdash` `\\goal` |
-"
+-/
+DefinitionDoc GameLogic.AsciiTable as "Unicode Table"
 
-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)
@@ -220,4 +227,5 @@ Here's a version where you can see it aligned
  ((¬P) ∨ (Q ∧ P)) → Q  ↔ (Q ∨ (R ∨ (¬S)))
 (((¬P) ∨ (Q ∧ P)) → Q) ↔ (Q ∨ (R ∨ (¬S)))
 ```
-"
+-/
+DefinitionDoc GameLogic.Precedence as "Precedence"

Game/Doc/Lemmas.lean

@@ -4,40 +4,43 @@ namespace GameLogic
 
 def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
 
-LemmaDoc GameLogic.and_left as "and_left" in "∧" "
+/--
 # ∧ Elimination Left
 ### and_left : P ∧ Q -> P`
 
 If `h` is a term with a type like `AP∧ Q`
 
 `and_left h`, `h.left` or `h.1` are all expressions for denoting the left-hand side of the given evidence. In this case, the left side has a type of `P`.
-"
+-/
+TheoremDoc GameLogic.and_left as "and_left" in "∧"
 
 def and_right {P Q : Prop} (h : P ∧ Q) : Q := And.right h
 
-LemmaDoc GameLogic.and_right as "and_right" in "∧" "
+/--
 # ∧ Elimination Right
 ### and_right : P ∧ Q -> Q`
 
 If `h` is a term with a type like `P ∧ Q`
 
 `and_right h`, `h.right` or `h.2` are all expressions for denoting the right-hand side of the given evidence. In this case, the left side has a type of `Q`.
-"
+-/
+TheoremDoc GameLogic.and_right as "and_right" in "∧"
 
 def and_intro {P Q : Prop} (left : P) (right : Q) : P ∧ Q := And.intro left right
 
-LemmaDoc GameLogic.and_intro as "and_intro" in "∧" "
+/--
 # 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
 ```
 have h : P ∧ Q := and_intro e₁ e₂
 ```
-"
+-/
+TheoremDoc GameLogic.and_intro as "and_intro" in "∧"
 
 def false_elim {P : Prop} (h : False) : P := h.rec
 
-LemmaDoc GameLogic.false_elim as "false_elim" in "¬" "
+/--
 If
 ```
 -- Assumptions
@@ -48,11 +51,12 @@ then
 have t : T := false_elim h
 ```
 will allow you to write any well formed proposition in place of `T`. This makes `false_elim` the \"From `False`, anything goes\" function. **Ex falso quodlibet**.
-"
+-/
+TheoremDoc GameLogic.false_elim as "false_elim" in "¬"
 
 def or_inl {P Q : Prop} (p : P) : Or P Q := Or.inl p
 
-LemmaDoc GameLogic.or_inl as "or_inl" in "∨" "
+/--
 # 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.
 ```
@@ -67,11 +71,12 @@ have h : P ∨ Q := or_inl p
 have h := (or_inl p : P ∨ Q)
 have h := show P ∨ Q from or_inl p
 ```
-"
+-/
+TheoremDoc GameLogic.or_inl as "or_inl" in "∨"
 
 def or_inr {P Q : Prop} (q : Q) : Or P Q := Or.inr q
 
-LemmaDoc GameLogic.or_inr as "or_inr" in "∨" "
+/--
 # 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.
 ```
@@ -87,6 +92,8 @@ have h := (or_inl q : P ∨ Q)
 have h := show P ∨ Q from or_inl q
 ```
 "
+-/
+TheoremDoc GameLogic.or_inr as "or_inr" in "∨"
 
 def or_elim
   {P Q R : Prop}
@@ -95,7 +102,7 @@ def or_elim
   (right : Q → R) : R :=
     Or.elim h left right
 
-LemmaDoc GameLogic.or_elim as "or_elim" in "∨" "
+/--
 # 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.
 
@@ -116,33 +123,37 @@ pr : P → R
 qr : Q → R
 have r : R := or_elim pvq pr qr
 ```
-"
+-/
+TheoremDoc GameLogic.or_elim as "or_elim" in "∨"
 
 def iff_intro
   {P Q : Prop}
   (mp: P → Q)
   (mpr: Q → P) : P ↔ Q :=
     Iff.intro mp mpr
 
-LemmaDoc GameLogic.iff_intro as "iff_intro" in "↔" "
-  TODO 8888
-"
+/--
+TODO
+-/
+TheoremDoc GameLogic.iff_intro as "iff_intro" in "↔"
 
 def iff_mp {P Q : Prop} (h : P ↔ Q) : P → Q := h.mp
 
-LemmaDoc GameLogic.iff_mp as "iff_mp" in "↔" "
-  TODO 1234
-"
+/--
+TODO
+-/
+TheoremDoc GameLogic.iff_mp as "iff_mp" in "↔"
 
 def iff_mpr {P Q : Prop} (h : P ↔ Q) : Q → P := h.mpr
 
-LemmaDoc GameLogic.iff_mpr as "iff_mpr" in "↔" "
-  TODO 4321
-"
+/--
+TODO
+-/
+TheoremDoc GameLogic.iff_mpr as "iff_mpr" in "↔"
 
 def modus_ponens {P Q : Prop} (hpq: P → Q) (p: P) : Q := hpq p
 
-LemmaDoc GameLogic.modus_ponens as "modus_ponens" in "→" "
+/--
 In this game, the deductive rule *modus_ponens* is just function application.
 ```
 intro h : A ∧ B
@@ -170,40 +181,44 @@ There is are infix operators for function application; they look like `|>` and `
 It's twin, `|>` chains such that `x |> f |> g` is interpreted as `g (f x)`.
 
 What makes the infix operators usefull is that they can often replace a pair of brackets `(...)` making expressions easier to read.
-"
+-/
+TheoremDoc GameLogic.modus_ponens as "modus_ponens" in "→"
 
 def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
   ⟨ λ⟨l,r⟩ ↦ ⟨r,l⟩,
     λ⟨l,r⟩ ↦ ⟨r,l⟩
   ⟩
 
-LemmaDoc GameLogic.and_comm as "and_comm" in "∧" "
+/--
 # ∧ is commutative
 
 `and_comm` is evidence that `P ∧ Q ↔ Q ∧ P`
-"
+-/
+TheoremDoc GameLogic.and_comm as "and_comm" in "∧"
 
 def and_assoc {P Q R : Prop}: P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R :=
   ⟨ λ⟨p,q,r⟩ ↦ ⟨⟨p,q⟩,r⟩,
     λ⟨⟨p,q⟩,r⟩ ↦ ⟨p,q,r⟩
   ⟩
 
-LemmaDoc GameLogic.and_assoc as "and_assoc" in "∧" "
+/--
 # ∧ is Associative
 
 `and_assoc` is evidence that `P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
-"
+-/
+TheoremDoc GameLogic.and_assoc as "and_assoc" in "∧"
 
 def or_comm {P Q : Prop}: P ∨ Q ↔ Q ∨ P :=
   ⟨ (Or.elim · Or.inr Or.inl),
     (Or.elim · Or.inr Or.inl)
   ⟩
 
-LemmaDoc GameLogic.or_comm as "or_comm" in "∨" "
+/--
 # ∨ is commutative
 
 `or_comm` is evidence that `P ∨ Q ↔ Q ∨ P`
-"
+-/
+TheoremDoc GameLogic.or_comm as "or_comm" in "∨"
 
 -- or_assoc
 def or_assoc {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R :=
@@ -238,15 +253,16 @@ example {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R := by
     (Or.inr ∘ Or.inr))
   exact ⟨mp,mpr⟩
 
-LemmaDoc GameLogic.or_assoc as "or_assoc" in "∨" "
+/--
 # ∨ is Associative
 
 `or_assoc` is evidence that `P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
-"
+-/
+TheoremDoc GameLogic.or_assoc as "or_assoc" in "∨"
 
 def imp_trans {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) (p : P): R := hqr (hpq p)
 
-LemmaDoc GameLogic.imp_trans as "imp_trans" in "→" "
+/--
 # → is transitive
 `P → Q` and `Q → R` implies `P → R`
 ```
@@ -260,7 +276,8 @@ Of course, because of `and_comm`, you know you can flip this around too.
 `imp_trans` has an infix operator. This looks like `≫` (which is written as “`\\gg`”).
 
 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.
-"
+-/
+TheoremDoc GameLogic.imp_trans as "imp_trans" in "→"
 
 infixl:85 " ≫ " => λa b ↦ Function.comp b a  -- type as \gg
 
@@ -269,17 +286,18 @@ def not_not_not {P : Prop}: ¬¬¬P ↔ ¬P := ⟨
   (λnp nnp ↦ nnp $ np)
 ⟩
 
-LemmaDoc GameLogic.not_not_not as "not_not_not" in "↔ extra" "
+/--
 # 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
 ```
-"
+-/
+TheoremDoc GameLogic.not_not_not as "not_not_not" in "↔ extra"
 
 def modus_tollens {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
 
-LemmaDoc GameLogic.modus_tollens as "modus_tollens" in "→" "
+/--
 # Modus Tollens
 Denying the consequent.
 
@@ -292,14 +310,16 @@ mt : (P → Q) → ¬Q → ¬P
 
 ### Infix Operator:
 `modus_tollens` is a specialized version of `imp_trans`, which makes it possible to use `≫` (which is written as “`\\gg`”) as an infix operator for `modus_tollens`.
-"
+-/
+TheoremDoc GameLogic.modus_tollens as "modus_tollens" in "→"
 
 def identity {P : Prop}(p : P) : P := p
 
-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.
 ```
 identity : P → P
 ```
-"
+-/
+TheoremDoc GameLogic.identity as "identity" in "→"