Level Updates

Author: Trequetrum

Game.lean

@@ -8,11 +8,13 @@ import Game.Levels.AndIntro
 import Game.Levels.ImpIntro
 import Game.Levels.NotIntro
 import Game.Levels.OrIntro
+import Game.Levels.IffIntro
 
 -- Here's where we show how to glue the worlds together
 Dependency AndIntro → ImpIntro
 Dependency ImpIntro → NotIntro
-
+Dependency ImpIntro → OrIntro
+Dependency ImpIntro → IffIntro
 
 -- Here's what we'll put on the title screen
 Title "A Lean Intro to Logic"
@@ -26,16 +28,16 @@ To play this puzzler you'll need to learn some notation. Unlike learning how to
 Below, you're provided with whirlwind tour of the notation at play as well as a bit of motivation for why the notation looks the way it does. This is all done through a single example. Many of the details will seem lacking; The concepts covered here will be addressed with more detail during the tutorial worlds of this game.
 
 # But first, a tip!
-This introduction as well as some of the tutotial levels can get a bit wordy. The three column panels — text on the left, game worlds in the middle, and your inventory on the right — can all be expanded or shrunk as nesesary. Every screen is different, so do feel encouraged to re-size these pannels.
+This introduction as well as some of the tutorial levels can get a bit wordy. The three column panels — text on the left, game worlds in the middle, and your inventory on the right — can all be expanded or shrunk as necessary. Every screen is different, so do feel encouraged to re-size these panels.
 
 # Building some notation
 Consider the following argument stated in natural language:
 
-\"Either cat fur or dog fur was found at the scene of the crime. If dog fur was found at the scene of the crime, officer Thompson had an allergy attack. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. But officer Thompson didn’t have an allergy attack, and so therefore Macavity must be responsible for the crime.\"
+“Either cat fur or dog fur was found at the scene of the crime. If dog fur was found at the scene of the crime, Officer Thompson had an allergy attack. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. But Officer Thompson didn’t have an allergy attack, and so therefore Macavity must be responsible for the crime.” [¹]
 
 Does this argument convince you? The validity of this argument can be made more obvious by representing the chain of reasoning leading from the premises to the conclusion:
 1. Either cat fur was found at the scene of the crime, or dog fur was found at the scene of the crime. (Premise)
-2. If dog fur was found at the scene of the crime, then officer Thompson had an allergy attack. (Premise)
+2. If dog fur was found at the scene of the crime, then Officer Thompson had an allergy attack. (Premise)
 3. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. (Premise)
 4. Officer Thompson did not have an allergy attack. (Premise)
 5. Dog fur was not found at the scene of the crime. (Follows from 2 and 4)
@@ -48,7 +50,7 @@ If you take a moment to re-read them again, lines 5, 6, & 7 are all slightly dif
 - Line 6 is using the process of elimination on two options. This is the style of reasoning responsible for Sherlock Holmes' most famous quote — \"When you have eliminated the impossible, whatever remains, however improbable, must be the truth\". We'll give this a name too: **modus tollendo ponens**
 - Line 7 is the conclusion and is applying the \"if ... then ...\" statement on line 3. We'll call this one **modus ponens**.
 
-We won't always be denoting these with latin names, but the general process of being able to give some generically useful deductive reasoning a name is nice. It makes them easier to reference. During the course of this game some of your proofs will be given names and correspondingly unlocked in your inventory. Thus names are a way to avoid proving the same thing over and over again.
+We won't always be denoting these with Latin names, but the general process of being able to give some generically useful deductive reasoning a name is nice. It makes them easier to reference. During the course of this game some of your proofs will be given names and correspondingly unlocked in your inventory. Thus names are a way to avoid proving the same thing over and over again.
 
 # Propositions
 If we separate out the 4 true/false statements required for our line of reasoning and introduce some connectives, we can see the exact same argument in a more concise form. The numbers 1 - 7 here are meant to match exactly with the natural language above.
@@ -114,6 +116,10 @@ To introduce new evidence — such as `h₅` — you need to write out an expres
 In this game, each level will ask you to provide evidence of some proposition. This will often involve using the evidence you already have in some way.
 
 Click on the first world — **Party Invites** — to get started.
