Update lvls

Game.lean

@@ -5,16 +5,33 @@ import GameServer.Commands
 -- in this case). Each world consists of a finite number of levels, and levels
 -- are numbered 1,2,3,4... inside the level files.
 import Game.Levels.AndIntro
+import Game.Levels.AndTactic
 import Game.Levels.ImpIntro
+import Game.Levels.ImpTactic
 import Game.Levels.NotIntro
+import Game.Levels.NotTactic
 import Game.Levels.OrIntro
+import Game.Levels.OrTactic
 import Game.Levels.IffIntro
+import Game.Levels.IffTactic
 
 -- Here's where we show how to glue the worlds together
+-- Intro World Dependencies
 Dependency AndIntro → ImpIntro
 Dependency ImpIntro → NotIntro
 Dependency ImpIntro → OrIntro
 Dependency ImpIntro → IffIntro
+-- Intro—Tactic Dependencies
+Dependency AndIntro → AndTactic
+Dependency ImpIntro → ImpTactic
+Dependency OrIntro → OrTactic
+Dependency NotIntro → NotTactic
+Dependency IffIntro → IffTactic
+-- Tactic World Dependencies
+Dependency AndTactic → ImpTactic
+Dependency ImpTactic → OrTactic
+Dependency ImpTactic → NotTactic
+Dependency ImpTactic → IffTactic
 
 -- Here's what we'll put on the title screen
 Title "A Lean Intro to Logic"
@@ -157,7 +174,7 @@ Warning: In most browsers, deleting cookies will also clear the local storage
 Languages "English"
 CaptionShort "Lean intro to Logic"
 CaptionLong "Self-contained friendly introduction to constructive logic"
--- CoverImage "images/cover.png"
+CoverImage "images/logic0101.png"
 
 /-! Build the game. Show's warnings if it found a problem with your game. -/
 MakeGame

Game/Doc/Tactics.lean

@@ -118,17 +118,7 @@ TacticDoc rw
 
 /--
 ## 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`.
+`repeat t` repeatedly applies the tactic `t` to the goal. You don't need to use this tactic, it just speeds things up sometimes.
 -/
 TacticDoc «repeat»
 
@@ -145,3 +135,51 @@ 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`.
 -/
 TacticDoc nth_rewrite
+
+/--
+assumption tries to solve the main goal by searching your the assumptions in your proof state for a hypothesis with a compatible proposition
+-/
+TacticDoc assumption
+
+/--
+# Constructor
+Whenever there's a clear way to create new evidence **that matches the goal**, the constructor tactic will pick that for you. This replaces the current goal with one or more goals that together complete the construction.
+
+For example, if your goal is `P ∧ Q` then the `constructor` tactic will replace that goal with two separate subgoals. First you'll need to show evidence for `P`, then you'll need to show evidence for `Q`.
+-/
+TacticDoc constructor
+
+/--
+TODO
+-/
+TacticDoc cases
+
+/--
+TODO
+-/
+TacticDoc apply
+
+/--
+TODO
+-/
+TacticDoc intro
+
+/--
+TODO
+-/
+TacticDoc contradiction
+
+/--
+TODO
+-/
+TacticDoc exfalso
+
+/--
+TODO
+-/
+TacticDoc left
+
+/--
+TODO
+-/
+TacticDoc right

Game/Levels/AndIntro.lean

@@ -24,4 +24,34 @@ The real-world analogues for evidence of `A ∧ B` might be a box with evidence
 While real-world analogues can be anything, the abstract machinery used in this game will always be the same. In the case of the `∧` operator, the game stores the associated evidence in a tuple data structure.\\
 \\
 The details aren't important. Each level will be encoded for you into the symbols of a proof state. The puzzle, at its core, will be about symbol manipulation. Much of the text is there for added fun and flair.
+
+# **Aside**: Expressions
+If you're coming at this as a puzzle, part of the goal of the tutotial worlds is to teach you how to form expressions and to think about what they evaluate to. Consider how how these expressions all evaluate to the same number:
+```
+4 + 6
+(4) + 6
+(4) + (6)
+3 + 1 + 6
+3 + (1 + 6)
+4 + 4 + 2
+(4 * 2) + 2
+```
+and how some things which may look like expressions really are not:
+```
+4 6
+4 +
+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:
+```
+add 4 6
+add (4) 6
+add (4) (6)
+add (add 3 1) 6
+add 3 (add 1 6)
+add (add 4 4) 2
+add (mul 4 2) 2
+```
+We're not using expressions to express numbers, but many of the concepts do carry over. Instead of numbers, we're working with logical inferences.
 "

