levels

server/adam/Adam.lean

@@ -8,7 +8,7 @@ import Adam.Levels.Contradiction
 import Adam.Levels.Sum
 -- import Adam.Levels.Induction
 
-import Adam.Levels.Numbers
+--import Adam.Levels.Numbers
 import Adam.Levels.Inequality
 
 import Adam.Levels.Lean
@@ -32,7 +32,7 @@ ziemlich gleich wie wenn du später Lean im VSCode benützt.
 Rechts siehst du eine Übersicht der Welt dieses Spiels. Jeder Planet hat mehrere Levels,
 die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden dann grün.
 
-Klicke auf die erste Welt \"Aussagenlogik 1\" um deine Reise zu starten.
+Klicke auf die erste Welt \"Logo\" um deine Reise zu starten.
 
 ### Spielstand
 
@@ -71,7 +71,7 @@ Path Lean → SetTheory → SetTheory2 → SetFunction → Module
 Path Lean → Function → SetFunction
 
 
-Path SetTheory2 → Numbers
+-- Path SetTheory2 → Numbers
 Path Module → Basis → Module2
 
 MakeGame

server/adam/Adam/LemmaDocs.lean

@@ -1,7 +1,7 @@
 import GameServer.Commands
 
 -- Wird im Level "Implication 11" ohne Beweis angenommen.
-LemmaDoc not_not as "not_not" in "Logic"
+LemmaDoc Classical.not_not as "not_not" in "Logic"
 "
 `not_not {A : Prop} : ¬¬A ↔ A`
 

server/adam/Adam/Levels/Implication/L01_Intro.lean

@@ -27,7 +27,7 @@ Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
   **Robo** *(leise zurück)*:  So wie der aussieht, fürchte ich, das wird er auch nicht verstehen.
     Schreib den Beweis lieber aus.
 
-  *Du**: Aber wie denn?  Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …'
+  **Du**: Aber wie denn?  Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …'
 
   **Robo**: Ja, gute Idee.  Wähle dazu für Deine Annahme einfach einen Namen, zum Beispiel `h`, und schreib `intro h`."
   intro hA

server/adam/Adam/Levels/Implication/L07_Rw.lean

@@ -24,7 +24,7 @@ Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) :
   rw [h₁]
   Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
 
