story

server/testgame/TestGame/Levels/Implication.lean

@@ -26,5 +26,8 @@ aber niemand von den Einwohnern wusste was davon...
 **Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
 erzählen…
 
-Und damit leitet Robo den Landeanflug ein.
+Und damit leitet Robo den Landeanflug ein. Implis scheint ein riesiger Tagbau zu sein auf
+dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und queer.
+
+Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
 "

server/testgame/TestGame/Levels/Implication/L01_Intro.lean

@@ -1,4 +1,5 @@
 import TestGame.Metadata
+import Mathlib.Tactic.Tauto
 
 set_option tactic.hygienic false
 
@@ -10,31 +11,27 @@ Title "Intro"
 
 Introduction
 "
-## Implikationen
-
-In diesem Kapitel lernst du Implikation ($\\Rightarrow$) und Genau-dann-wenn
-($\\Leftrightarrow$) kennen.
-Dazu lernst du, wie man bereits bewiesene Sätze verwendet.
-
-Seien `(A B : Prop)` zwei logische Aussagen. Eine Implikation $A \\Rightarrow B$ schreibt
-man in Lean als `A → B` (`\\to`).
-
-Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit
-`intro ha` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen.
+**Operationsleiter**: Sagt mal, könnt ihr mir hier weiterhelfen?
 "
 
-Statement
-    "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr."
-    (A B : Prop) (hb : B) : A → (A ∧ B) := by
+Statement "" (A B : Prop) (hb : B) : A → (A ∧ B) := by
   intro hA
   constructor
   assumption
   assumption
 
-HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
-"Mit `intro ha` kann man annehmen, dass $A$ wahr ist. danach muss man $A \\land B$ zeigen."
+NewTactic intro
+DisabledTactic tauto
+
+Hint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
+"**Du**: Einen Moment, das ist eine Implikation (`\\to`),
+also `A` impliziert `A und B`, soweit so gut, also eine Tautologie.
+
+**Robo**: Die scheinen hier `tauto` auch nicht zu verstehen.
+Implikationen kannst du aber mit `intro h` angehen."
 
 Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
-"Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
+"**Du**: Jetzt habe ich also angenommen, dass `A` wahr ist und muss `A ∧ B` zeigen,
+das kennen wir ja schon."
 
-NewTactic intro constructor assumption
+Conclusion "Der Operationsleiter nickt bedacht."

server/testgame/TestGame/Levels/Implication/L02_Revert.lean

@@ -9,34 +9,26 @@ Level 2
 Title "Revert"
 
 Introduction
-"
-Mit `intro` kann man also eine Implikation aus dem Goal entfernen, indem man
-die Implikationsprämisse zu den *Annahmen* hinzufügt:
-
-```
-example : A → B :=
-  [Beweis]
-```
-
-wird zu
-
-```
-example (ha : A) : B :=
-  [Beweis]
-```
-
-Seltener kann auch die andere Richtung nützlich sein. Mit `revert ha` kann man die Annahme
-`ha` entfernen und als Implikationsprämisse vor's Goal hängen.
-"
+"Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
 
 Statement
-"Angenommen $A$ ist eine wahre Aussage und man hat eine Implikation $A \\Rightarrow B$, zeige
-dass $B$ wahr ist."
+""
     (A B : Prop) (ha : A) (h : A → B) : B := by
   revert ha
   assumption
 
-HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
-"Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
+NewTactic revert
+DisabledTactic tauto
+
+Hint (A : Prop) (B : Prop) (ha : A) (h : A → B) : B =>
+"**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
+Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
+
+**Du**: Das wirkt etwas unnatürlich.
+
+**Robo**: Schon, ja. Aber als Tool kann das manchmal nützlich sein."
+
+Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
+die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
 
-NewTactic revert assumption
+Daraufhin lächelt der Fragende nur vorahnend."

server/testgame/TestGame/Levels/Implication/L03_Apply.lean

@@ -9,6 +9,8 @@ Title "Apply"
 
 Introduction
 "
+Sein Kollege zieht eine Linie unter deinen Beweis, schreibt ein durchgestrichenes ~`revert`~
+hin und gibt dir das Blatt wieder.
 `revert` ist aber nur selten der richtige Weg.
 
 Im vorigen Beispiel würde man besser die Implikation $A \\Rightarrow B$ *anwenden*, also