Game/Levels/AndIntro/L01.lean

@@ -8,23 +8,19 @@ Title "Exactly! It's in the premise"
 
 NewTactic exact
 NewDefinition GameLogic.AsciiTable
+OnlyTactic exact
 
 Introduction "
 # Introduction
-You've made a todo list, so you've begun to plan your party. Exhibit evidence that you're planning the party.
+You've made a todo list, so you've begun to plan your party.
 ## Proposition Key:
 `P` — You're **P**lanning a party
 ## Assumptions
 `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.\\
+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.\\
 \\
-It's entered like this:
-```
-Goal: P
-exact <<expression that evaluates to evidence for P>>
-```
-You can use the `exact` tactic to give `todo_list` as your answer.\\
+The expression looks like `exact e` were `e` is an expression the game will accept for the current Goal.\\
 \\
 ⋆Spoilers!⋆ If you enter “`exact todo_list`,” you will have completed this level.
 

Game/Levels/AndIntro/L02.lean

@@ -8,35 +8,31 @@ Title "And Introduction"
 
 NewTheorem GameLogic.and_intro
 NewDefinition GameLogic.and_def
+OnlyTactic exact
 
 Introduction "
+# `∧`
+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.
+
 # Sending Invitations in a Single Package
 You have two letters, one extending an invitation to Pippin and the other to Sybeth. 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've labelled the box explicitly, specifying that Pippin's invitation is on the left and Sybeth'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**ippin is invited to the party”
 - S — “**S**ybeth is invited to the party”
-# `∧`
-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 Pippin is evidence that Pippin is invited to the party
 - `s : S` — Your invitation for Sybeth is evidence that Sybeth 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 uppercase letters)
 
-# Juxtapose!
-Throughout this game, most of the expressions you will learn are expressed with a name juxtaposed in front of some number of parameters. The form is something like `(name_a param1 param2)`\\
-\\
-In general, “params” can themsevles be the result of any expression as well. You'll often see nested expressions like `(name_a (name_b param1 param2) param2)` where `(name_b param1 param2)` is the first parameter to `name_a` in this example.
-
 # Using the `∧` Construtor
 This level has unlocked “`∧`” 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.
-
+The help-page has even more detail about creating conjunctions like this (There's a common shorthand using angle-brackers `⟨` `⟩`).
 
 # A reminder
 Use the `exact` tactic to exhibit evidence for a goal
@@ -54,7 +50,6 @@ You've got evidence that Pippin and Sybeth are invited to the party.\\
 Here are some answers the game would have accepted:
 ```
 exact and_intro p s
-exact {left := p, right := s}
 exact ⟨p,s⟩
 ```
 "

Game/Levels/AndIntro/L03.lean

@@ -8,6 +8,9 @@ Title "The Have Tactic"
 
 NewDefinition GameLogic.Precedence
 NewTactic «have»
+OnlyTactic
+  exact
+  «have»
 
 Introduction "
 # Too Many Invites
@@ -23,7 +26,6 @@ Nesting boxes like this is a way to get around the “two items per box” rule.
 - O — **O**rin is invited to the party
 - U — **U**riel is invited to the party
 
-
 # The `have` Tactic
 You can complete this level with your knowledge from the previous level without using this new tactic. For example, either of these would work:
 ```