-  **Robo**: Dann schreibst du ein `←` vor den Namen, also `rw [← hₓ]`."
+  **Robo**: Dann schreibst du ein `←` (`\\l`, also klein \"L\") vor den Namen, also `rw [← hₓ]`."
   Branch
     rw [← h₃]
     Hint "**Du**: Ehm, das war verkehrt.

server/adam/Adam/Levels/Implication/L12_Rw.lean

@@ -39,5 +39,5 @@ Conclusion
 "
 
 DisabledTactic tauto apply
-NewLemma not_not
+NewLemma Classical.not_not
 LemmaTab "Logic"

server/adam/Adam/Levels/Predicate/L01_Ring.lean

@@ -10,7 +10,7 @@ Level 1
 Title "Natürliche Zahlen"
 
 Introduction
-""
+"Du schaust Dir die erste Seite an."
 
 Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
   Hint "**Du**: Das ist doch Schulmathematik! Man rechnet das einfach aus,

server/adam/Adam/Levels/Predicate/L02_Rewrite.lean

@@ -29,5 +29,3 @@ Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c :
 
 Conclusion
 ""
-
-NewTactic assumption rw

server/adam/Adam/Levels/Predicate/L03_Rewrite.lean

@@ -16,7 +16,7 @@ $$
 \\begin{aligned}
   a &= b \\\\
   a + a ^ 2 &= b + 1 \\\\
-  \\vdash b + b ^ 2 = b + 1
+  \\vdash b + b ^ 2 &= b + 1
 \\end{aligned}
 $$
 "
@@ -29,5 +29,5 @@ $$
   assumption
 
 Conclusion "
-**Robo**: Noch ein Trick: Mit `rw [{h}] at *` kann man gleichzeitig mittels `{h}` **alle** Annahmen und das Goal umschreiben.
+**Robo**: Noch ein Trick: Mit `rw [h] at *` kann man gleichzeitig mittels `h` **alle** Annahmen und das Goal umschreiben.
 "

server/adam/Adam/Levels/Predicate/L05_Rfl.lean

@@ -1,4 +1,5 @@
 import Adam.Metadata
+import Mathlib.Tactic.Ring
 
 Game "Adam"
 World "Predicate"

server/adam/Adam/Levels/Predicate/L06_Exists.lean

@@ -33,14 +33,13 @@ Schließlich taucht von irgendwo aus der Menge folgendes Papier auf:
 "
 
 Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
-  Hint "**Robo**: Du kannst Dir mit `unfold Even` auch hier auf dem Papier die Definition sehen."
+  Hint "**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."
   Branch
     unfold Even
     Hint "Robo**: Am besten machst Du auch noch `unfold Even at h`, damit Du verstehst, was los ist."
-  Hint "**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. "
   unfold Even at *
   Hint "**Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = n` …
 
@@ -56,6 +55,7 @@ Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
     rw [hr]
     Hint "**Robo**: Das geht auch, jetzt musst Du aber wirklich `use` verwenden."
     use 2 * r ^ 2
+    Hint (hidden := true) "**Du**: Ah, und jetzt `ring`!"
     ring
   use 2 * r ^ 2
   Hint "**Du**: Ah, und jetzt `ring`!

server/adam/Adam/Levels/Predicate/L07_Exists.lean

@@ -20,23 +20,52 @@ Sofort taucht das nächste Blatt auf.  Anscheinend hatten sie sich auf einen Kom
 "
 
 Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by
-  unfold Odd at *
+  Hint (hidden := true) "**Robo**: mit `rcases h with ⟨r, hr⟩` kannst du wieder
+  das `r` nehmen, das laut Annahme existieren muss.
+
+  **Robo**: Oder aber, du fängst mit `unfold Odd at *` an."
+  Branch
+    unfold Odd
+    Hint "**Robo**: Mit `unfold Odd at *` öffnest du alle Definitionen von `Odd`."
+    unfold Odd at *
+  Branch
+    unfold Odd at *
+    Hint (hidden := true) "**Robo**: mit `rcases h with ⟨r, hr⟩` kannst du wieder
+    das `r` nehmen, das laut Annahme existieren muss."
+    rcases h with ⟨r, hr⟩
+    Hint "**Robo**: Ich hab noch einen Trick auf Lager:
+    Wenn du jetzt noch nicht weißt, welche Zahl Du einsetzen musst, könntest
+    Du schon jetzt mit `rw [{hr}]` weitermachen …"
+    Branch
+      rw [hr]
+      Hint "**Robo**: Wenn Du jetzt `ring` brauchst, dann schreibt es einfach alles in
+      Normalform um, das hilft beim Vergleichen."
+      ring
+      Hint "**Du**: Was bedeutet `ring_nf`?
+
+      **Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
+      schreiben, aber die funktionieren praktisch gleich."
+    use 2 * (r + r ^ 2)
+    ring
   rcases h with ⟨r, hr⟩
   Hint "**Robo**: Ich hab noch einen Trick auf Lager:
-  Wenn du jetzt herausfinden willst, welche Zahl Du einsetzen musst, könntest
-  Du schon jetzt mit `rw [{hr}]` weitermachen …"
-  rw [hr]
-  Hint "**Robo**: Wenn Du jetzt `ring` benötigst, dann schreibt es einfach alles in
-  Normalform um, das hilft beim Vergleichen."
-  ring
-  Hint "**Du**: Was bedeutet `ring_nf`?
+    Wenn du jetzt noch nicht weißt, welche Zahl Du einsetzen musst, könntest
+    Du schon jetzt mit `rw [{hr}]` weitermachen…"
+  Branch
+    rw [hr]
+    Hint "**Robo**: Wenn Du jetzt `ring` brauchst, dann schreibt es einfach alles in
+    Normalform um, das hilft beim Vergleichen."
+    ring
+    Hint "**Du**: Was bedeutet `ring_nf`?
 
-  **Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
-  schreiben, aber die funktionieren praktisch gleich."
+    **Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
+    schreiben, aber die funktionieren praktisch gleich."
   use 2 * (r + r ^ 2)
+  rw [hr]
   ring
-
 -- TODO: Allow `ring_nf` as part of `ring`.
 
 Conclusion "Applaus!"
 
+-- TODO: THis level would be a good example where a `Hint (defeq := true)` would be desirable
+-- in order to reduce the number of hints that are duplicated.

server/adam/Adam/Levels/Predicate/L08_Forall.lean

@@ -7,6 +7,8 @@ import Mathlib.Tactic.Ring
 import Mathlib.Algebra.Parity
 import Mathlib
 
+set_option tactic.hygienic false
+
 Game "Adam"
 World "Predicate"
 Level 8

server/adam/Adam/Levels/Predicate/L09_PushNeg.lean

@@ -68,10 +68,14 @@ Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
   use n
   Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
   rw [←even_iff_not_odd]
+  -- TODO: if I write `tauto` here, I get a weird error
   unfold Even
   use n
   --ring
 
+NewTactic push_neg
+NewLemma Nat.even_iff_not_odd Nat.odd_iff_not_even not_exists not_forall
+
 Conclusion "Die Formalosophinnen sind ganz begeistert.
 Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
 
@@ -83,7 +87,9 @@ Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
 
 Die Frage war wieder zu konkret.  Betretenes Schweigen.
 
-**Robo**:  Lass nur.  Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da drüben.  Und bevor Du fragst – hier ist wieder ein Überblick, was Du auf diesem Planeten gelernt hast.
+**Robo**:  Lass nur.  Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da
+drüben.  Und bevor Du fragst – hier ist wieder ein Überblick, was Du auf diesem Planeten
+gelernt hast.
 
 |               | Beschreibung                |
 |:--------------|:----------------------------|
@@ -104,6 +110,3 @@ Die Frage war wieder zu konkret.  Betretenes Schweigen.
 | 16    | `push_neg`                | Für `¬∃` und `¬∀` im Goal.                             |
 
 "
-
-NewTactic push_neg
-NewLemma Nat.even_iff_not_odd Nat.odd_iff_not_even not_exists not_forall