cleanup Quantus; introduce decide

Game.lean

@@ -13,6 +13,8 @@ import Game.Levels.Robotswana
 
 import Game.Levels.End
 
+import Game.Levels.NewStuff.Prime
+
 import Game.Levels.FunctionSurj
 import Game.Levels.FunctionInj
 import Game.Levels.FunctionBij
@@ -95,10 +97,16 @@ CoverImage "images/Cover.png"
 Dependency Robotswana → End
 Dependency Cantor → End
 
+-- Dependency Babylon → FunctionSurj
+
+
+-- because of `∃!`
+Dependency Prime → FunctionInj
+-- Because of def `Injective`
+Dependency FunctionInj → FunctionBij
+
 
--- Dependency Sum → FunctionSurj
--- Dependency FunctionInj → FunctionBij -- Because of def `Injective`
--- set_option lean4game.showDependencyReasons true
+set_option lean4game.showDependencyReasons true
 
 /-! Build the game. Show's warnings if it found a problem with your game.
 

Game/Doc/Tactic.lean

@@ -780,7 +780,28 @@ Die Taktik `trans B` erstellt dann aus dem Goal zwei neue `A ↔ B` und `B ↔ C
 TacticDoc trans
 
 /--
-TODO
+`decide` kann Aussagen beweisen, für die es einen einfachen Algorithmus
+gibt, der die Wahr- oder Falschheit der Aussage bestimmt.
+
+Wichtige Beispiele sind:
+
+* `True`
+* Aussagen zu konkreten Zahlen, wie `Even 4`, `2 ≤ 5`, `4 ≠ 6`, …
+
+
+## Details
+
+Konkret sucht `decide` für eine Aussage `P`  nach einer Instanz `Decidable P`
+welche dann evaluiert entweder wahr oder falsch rausgibt.
+
+## Beispiel
+
+Folgendes kann mit `decide` gelöst werden:
+
+```
+Goal:
+  ¬ Odd 40
+```
 -/
 TacticDoc decide
 

Game/Levels/FunctionBij/L03_Equivalence.lean

@@ -37,5 +37,5 @@ Statement finThreeArrowEquiv {A : Type} : (Fin 3 → A) ≃ A × A × A := by
   · intro t
     simp
 
-NewTactic fconstructor exact fin_cases
+NewTactic fin_cases
 -- TODO: fin_cases should be in set-theory

Game/Levels/Luna.lean

@@ -7,7 +7,7 @@ import Game.Levels.Luna.L04_Linarith
 The planet Luna is about inequalities `≤` and the tactic `linarith`.
 -/
 
-World "Inequality"
+World "Luna"
 Title "Luna"
 
 Image "images/MoonLuna.png"

Game/Levels/Luna/L01_LE.lean

@@ -1,6 +1,6 @@
 import Game.Metadata
 
-World "Inequality"
+World "Luna"
 Level 1
 
 Title "Kleinergleich"

Game/Levels/Luna/L02_Pos.lean

@@ -3,7 +3,7 @@ import Game.Metadata
 
 open Nat
 
-World "Inequality"
+World "Luna"
 Level 2
 
 Title "Kleinergleich"

Game/Levels/Luna/L03_Linarith.lean

@@ -1,7 +1,7 @@
 import Game.Metadata
 
 
-World "Inequality"
+World "Luna"
 Level 3
 
 Title "Linarith"

Game/Levels/Luna/L04_Linarith.lean

@@ -1,6 +1,6 @@
 import Game.Metadata
 
-World "Inequality"
+World "Luna"
 Level 4
 
 Title "Linarith"

Game/Levels/NewStuff/Prime.lean

@@ -12,7 +12,7 @@ The planet `Prime` is about prime numbers and divisibility.
 -/
 
 World "Prime"
-Title "[WIP] Primzahlen"
+Title "Primzahlen"
 
 Introduction "Ihr schlendert durch die Befestigung ohne direktes Ziel. Und sprecht mit
 verschiedenen Einwohnern."

Game/Levels/NewStuff/Prime/L04_ExistsUnique.lean

@@ -20,8 +20,11 @@ Statement : ∃! p, Nat.Prime p ∧ Even p := by
   use 2
   dsimp
   constructor
-  simp
-  exact Nat.prime_two
+  · decide
+  -- simp
+  -- exact Nat.prime_two
   rintro y ⟨hy, hy'⟩
   rw [←Nat.Prime.even_iff hy]
   assumption
+
+NewDefinition ExistsUnique

Game/Levels/NewStuff/Prime/L07_InfinitudePrimes.lean

@@ -19,9 +19,7 @@ open Nat
 Statement Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by
   -- based on project by Maren
   Hint "**Du**: `minFac (n ! + 1)` ist der kleinste Primfaktor von $n! + 1$"
-
-  let q := minFac (n ! + 1)
-  use q
+  use minFac (n ! + 1)
   constructor
   · apply le_minFac_factorial_succ n
   · apply minFac_factorial_succ_prime n

Game/Levels/Quantus/L06_Exists.lean

@@ -60,30 +60,30 @@ Statement Nat.even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
     was ausgerechnet `1 = 1 / 2 + 1 / 2 = 0 + 0` ist, du bist also auf dem Holzweg!
     "
   Hint "
-    **Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = {n}` …
+    **Du**: Also von `{h}` weiß ich jetzt, dass ein `s` existiert, so dass `s + s = {n}` …
 