+
+----
+
+[¹]Logic example taken from [IEP](https://iep.utm.edu/propositional-logic-sentential-logic/#H5) entry: *Propositional Logic*.
 "
 
 Info "
@@ -123,9 +129,9 @@ 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 writting proof terms — rather than using tactics. In fact, logic proof automation is such that the tactic **`tauto`** can solve any propositional logic theorem (Though possible, that's an NP-Complete problem).
+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.
 
-The main thrust of this game is to create puzzles that are fun to think through on your own. I can write a simple algorithm that solves every proper Sudoku. Yet, when I spend a train-ride scribbling numbers into boxes in my sudoku book, I never lament how much faster my phone's CPU could do the job.
+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.
 
 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

@@ -46,6 +46,7 @@ have h₃ : P ∧ Q := {left := p, right := q}
 have h₄ := ({left := p, right := q} : P ∧ Q)
 have h₅ := {left := p, right := q : P ∧ Q}
 -- Implicit Constructuer, annotations based on context
+-- Type these angle brackets with “\\<” and “\\>”
 have h₆ : P ∧ Q := ⟨p,q⟩
 have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
@@ -55,7 +56,7 @@ DefinitionDoc FunElim as "→ elim" "
 # Function Application/Implication Elimination
 `P → Q` is propostion given to functions from evidence of `P` to evidence of `Q`.
 # Juxtaposition
-Juxtaposition just means \"to place next to each other,\" which is what we'll do to give a parameter to a function.
+Juxtaposition just means “to place next to each other,” which is what we'll do to give a parameter to a function.
 ### Example
 You should already be familiar with `and_intro`. It is a funtion that takes two parameters.
 ```

Game/Doc/Lemmas.lean

@@ -19,7 +19,17 @@ have h : A ∧ B := and_intro a b
 have h : A ∧ B := modus_ponens (modus_ponens and_intro a) b
 ```
 
-You should never use this lemma and just use function application instead as that will generally be clearer.
+You should never use this style of prefix `modus_ponens` and just use function application instead as that will generally be clearer.
+
+----
+# Infix Modus Ponens
+There is are infix operators for function application; they look like `|>` and `<|`. `f <| x`, and `x |> f` means the same as the same as `f x`.
+
+`<|` parses `x` with lower precedence, which means that `f <| g $ <|` is interpreted as `(f (g x))` rather than `((f g) x)`.
+
+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.
 "
 
 def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
@@ -83,14 +93,26 @@ example {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R := by
   exact ⟨mp,mpr⟩
 
 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 "→" "
 # → is transitive
 `P → Q` and `Q → R` implies `P → R`
 ```
 imp_trans : (P → Q) → (Q → R) → P → R
 ```
+
+Of course, because of `and_comm`, you know you can flip this around too.
+`Q → R` and `P → Q` implies `P → R` has a near-identical proof.
+
+### Infix Operator:
+`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.
 "
 
+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)
@@ -114,6 +136,9 @@ Therefore, not P.
 ```
 mt : (P → Q) → ¬Q → ¬P
 ```
+
+### Infix Operator:
+`mt` is a specialized version of `imp_trans`, which makes it possible to use `≫` as an infix operator for `mt`.
 "
 
 def identity {P : Prop}(p : P) : P := p

Game/Doc/Tactics.lean

@@ -2,9 +2,9 @@ import GameServer.Commands
 
 TacticDoc exact "
 # 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 `have` 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 weather 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.
+`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.
 
 # Errors
 Because most of the starting levels use only the `exact` tactic and an expression, it's common to forget to specify the tactic. Sometimes this raises the error:

Game/Levels/AndIntro.lean

@@ -17,7 +17,7 @@ You're hosting your yearly soirée, and it's time to start planning! Last year y
 \\
 This year will be different‼ This year, if you want to be sure that there will be fancy cheeses, you had better have evidence that somebody is bringing the cheese platter.
 
-World 1: **Party Invites** is a tutorial world that is meant to introduce you to conjunction — the logical \"and\". The symbol used to denote an \"and\" looks like \"`∧`\". You'll learn to how to use evidence to create an `∧` and how also how to get evidence out when it's been `∧`ed together.\\
+World 1: **Party Invites** is a tutorial world that is meant to introduce you to conjunction — the logical “and”. The symbol used to denote an “and” looks like “`∧`”. You'll learn to how to use evidence to create an `∧` and how also how to get evidence out when it's been `∧`ed together.\\
 \\
 The real-world analogues for evidence of `A ∧ B` might be a box with evidence for `A` and evidence for `B`, an audio recording with both pieces of evidence, or a tree with evidence in its branches.\\
 \\

Game/Levels/AndIntro/L01.lean

@@ -14,10 +14,7 @@ You've made a todo list, so you've begun to plan your party. Exhibit evidence th
 ## Proposition Key:
 `P` — You're **P**lanning a party
 ## Assumptions
-`h : P` — Can be read as `h` is evidence for `P`\\
-\\
-On the one hand, you can think of `h` as a reference to the assumption `P`. On the other hand, given the flavour text above, you can imagine that `h` is the name you've give your todo list (because your todo list is evidence for the proposition that \"You're **P**lanning a party\")
-
+`todo_list : P` — Can be read as `todo_list` “is evidence for” `P`\\
 # 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 premises directly, but as you learn how to form expressions the `exact` tactic will accept those too.\\
 \\
@@ -26,9 +23,9 @@ It's entered like this:
 Goal: P
 exact <<expression that evaluates to evidence for P>>
 ```
-You can use the `exact` tactic to give `h` as your answer.\\
+You can use the `exact` tactic to give `todo_list` as your answer.\\
 \\
-⋆Spoilers!⋆ If you enter \"`exact h`\", you will have completed this level.
+⋆Spoilers!⋆ If you enter “`exact todo_list`,” you will have completed this level.
 
 # Become Familiar with the User Interface!
 
@@ -37,17 +34,16 @@ Found in the middle bottom of the screen, the proof state tells you what objects
 ## 1. Objects:
 In this level, you'll notice that there is only one proposition. `P : Prop` is the game's way of telling you that it knows that `P` is a proposition. You can check out the **Proposition Key** above to learn what it's denoting in this level if you're interested.
 ## 2. Assumptions:
-You'll notice that you have some evidence too. The shorthand for a proposition traditionally starts with a capital letter and the shorthand for evidence traditionally starts with a lowercase letter.
-1. `h : P` — again, you can read this as `h` is evidence for `P`. If the line said `h : ¬P` instead, then that would be saying that `h` is evidence that you're not planning a party.
+Most levels will give you some starting assumptions that take the form of evidence for some propositions. The shorthand for a proposition traditionally starts with a capital letter and the shorthand for evidence traditionally starts with a lowercase letter.
 ## 3. Goal:
 The goal is always a proposition that you want to exhibit some evidence for. In this level, one of your assumptions already contains evidence for the goal. That will certainly not always be the case.
 # Inventory
 On the right of the screen is your inventory of tactics, definitions, and theorems. Once unlocked, you can click them to read about what they do.
 "
 
 /-- Exhibit evidence that you're planning a party. -/
-Statement (P : Prop)(h : P) : P := by
-  exact h
+Statement (P : Prop)(todo_list : P) : P := by
+  exact todo_list
 
 Conclusion "
 Congratulations, not only have you started your todo list, you've learned how to exhibit the list as evidence that you've started planning the party.

Game/Levels/AndIntro/L02.lean

@@ -7,25 +7,25 @@ Title "And Introduction"
 NewDefinition and_intro
 
 Introduction "
-# Sending out some Invites
-You have two letters, one is an invitation for Paul and one is for Sarah, the two of them live together so you'd like to combine their invites into a single item to be shipped. The box you're putting them in has room for two items, one on the left and one of the right.\\
+# Sending Invitations in a Single Package
+You have two letters, one extending an invitation to Paul and the other to Sarah. Since they share a residence, you'd like to consolidate their invites into a single package for shipping. The box you're using has space for two items, one on the left and one on the right.\\
 \\
-You label the box to say that Paul's invite on the left and Sarah's invite on the right. That way nobody can be confused about what's in the box. Also, once they open the box, they'll know exactly where to look for the invite without needing to check the entire box.
+You've labelled the box explicitly, specifying that Paul's invitation is on the left and Sarah's invitation is on the right. This ensures there's no confusion about the contents of the box. Upon opening it, they will easily locate their respective invites without the need to search the entire package.
 # Proposition Key:
-- P — \"**P**aul is invited to the party\"
-- S — \"**S**arah is invited to the party\"
+- P — “**P**aul is invited to the party”
+- S — “**S**arah is invited to the party”
 # `∧`
-The hat symbol \" ∧ \" is how logicians denote a logical \"and\". `A ∧ B` means \"A and B\". It works the way you would intuitively expect. Like a lot of math operators (like `+,-,÷,×`,and others), the `∧` symbol is an infix operator. This means it has a left side and a right side. Looking at `A ∧ B`, you can see that `A` is on the left and `B` is on the right.\\
+The hat symbol “ ∧ ” is how logicians denote a conjunction — a logical “and”. `A ∧ B` means “A and B”. It works the way you would intuitively expect. Like a lot of math operators (`+,-,÷,×`,and others), the `∧` symbol is an infix operator. This means it has a left side and a right side. Looking at `A ∧ B`, you can see that `A` is on the left and `B` is on the right.\\
 \\
 In this game, that means anything operating as evidence for `A ∧ B` will have a left part and a right part as well. The box described in the intro works this way.
 # Assumptions
 - `p : P` — Your invitation for Paul is evidence that Paul is invited to the party
 - `s : S` — Your invitation for Sarah is evidence that Sarah is invited to the party
 # Goal
-Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use evidence (generally lowercase letters), to deduce new propositions (generally upercase letters)
+Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use evidence (generally lowercase letters), to deduce new propositions (generally uppercase letters)
 
 # A new definition
-This level has unlocked \"∧ intro\" under definitions. This has made the `and_intro` constructor 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.\\
+This level has unlocked “∧ intro” under definitions. This has made the `and_intro` constructor 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.
 # A reminder