Merge branch 'main' of https://github.com/hhu-adam/Robo into main

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

@@ -2,12 +2,13 @@ import Game.Levels.Luna.L01_LE
 import Game.Levels.Luna.L02_Pos
 import Game.Levels.Luna.L03_Linarith
 import Game.Levels.Luna.L04_Linarith
+import Game.Levels.Luna.L05_Trichotomy
 
 /-!
 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/Luna/L05_Trichotomy.lean

@@ -0,0 +1,35 @@
+import Game.Metadata
+
+World "Luna"
+Level 5
+
+Title "Trichotomie"
+
+Introduction
+"
+"
+
+Statement {A : Prop} (x y : ℤ) (h₁ : x ≤ y → A) (h₂ : y < x → A) : A := by
+  Hint (strict := true) "
+    **Robo**: Ein sehr nützliches Resultat ist `lt_trichotomy {x} {y}`:
+
+    ${x} < {y}$ oder ${x} = {y}$ oder ${x} > {y}$
+
+    Typischerweise kann man dieses wie folgt verwenden:
+
+    ```
+    obtain h | h | h := lt_trichotomy x y
+    ```
+  "
+  obtain h | h | h := lt_trichotomy x y
+  · Hint "**Robo**: Beachte, dass du jetzt 3 Goals hast, eines pro Fall!"
+    apply h₁
+    linarith
+  · apply h₁
+    linarith
+  · apply h₂
+    assumption
+
+Conclusion ""
+
+NewTheorem lt_trichotomy

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.lean

@@ -2,7 +2,7 @@ import Game.Levels.Quantus.L01_Ring
 import Game.Levels.Quantus.L02_Rewrite
 import Game.Levels.Quantus.L03_Rewrite
 import Game.Levels.Quantus.L04_Ring
-import Game.Levels.Quantus.L05_Rfl
+import Game.Levels.Quantus.L05_Decide
 import Game.Levels.Quantus.L06_Exists
 import Game.Levels.Quantus.L07_Exists
 import Game.Levels.Quantus.L08_Forall
@@ -53,6 +53,6 @@ wir es ja insbesondere der Königin übergeben.
 Robo spuckt es aus, wirft es in die Menge, und die Formalosophinnen reißen es auf. Darin befinden
 sich ein paar lose Seiten, die sie sofort eingehend studieren.
 
-Zwei Minuten später liegen die Seiten wieder bei Euch. Es sind wieder mathematische Probleme.
+Zwei Minuten später liegen die Seiten wieder bei euch. Es sind wieder mathematische Probleme.
 Und die Formalosophinnen wollen sehen, wie Ihr sie löst.
 "

Game/Levels/Quantus/L05_Decide.lean

@@ -0,0 +1,47 @@
+import Game.Metadata
+
+
+World "Quantus"
+Level 5
+
+Title ""
+
+Introduction
+"
+Ihr habt nun alle Fragen aus dem königlichen Päckchen beantwortet, und die Formalosophinnen
+applaudieren. Dann wollen Sie aber auch noch ein paar Fragen stellen, aber sie können sich
+nicht einigen, welche.
+Ihr hört abwechselnd die Rufe „Even“ und „Odd“ aus der Menge heraus. Deshalb zeigt dir Robo
+vorsichtshalber schon einmal die entsprechende Definition:
+
+```
+def Even (n : ℕ) : Prop := ∃ r, n = r + r
+```
+
+Bevor er zu `Odd` weitergehen kann,
+taucht von irgendwo aus der Menge folgendes Papier auf:
+"
+
+Statement : Even 42 := by
+  Hint "
+    **Robo**: Moment! Dafür brauchst du die Definition gar nicht!
+
+    **Du**: Das ist ja irgendwie trivial…
+
+    **Robo**: Erinnerst du dich? `decide` kann alle Aufgaben lösen, bei denen es einen
+    einfachen Algorithmus gibt um die Wahrheit zu bestimmen.
+    Aussagen zu konkreten Zahlen fallen meistens in diese Kategorie!
+  "
+  decide
+
+Conclusion
+"
+**Du**: Was kann denn `decide` noch alles?
+
+**Robo**: Konkret hat hier jemand einen ausführbaren
+Algorithmus angegeben, wie entschieden werden
+soll, ob `Even 42` wahr oder falsch ist. Wenn `decide` also so einen Algorithmus kennt,
+dann kann es die Aufgabe lösen.
+"
+
+OnlyTactic decide

Game/Levels/Quantus/L06_Exists.lean

@@ -7,11 +7,8 @@ Title "Gerade/Ungerade"
 
 Introduction
 "
-Ihr habt nun alle Fragen aus dem königlichen Päckchen beantwortet, und die Formalosophinnen
-applaudieren. Dann wollen Sie aber auch noch ein paar Fragen stellen, aber sie können sich
-nicht einigen, welche.
-Ihr hört abwechselnd die Rufe „Even“ und „Odd“ aus der Menge heraus. Deshalb zeigt dir Robo
-vorsichtshalber schon einmal die entsprechenden Definitionen an:
+Die Rufe „Even“ und „Odd“ aus der Menge sind noch lange nicht verstummt, deshalb
+zeigt dir Robo nochmals die Definitionen:
 
 ```
 def Even (n : ℕ) : Prop := ∃ r, n = r + r
@@ -23,7 +20,7 @@ und
 def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
 ```
 
-Schließlich taucht von irgendwo aus der Menge folgendes Papier auf:
+Damit erhaltet ihr auch ein weiteres Blatt:
 "
 
 open Nat
@@ -36,7 +33,12 @@ Statement Nat.even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
     **Robo**: Wie du oben siehst, ist `Even {n}` dadurch definiert,
     dass ein `r` existiert so dass `r + r = {n}` ist. Am besten
     öffnest du diese Definition mit `unfold Even at *` einmal.
-    Dann siehst du besser, was los ist."
+    Dann siehst du besser, was los ist.
+
+    **Du**: Was ist mit `decide`?
+
+    **Robo**: `decide` wird nicht funktionieren, da `{n}` keine konkrete sondern
+    eine beliebige Zahl ist. Da musst du schon etwas Arbeit leisten!"
   Branch
     unfold Even
     Hint "
@@ -58,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