-    **Robo**: Mit `obtain ⟨r, hr⟩ := {h}` kannst du dieses `r` tatsächlich einführen."
-  obtain ⟨r, hr⟩ := h
+    **Robo**: Mit `obtain ⟨s, hs⟩ := {h}` kannst du dieses `s` tatsächlich einführen."
+  obtain ⟨s, hs⟩ := h
   Hint "
     **Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = {n} ^ 2`?
 
     **Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
   Hint (hidden := true) "
-    **Robo**: Also sowas ähnliches wie `use 4 * {r} ^ 3`, aber ich kann
+    **Robo**: Also sowas ähnliches wie `use 4 * {s} ^ 3`, aber ich kann
     dir leider nicht sagen, welche Zahl passt."
   Branch
-    rw [hr]
+    rw [hs]
     Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
-    use 2 * r ^ 2
+    use 2 * s ^ 2
     Hint (hidden := true) "**Du**: Ah, und jetzt `ring`!"
     ring
-  use 2 * r ^ 2
+  use 2 * s ^ 2
   Hint "
     **Du**: Ah, und jetzt `ring`!
 
     **Robo**: Aber zuerst musst du noch mit
-    `rw` `n` durch `{r} + {r}` ersetzen, da `ring` das sonst nicht weiß."
-  rw [hr]
+    `rw` `n` durch `{s} + {s}` ersetzen, da `ring` das sonst nicht weiß."
+  rw [hs]
   ring
 
 NewTactic unfold use

Game/Levels/Quantus/L09_PushNeg.lean

@@ -16,7 +16,7 @@ open Function
 Statement {X : Type} (P : X → Prop) :
     ¬ (∃ x : X, P x) ↔ ∀ x : X, ¬ P x := by
   Hint "
-    **Du**: Was ist denn jetzt dieses P?
+    **Du**: Was ist denn jetzt dieses `{P}`?
 
     **Robo**: `{P}` ist wieder irgendeine Aussage; eine Aussage über Objekte vom Typ `{X}`.
               Zum Beispiel könnte `{X}` wieder der Typ der natürlichen Zahlen sein.
@@ -34,28 +34,28 @@ Statement {X : Type} (P : X → Prop) :
 
     **Robo**: Genau. Was du brauchst, ist `push_neg`."
   Branch
+    constructor
+    intro h
+    Hint (hidden := true) "
+      **Robo**: `push_neg` schiebt von links nach rechts. Du kannst es hier also nicht auf
+      das Beweisziel anwenden, wohl aber auf `{h}`."
+    push_neg at h
+    assumption
+    intro h
     push_neg
-    Hint (hidden := true) "**Robo**: Das ist jetzt eine Tautologie, oder?"
-    tauto
-  constructor
-  intro h
-  Hint (hidden := true) "
-    **Robo**: `push_neg` schiebt von links nach rechts. Du kannst es hier also nicht auf
-    das Beweisziel anwenden, wohl aber auf `{h}`."
-  push_neg at h
-  assumption
-  intro h
+    assumption
   push_neg
-  assumption
+  rfl
 
 NewTactic push_neg
+DisabledTactic tauto
 
 Conclusion
 "
-**Robo**: Gut gemacht. Intern benutzt `push_neg` übringens zwei Lemmas:
+**Robo**: Gut gemacht. Intern benutzt `push_neg` übrigens zwei Lemmas:
 
- - `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
- - `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
+ - `not_exists (P : X → Prop) : ¬ (∃ x, P x) ↔ ∀ x, (¬ P x)`
+ - `not_forall (P : X → Prop) : ¬ (∀ x, P x) ↔ ∃ x, (¬ P x)`
 
 Das erste Lemma ist die Aussage, die du gerade gezeigt hast.
 

Game/Levels/Quantus/L11_DrinkersParadox.lean

@@ -7,7 +7,7 @@ Title "Drinker's Paradox"
 
 Introduction
 "
-**Du**: Könnte ihr eigentlich immer nur im Chor oder durcheinander reden?
+**Du**: Könnt ihr eigentlich immer nur im Chor oder durcheinander reden?
 
 Wieder herrscht längeres Schweigen. Dann auf einmal:
 
@@ -33,40 +33,40 @@ open Function
 Statement {People : Type} [h_nonempty : Nonempty People] (isDrinking : People → Prop) :
     ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by
   Hint "
-    **Du**: Also, `isDrinking` ist wieder so ein Prädikat …
-    Wenn `p` eine Person ist, ist `isDrinking p` eine Aussage,
+    **Du**: Also, `{isDrinking}` ist wieder so ein Prädikat …
+    Wenn `p` eine Person ist, ist `{isDrinking} p` eine Aussage,
     die wahr oder falsch ist. Soweit so gut.
-    Und was bedeutet `Nonempty People`?
+    Und was bedeutet `Nonempty {People}`?
 
     **Robo**: Das ist Leansch für nicht-leer. Das heißt einfach, es gibt mindestens eine Person.
-    Mit `use Classical.arbitrary People` kannst du dir eine `pers : Person` aussuchen und verwenden,
+    Mit `use Classical.arbitrary {People}` kannst du dir eine `pers : {People}` aussuchen und verwenden,
     die es per Annahme gibt.
 
     **Du**: Und wie fang ich jetzt an?
 
     **Robo**: Ich sagte doch, schau am besten Mal in deine Handbibliothek.
     Wenn ich mich richtige erinnere, hilft eine Fallunterscheidung, ob die Aussage
-    `∀ (y : People), isDrinking y` wahr oder falsch ist."
+    `∀ (y : {People}), {isDrinking} y` wahr oder falsch ist."
   Hint (hidden := true) "**Robo**: Schau mal `by_cases` an."
   by_cases h : ∀ y, isDrinking y
-  Hint (hidden := true) "
-    **Du**: Und wen nehm ich jetzt?
-
-    **Robo**: Wie gesagt, mit `use Classical.arbitrary People` kannst du eine beliebige
-    Person auswählen und verwenden."
-  use Classical.arbitrary People
-  intro
-  assumption
-  Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen."
-  push_neg at h
-  Hint (hidden := true) "**Du**: Also nach `{h}` existiert ja eine Person, die nicht trinkt. Könnte ich diese brauchen damit die Aussage trivialerweise wahr wird?
-
-  **Robo**: Schau dir mal an wie man `obtain` auf die Annahme `{h}` anwenden könnte."
-  obtain ⟨p, hp⟩ := h
-  use p
-  intro hp'
-  Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?"
-  contradiction
+  · Hint (hidden := true) "
+      **Du**: Und wen nehm ich jetzt?
+
+      **Robo**: Wie gesagt, mit `use Classical.arbitrary {People}` kannst du eine beliebige
+      Person auswählen und verwenden."
+    use Classical.arbitrary People
+    intro
+    assumption
+  · Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen."
+    push_neg at h
+    Hint (hidden := true) "**Du**: Also nach `{h}` existiert ja eine Person, die nicht trinkt. Könnte ich diese brauchen damit die Aussage trivialerweise wahr wird?
+
+    **Robo**: Schau dir mal an wie man `obtain` auf die Annahme `{h}` anwenden könnte."
+    obtain ⟨p, hp⟩ := h
+    use p
+    intro hp'
+    Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?"
+    contradiction
 
 /-- TODO -/
 TheoremDoc Classical.arbitrary as "Classical.arbitrary" in "Logic"
@@ -93,6 +93,7 @@ Conclusion
 |:------|:--------------------------|:-------------------------------------------------------|
 | *13ᶜ* | `rw`                      | Umschreiben mit Gleichungen.                           |
 | 15    | `ring`                    | Löst Gleichungen mit `+, -, *, ^`.                     |
+| *4ᵇ*  | `decide`                  | Kann auch Aussagen zu konkreten Zahlen beantworten.    |
 | 16    | `unfold`                  | Setzt visuell die Bedeutung einer Definition ein.      |
 | 17    | `use`                     | Um ein `∃` im Goal anzugehen.                          |
 | *7ᵈ*  | `obtain ⟨x, hx⟩ := h`     | Um ein `∃` in den Annahmen zu zerlegen.                |

development-status.md

@@ -1,9 +1,9 @@
 
 | Planet                 | new name | levels         | tried? | hints  | story  | summary | picture | desirable changes                                                                                     |
 |:-----------------------|:---------|:---------------|:-------|:-------|:-------|:--------|:--------|:------------------------------------------------------------------------------------------------------|
-| Logos                  | ==       | +++            | +++    | +++    | +++    | +       | +++     | JE: DONE TODO: TacticDoc `decide`.                                                                                            |
+| Logos                  | ==       | +++            | +++    | +++    | +++    | +       | +++     | JE: DONE                                                                                              |
 | Implis                 | ==       | +++            | +++    | +++    | ++     | +       | +++     | JE: DONE                                                                                              |
-| Quantus                | ==       | +++            | +++    | +++    | +++    | +       | +++     | (add ∃! ? -- see Prime planet);  TODO: replace L05 by `decide`  (eg: prove that 5 is odd or 8 is even)                            |
+| Quantus                | ==       | +++            | +++    | +++    | +++    | +       | +++     | JE: DONE                                                                                              |
 | Spinoza                | ==       | ++             | ++     | ++     | ++     |         | +++     | TODO: add TFAE tactics (used in boss of FunctionSurj)                                                 |
 | Luna                   | ==       | +              | +++    | +++    | +++    |         | +++     | TODO: level explaining `obtain h_lt \| h_eq \| h_gt := lt_trichotomy a b` (needed in FunctionInj L04) |
 | Babylon                | ==       | +              | +++    | +++    | +++    |         | +++     | TODO: add sum over zeroes, adding over singleton                                                      |
@@ -17,7 +17,7 @@
 | ~FiniteSetTheory       | TODO     | TODO           |        |        |        |         | TODO    |                                                                                                       |
 | SymmSquare             | TODO     | o TODO: L08    | TODO   | TODO   | TODO   |         | TODO    |                                                                                                       |
 | Quotient               | TODO     | 7-?            | TODO   |        | TODO   |         | TODO    |                                                                                                       |
-| Prime                  | TODO     | +              | TODO   | TODO   | TODO   |         | TODO    | TODO: introduce ∃!                                                                      |
+| Prime                  | TODO     | +              | TODO   | TODO   | TODO   |         | TODO    | TODO: introduce ∃!                                                                                    |
 | ? RealUncountable      | TODO     | TODO .         |        |        |        |         |         |                                                                                                       |
 | GoodByePlanet          |          | TODO (.)       |        |        |        |         | +++     | JE: added empty `End` planet                                                                          |
 |                        |          |                |        |        |        |         |         |                                                                                                       |
@@ -64,7 +64,7 @@ Trick `obtain h_lt | h_eq | h_gt := lt_trichotomy a b` needs to be explained on
 
 #### L05: use the fact that StrictMono is injective
 Perhaps swap L04 and L05 (L05 is the easier level, and motivates L04)
-    
+
 Both L04 and L05 could be move closer to levels about ‘existence of left inverse implies injectivity`.
 
 #### L06: succ has left inverse, using if … then … else