From 0b73d32ab08647cfd2e29ec11a000b3bce124dae Mon Sep 17 00:00:00 2001 From: Marco Colombo Date: Wed, 10 Jul 2024 12:49:45 +0200 Subject: [PATCH] Fix typos. --- Game/Doc/Lemmas.lean | 8 ++++---- Game/Doc/Tactics.lean | 2 +- Game/Levels/AndIntro/L02.lean | 2 +- Game/Levels/AndTactic/L05.lean | 2 +- Game/Levels/IffIntro/L01.lean | 2 +- Game/Levels/IffIntro/L02.lean | 2 +- Game/Levels/IffIntro/L07.lean | 2 +- Game/Levels/IffTactic/L02.lean | 2 +- Game/Levels/IffTactic/L05.lean | 2 +- Game/Levels/ImpIntro.lean | 2 +- Game/Levels/ImpIntro/L08.lean | 2 +- Game/Levels/ImpIntro/L09.lean | 2 +- Game/Levels/NotIntro/L02.lean | 4 ++-- Game/Levels/NotIntro/L05.lean | 2 +- Game/Levels/NotIntro/L08.lean | 2 +- Game/Levels/NotIntro/L09.lean | 4 ++-- Game/Levels/NotIntro/L10.lean | 6 +++--- Game/Levels/NotIntro/L11.lean | 4 ++-- Game/Levels/NotIntro/L12.lean | 2 +- Game/Levels/NotTactic/L02.lean | 2 +- Game/Levels/NotTactic/L03.lean | 2 +- Game/Levels/NotTactic/L08.lean | 2 +- Game/Levels/NotTactic/L10.lean | 2 +- Game/Levels/OrIntro/L02.lean | 2 +- Game/Levels/OrIntro/L03.lean | 4 ++-- Game/Levels/OrIntro/L05.lean | 2 +- 26 files changed, 35 insertions(+), 35 deletions(-) diff --git a/Game/Doc/Lemmas.lean b/Game/Doc/Lemmas.lean index 334b80c..79efb15 100755 --- a/Game/Doc/Lemmas.lean +++ b/Game/Doc/Lemmas.lean @@ -8,7 +8,7 @@ def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h # ∧ Elimination Left ### `and_left : P ∧ Q -> P` -If `h` is a term with a type like `AP∧ Q` +If `h` is a term with a type like `P ∧ 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`. -/ @@ -104,7 +104,7 @@ def or_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. +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 guarantee something. or_elim is also evidence: ``` @@ -116,7 +116,7 @@ or_elim : (P ∨ Q) → (P → R) → (Q → R) → R` 2. evidence an implication on the left, 3. evidence for an implication on the right. # Example -`or_elim` is your first 3-paramater function. +`or_elim` is your first 3-parameter function. ``` pvq: P ∨ Q pr : P → R @@ -202,7 +202,7 @@ 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. +What makes the infix operators useful is that they can often replace a pair of brackets `(...)` making expressions easier to read. ---- # Computer Science diff --git a/Game/Doc/Tactics.lean b/Game/Doc/Tactics.lean index 2d81c64..a6ee0a5 100755 --- a/Game/Doc/Tactics.lean +++ b/Game/Doc/Tactics.lean @@ -2,7 +2,7 @@ import GameServer.Commands /-- # Summary -The `exact` tactic is a means through which you give the game your answer. Many levels can be done in multiple steps. You'll use the `exact` tactic when you're ready to create the final expression. It will be evaluated to see weather it matches the goal. +The `exact` tactic is a means through which you give the game your answer. Many levels can be done in multiple steps. You'll use the `exact` tactic when you're ready to create the final expression. It will be evaluated to see whether it matches the goal. `exact` will work with any expression and attempt to unify it with the current goal. The simplest such expression is just a name that — `:` — “is evidence for” the goal. More complicated expressions often make use of unlocked definitions and theorems as well as function abstraction and application. diff --git a/Game/Levels/AndIntro/L02.lean b/Game/Levels/AndIntro/L02.lean index 45208b1..bcee971 100755 --- a/Game/Levels/AndIntro/L02.lean +++ b/Game/Levels/AndIntro/L02.lean @@ -33,7 +33,7 @@ Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use eviden # Using the `∧` Construtor This level has unlocked “`∧`” under definitions. This has made the `and_intro` theorem available. You can use `and_intro` by giving it the two relevant pieces of evidence. The expression looks like: `and_intro e₁ e₂` where `e₁` and `e₂` are evidence.\\ \\ -The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `,` `⟩` ). +The help page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackets `⟨` `,` `⟩` ). # A reminder Use the `exact` tactic to exhibit evidence for a goal diff --git a/Game/Levels/AndTactic/L05.lean b/Game/Levels/AndTactic/L05.lean index 53e96ba..601c54f 100755 --- a/Game/Levels/AndTactic/L05.lean +++ b/Game/Levels/AndTactic/L05.lean @@ -12,7 +12,7 @@ OnlyTactic Introduction " # Rinse and Repeat -When you were writing expressions before, lvl 4 needed `and_left` while level 5 needed `and_right`. Tactics can incorperate an arbitrary amount of automation. In this case, because assumption will do a search through your assumptions for you, your proof for this level can be 100% identical to the one you used last level. +When you were writing expressions before, level 4 needed `and_left` while level 5 needed `and_right`. Tactics can incorporate an arbitrary amount of automation. In this case, because `assumption` will do a search through your assumptions for you, your proof for this level can be 100% identical to the one you used in the last level. " /-- Both P and Q entails just Q as well! -/ diff --git a/Game/Levels/IffIntro/L01.lean b/Game/Levels/IffIntro/L01.lean index e29e107..5da6890 100755 --- a/Game/Levels/IffIntro/L01.lean +++ b/Game/Levels/IffIntro/L01.lean @@ -14,7 +14,7 @@ OnlyTactic Introduction " # Coupled Conditionals -Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vise versa. Therefore Sybeth is playing Charades if and only if Alarfil playing. +Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vice versa. Therefore Sybeth is playing Charades if and only if Alarfil playing. # Proposition Key: - J — Alarfil is playing Charades - S — Sybeth is playing Charades diff --git a/Game/Levels/IffIntro/L02.lean b/Game/Levels/IffIntro/L02.lean index 291d3ed..0098eb5 100644 --- a/Game/Levels/IffIntro/L02.lean +++ b/Game/Levels/IffIntro/L02.lean @@ -4,7 +4,7 @@ open GameLogic World "IffIntro" Level 2 -Title "Conjuctive Iff" +Title "Conjunctive Iff" NewTheorem GameLogic.iff_mp diff --git a/Game/Levels/IffIntro/L07.lean b/Game/Levels/IffIntro/L07.lean index 3271e64..967729c 100644 --- a/Game/Levels/IffIntro/L07.lean +++ b/Game/Levels/IffIntro/L07.lean @@ -14,7 +14,7 @@ Introduction " # BOSS LEVEL This is an involved level. It doesn't require you to do anything tricky, but there are a lot of moving parts and it is easy to lose track of what you're doing.\\ \\ -I recommend editor mode. Think about what this is asking you to prove and use `have` to give yourself any auxillary facts that don't exist under your theorems. +I recommend editor mode. Think about what this is asking you to prove and use `have` to give yourself any auxiliary facts that don't exist under your theorems. " Statement (P Q R : Prop): (P ∧ Q ↔ R ∧ Q) ↔ Q → (P ↔ R) := by diff --git a/Game/Levels/IffTactic/L02.lean b/Game/Levels/IffTactic/L02.lean index 0508341..f66fc93 100644 --- a/Game/Levels/IffTactic/L02.lean +++ b/Game/Levels/IffTactic/L02.lean @@ -4,7 +4,7 @@ open GameLogic World "IffTactic" Level 2 -Title "Conjuctive Iff" +Title "Conjunctive Iff" OnlyTactic assumption diff --git a/Game/Levels/IffTactic/L05.lean b/Game/Levels/IffTactic/L05.lean index 8019ee8..d3db807 100644 --- a/Game/Levels/IffTactic/L05.lean +++ b/Game/Levels/IffTactic/L05.lean @@ -19,7 +19,7 @@ OnlyTactic Introduction " # A Longer Level -The `rw` tactic makes this level a cakewalk. For the redux version we're going to make this outright tedius, but this will show without a doubt that you've mastered simple propositional proofs.\\ +The `rw` tactic makes this level a cakewalk. For the redux version we're going to make this outright tedious, but this will show without a doubt that you've mastered simple propositional proofs.\\ \\ I suggest you finish the other redux worlds before doing this level.\\ \\ diff --git a/Game/Levels/ImpIntro.lean b/Game/Levels/ImpIntro.lean index 94c12bb..6dce284 100755 --- a/Game/Levels/ImpIntro.lean +++ b/Game/Levels/ImpIntro.lean @@ -22,7 +22,7 @@ This game uses the implication arrow “ → ”. “If A, then B” is the same \\ So far, we've been giving our evidence and propositions real-world analogues. Doing this is a bit less desirable with conditionals as real-world evidence is often based on our understanding and not some tangible object. For example; the evidence that “If it rained, then the driveway is wet” generally doesn't come in the form of peer-reviewed physics papers. You should be thinking of the flavour text for each level as an unrefined embellishment of the symbols you're actually concerned with.\\ \\ -That said, at the level the favour text works on, what would constitute evidence for a conditional statement? Well, for example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. An example of evidence for such a conditional could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\ +That said, at the level the flavour text works on, what would constitute evidence for a conditional statement? Well, for example; “If we have gnocchi, butter, parmesan, and black pepper, then we can cook *gnocchi cacio e pepe*”. An example of evidence for such a conditional could be a recipe with cooking instructions. You can think of the recipe as an argument explaining that the given ingredients are sufficient to be able to cook the dish.\\ \\ Another example might be a safe's combination, as evidence that “I can find the hidden safe” → “I can steal the contents of the safe”. Perhaps a certification is evidence that “I won the contract” → “I will renovate the client's yard”.\\ \\ diff --git a/Game/Levels/ImpIntro/L08.lean b/Game/Levels/ImpIntro/L08.lean index 7a19463..d0e453b 100755 --- a/Game/Levels/ImpIntro/L08.lean +++ b/Game/Levels/ImpIntro/L08.lean @@ -31,5 +31,5 @@ example (C D S : Prop) (h : (S → C) ∧ (S → D)) : S → C ∧ D := by exact λs ↦ ⟨l s, r s⟩ Conclusion " -You definitely have the knack of providing conditional arguements +You definitely have a knack for providing conditional arguments! " diff --git a/Game/Levels/ImpIntro/L09.lean b/Game/Levels/ImpIntro/L09.lean index fcb0d04..f92ca78 100755 --- a/Game/Levels/ImpIntro/L09.lean +++ b/Game/Levels/ImpIntro/L09.lean @@ -26,7 +26,7 @@ That's a bit convoluted, but you should be able to produce some evidence of this - `S` — Sybeth is bringing a snack " -/-- Write the nessesary nested function(s)! -/ +/-- Write the necessary nested function(s)! -/ Statement (R S : Prop) : R → (S → R) ∧ (¬S → R) := by exact λ(r : R) ↦ and_intro (λ(_ : S) ↦ r) (λ(_ : ¬S) ↦ r) diff --git a/Game/Levels/NotIntro/L02.lean b/Game/Levels/NotIntro/L02.lean index 6a99b82..a74be37 100755 --- a/Game/Levels/NotIntro/L02.lean +++ b/Game/Levels/NotIntro/L02.lean @@ -22,9 +22,9 @@ You've unlocked the \"false implies anything\" function. `false_elim` will take # A Tip Remember you can think of `h : ¬S` as `h : S → False`.\\ \\ -Once you've started with `λ(s : S) ↦ `, you'll then see that the expression `h s` evaluates to evidence for `False`. If ever you have evidence for `False`, you should aways immediatly consider using `false_elim` to create evidence for anything — which in this case will be `B`.\\ +Once you've started with `λ(s : S) ↦ `, you'll then see that the expression `h s` evaluates to evidence for `False`. If ever you have evidence for `False`, you should always immediately consider using `false_elim` to create evidence for anything — which in this case will be `B`.\\ \\ -There is no proof that \"keeps going\" once you've created evidence for `False`. Some proofs have multiple parts, so you may close off one line of reasoning and move on to another, but there can be no meaningfull logic in any context where evidence for `False` is present. +There is no proof that \"keeps going\" once you've created evidence for `False`. Some proofs have multiple parts, so you may close off one line of reasoning and move on to another, but there can be no meaningful logic in any context where evidence for `False` is present. " /-- ¬S is enough to show S → B -/ diff --git a/Game/Levels/NotIntro/L05.lean b/Game/Levels/NotIntro/L05.lean index d94d35d..3b6a751 100755 --- a/Game/Levels/NotIntro/L05.lean +++ b/Game/Levels/NotIntro/L05.lean @@ -23,7 +23,7 @@ Statement (B S : Prop)(h1 : B → S)(h2 : ¬S) : ¬B := by exact imp_trans h1 h2 Conclusion " -Congradulations. Did you recognise this proof? It's actually a slightly less general version of the proof you used in the \"**→ Tutotial world, level 4**\" to show that implication is transitive. +Congratulations. Did you recognise this proof? It's actually a slightly less general version of the proof you used in the \"**→ Tutotial world, level 4**\" to show that implication is transitive. --- Thinking of `h₂` as `Q → False`, you can actually use your imp_trans theorem here. diff --git a/Game/Levels/NotIntro/L08.lean b/Game/Levels/NotIntro/L08.lean index 1286653..611fd6f 100755 --- a/Game/Levels/NotIntro/L08.lean +++ b/Game/Levels/NotIntro/L08.lean @@ -18,7 +18,7 @@ Your cake order definitely has sprinkles, which means it's **not** missing sprin - `S` — The cake is topped with sprinkles " -/-- Negation into conjuction. -/ +/-- Negation into conjunction. -/ Statement (C S : Prop) (s: S) : ¬(¬S ∧ C) := by exact λ(nsc : ¬S ∧ C) ↦ nsc.left s diff --git a/Game/Levels/NotIntro/L09.lean b/Game/Levels/NotIntro/L09.lean index 97fb493..2f76e3e 100755 --- a/Game/Levels/NotIntro/L09.lean +++ b/Game/Levels/NotIntro/L09.lean @@ -12,9 +12,9 @@ OnlyTactic Introduction " # Allergy #1 -Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avacado at the party +Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avocado at the party # Proposition Key: -- `A` — There's avacado at the party +- `A` — There's avocado at the party - `P` — Pippin is attending the party " diff --git a/Game/Levels/NotIntro/L10.lean b/Game/Levels/NotIntro/L10.lean index 691d20d..6e005db 100755 --- a/Game/Levels/NotIntro/L10.lean +++ b/Game/Levels/NotIntro/L10.lean @@ -4,7 +4,7 @@ open GameLogic World "NotIntro" Level 10 -Title "Conjunction Implicaiton" +Title "Conjunction Implication" OnlyTactic exact @@ -12,9 +12,9 @@ OnlyTactic Introduction " # Allergy #2 -We cannot have both Pippin and avacado at the party. Which means that if Pippin is attending, then there will not be any avacado. +We cannot have both Pippin and avocado at the party. Which means that if Pippin is attending, then there will not be any avocado. # Proposition Key: -- `A` — There's avacado at the party +- `A` — There's avocado at the party - `P` — Pippin is attending the party " diff --git a/Game/Levels/NotIntro/L11.lean b/Game/Levels/NotIntro/L11.lean index 9d70452..35fdedb 100755 --- a/Game/Levels/NotIntro/L11.lean +++ b/Game/Levels/NotIntro/L11.lean @@ -12,9 +12,9 @@ OnlyTactic Introduction " # Allergy: Triple Confusion -Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avacado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\" +Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avocado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\" # Proposition Key: -- `A` — You're bringing avacado +- `A` — You're bringing avocado " /-- ¬A is stable. -/ diff --git a/Game/Levels/NotIntro/L12.lean b/Game/Levels/NotIntro/L12.lean index 1423cbe..6530b57 100755 --- a/Game/Levels/NotIntro/L12.lean +++ b/Game/Levels/NotIntro/L12.lean @@ -29,7 +29,7 @@ example (B C : Prop) (h : ¬(B → C)) : ¬¬B := by exact λnb ↦ h (nb ≫ false_elim) Conclusion " -These unintuitive statements highlight the inherent challenge in contemplating the *potential* existence (or definite non-existance) of implications. +These unintuitive statements highlight the inherent challenge in contemplating the *potential* existence (or definite non-existence) of implications. That's a twist of logic, to be sure! " diff --git a/Game/Levels/NotTactic/L02.lean b/Game/Levels/NotTactic/L02.lean index aa8326f..14278f4 100755 --- a/Game/Levels/NotTactic/L02.lean +++ b/Game/Levels/NotTactic/L02.lean @@ -12,7 +12,7 @@ OnlyTactic contradiction Introduction " -# Contradiciton +# Contradiction This level introduces a relatively powerful tactic. Contradiction is a finishing tactic that will look through your assumptions and discharge some of the more obvious contradictions in order to solve any goal.\\ \\ examples: diff --git a/Game/Levels/NotTactic/L03.lean b/Game/Levels/NotTactic/L03.lean index f65a76e..9ef4519 100755 --- a/Game/Levels/NotTactic/L03.lean +++ b/Game/Levels/NotTactic/L03.lean @@ -15,7 +15,7 @@ OnlyTactic Introduction " # exfalso -`exfalso` is **Contradiction**'s younger brother. Using `exfalso` turns your goal to `False`. This is the same thing as using `apply false_elim`. Using the principle that “from nonsense, follows nonsense,” if you spot a constradiction in your assumptions, you can make progress by changing your goal to `False.`\\ +`exfalso` is **Contradiction**'s younger brother. Using `exfalso` turns your goal to `False`. This is the same thing as using `apply false_elim`. Using the principle that “from nonsense, follows nonsense,” if you spot a contradiction in your assumptions, you can make progress by changing your goal to `False.`\\ \\ Remember that because `¬P` is the same as `P → False`, you can use the `apply` tactic on evidence for `¬P` " diff --git a/Game/Levels/NotTactic/L08.lean b/Game/Levels/NotTactic/L08.lean index db9a103..51190a6 100755 --- a/Game/Levels/NotTactic/L08.lean +++ b/Game/Levels/NotTactic/L08.lean @@ -17,7 +17,7 @@ Introduction " 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. " -/-- Negation into conjuction. -/ +/-- Negation into conjunction. -/ Statement (P Q : Prop) (h: Q) : ¬(¬Q ∧ P) := by intro nqp cases nqp diff --git a/Game/Levels/NotTactic/L10.lean b/Game/Levels/NotTactic/L10.lean index 1765d87..a9f5698 100755 --- a/Game/Levels/NotTactic/L10.lean +++ b/Game/Levels/NotTactic/L10.lean @@ -4,7 +4,7 @@ open GameLogic World "NotTactic" Level 10 -Title "Conjunction Implicaiton" +Title "Conjunction Implication" OnlyTactic assumption diff --git a/Game/Levels/OrIntro/L02.lean b/Game/Levels/OrIntro/L02.lean index dd21e29..2d75a68 100755 --- a/Game/Levels/OrIntro/L02.lean +++ b/Game/Levels/OrIntro/L02.lean @@ -28,7 +28,7 @@ Statement (O S : Prop)(s : S) : K ∨ S := by Conclusion " Almost a repeat of level 1. That was fast. -You'll notice that last time you showed evidence for a proposition involving “Oranges are a vegetable” even though you probably know that oranges are a fruit and not a vegitable. This time you did the same for “sprinkles are super colourful,” which you probably know is true. +You'll notice that last time you showed evidence for a proposition involving “Oranges are a vegetable” even though you probably know that oranges are a fruit and not a vegetable. This time you did the same for “sprinkles are super colourful,” which you probably know is true. What this demonstrates is that `∨` is an inclusive “or”, which means at least one of the propositions is true. It could be both or just one. " diff --git a/Game/Levels/OrIntro/L03.lean b/Game/Levels/OrIntro/L03.lean index 810d9d1..76b14a0 100755 --- a/Game/Levels/OrIntro/L03.lean +++ b/Game/Levels/OrIntro/L03.lean @@ -19,14 +19,14 @@ Here's the deal. Ilyn and Cyna both said they're bringing board games and you're - `C` — Cyna is coming to the party - `I` — Ilyn is coming to the party # 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. +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 guarantee something. # You've unlocked `or_elim` `or_elim` has three parameters: 1. takes evidence for a disjunction, 2. evidence an implication on the left, 3. evidence for an implication on the right. -`or_elim` is your first 3-paramater function. The associated proposition is `or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`. +`or_elim` is your first 3-parameter function. The associated proposition is `or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`. ``` pvq: P ∨ Q pr : P → R diff --git a/Game/Levels/OrIntro/L05.lean b/Game/Levels/OrIntro/L05.lean index 30cb5cf..52fc86d 100755 --- a/Game/Levels/OrIntro/L05.lean +++ b/Game/Levels/OrIntro/L05.lean @@ -16,7 +16,7 @@ Introduction " If the cake arrives, then everybody will rejoice. Either the cake arrives or you get a refund. Therefore, either everybody will rejoice or you get a refund! That's a win-win situation. # Proposition Key: - C — The cake arrives -- J — Everybody is joyfull +- J — Everybody is joyful - R — You get a refund "