more levels

.gitignore

@@ -1,3 +1,5 @@
 node_modules
 client/dist
-server/build
+server/build
+**/lean_packages/
+

server/testgame/TestGame.lean

@@ -5,3 +5,12 @@ import TestGame.Levels.Logic.L03_Assumption
 import TestGame.Levels.Logic.L03b_Assumption
 import TestGame.Levels.Logic.L04_Rewrite
 import TestGame.Levels.Logic.L05_Apply
+import TestGame.Levels.Logic.L05b_Apply
+import TestGame.Levels.Logic.L05c_Apply
+import TestGame.Levels.Logic.L06_Iff
+import TestGame.Levels.Logic.L06b_Iff
+import TestGame.Levels.Logic.L06c_Iff
+import TestGame.Levels.Logic.L06d_Iff
+import TestGame.Levels.Logic.L07_And
+import TestGame.Levels.Logic.L08_Or
+import TestGame.Levels.Logic.L08b_Or

server/testgame/TestGame/Levels/Logic/L05_Apply.lean

@@ -1,4 +1,5 @@
 import TestGame.Metadata
+import Mathlib
 
 Game "TestGame"
 World "TestWorld"

server/testgame/TestGame/Levels/Logic/L05c_Apply.lean

@@ -13,12 +13,10 @@ und das Goal wird zu `B`.
 "
 
 Statement
-    (A B C: Prop) (f : A → B) (g : B → C) : A → C := by
+    (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
   intro hA
   apply g
   apply f
   assumption
 
-Tactics intro
+Tactics intro apply assumption
-Tactics apply
-Tactics assumption

server/testgame/TestGame/Levels/Logic/L06c_Iff.lean

@@ -1,5 +1,8 @@
 import TestGame.Metadata
 import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+
+set_option tactic.hygienic false
 
 Game "TestGame"
 World "TestWorld"
@@ -19,9 +22,8 @@ man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<`
 Statement
     (A B : Prop) : (A ↔ B) → (A → B) := by
   intro h
-  cases h
+  rcases h
-  case intro x y =>
+  exact mp
-  assumption
 
 Message (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
 "Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
@@ -40,3 +42,21 @@ mehreren Teilen.
 "
 
 Tactics intro apply rcases assumption
+
+
+
+
+
+
+
+-- TODO: The new `cases` works differntly. There is also `cases'`
+example (A B : Prop) : (A ↔ B) → (A → B) := by
+  intro h
+  cases h with
+  | intro a b =>
+    assumption
+
+example (A B : Prop) : (A ↔ B) → (A → B) := by
+  intro h
+  cases' h with a b
+  assumption

server/testgame/TestGame/Levels/Logic/L07_And.lean

@@ -1,6 +1,8 @@
 import TestGame.Metadata
 import Std.Tactic.RCases
 
+set_option tactic.hygienic false
+
 Game "TestGame"
 World "TestWorld"
 Level 13

server/testgame/TestGame/Levels/Logic/L08_Or.lean

@@ -1,5 +1,8 @@
 import TestGame.Metadata
-import Mathlib
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
 
 Game "TestGame"
 World "TestWorld"
@@ -9,47 +12,14 @@ Title "Oder"
 
 Introduction
 "
-Das logische ODER `A ∨ B` (`\\or`) funktioniert
+Das logische ODER `A ∨ B` (`\\or`) funktioniert ein wenig anders als das UND.
+
+Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden,
+welche Seite man beweisen möchte.
 "
 
-Statement
+Statement (A B : Prop) (hA : A) : A ∨ (¬ B) := by
-    (A B C : Prop) (h : (A ∨ B) ∨ C) : B ∨ (C ∨ A) := by
+  left
-  cases h
+  assumption
 
-
+Tactics left right assumption
-
-
-Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
-"`↔` oder `∧` im Goal kann man mit `constructor` aufteilen."
-
--- if they don't use `intro ⟨_, _⟩`.
-Message (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B =>
-"Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen."
-
--- if they don't use `intro ⟨_, _⟩`.
-Message (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) =>
-"Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` aufteilen."
-
-Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
-"Wieder in Einzelteile aufteilen..."
-
-Message (A : Prop) (B : Prop) : A ∧ (A → B) =>
-"Immer das gleiche ... noch mehr aufteilen."
-
-Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B =>
-"Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen,
-wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`).
-
-Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht,
-dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen,
-dass `B` wahr ist."
-
-Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
-"Sieht nach einem Fall für `apply` aus."
-
-
--- TODO
-
-
-Tactics apply rcases
-Tactics assumption

server/testgame/TestGame/Levels/Logic/L08b_Or.lean

@@ -0,0 +1,58 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "TestWorld"
+Level 15
+
+Title "Oder"
+
+Introduction
+"
+Wenn man hingegen ein ODER - `(h : A ∨ B)` - in den Annahmen hat, kann man dieses
+ähnlich wie beim UND mit `rcases h` aufteilen.
+
+ABER! Beim UND `(h : A ∧ B)` hat man dann zwei neue Annahmen erhalten, und diese hat man mit
+`rcases h with ⟨hA, hB⟩` benannt. Beim ODER `(h : A ∨ B)` kriegt man stattdessen zwei **Goals**
+wo man annimmt, dass entweder die linke oder rechte Seite von `h` war ist.
+Diese Annahme benennt man dann mit `rcases h with hA | hB`.
+"
+
+Statement and_or_imp
+  "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
+    (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
+  rcases h with h₁ | h₂
+  left
+  rcases h₁ with ⟨x, y⟩
+  assumption
+  right
+  constructor
+  apply h₂
+  assumption
+  assumption
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`. Der `|` signalisiert
+dass `h₁` und `h2` die Namen der neuen Annahmen in den verschiedenen Fällen sind."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER im Goal kann mit `left` oder `right` angegangen werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B =>
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen.
+Der Konstruktor `⟨⟩` signalisiert hier, dass dann nur ein Goal aber zwei neu benannte
+Annahmen erhält."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C =>
+"Sackgasse."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
+"Hmmm..."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
+"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
+
+Tactics left right assumption constructor rcases

server/testgame/TestGame/TacticDocs.lean

@@ -103,6 +103,19 @@ TacticDoc rcases
 TODO
 "
 
+TacticDoc left
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc right
+"
+## Beschreibung
+
+TODO
+"