Merge branch 'main' of github.com:hhu-adam/lean4game

README.md

@@ -8,6 +8,8 @@ The project is currently mostly copied from Patrick Massot's [NNG4](https://gith
 Building this requires a [npm](https://www.npmjs.com/) toolchain. After cloning the repository you should run
 `npm install` to pull in all dependencies. For development and experimentation, you can run `npm start` that will perform a non-optimized build and then run a local webserver on port 3000.
 
+### Progress
+This is a work in progress. In the future there are plans to host a server managing different public learning games for Lean4, but for now the target is to provide the first games (in German and eventually English) by April 2023.
 
 ## NPM Scripts
 
@@ -23,4 +25,4 @@ On the server side, the command will set up a docker image containing the Lean s
 ## Security
 
 Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container
-secured by [gVisor](https://gvisor.dev/).
+secured by [gVisor](https://gvisor.dev/).

server/testgame/TestGame.lean

@@ -14,3 +14,17 @@ import TestGame.Levels.Logic.L06d_Iff
 import TestGame.Levels.Logic.L07_And
 import TestGame.Levels.Logic.L08_Or
 import TestGame.Levels.Logic.L08b_Or
+import TestGame.Levels.Logic.L08c_Or
+import TestGame.Levels.Naturals.L01_Ring
+import TestGame.Levels.Naturals.L02_Ring
+import TestGame.Levels.Naturals.L03_Exists
+import TestGame.Levels.Naturals.L04_Forall
+import TestGame.Levels.Negation.L01_False
+import TestGame.Levels.Negation.L02_Contra
+import TestGame.Levels.Negation.L03_Contra
+import TestGame.Levels.Negation.L04_Contra
+import TestGame.Levels.Negation.L05_Not
+import TestGame.Levels.Negation.L06_ByContra
+import TestGame.Levels.Negation.L07_Contrapose
+import TestGame.Levels.Negation.L08_Contrapose
+import TestGame.Levels.Negation.L09_PushNeg

server/testgame/TestGame/HelperTools.lean

@@ -0,0 +1,11 @@
+import Lean
+
+-- show all available options
+instance : ToString Lean.OptionDecl where
+  toString a := toString a.defValue ++ ", [" ++ toString a.group ++ "]: " ++ toString a.descr
+
+def showOptions : IO Unit := do
+  let a <- Lean.getOptionDeclsArray
+  IO.println f! "{a}"
+
+#eval showOptions

server/testgame/TestGame/LemmaDocs.lean

@@ -12,3 +12,35 @@ import GameServer.Commands
 
 -- LemmaSet addition : "Addition lemmas" :=
 -- zero_add add_zero
+
+LemmaDoc not_not as not_not in "Logic"
+"`∀ (A : Prop), ¬¬A ↔ A`."
+
+
+
+
+
+LemmaDoc even as even in "Nat"
+"
+`even n` ist definiert als `∃ r, a = 2 * r`.
+Die Definition kann man mit `unfold even at *` einsetzen.
+"
+
+LemmaDoc odd as odd in "Nat"
+"
+`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
+Die Definition kann man mit `unfold odd at *` einsetzen.
+"
+
+LemmaDoc not_odd as not_odd in "Nat"
+"`¬ (odd n) ↔ even n`"
+
+LemmaDoc not_even as not_even in "Nat"
+"`¬ (even n) ↔ odd n`"
+
+LemmaDoc even_square as even_square in "Nat"
+"`∀ (n : ℕ), even n → even (n ^ 2)`"
+
+
+LemmaSet natural : "Natürliche Zahlen" :=
+even odd not_odd not_even

server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean

@@ -0,0 +1,61 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+def even (a : ℕ) : Prop := ∃ r, a = 2 * r
+def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1
+
+lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry
+
+lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry
+
+lemma even_square (n : ℕ) : even n → even (n ^ 2) := by
+  intro ⟨x, hx⟩
+  unfold even at *
+  use 2 * x ^ 2
+  rw [hx]
+  ring
+
+def prime (n : ℕ) : Prop := (2 ≤ n) ∧ ∀ a b, n = a * b → a = 1 ∨ b = 1
+
+Game "TestGame"
+World "Nat"
+Level 4
+
+Title "Für alle"
+
+Introduction
+"
+Eine Primzahl könnte man folgendermassen implementieren:
+```
+def prime (p : ℕ) : Prop := (2 ≤ p) ∧ (∀ a b, p = a * b → a = 1 ∨ b = 1)
+```
+Also, eine Zahl `p` ungleich `0` oder `1`, für die gilt wenn `a * b = p` dann ist
+entweder `a` oder `b` eins.
+
+(Tatsächlich ist eine Primzahl dann etwas genereller definiert, aber dazu mehr später.)
+
+
+
+
+"
+
+Statement
+  "Wenn `n * m` eine Primzahl ist, dann ist einer der beiden Faktoren eins."
+  (p n m : ℕ) (h : prime p) (h₂ : p = m * n) : n = 1 ∨ m = 1 := by
+  unfold prime at h
+  rcases h with ⟨l, r⟩
+  apply r
+  rw [h₂]
+  ring
+
+
+
+Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) =>
+"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
+`(x : ℕ) → `"
+
+Tactics ring intro unfold

server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean

@@ -0,0 +1,25 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Function"
+Level 1
+
+Title "Funktionen"
+
+Introduction
+"
+Funktionen werden in Lean als `(f : ℕ → ℕ)` geschrieben (`\\to`), also mit dem gleichen
+Pfeil wie Implikationen. Entsprechend kann man Implikationen und Funktionen genau
+gleich behandeln.
+
+"
+
+Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
+  let g := fun (x : ℕ) ↦ 0
+  use g
+  simp
+
+Conclusion ""
+
+Tactics use simp

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

@@ -4,6 +4,9 @@ import Mathlib.Tactic.LeftRight
 
 --set_option tactic.hygienic false
 
+--set_option autoImplicit false
+
+
 Game "TestGame"
 World "TestWorld"
 Level 15

server/testgame/TestGame/Levels/Naturals/L03_Exists.lean

@@ -4,6 +4,7 @@ import Mathlib.Tactic.Contrapose
 import Mathlib.Tactic.Use
 import Mathlib.Tactic.Ring
 
+import TestGame.ToBePorted
 
 Game "TestGame"
 World "Nat"
@@ -32,12 +33,7 @@ Hierzu gibt es 3 wichtige Taktiken:
    soll. Das macht man mit `use y`
 "
 
--- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
-def even (a : ℕ) : Prop := ∃ r, a = 2 * r
-
-def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1
-
-Statement (n : ℕ) (h : even n) : even (n ^ 2) := by
+Statement even_square (n : ℕ) (h : even n) : even (n ^ 2) := by
   unfold even at *
   rcases h with ⟨x, hx⟩
   use 2 * x ^ 2

server/testgame/TestGame/Levels/Naturals/L04_Forall.lean

@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Nat"
+Level 4
+
+Title "Für alle"
+
+Introduction
+"
+Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
+
+Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
+"
+
+Statement : ∀ (x : ℕ), (even x) → odd (1 + x) := by
+  intro x h
+  unfold even at h
+  unfold odd
+  rcases h with ⟨y, hy⟩
+  use y
+  rw [hy]
+  ring
+
+Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) =>
+"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
+`(x : ℕ) → `"
+
+Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
+praktisch gleich. Mehr dazu später."
+
+Tactics ring intro unfold

server/testgame/TestGame/Levels/Negation/L01_False.lean

@@ -6,7 +6,7 @@ Game "TestGame"
 World "Contradiction"
 Level 1
 
-Title "Widerspruch"
+Title "Widerspruch beweist alles."
 
 Introduction
 "

server/testgame/TestGame/Levels/Negation/L02_Contra.lean

@@ -2,11 +2,13 @@ import TestGame.Metadata
 import Std.Tactic.RCases
 import Mathlib.Tactic.LeftRight
 
+import TestGame.ToBePorted
+
 Game "TestGame"
 World "Contradiction"
 Level 2
 
-Title "Widerspruch"
+Title "Ad absurdum"
 
 Introduction
 "
@@ -16,14 +18,11 @@ also `(h : A)` und `(g : ¬ A)`. (`\\not`)
 
 Statement
   "Ein Widerspruch impliziert alles."
-    (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by
+    (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by
   contradiction
 
 Conclusion
 "
-Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass
-\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\".
 "
--- TODO: Oder doch ganz entfernen?
 
 Tactics contradiction

server/testgame/TestGame/Levels/Negation/L03_Contra.lean

@@ -1,31 +1,41 @@
 import TestGame.Metadata
 import Std.Tactic.RCases
 import Mathlib.Tactic.LeftRight
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
 
 Game "TestGame"
 World "Contradiction"
 Level 3
 
-Title "Widerspruch"
+Title "Ad absurdum"
 
 Introduction
 "
-Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form
-`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ`
-oder auch Annahmen der Form `A ≠ A` (`\\ne`).
+Aber, die Aussagen müssen wirklich exakte Gegenteile sein.
+
+Hier musst du zuerst eines der Lemmas `not_odd : ¬ odd n ↔ even n` oder
+`not_even : ¬ even n ↔ odd n` benützen, um einer der Terme umzuschreiben.
 "
 
 Statement
   "Ein Widerspruch impliziert alles."
-    (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
-  rw [g₁] at h
+  (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
+  rw [← not_even] at h₂
   contradiction
 
-Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A =>
-  "Recap: `rw [...] at h` hilft dir hier."
+Message (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 =>
+"Schreibe zuerst eine der Aussagen mit `rw [←not_even] at h₂` um, damit diese genaue
+Gegenteile sind."
 
-Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A =>
-  "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt
-  einen Widerspruch."
+Conclusion
+"
+Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass
+\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\".
+"
+-- TODO: Oder doch ganz entfernen?
 
 Tactics contradiction

server/testgame/TestGame/Levels/Negation/L04_Contra.lean

@@ -1,20 +1,31 @@
 import TestGame.Metadata
-import Mathlib
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
 
 Game "TestGame"
 World "Contradiction"
 Level 4
 
-Title "Widerspruch"
+Title "Ad absurdum"
 
 Introduction
 "
+Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form
+`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ`
+oder auch Annahmen der Form `A ≠ A` (`\\ne`).
 "
 
-
 Statement
-    (A : Prop) : A := by
-  by_contradiction
+  "Ein Widerspruch impliziert alles."
+    (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
+  rw [g₁] at h
+  contradiction
+
+Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A =>
+  "Recap: `rw [...] at h` hilft dir hier."
 
+Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A =>
+  "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt
+  einen Widerspruch."
 
 Tactics contradiction

server/testgame/TestGame/Levels/Negation/L05_Not.lean

@@ -5,16 +5,19 @@ Game "TestGame"
 World "Contradiction"
 Level 5
 
-Title "Widerspruch"
+Title "Nicht-nicht"
 
 Introduction
 "
+Wenn man ein Nicht (`¬`) im Goal hat, will man meistens einen Widerspruch starten,
+wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form
+`¬ (¬ A)`, in welchem Fall das Lemma `not_not` nützlich ist.
 "
 
-
 Statement
-    (A : Prop) : A := by
-  not_not
+    (A : Prop) : ¬ (¬ A) ↔ A := by
+  rw [not_not]
 
+Tactics rw
 
-Tactics contradiction
+Lemmas not_not

server/testgame/TestGame/Levels/Negation/L06_ByContra.lean

@@ -0,0 +1,48 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Contradiction"
+Level 6
+
+Title "Widerspruch"
+
+Introduction
+"
+Um einen Beweis per Widerspruch zu führen, kann man mit `by_contra h` annehmen,
+dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen.
+"
+
+Statement
+  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
+    (n : ℕ) (h : odd (n ^ 2)) : odd n := by
+  by_contra g
+  rw [not_odd] at g
+
+  suffices ¬ odd (n ^ 2) by contradiction -- TODO: I don't like this
+
+  rw [not_odd]
+  apply even_square
+  assumption
+
+Message : false =>
+"Es gibt mehrere Möglichkeiten, wie man nach einem `by_contra` weitergeht.
+
+Hier wollen wir einen Widerspruch zu `h` machen. Wir machen das mit
+`suffices ¬ odd (n ^ 2) by contradiction`, worauf man dann nur noch `¬ odd (n ^ 2)`
+zeigen muss."
+
+Hint (n : ℕ) : ¬ (odd (n ^ 2)) =>
+"Das Lemma `not_odd` ist hilfreich."
+
+Message (n: ℕ) (h : odd (n ^ 2)) (g : even n) : even (n ^ 2) =>
+"Das haben wir schon gezeigt. Mit `apply even_square` kannst du das Lemma anwenden."
+
+Tactics contradiction by_contra rw apply assumption -- TODO: suffices
+
+Lemmas odd even not_odd not_even even_square

server/testgame/TestGame/Levels/Negation/L06_PushNeg.lean

@@ -1,20 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Contradiction"
-Level 6
-
-Title "Widerspruch"
-
-Introduction
-"
-"
-
-
-Statement
-    (A : Prop) : A := by
-  pushNeg
-
-
-Tactics contradiction

server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean

@@ -0,0 +1,33 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Contradiction"
+Level 7
+
+Title "Kontraposition"
+
+Introduction
+"
+Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
+Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
+logisch equivalent sind.
+
+Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
+"
+
+Statement
+  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    (n : ℕ) : odd (n ^ 2) → odd n := by
+  contrapose
+  rw [not_odd]
+  rw [not_odd]
+  apply even_square
+
+Tactics contrapose rw apply
+Lemmas even odd not_even not_odd even_square

server/testgame/TestGame/Levels/Negation/L07_Contraposition.lean

@@ -1,23 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-
-Game "TestGame"
-World "Contradiction"
-Level 7
-
-Title "Kontraposition"
-
-Introduction
-"
-Im Gegensatz zum Widerspruch, wo
-"
-
-Statement
-  "Ein Widerspruch impliziert alles."
-    (A B : Prop) (h : ¬ B → ¬ A) (hA : A) : B := by
-  revert hA
-  contrapose
-  assumption
-
-Tactics contradiction

server/testgame/TestGame/Levels/Negation/L08_Contra.lean

@@ -1,26 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-
-Game "TestGame"
-World "Contradiction"
-Level 8
-
-Title "Kontraposition"
-
-Introduction
-"
-Im Gegensatz zum Widerspruch, wo
-"
-
--- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
-
--- Statement
---   "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
---     (n : ℕ) (h : odd n ^ 2) : odd n := by
---   byContradiction g
---   rw [not_odd] at g
---   ...
---   contradiction
-
-Tactics contradiction

server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean

@@ -0,0 +1,32 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Contradiction"
+Level 8
+
+Title "Kontraposition"
+
+Introduction
+"
+Lean Trick: Wenn das Goal nicht bereits eine Implikation ist, sondern man eine Annahme `h` hat, die
+Man gerne für die Kontraposition benützen würde, kann man mit `revert h` diese als
+Implikationsannahme ins Goal schreiben.
+"
+
+Statement
+  "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+    (n : ℕ) (h : odd (n ^ 2)): odd n := by
+  revert h
+  contrapose
+  rw [not_odd]
+  rw [not_odd]
+  apply even_square
+
+Tactics contrapose rw apply revert
+Lemmas even odd not_even not_odd even_square

server/testgame/TestGame/Levels/Negation/L09_Contraposition.lean

@@ -1,27 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-
-Game "TestGame"
-World "Contradiction"
-Level 9
-
-Title "Kontraposition"
-
-Introduction
-"
-Im Gegensatz zum Widerspruch, wo
-"
-
--- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
-
--- Statement
---   "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
---     (n : ℕ) (h : odd n ^ 2) : odd n := by
---   revert h
---   contrapose
---   rw [not_odd]
---   intro
---   trivial (?)
-
-Tactics contradiction

server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean

@@ -0,0 +1,36 @@
+import TestGame.Metadata
+import Mathlib.Tactic.PushNeg
+import Mathlib
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Contradiction"
+Level 9
+
+Title "PushNeg"
+
+Introduction
+"
+Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
+mit `push_neg` das `¬` durch den Quantor hindurchschieben.
+"
+
+Statement
+  "Es existiert keine natürliche Zahl, die grösser als alle anderen."
+  : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
+  push_neg
+  intro n
+  use 3*n + 6
+  rw [not_odd]
+  unfold even
+  use 2*n + 3
+  ring
+
+Message (n : ℕ) : (Exists fun k ↦ ¬odd (n + k)) =>
+"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutz `use ...`
+mit der richtigen Zahl."
+
+Conclusion ""
+
+Tactics push_neg intro use rw unfold ring

server/testgame/TestGame/Levels/Quantors/L01_Exists.lean

@@ -1,69 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-
-Game "TestGame"
-World "Quantors"
-Level 9
-
-Title "Kontraposition"
-
-Introduction
-"
-Häufig enthalten logische Aussagen die Quantoren \"für alle `x`\" und
-\"es existiert ein `x`, so dass\". In Lean schreibt man diese wie in der Mathe
-mit den Zeichen `∀` und `∃` (`\\forall`, `\\exists`):
-
-Beide können mehrere Variablen annehmen: `∃ (x : ℕ) (y : ℕ), x ^ 3 = 2 * y + 1` ist das selbe
-wie `∃ (x : ℕ), (∃ (y : ℕ), x ^ 3 = 2 * y + 1)`.
-
-Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
-ein `x` erhalten, dass die Aussage erfüllt.
-
-Bei einem Exists-Statement im Goal kann man mit `use` das Element angeben, dass dieses `∃ x,`
-erfüllt.
-"
-
--- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
-def even (a : ℕ) : Prop := ∃ r, a = r + r
-
-def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1
-
-Statement (n : ℕ) (h : even n) : even (n ^ 2) := by
-  unfold even at *
-  rcases h with ⟨x, hx⟩
-  use 2 * x ^ 2
-  rw [hx]
-  ring
-
--- TODO: Server PANIC because of the `even`.
---
--- Message (n : ℕ) (h : even n) : even (n ^ 2) =>
--- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
--- `unfold even at *` ersetzen.
--- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
--- genau gleich, wenn du das `unfold` rauslöscht."
-
-Message (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
-"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
-ein `x` erhalten, dass die Aussage erfüllt."
-
-Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
-"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
-die Aussage erfüllen soll."
-
-Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r =>
-"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
-die Aussage erfüllen soll."
-
-Message (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
-"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu
-`x + x` umschreiben..."
-
-Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
-"Die Taktik `ring` löst solche Gleichungen."
-
-Tactics unfold rcases use rw ring

server/testgame/TestGame/Levels/Quantors/L02_Forall.lean

@@ -1,39 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-
-Game "TestGame"
-World "Quantors"
-Level 9
-
-Title "Kontraposition"
-
-Introduction
-"
-Bei einem `∀ x,` im Goal kann man mit `intro x` annehmen, dass man ein solches `x` hat.
-
-Ein `(h : ∀ x, _)` in den Annahmen kann ....
-"
-
--- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
-def even (a : ℕ) : Prop := ∃ r, a = r + r
-def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1
-
-Statement : ∀ (x : ℕ), even x → even (x + 2) := by
-  intro x h
-  unfold even at *
-  rcases h with ⟨y, hy⟩
-  use y + 1
-  rw [hy]
-  ring
-
--- Message (n : ℕ) (h : even n) : even (n ^ 2) =>
--- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
--- `unfold even at *` ersetzen.
--- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
--- genau gleich, wenn du das `unfold` rauslöscht."
-
-Tactics unfold rcases use rw ring intro

server/testgame/TestGame/Levels/Quantors/TMP.lean

@@ -1,22 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-
-Game "TestGame"
-World "Contradiction"
-Level 3
-
-Title "Widerspruch"
-
-Introduction
-"
-Ähnlich siehts aus, wenn man Annahmen hat, die direkte Negierung voneinander sind,
-also `(h : A)` und `(g : ¬ A)`.
-"
-
-Statement
-  "Ein Widerspruch impliziert alles."
-    (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by
-  contradiction
-
-Tactics contradiction

server/testgame/TestGame/TacticDocs.lean

@@ -117,6 +117,13 @@ TacticDoc right
 TODO
 "
 
+TacticDoc simp
+"
+## Beschreibung
+
+TODO
+"
+
 TacticDoc contradiction
 "
 ## Beschreibung
@@ -124,6 +131,36 @@ TacticDoc contradiction
 TODO
 "
 
+TacticDoc push_neg
+"
+## Beschreibung
+
+TODO
+"
+
+
+TacticDoc contrapose
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc revert
+"
+## Beschreibung
+
+TODO
+"
+
+
+TacticDoc by_contra
+"
+## Beschreibung
+
+TODO
+"
+
 TacticDoc ring
 "
 ## Beschreibung

server/testgame/TestGame/ToBePorted.lean

@@ -0,0 +1,16 @@
+import Mathlib
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+def even (a : ℕ) : Prop := ∃ r, a = 2 * r
+def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1
+
+lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry
+
+lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry
+
+lemma even_square (n : ℕ) : even n → even (n ^ 2) := by
+  intro ⟨x, hx⟩
+  unfold even at *
+  use 2 * x ^ 2
+  rw [hx]
+  ring

server/testgame/lakefile.lean

@@ -6,10 +6,12 @@ require GameServer from ".."/"leanserver"
 require mathlib from git
   "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350"
 
-set_option tactic.hygienic false
-set_option autoImplicit false
+--set_option tactic.hygienic false
+--set_option autoImplicit false
 
 package TestGame
 
 @[default_target]
-lean_lib TestGame
+lean_lib TestGame {
+  moreLeanArgs := #["-DautoImplicit=false"]
+}