@@ -32,7 +34,7 @@ exact ⟨⟨a,i⟩,⟨o,u⟩⟩
 ```
 Instead of nesting this way, you can break the process down into steps using the `have` tactic. Enter “`have ai := and_intro a i`” to create your first box. After it's entered, it will appear under assumptions in the proof state. Now enter “`have ou := and_intro o u`” to create the second box.\\
 \\
-Your proof state should now have the following assumptions:
+If you followed this suggestion, your proof state should now have the following assumptions:
 ```
 Assumptions:
 a: A
@@ -50,21 +52,12 @@ Finally, now you can place these two boxes — `ai` and `ou` — into a third bo
 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
   have ou := and_intro o u
+  Hint (hidden := true) "exact and_intro {ai} {ou}"
   exact and_intro ai ou
 
+example (A I O U : Prop)(a : A)(i : I)(o : O)(u : U) : (A ∧ I) ∧ O ∧ U := by
+  exact ⟨⟨a,i⟩,⟨o,u⟩⟩
 
 Conclusion "
 Great! Another 4 invites sent out. You're getting the hang of this.
-
-----
-````
--- 1. Alarfil and Ilyn: A ∧ I
-have h₁ := and_intro a i
-
--- 2. Orin and Uriel: O ∧ U
-have h₂ := and_intro o u
-
--- 3. both boxes in a final box
-exact and_intro h₁ h₂
-````
 "

Game/Levels/AndIntro/L04.lean

@@ -7,6 +7,9 @@ Level 4
 Title "And Elimination"
 
 NewTheorem GameLogic.and_left
+OnlyTactic
+  exact
+  «have»
 
 Introduction "
 # Using Only What Is Needed
@@ -17,34 +20,33 @@ You'd like to convince Cyna to join the party. You know that Cyna is good friend
 - P — \"**P**ippin is coming to the party\"
 - S — \"**S**ybeth is coming to the party\"
 # Assumptions:
-- `h : P ∧ S` — The voicemail (`h`) is evidence that `P ∧ S`
+- `vm : P ∧ S` — The voicemail (`vm`) is evidence that `P ∧ S`
 # Convincing Cyna
-Cyna is close with Pippin, but you don't know much about his friendship with Sybeth. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `h`.\\
+Cyna is close with Pippin, but you don't know much about his friendship with Sybeth. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `vm`.\\
 \\
 This can be done with either of these two methods:
 ```
-have p := h.left
-have p := and_left h
+have p := and_left vm
+have p := vm.left
 ```
 Once you've done this, you're very close to level 1 again where the Goal is directly in your assumptions.
 "
 
 /-- Exhibit evidence that Pippin is coming to the party. -/
-Statement (P S : Prop)(h: P ∧ S) : P := by
-  have p := h.left
+Statement (P S : Prop)(vm: P ∧ S) : P := by
+  have p := and_left vm
+  exact p
+
+example (P S : Prop)(vm: P ∧ S) : P := by
+  have p := vm.left
   exact p
 
 Conclusion "
 You've got a proof that Pippin is coming to the party! Lets see if Cyna will attend as well.
 
 ----
-Which proof did you use?
-```lean
-have p := h.left
-exact p
-```
-or
+A reminder that expressions work with the `have` and `exact` tactics in much the same way. You can also solve this level without `have`.
 ```lean
-exact h.left
+exact vm.left
 ```
 "

Game/Levels/AndIntro/L05.lean

@@ -7,6 +7,9 @@ Level 5
 Title "And Elimination 2"
 
 NewTheorem GameLogic.and_right
+OnlyTactic
+  exact
+  «have»
 
 Introduction "
 # Another Unlock
@@ -16,7 +19,7 @@ Can you figure this one out?
 /-- Both P and Q entails just Q as well! -/
 Statement (P Q : Prop)(h: P ∧ Q) : Q := by
   Hint (hidden := true) "`exact h.right`"
-  exact h.right
+  exact and_right h
 
 Conclusion "
 Nice. Onward!