diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean index 5131e4a..e6101d0 100755 --- a/Game/Doc/Definitions.lean +++ b/Game/Doc/Definitions.lean @@ -12,18 +12,18 @@ An “And” can be introduced with the `and_intro` theorem. Conjunctions and bi p : P q : Q -- Each new term is evidence for P ∧ Q --- Explicit Constructer, no annotations needed +-- Explicit Constructor, no annotations needed have h₁ := and_intro p q have h₂ := and_intro (left := p) (right := q) --- Implicit Constructuer, annotations based on context +-- Implicit Constructor, annotations based on context -- Type these angle brackets with “\<” and “\>” have h₆ : P ∧ Q := ⟨p,q⟩ have h₇ := (⟨p,q⟩ : P ∧ Q) ``` ## Elimination 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` +1. Acquire evidence for `P` using `and_left h` or `h.left` +2. Acquire evidence for `Q` using `and_right` or `h.right` -/ DefinitionDoc GameLogic.and_def as "∧" @@ -64,18 +64,18 @@ An “If and only if” can be introduced with the `iff_intro` theorem. Bicondit h₁ : P → Q h₂ : Q → P -- Each new term is evidence for P ↔ Q --- Explicit Constructer, no annotations needed +-- Explicit Constructor, no annotations needed have h₁ := iff_intro h₁ h₂ have h₂ := iff_intro (mp := h₁) (mpr := h₂) --- Implicit Constructuer, annotations based on context +-- Implicit Constructor, annotations based on context -- Type these angle brackets with “\<” and “\>” have h₆ : P ↔ Q := ⟨h₁, h₂⟩ have h₇ := (⟨h₁, h₂⟩ : P ↔ Q) ``` ## Elimination An “If and only if” like `h : P ↔ Q` can be reduced in two ways: -1. Aquire evidence for `P → Q` using `iff_mp h` or `h.mp` -2. Aquire evidence for `Q → P` using `iff_mpr h` or `h.mpr` +1. Acquire evidence for `P → Q` using `iff_mp h` or `h.mp` +2. Acquire evidence for `Q → P` using `iff_mpr h` or `h.mpr` ## Rewrite Biconditionals let you use the `rewrite` tactic to change goals or assumptions. -/ diff --git a/Game/Levels/AndIntro.lean b/Game/Levels/AndIntro.lean index 96cb2c4..9d8cca1 100755 --- a/Game/Levels/AndIntro.lean +++ b/Game/Levels/AndIntro.lean @@ -43,7 +43,7 @@ and how some things which may look like expressions really are not: 4 (++) 6 (4 +) 6 ``` -The expressions that this game is asking you to form are mostly in prefix form. In context, this means the operation is given a textual name instead of a symbol and the parameters are separated by spaces **after** the name. For example; the above expressions may look like: +The expressions that this game is asking you to form are mostly in prefix form. In context, this means the operation is given a textual name instead of a symbol and the parameters are separated by spaces **after** the name. For example, the above expressions may look like: ``` add 4 6 add (4) 6 diff --git a/Game/Levels/AndIntro/L01.lean b/Game/Levels/AndIntro/L01.lean index 6d80dea..6c329d4 100755 --- a/Game/Levels/AndIntro/L01.lean +++ b/Game/Levels/AndIntro/L01.lean @@ -19,7 +19,7 @@ You've made a todo list, so you've begun to plan your party. ## Assumptions `todo_list : P` — Can be read as “The `todo_list` is evidence that you're `P`lanning a party” # The Exact Tactic -The Exact tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the assumptions directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\ +The `exact` tactic is — for now — the means through which you give the game your answer. It's your way of declaring that you're done. In this level, you're just going to be using one of the assumptions directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\ \\ The input will look like `exact e` where `e` is an expression the game will accept for the current Goal.\\ \\ diff --git a/Game/Levels/AndIntro/L08.lean b/Game/Levels/AndIntro/L08.lean index 0b1fab3..84fa944 100755 --- a/Game/Levels/AndIntro/L08.lean +++ b/Game/Levels/AndIntro/L08.lean @@ -49,7 +49,7 @@ have c := h.right.right.left.left -- build C ∧ P ∧ S have cps := and_intro c psa.left --- exibit A ∧ C ∧ P ∧ S +-- exhibit A ∧ C ∧ P ∧ S exact and_intro psa.right cps ``` " diff --git a/Game/Levels/ImpIntro/L01.lean b/Game/Levels/ImpIntro/L01.lean index 5178ecc..62f2e50 100755 --- a/Game/Levels/ImpIntro/L01.lean +++ b/Game/Levels/ImpIntro/L01.lean @@ -26,7 +26,7 @@ You use an implication the same way you've been using `and_intro`, `and_left`, a - assumption `h₁ : A → B` - have `b : B := h₁ a` -You can read `h₁ a` as modus ponens. In fact, you've unlocked a theorem called modus_ponens that you could use here. Since modus ponens is implemented as function application, you can — and should — always just Juxtapose instead. +You can read `h₁ a` as modus ponens. In fact, you've unlocked a theorem called `modus_ponens` that you could use here. Since modus ponens is implemented as function application, you can — and should — always just Juxtapose instead. # A note You'll often see assumptions given one or two letter names (`p`, `r`, `q`, `h₁`, `h₂`, `h₃`, etc). Assumptions are generally not long-lived. They are part of some expression, exhibit some implication, and then are discarded. Their names in this context don't need to be particularly memorable.\\ \\ diff --git a/Game/Levels/NotTactic/L08.lean b/Game/Levels/NotTactic/L08.lean index 51190a6..b55db93 100755 --- a/Game/Levels/NotTactic/L08.lean +++ b/Game/Levels/NotTactic/L08.lean @@ -14,7 +14,7 @@ OnlyTactic Introduction " # Pattern matching tip -You can solve this level using the knowledge you've aquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level. +You can solve this level using the knowledge you've acquired so far. If you've used a language with destructuring or pattern matching before, then you can introduce and pattern-match in one step with `intro ⟨nq, p⟩`. Doing so means you won't need the `cases` tactic for this level. " /-- Negation into conjunction. -/