Add introductory levels

2022-12-01 16:00:18 +01:00
parent 0273d6a465 9e8518568a
commit 7091f8adac
26 changed files with 801 additions and 110 deletions
@@ -1,3 +1,5 @@
 node_modules
 client/dist
-server/build
+server/build
+**/lean_packages/
+
@@ -48,11 +48,12 @@ elab "Introduction" t:str : command => do
  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}

 /-- Define the statement of the current level. -/
-elab "Statement" sig:declSig val:declVal : command => do
+elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
  let lvlIdx ← getCurLevelIdx
  let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
  elabCommand (← `(theorem $(mkIdent declName) $sig $val))
  modifyCurLevel fun level => pure {level with goal := sig}
+-- TODO: Do something with the lemma name.

 /-- Define the conclusion of the current game or current level if some
 building a level. -/
@@ -131,6 +132,10 @@ local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
 macro "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
  `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg)

+/-- Declare a hint in reaction to a given tactic state in the current level. -/
+macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
+  `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg)
+  -- TODO: implement me?

 /-! ## Tactics -/

@@ -0,0 +1,10 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers" : [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true
+}
@@ -1,6 +1,16 @@
 import TestGame.Metadata
-import TestGame.Levels.Level1
-import TestGame.Levels.Level2
-import TestGame.Levels.Level3
-import TestGame.Levels.Level4
-import TestGame.Levels.Level5
+import TestGame.Levels.Logic.L01_Rfl
+import TestGame.Levels.Logic.L02_Rfl
+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
@@ -1,14 +1,14 @@
 import GameServer.Commands
-import TestGame.MyNat
+-- import TestGame.MyNat

-LemmaDoc zero_add as zero_add in "Addition"
-"This lemma says `∀ a : ℕ, 0 + a = a`."
+-- LemmaDoc zero_add as zero_add in "Addition"
+-- "This lemma says `∀ a : ℕ, 0 + a = a`."

-LemmaDoc add_zero as add_zero in "Addition"
-"This lemma says `∀ a : ℕ, a + 0 = a`."
+-- LemmaDoc add_zero as add_zero in "Addition"
+-- "This lemma says `∀ a : ℕ, a + 0 = a`."

-LemmaDoc add_succ as add_succ in "Addition"
-"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
+-- LemmaDoc add_succ as add_succ in "Addition"
+-- "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."

-LemmaSet addition : "Addition lemmas" := 
-zero_add add_zero
+-- LemmaSet addition : "Addition lemmas" :=
+-- zero_add add_zero
@@ -0,0 +1,35 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 1
+
+Title "Aller Anfang ist... ein Einzeiler?"
+
+Introduction
+"
+Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
+unterstützt und verifiziert schreiben kann.
+
+Ein Beweis besteht in Lean aus verschiedenen **Taktiken**, welche ungefähr einem
+logischen Schritt entsprechen, den man auf Papier aufschreiben würde.
+
+Rechts im **Infoview** siehst den Status des aktuellen Beweis.
+Du siehst ein oder mehrere offene **Goals** (mit einem `⊢` davor), die du noch zeigen musst.
+Wenn du eine Taktik hinschreibst, dann versucht Lean diesen Schritt beim
+ersten offenen Goal zu machen.
+Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
+"
+
+Statement "Zeige `42 = 42`." : 42 = 42 := by
+  rfl
+
+Message : 42 = 42 =>
+"Die erste Taktik ist `rfl`, die ein Goal von der Form `A = A` beweist."
+
+Hint : 42 = 42 =>
+"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein gefolgt von ENTER."
+
+Conclusion "Bravo!"
+
+Tactics rfl
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 2
+
+Title "Definitionally equal"
+
+Introduction
+"
+Achtung: `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
+definiert sind, auch wenn diese unterschiedlich dargestellt werden.
+So sind `1 + 1` und `2` per Definition das Gleiche, da sie beide von Lean als `0.succ.succ`
+gelesen werden.
+
+Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab.
+"
+
+Statement "Zeige dass eins plus eins zwei ist." : 1 + 1 = 2 := by
+  rfl
+
+Conclusion
+"
+Im weiteren führen die meisten anderen Taktiken `refl` automatisch am Ende aus,
+deshalb musst du dieses häufig gar nicht mehr schreiben.
+"
+
+Tactics rfl
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 3
+
+Title "Annahmen"
+
+Introduction
+"
+Mathematische Aussagen haben Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine
+natürliche Zahl\", oder auch wahre Aussagen über diese Objekte, wie zum Beispiel
+\"und angenommen, dass `n` strikt grösser als `1` ist\".
+
+In Lean schreibt man beides mit dem gleichen Syntax: `(n : ℕ) (h : 1 < n)` definiert
+zuerst `n` als natürliche Zahl und kreeirt eien Annahme, dass `1 < n`. Dieser Annahme geben wir
+den Namen `h`.
+
+Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
+"
+
+Statement triviale_angelegenheit
+    "Angenommen `1 < n`. dann ist `1 < n`."
+    (n : ℕ) (h : 1 < n) : 1 < n := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Basic -- TODO
+
+Game "TestGame"
+World "TestWorld"
+Level 4
+
+Title "Logische Aussagen: `Prop`"
+
+Introduction
+"
+Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. Damit sagt man noch nicht,
+ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man an, dass
+`A` wahr ist: `hA` ist ein Beweis der Aussage `A`.
+"
+
+-- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
+Statement mehr_triviales
+    "
+    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
+    Zeige, dass `A` wahr ist.
+    "
+    (A : Prop) (hA : A) : A := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
@@ -0,0 +1,53 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 5
+
+Title "Rewrite"
+
+Introduction
+"
+Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern man braucht
+mehrere Schritte im Beweis.
+
+Wenn man eine Annahme `(h : X = Y)` hat die sagt, dass `X` und `Y` gleich sind,
+kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
+das eine durch das andere zu ersetzen.
+"
+
+Statement umschreiben
+    "
+    Angenommen man hat die Gleichheiten
+    `a = b`, `a = d`, `c = d`.
+    Zeige dass `b = c`.
+    "
+    (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rw [h₁]
+  rw [←h₂]
+  assumption
+
+-- Gleich am Anfang anzeigen.
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+"Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
+`c` im Goal mit `d` ersetzen."
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man schreibt diese mit
+`\\1`, `\\2`, `\\3`, …"
+
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
+"Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
+`(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
+
+-- TODO: Muss ich das wirklich mehrmals auflisten?
+Message (x : ℕ) : x = x =>
+"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
+anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
+
+Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben
+anstatt dem Goal."
+-- TODO: Das macht es doch unmöglich mit den Messages...
+
+Tactics assumption
+Tactics rw
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "TestWorld"
+Level 6
+
+Title "Implikation"
+
+Introduction
+"
+Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
+die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
+Aussage `A`.
+
+Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
+`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
+
+Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
+diese mit `apply h` anwenden.
+Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\".
+"
+
+Statement
+    "
+    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist.
+    "
+    (A B : Prop) (hA : A) (g : A → B) : B := by
+  apply g
+  assumption
+
+Message (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
+"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch `A` zeigen,
+dafür hast du bereits einen Beweis in den Annahmen."
+
+Tactics apply
+Tactics assumption
@@ -0,0 +1,43 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 7
+
+Title "Implikation"
+
+Introduction
+"
+Angenommen man hat folgende Implikationen und weiss dass Aussage `A` wahr ist.
+```
+A → B ← C
+    ↓   ↓
+D → E → F
+```
+Beweise Aussage `F`.
+"
+
+Statement
+    "
+    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist.
+    "
+    (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E)
+     (i : D → E) (k : E → F) (m : C → F) : F := by
+  apply k
+  apply h
+  apply f
+  assumption
+
+Message  (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+    (hA : A) (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F) : C =>
+"Sackgasse. Probier doch einen anderen Weg."
+
+Message  (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+    (hA : A) (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F) : D =>
+"Sackgasse. Probier doch einen anderen Weg."
+
+Tactics apply
+Tactics assumption
@@ -0,0 +1,22 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 8
+
+Title "Implikation"
+
+Introduction
+"
+Wenn das Goal von der Form `A → B` ist, kann man mit `intro` annehmen, dass `A` wahr ist
+und das Goal wird zu `B`.
+"
+
+Statement
+    (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+  intro hA
+  apply g
+  apply f
+  assumption
+
+Tactics intro apply assumption
@@ -0,0 +1,30 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 9
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Genau-dann-wenn `A ↔ B` (`\\iff`) besteht aus zwei Implikationen `A → B` und `B → A`.
+
+Als erstes kann man mit `rw` Annahmen der Form `(h : A ↔ B)` genau gleich wie Gleichungen
+`(h : a = b)` benützen, um das Goal umzuschreiben.
+
+Hier also nochmals die Gleiche Aufgabe, aber diesmal mit Iff-Statements von Aussagen anstatt
+Gleichungen von natürlichen Zahlen.
+"
+
+Statement
+    "
+    Zeige dass `B ↔ C`.
+    "
+    (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
+  rw [h₁]
+  rw [←h₂]
+  assumption
+
+Tactics rw
+Tactics assumption
@@ -0,0 +1,39 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 10
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Als nächstes will man oft ein Iff-Statement `A ↔ B` wie zwei einzelne Implikationen
+`A → B` und `B → A` behandeln.
+
+Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in die Einzelteile
+`A → B` und `B → A` zerlegen.
+
+"
+
+Statement
+    "
+    Zeige dass `B ↔ C`.
+    "
+    (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+  constructor
+  assumption
+  assumption
+
+
+Conclusion
+"
+Die Taktik `constructor` heisst so, weil `↔` als \"Struktur\" definiert ist, die
+aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, es soll versuchen,
+ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
+"
+
+Tactics constructor
+Tactics assumption
+
+-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
@@ -0,0 +1,62 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "TestWorld"
+Level 11
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Umgekehrt, wenn man eine Annahme `(h : A ↔ B)` hat, kann man auf verschiedene
+Arten die Einzelteile `A → B` und `B → A` extrahieren.
+
+- mit `rcases h` oder `rcases h with ⟨h₁, h₂⟩` teilt man die Annahme `h` auf. (Im zweiten Fall gibt
+man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<` und `\\>`).
+
+"
+Statement
+    (A B : Prop) : (A ↔ B) → (A → B) := by
+  intro h
+  rcases h
+  exact mp
+
+Message (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
+"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
+
+Conclusion
+"
+Anstatt
+```
+intro h
+rcases h with ⟨h₁, h₂⟩
+```
+kann man direkt `intro ⟨h₁, h₂⟩` schreiben.
+Wie du schon gesehen hast, sind diese Klammern `⟨⟩` Lean's Syntax für eine Struktur aus
+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
@@ -0,0 +1,33 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 12
+
+Title "Genau dann wenn"
+
+Introduction
+"
+Man kann auch die einzelnen Richtungen benützen, ohne `h` selber zu verändern:
+
+- `h.1` und `h.2` sind direkt die einzelnen Richtungen. Man kann also z.B. mit `apply h.1` die
+Implikation `A → B` auf ein Goal `B` anwenden.
+- `h.mp` und `h.mpr` sind die bevorzugten Namen anstatt `.1` und `.2`. \"mp\" kommt von
+\"Modus Ponens\", aber das ist hier irrelevant.
+"
+
+Statement
+    "
+    Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen.
+    "
+    (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+  intro hA
+  apply g
+  apply h.mp
+  assumption
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
+"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
+
+Tactics apply
+Tactics assumption
@@ -0,0 +1,71 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "TestWorld"
+Level 13
+
+Title "Und"
+
+Introduction
+"
+Das logische UND `A ∧ B` (`\\and`) funktioniert sehr ähnlich zum Iff (`↔`).
+Grund dafür ist, dass `A ∧ B` auch eine Struktur aus zwei Teilen `⟨A, B⟩` ist.
+
+Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
+`.1` und `.2` für die Einzelteile brauchen, diese heissen lediglich
+`h.left` und `h.right` anstatt `.mp` und `.mpr`.
+"
+
+Statement
+    (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
+  constructor
+  intro h
+  rcases h with ⟨h₁, h₂⟩
+  constructor
+  assumption
+  apply h₂
+  assumption
+  intro h
+  rcases h with ⟨h₁, h₂⟩
+  constructor
+  assumption
+  intro
+  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
@@ -0,0 +1,25 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "TestWorld"
+Level 14
+
+Title "Oder"
+
+Introduction
+"
+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 (A B : Prop) (hA : A) : A ∨ (¬ B) := by
+  left
+  assumption
+
+Tactics left right assumption
@@ -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
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "TestWorld"
+Level 1
+
+Title "Annahmen"
+
+Introduction "yadaa yadaa"
+
+class MyClass (n : ℕ) where
+
+Statement name
+"Beweise dieses Lemma."
+(n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := sorry
+  mul_assoc := sorry
+
+--@[exercise]
+instance instTest (n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := by
+    sorry
+  mul_assoc := by
+    sorry
+
+--@[exercise]
+lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rewrite [h₁]
+  rw [←h₂]
+  assumption
+
+
+Conclusion ""
+
+Tactics assumption
@@ -1,7 +1,8 @@
 import GameServer.Commands
-import TestGame.MyNat
+--import TestGame.MyNat
 import TestGame.TacticDocs
 import TestGame.LemmaDocs
+import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.

 Game "TestGame"

@@ -10,10 +11,10 @@ Title "The Natural Number Game"
 Introduction
 "This is a sad day for mathematics. While trying to find glorious new foundations for mathematics,
 someone removed the law of excluded middle and the axiom of choice. Unsurprisingly,
-everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage 
+everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage
 but now we need to rebuild all of mathematics from scratch.

-As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from 
+As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from
 the axioms that Giuseppe Peano found under the collapsed tower of number theory. You've been equipped
 with a level 1 spell book. Good luck."

@@ -31,4 +32,4 @@ World "v4"

 Path TestWorld → w1 → w2 → w3
 Path w1 → v1 → v2 → v3 → w3
-Path v3 → v4
+Path v3 → v4
@@ -1,6 +1,6 @@
 axiom MyNat : Type

-notation "ℕ" => MyNat
+--notation "ℕ" => MyNat

 --axiom zero : ℕ

@@ -17,4 +17,3 @@ axiom add_zero : ∀ a : ℕ, a + 0 = a
 axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)

@[elab_as_elim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
-
@@ -4,29 +4,131 @@ import TestGame.Tactics

 TacticDoc rfl
 "
-## Summary
+## Beschreibung

-`rfl` proves goals of the form `X = X`.
+`rfl` beweist ein Goal der Form `X = X`.

-## Details
+## Detail

-The `rfl` tactic will close any goal of the form `A = B`
-where `A` and `B` are *exactly the same thing*.
+`rfl` beweist jedes Goal `A = B` wenn `A` und `B` genau das gleiche sind.
+Wichtig ist nicht, ob diese im Infoview gleich aussehen, sondern ob sie in
+Lean gleich definiert sind.

-### Example:
-If it looks like this in the top right hand box:
+## Beispiel
+`rfl` kann folgenes Goal beweisen:
+```
+Objects
+  a b c : ℕ
+Prove:
+  (a + b) * c = (a + b) * c
+```
+
+`rfl` kann auch folgendes beweisen:
+```
+Objects
+  n : ℕ
+Prove:
+  1 + 1 = 2
+```
+denn Lean liest dies intern als `0.succ.succ = 0.succ.succ`.
+"
+
+TacticDoc assumption
+"
+## Beschreibung
+
+`assumption` sucht nach einer Annahme, die genau dem Goal entspricht.
+
+## Beispiel
+Wenn das Goal wie folgt aussieht:
 ```
 Objects
  a b c d : ℕ
+  h : a + b = c
+  g : a * b = 16
+  t : c = 12
 Prove:
-  (a + b) * (c + d) = (a + b) * (c + d)
+  a + b = c
 ```

-then
+dann findet `assumption` die Annahme `h`und schliesst den Beweis.
+"
+
+TacticDoc rewrite
+"
+## Beschreibung
+
+Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+"
+
+TacticDoc rw
+"
+## Beschreibung
+
+Wenn man eine Annahme `(h : X = Y)` hat, kann man mit
+`rw [h]` alle `X` im Goal durch `Y` ersetzen.
+
+## Detail
+- `rw [←h]` wendet `h` rückwärts an und ersetzt alle `Y` durch `X`.
+- `rw [h, g, ←f]`: Man kann auch mehrere `rw` zusammenfassen.
+- `rw [h] at h₂` ersetzt alle `X` in `h₂` zu `Y` (anstatt im Goal).
+
+`rw` funktioniert gleichermassen mit Annahmen `(h : X = Y)` also auch
+mit Theoremen/Lemmas der Form `X = Y`
+
+## Beispiel
+
+TODO
+"
+
+
+TacticDoc apply
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc constructor
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc rcases
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc left
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc right
+"
+## Beschreibung
+
+TODO
+"
+
+
+
+
+
+
+
+
+
+
+

-`rfl`

-will close the goal and solve the level."

 TacticDoc induction_on
 "
@@ -67,82 +169,9 @@ Prove:
 ```
 "

-TacticDoc rewrite
-"
-## Summary

-If `h` is a proof of `X = Y`, then `rewrite [h],` will change
-all `X`s in the goal to `Y`s. Variants: `rewrite [<- h]` (changes
-`Y` to `X`) and
-`rewrite [h] at h2` (changes `X` to `Y` in hypothesis `h2` instead
-of the goal).
-
-## Details
-
-The `rewrite` tactic is a way to do \"substituting in\". There
-are two distinct situations where use this tactics.
-
-1) If `h : A = B` is a hypothesis (i.e., a proof of `A = B`)
-in your local context (the box in the top right)
-and if your goal contains one or more `A`s, then `rewrite h`
-will change them all to `B`'s. 
-
-2) The `rewrite` tactic will also work with proofs of theorems
-which are equalities (look for them in the inventory).
-For example, if your inventory contains `add_zero x : x + 0 = x`, 
-then `rewrite [add_zero]` will change `x + 0` into `x` in your goal 
-(or fail with an error if Lean cannot find `x + 0` in the goal).
-
-Important note: if `h` is not a proof of the form `A = B`
-or `A ↔ B` (for example if `h` is a function, an implication,
-or perhaps even a proposition itself rather than its proof),
-then `rewrite` is not the tactic you want to use. For example,
-`rewrite [P = Q]` is never correct: `P = Q` is the true-false
-statement itself, not the proof.
-If `h : P = Q` is its proof, then `rewrite [h]` will work.
-
-Pro tip 1: If `h : A = B` and you want to change
-`B`s to `A`s instead, try `rewrite [<- h]` (get the arrow with `\\l` and
-note that this is a small letter L, not a number 1).
-
-### Example:
-If it looks like this in the top right hand box:
-```
-Objects
-  x y : ℕ
-Assumptions  
-  h : x = y + y
-Prove:
-  succ (x + 0) = succ (y + y)
-```
-
-then
-
-`rewrite [add_zero]`
-
-will change the goal into `succ x = succ (y + y)`, and then
-
-`rewrite [h]`
-
-will change the goal into `succ (y + y) = succ (y + y)`, which
-can be solved with `rfl,`.
-
-### Example: 
-You can use `rewrite` to change a hypothesis as well. 
-For example, if your local context looks like this:
-```
-Objects
-  x y : ℕ
-Assumptions
-  h1 : x = y + 3
-  h2 : 2 * y = x
-Prove:
-  y = 3
-```
-then `rewrite [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
-"

 TacticDoc intro
 "Useful to introduce stuff"

-TacticSet basics := rfl induction_on intro rewrite
+TacticSet basics := rfl induction_on intro rewrite
@@ -1,5 +1,5 @@
 import Lean
-import TestGame.MyNat
+-- import TestGame.MyNat

 open Lean Elab Tactic

@@ -8,5 +8,5 @@ elab "swap" : tactic => do
  | g₁::g₂::t => setGoals (g₂::g₁::t)
  | _ => pure ()

-- macro "induction_on" n:ident : tactic => 
-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
+-- macro "induction_on" n:ident : tactic =>
+-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
@@ -3,6 +3,9 @@ open Lake DSL

 require GameServer from ".."/"leanserver"

+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"@"b1cf06cb126ee163a7dc895c1aee17946ff20900"
+
 package TestGame

@[default_target]