@@ -18,21 +20,24 @@ Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die K
 (also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen.
 "
 
-Statement
-    "Seien $A, B$ logische Aussagen, wobei $A$ wahr ist und $A \\Rightarrow B$.
-    Zeige, dass $B$ wahr ist."
-    (A B : Prop) (hA : A) (g : A → B) : B := by
-  apply g
+Statement "" (A B : Prop) (hA : A) (h : A → B) : B := by
+  apply h
   assumption
 
-HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B =>
-"Mit `apply g` kannst du die Implikation `g` anwenden."
+NewTactic apply
+DisabledTactic revert tauto
 
-HiddenHint (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."
+Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
+"**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
+`apply {h}` die Implikation anzuwenden."
 
-NewTactic apply assumption
+Hint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
+"**Du**: Und jetzt genügt es also `A` zu zeigen."
+
+Conclusion "**Robo** Übrigens mit `apply LEMMA` kannst auch jedes Lemma anwenden, dessen
+Aussage mit dem Goal übereinstimmt.
+
+Die beiden Fragenden schauen das Blatt an und murmeln zustimmend."
 
 -- Katex notes
 -- `\\(    \\)` or `$   $` for inline

server/testgame/TestGame/Levels/Implication/L04_Apply.lean

@@ -10,26 +10,30 @@ Title "Implikation"
 
 Introduction
 "
-Hier eine Übung zu Implikationen.
-Fast immer ist es der richtige Weg, wenn du mit `intro` anfängst.
+**Du** *(zu Robo)*: Testen die uns eigentlich hier?
+
+Ein älteres Gruppenmitglied schiebt ein Tablet über den Tisch und beginnt in leiser
+Stimme zu erklären.
+
+**Mitarbeiterin**: Eines unserer Kontrollelemente ist kaputt und ist verwirrt, wo Sachen hinkommen.
+Gesteuert werden diese über Panels, und hier hab ich das Übungspanel, mit dem wir neue
+Ingeneure ausbilden:
 "
 
-Statement
-    "Angenommen man weiss $A \\Rightarrow B \\Rightarrow C$, zeige dass $A \\Rightarrow C$."
-    (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+Statement "" (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
   intro hA
   apply g
   apply f
   assumption
 
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
-"Mit `intro hA` kann man annehmen, dass $A$ wahr ist. danach muss man $B$ zeigen."
+Hint (A B C : Prop) (f : A → B) (g : B → C) : A → C =>
+"**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
+kombinieren?
 
-Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
-"Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
+**Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch.
+"
 
 HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
-"Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
-diese mit `apply` an."
+"**Robo**: Das ist wieder eine Anwendung von `apply`."
 
-NewTactic intro apply assumption revert
+DisabledTactic tauto

server/testgame/TestGame/Levels/Implication/L05_Apply.lean

@@ -8,46 +8,63 @@ Title "Implikation"
 
 Introduction
 "
-Noch eine Übung: Angenommen man hat folgende Implikationen:
+Selbstsicher folgt ihr den Anweisungen und geht nach draussen zum
+defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
 $$
 \\begin{CD}
   A  @>{f}>> B       @<{g}<< C       \\\\
   @. @V{h}VV @V{m}VV \\\\
-  D  @>{i}>> E       @>{k}>> F
+  D  @>{i}>> E       @>{k}>> F       \\\\
+  @A{m}AA @A{n}AA @V{p}VV \\\\
+  G  @<{q}<< H       @>{r}>> I
 \\end{CD}
 $$
 "
 
 Statement
     "Beweise $A \\Rightarrow F$."
-    (A B C D E F : Prop) (f : A → B) (g : C → B) (h : B → E)
-     (i : D → E) (k : E → F) (m : C → F) : A → F := by
+    (A B C D E F G H I : Prop)
+    (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F)
+    (n : G → D) (p : H → E) (q : F → I)
+    (r : H → G) (s : H → I) : A → I := by
   intro ha
+  apply q
   apply k
   apply h
   apply f
   assumption
 
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
+Hint (A B C D E F G H I : Prop)
     (f : A → B) (g : C → B) (h : B → E)
-    (i : D → E) (k : E → F) (m : C → F) : A → F =>
-"Wieder ist es schlau, mit `intro` anzufangen."
+    (i : D → E) (k : E → F) (m : C → F)
+    (n : G → D) (p : H → E) (q : F → I)
+    (r : H → G) (s : H → I) : A → I =>
+"**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
 
-HiddenHint (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) : F =>
-"Versuch mit `apply` den richtigen Weg zu finden."
+**Robo**: Und dann fängst du am besten wieder mit `intro` an."
 
-Hint (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."
+HiddenHint (A B C D E F G H I : Prop)
+    (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F)
+    (n : G → D) (p : H → E) (q : F → I)
+    (r : H → G) (s : H → I) (a : A) : I =>
+"**Robo**: Na wieder `apply`, was sonst."
 
-Hint (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."
+Hint (A B C D E F G H I : Prop)
+    (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F)
+    (n : G → D) (p : H → E) (q : F → I)
+    (r : H → G) (s : H → I) (a : A) : H =>
+"**Robo**: Das sieht nach einer Sackgasse aus…"
+
+Hint (A B C D E F G H I : Prop)
+    (f : A → B) (g : C → B) (h : B → E)
+    (i : D → E) (k : E → F) (m : C → F)
+    (n : G → D) (p : H → E) (q : F → I)
+    (r : H → G) (s : H → I) (a : A) : C =>
+"**Robo**: Nah, da stimmt doch was nicht…"
 
-NewTactic apply assumption revert intro
+DisabledTactic tauto
 
 -- https://www.jmilne.org/not/Mamscd.pdf

server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean

@@ -62,28 +62,30 @@ Im nachfolgenden beweisen wir die Eigenschaften einzeln.
 
 Statement
 "Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
-    : Module ℚ ℝ :=
-  { smul := fun a r ↦ ↑a * r,
-    smul_zero := by
-      intro a
-      rw [smul_zero]
-    zero_smul := by
-      intro a
-      change (0 : ℚ) * a = 0
-      simp
-    one_smul := by
-      intro b
-      change (1 : ℚ) * b = b
-      rw [Rat.cast_one, one_mul]
-    smul_add := by
-      intro a x y
-      change a * (x + y) = a * x + a * y
-      rw [mul_add]
-    add_smul := by
-      intro r s x
-      change (r + s : ℚ) * x = r * x + s * x
-      rw [Rat.cast_add, add_mul]
-    mul_smul := by
-      intro x y b
-      change (x * y : ℚ) * b = x * (y * b)
-      rw [Rat.cast_mul, mul_assoc]}
+    : Module ℚ ℝ := by
+  refine {
+    smul := fun a r => ↑a * r
+    smul_zero := ?smul_zero
+    zero_smul := ?zero_smul
+    one_smul := ?one_smul
+    smul_add := ?smul_add
+    add_smul := ?add_smul
+    mul_smul := ?mul_smul }
+
+  · intro b
+    change (1 : ℚ) * b = b
+    rw [Rat.cast_one, one_mul]
+  · intro x y b
+    change (x * y : ℚ) * b = x * (y * b)
+    rw [Rat.cast_mul, mul_assoc]
+  · intro a
+    rw [smul_zero]
+  · intro a x y
+    change a * (x + y) = a * x + a * y
+    rw [mul_add]
+  · intro r s x
+    change (r + s : ℚ) * x = r * x + s * x
+    rw [Rat.cast_add, add_mul]
+  · intro a
+    change (0 : ℚ) * a = 0
+    simp

server/testgame/TestGame/Levels/SetTheory.lean

@@ -23,6 +23,21 @@ Game "TestGame"
 World "SetTheory"
 Title "Mengenlehre"
 
+Introduction
+"Der größere der beiden Monde sieht dunkelrot und karg aus. Trotzdem sollen dort nomadische
+Gesellschaften wohnen, die sich in der Einöde zurechtfinden.
+
+Ihr steuert einen der wenigen befestigten Standorte am Fusse eines Berges an.
+
+**Robo**: Die Bevölkerung hier lebt so abgekapselt vom Rest des Universums, dass sie sich
+vermutlich noch viel besser mit alter Sprache und Schrift auskennt.
+
+**Du**: Hoffen wir, dass sie uns weiterhelfen können dieses Buch der Urbilder zu entschlüsseln.
+
+Sofort begrüßt euch eine ältere Frau, die sich als *Mengitte*, die Beschützerin des Mondes,
+vorstellt.
+"
+
 Game "TestGame"
 World "SetTheory2"
 Title "Mehr Mengenlehre"

server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean

@@ -14,29 +14,47 @@ Title "Mengen"
 
 Introduction
 "
-In diesem Kapitel schauen wir uns Mengen an.
+**Mengitte**: Ich würde leider den Inhalt jenes Buches eh nicht verstehen. Aber der beste Weg für
+euch, dieses zu entschlüsseln ist, euch ausgiebig mit der Bevölkerung hier zu unterhalten.
+Lebt mit ihnen, redet mit ihnen und ihr werdet die Sprache automatisch lernen.
 
-Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst,
-alle Elemente in einer Menge haben den gleichen Typ.
+**Mengitte**: Seit aber vorgewarnt, die Leute hier denken ganz viel über Mengen nach,
+womit sie immer *homogene Mengen* meinen. Eine Menge natürlicher Zahlen `{1, 4, 6}` ist
+verständlich, aber sowas wie eine Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` gibt es hier
+einfach nicht. Punkt.
 
-Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine
-Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben.
+**Robo**: Als Kontext: Wenn `A` ein beliebiger `Type` ist, dann ist `(U : Set A)` eine Menge
+mit Elementen aus `A`
 
-Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus
-`X`.  `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied
-zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht
-austauschbar!
-
-Um zu beweisen, dass etwas in `univ` ist, kannst du verschiedenste deiner Taktiken anwenden,
-zum Beispiel `tauto`.
+**Mengitte**: Damit ich weiss, dass ihr euch grundsätzlich mit den Leuten austauschen könnt,
+erklärt mir doch folgendes:
 "
 
 open Set
 
-Statement mem_univ
-    "4 ist ein Element der Menge aller natürlichen Zahlen." {A : Type _} (x : A) :
-    x ∈ (univ : Set A) := by
+Statement mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by
   trivial
-  -- tauto
 
-NewTactic tauto trivial
+Hint (A : Type) (x : A) : x ∈ (univ : Set A) =>
+"**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
+
+**Robo** … und `univ` ist die Menge aller Elemente in `A`.
+
+**Du** ist das nicht einfach `A` selber?
+
+**Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
+
+**Du**: Unlogisch.
+
+**Mengites**: Naja, Typen und Mengen sind halt zwei unterschiedliche Sachen und wenn ihr
+über Mengen sprechen wollt, müssen alles Mengen sein.
+
+**Du**: Na gut. Und wieso `x ∈ univ` und nicht `x : univ` wie bei Typen?
+
+**Robo**: Jedes Element `(x : A)` hat entweder die Eigenschaft `x ∈ U` oder `x ∉ U` für eine
+Menge `(U : Set A)`. (`\\in`, `\\nin`)
+
+**Du**: Also das ist ja dann trivial. Hoffentlich sehen die das hier auch so…
+"
+
+Conclusion "**Mengitte**: Ja das stimmt schon. Dann wünsche ich euch viel Erfolg auf eurer Reise!"

server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean

@@ -13,17 +13,22 @@ Title "leere Menge"
 
 Introduction
 "
-Gleich wie bei `univ` gibt es leere Mengen `∅` von verschiedenen Typen.
-So ist `(∅ : Set ℕ)` in Lean nicht das gleiche wie `(∅ : Set ℤ)`. (`\\empty`)
-
-Zudem hat die Verneinung `¬ (x ∈ A)` die Notation `x ∉ A` (`\\nin`), gleich wie bei `=` and `≠`.
-
-Um zu zeigen, dass etwas nicht in der leeren Menge ist, kannst du wieder `tauto` verwenden.
+Ihr zieht also durch die Gegend und redet mit den Leuten. Ein Junge rennt zu euch und fragt:
 "
 
 open Set
 
-Statement not_mem_empty
-    "Kein Element ist in der leeren Menge enthalten." {A : Type _} (x : A) :
+Statement not_mem_empty "" {A : Type} (x : A) :
     x ∉ (∅ : Set A) := by
   tauto
+
+NewLemma mem_univ
+
+Hint (A : Type) (x : A) : x ∉ (∅ : Set A) =>
+"**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles tautologisches Zeugs...
+
+**Robo**: Dann behaupte das doch. (`\\empty`)"
+
+Conclusion "Der Junge rennt weiter.
+
+**Du**: So wird das ganze schon angenehmer."