+
Weitere Goals
{goals.goals.slice(1).map((goal, i) =>
)}
diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css
index 6a03114..650a679 100644
--- a/client/src/components/infoview/infoview.css
+++ b/client/src/components/infoview/infoview.css
@@ -75,3 +75,7 @@
.command-line-input .monaco-editor .scroll-decoration {
box-shadow: none;
}
+
+.other-goals .goals-section-title, .other-goals summary, .other-goals summary .font-code {
+ color: #5191d1;
+}
diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx
index bde2910..dcb0ec7 100644
--- a/client/src/components/infoview/main.tsx
+++ b/client/src/components/infoview/main.tsx
@@ -33,9 +33,8 @@ export function Main(props: {world: string, level: number}) {
if (ec.events.changedCursorLocation.current &&
ec.events.changedCursorLocation.current.uri === params.uri) {
- dispatch(codeEdited)
+ dispatch(levelCompleted({world: props.world, level: props.level}))
}
- dispatch(levelCompleted({world: props.world, level: props.level}))
},
[]
);
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 1674572..b95cf9c 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -35,16 +35,15 @@
background-color: #e9f2fb;
}
-.infoview {
- padding: 1em;
-}
-
-.exercise {
- padding: 1em;
+.introduction-panel, .infoview, .exercise, .conclusion {
+ padding-top: 1em;
+ padding-left: 1em;
+ padding-right: 1em;
+ padding-bottom: 0;
}
-.conclusion {
- padding: 1em;
+.infoview {
+ padding-top: 0em;
}
.exercise {
@@ -64,10 +63,6 @@
margin-bottom: 0;
}
-.introduction-panel {
- padding: 1em;
-}
-
.input-mode-switch {
margin: 0;
display: flex;
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index d3f78cd..bd5268c 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -4,7 +4,7 @@ import { Connection } from '../connection'
interface GameInfo {
title: null|string,
introduction: null|string,
- worlds: null|{nodes: {[id:string]: {id: string, title: string}}, edges: string[][]},
+ worlds: null|{nodes: {[id:string]: {id: string, title: string, introduction: string}}, edges: string[][]},
worldSize: null|{[key: string]: number},
authors: null|string[],
conclusion: null|string,
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 1d248a7..71500af 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -174,7 +174,10 @@ structure World where
deriving Inhabited
instance : ToJson World := ⟨
- fun world => Json.mkObj [("name", toJson world.name), ("title", world.title)]
+ fun world => Json.mkObj [
+ ("name", toJson world.name),
+ ("title", world.title),
+ ("introduction", world.introduction)]
⟩
/-! ## Game -/
diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index 1669b22..a6d5646 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -23,22 +23,9 @@ Game "TestGame"
Title "Lean 4 game"
Introduction
"
-Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
-bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
-Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
-
-Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
-sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
-seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
-herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
-keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
-
-Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
-überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie
-exklusiv in einem Dir fremden Dialekt. Zum Glück hat Robo mit Dir das Universum gewechselt.
-Robo, das ist Dein kleiner SmartElf. Robo kann zwar auch keine Mathematik, aber es scheint,
-er kann irgendetwas mit dem Formalosophendialekt anfangen.
+TODO
"
+
Conclusion
"Fertig!"
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index 46372a3..865cc85 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -73,6 +73,34 @@ DefinitionDoc Odd
Die Definition kann man mit `unfold odd at *` einsetzen.
"
+DefinitionDoc Injective
+"
+`Injective f` ist als
+
+```
+∀ {a b : U}, a < b → f a < f b
+```
+definiert.
+"
+
+DefinitionDoc Surjective
+"
+"
+
+DefinitionDoc Bijective
+"
+"
+
+DefinitionDoc StrictMono
+"
+`StrictMono`
+
+```
+∀ {a b : U}, f a f b → a = b
+```
+
+"
+
LemmaDoc not_odd as not_odd in "Nat"
"`¬ (odd n) ↔ even n`"
@@ -129,3 +157,24 @@ LemmaDoc add_pow_two as add_pow_two in "Nat"
LemmaDoc Finset.sum_comm as Finset.sum_comm in "Sum"
""
+
+LemmaDoc Function.comp_apply as Function.comp_apply in "Function"
+""
+
+LemmaDoc not_le as not_le in "Logic"
+""
+
+LemmaDoc if_pos as if_pos in "Logic"
+""
+
+LemmaDoc if_neg as if_neg in "Logic"
+""
+
+LemmaDoc StrictMono.injective as StrictMono.injective in "Function"
+""
+
+LemmaDoc StrictMono.add as StrictMono.add in "Function"
+""
+
+LemmaDoc Odd.strictMono_pow as Odd.strictMono_pow in "Function"
+""
diff --git a/server/testgame/TestGame/Levels/Function.lean b/server/testgame/TestGame/Levels/Function.lean
index b5f0bb8..6eb4eee 100644
--- a/server/testgame/TestGame/Levels/Function.lean
+++ b/server/testgame/TestGame/Levels/Function.lean
@@ -3,6 +3,7 @@ import TestGame.Levels.Function.L02_Let
import TestGame.Levels.Function.L03_Composition
import TestGame.Levels.Function.L06_Piecewise
import TestGame.Levels.Function.L07_Injective
+import TestGame.Levels.Function.L07'_Injective
import TestGame.Levels.Function.L08_Injective
import TestGame.Levels.Function.L09_Surjective
import TestGame.Levels.Function.L10_Bijective
diff --git a/server/testgame/TestGame/Levels/Function/L02_Let.lean b/server/testgame/TestGame/Levels/Function/L02_Let.lean
index d6ea306..247c040 100644
--- a/server/testgame/TestGame/Levels/Function/L02_Let.lean
+++ b/server/testgame/TestGame/Levels/Function/L02_Let.lean
@@ -66,7 +66,7 @@ HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 =>
Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
"
-Definitionen muss man anundzu manuell einsetzen um den Taktiken zu helfen.
+Definitionen muss man manchmal manuell einsetzen um den Taktiken zu helfen.
Das macht man mit `unfold f` (oder alternativ mit `rw [f]`).
"
diff --git a/server/testgame/TestGame/Levels/Function/L03_Composition.lean b/server/testgame/TestGame/Levels/Function/L03_Composition.lean
index ba637b3..416e8bb 100644
--- a/server/testgame/TestGame/Levels/Function/L03_Composition.lean
+++ b/server/testgame/TestGame/Levels/Function/L03_Composition.lean
@@ -16,5 +16,7 @@ TODO
Statement
"TODO: Find an exercise."
- (U S T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x) := by
+ (U T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x) := by
simp only [Function.comp_apply]
+
+NewLemmas Function.comp_apply
diff --git a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
index d79413f..97bbfcd 100644
--- a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
+++ b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
@@ -9,19 +9,171 @@ Title ""
Introduction
"
+Du kommst an eine Tür mit zwei Wächtern. Der eine hat ein Schild
+
+```
+def f : ℚ → ℚ := fun x ↦ 5 * x
+```
+
+der andere eines mit
+
+```
+def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
+```
+
+Auf der Tür steht groß:
"
+example (P : Prop) [Decidable P] (a b : ℕ) (h : P) : ite P a b = a := if_pos h
+
open Set
-def f2 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+namespace LevelFunction4
+
+def f : ℚ → ℚ := fun x ↦ 5 * x
+def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
+
+
+-- #eval (f2 + f2) 2
+
+-- #check range f2
+
+Statement ""
+ : f ∘ g = g ∘ f := by
+ funext x
+ simp_rw [Function.comp_apply]
+ unfold g
+ by_cases 0 ≤ x
+ have h' : 0 ≤ f x
+ unfold f
+ linarith
+ rw [if_pos h', if_pos h]
+ unfold f
+ ring
+ have h' : ¬ (0 ≤ f x)
+ unfold f
+ linarith
+ rw [if_neg h, if_neg h']
+ unfold f
+ ring
+
+NewTactics funext by_cases simp_rw linarith
+
+NewLemmas not_le if_pos if_neg
+
+
+Hint : f ∘ g = g ∘ f =>
+"
+**Robo**: Schau mal, die beiden haben zwei Funktionen, eine davon mit stückweiser Definition.
+
+**Du**: Und ich soll zeigen, dass die beiden vertauschbar sind?
+
+**Robo**: Genau, am besten wählst du mit `funext x` ein beliebiges Element aus, und zeigst das
+dann für dieses.
+"
+
+-- TODO: These 5 hints should be mutually exclusive. i.e. they should not trigger
+-- if a assumption is missing.
+Hint (x : ℚ) : (f ∘ g) x = (g ∘ f) x =>
+"
+**Du**: Ah und jetzt kann ich erst einmal `(g ∘ f) {x}` zu `g (f {x})` umschreiben?
+
+**Robo**: Mit `simp_rw` geht das übrigens schneller.
+
+**Robo**: Und danach willst du eien Fallunterscheidung
+machen, `by_cases h : 0 ≤ {x}`.
+
+**Du**: Damit krieg ich die Fälle `0 ≤ {x}` und `{x} < 0`?
+
+**Robo**: Genau! Oder präziser `0 ≤ {x}` und `¬(0 ≤ {x})`. Das ist nicht ganz das gleiche, und man
+könnte mit dem Lemma `not_le` zwischen `¬(0 ≤ {x})` und `0 < {x}` wechseln.
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) : f (g x) = g (f x) =>
+"
+**Robo**: Um das ausrechnen zu können, brauchst du nicht nur `0 ≤ x` sondern auch noch
+eine Annahme `0 ≤ f x`.
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = g (f x) =>
+"
+**Du**: Mit den beiden Annahmen habe ich ja jetzt `(if 0 ≤ x then _)` wobei `0 ≤ x` wahr ist,
+kann ich das dann einfach vereinfachen?
+
+**Robo**: Dafür must du zuerst die Definition von `g` öffnen, also `unfold`. Und dann mit
+dem Lemma `if_pos {h}` das umschreiben.
+"
+
+Hint (x : ℚ) (h : ¬ 0 ≤ x) : f (g x) = g (f x) =>
+"
+**Du**: Ich sehe, das ist jetzt der zweite Fall, da brauch ich sicher wieder eine zweite Annahme
+`¬(0 ≤ f x)`…
+"
+
+Hint (x : ℚ) (h : ¬ 0 ≤ x) (h₂ : ¬ 0 ≤ f x) : f (g x) = g (f x) =>
+"
+**Robo**: Jetzt ist der Zeitpunkt wo die Definition von `g` geöffnet sein sollte.
+
+**Robo**: Wenn man ein If-Statement mit wahrer Prämisse mit `if_pos` vereinfacht, dann
+braucht man für eine falsche Prämisse…
+
+**Du**: `if_neg`?
+"
+-- END TODO
+HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = g (f x) =>
+"
+**Robo**: Jetzt das Gleiche noch mit `if_pos {h₂}`.
+"
+
+HiddenHint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = 2 * f x =>
+"
+**Robo**: Jetzt das Gleiche noch mit `if_pos {h}`.
+"
+
+Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (2 * x) = 2 * f x =>
+"
+**Robo**: Wenn du jetzt noch die Definition von `f` öffnest, dann kann `ring` den
+Rest ausrechnen.
+"
+
+
+-- TODO: This are also showing in the case of the Hint below
+-- Proof of `0 ≤ f x`.
+Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
+" **Robo**: Wenn du die Definition von `f` öffnest, dann hast du schon das wissen,
+um das zu beweisen."
+HiddenHint (x : ℚ) (h : 0 ≤ x) : 0 ≤ f x =>
+"**Du** *(in Gedanken)*: Was war das nochmals... Ungleichungen... `linarith`!"
+
+HiddenHint (x : ℚ) (h : ¬0 ≤ x) : ¬ 0 ≤ f x =>
+" **Robo**: Das ist das selbe wie vorhin…"
+
+
+-- Hint for modifying `h` wrongly.
+Hint (x : ℚ) (h : x < 0) : f (g x) = g (f x) =>
+"
+**Robo**: Das war nicht so ideal, hier brauchst du die Annahme in der Form `({h} : ¬ 0 ≤ {x})`!
+"
+
+-- TODO: In this case we get to see the Hints above
+Hint (x : ℚ) (h : 0 ≤ x) : 0 ≤ x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
+geschrieben hast."
+
+Hint (x : ℚ) (h : 0 ≤ f x) : 0 ≤ f x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_pos]` anstatt `rw [if_pos {h}]`
+geschrieben hast."
-#eval (f2 + f2) 2
+Hint (x : ℚ) (h : ¬ 0 ≤ x) : ¬ 0 ≤ x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
+geschrieben hast."
-#check range f2
+Hint (x : ℚ) (h : ¬ 0 ≤ f x) : ¬ 0 ≤ f x =>
+"**Robo**: Dieses Goal ist entstanden, als du `rw [if_neg]` anstatt `rw [if_neg {h}]`
+geschrieben hast."
-Statement
-""
- : True := by
- trivial
+Conclusion
+"Zufrieden tauschen die beiden Wächter ihren Platz und geben so dabei den
+Durchgang frei."
-#check Set.piecewise
+end LevelFunction4
diff --git a/server/testgame/TestGame/Levels/Function/L07'_Injective.lean b/server/testgame/TestGame/Levels/Function/L07'_Injective.lean
new file mode 100644
index 0000000..8b2447c
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Function/L07'_Injective.lean
@@ -0,0 +1,79 @@
+import TestGame.Metadata
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Function"
+Level 6
+
+Title ""
+
+Introduction
+"
+Sofort hackt die ältere Gestalt nach:
+"
+open Set Function
+
+example (f : ℤ → ℤ) (h : StrictMono f) : Injective f := by
+ apply StrictMono.injective
+ assumption
+
+-- Odd.strictMono_pow
+
+Statement "" : Injective (fun (n : ℤ) ↦ n^3 + (n + 3)) := by
+ apply StrictMono.injective
+ apply StrictMono.add
+ apply Odd.strictMono_pow
+ trivial
+ intro a b
+ simp
+
+NewDefinitions Injective
+NewLemmas StrictMono.injective StrictMono.add Odd.strictMono_pow
+
+
+Hint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Du**: Hmm, das ist etwas schwieriger…
+
+**Robo**: Aber ich hab einen Trick auf Lager:
+Das Lemma `StrictMono.injective` sagt, dass jede strikt monotone Funktion injektive ist,
+und ich habe das Gefühl Monotonie ist hier einfacher zu zeigen."
+
+HiddenHint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Robo**: `apply` ist wonach du suchst."
+
+Hint : StrictMono fun (n : ℤ) => n ^ 3 + (n + 3) =>
+"**Du**: Jetzt möchte ich strikte Monotonie von `n ^ 3` und `n + 3` separat zeigen,
+schliesslich scheint es mir als wär das zweite wieder einfach.
+
+**Robo**: Dafür hab ich `StrictMono.add` bereit!"
+
+Hint : StrictMono fun (x : ℤ) => x ^ 3 =>
+"**Du**: Hmm, darauf hab ich jetzt wenig Lust. Gibt's dafür auch was? Das gilt ja nur
+wenn der Exponent ungerade ist.
+
+**Robo**: Du könntest mal `Odd.strictMono_pow` versuchen…"
+
+HiddenHint : Odd 3 =>
+"**Du**: Ist das nicht ne Trivialität? Warte mal!"
+
+Hint : StrictMono fun (x : ℤ) => x + 3 =>
+"**Du**: Ha! Und dieser Teil funktioniert sicher gleich wie Injektivität vorhin!"
+
+
+
+
+
+
+Hint (a b : ℤ) : a ^ 3 + (a + 3) = b ^ 3 + (b + 3) → a = b =>
+"**Robo**: Ich glaube, dieser Weg ist zu steinig. Fang doch nochmals von vorne an!
+"
+
+Hint (a b : ℤ) (h : a ^ 3 + (a + 3) = b ^ 3 + (b + 3)) : a = b =>
+"**Robo**: Ich glaube, dieser Weg ist zu steinig. Fang doch nochmals von vorne an!
+"
+
+Conclusion "**Du**: Danke vielmals!
+
+Und ihr läst das Wesen mit im Gang stehen weiter über Injectivität nachdenkend."
diff --git a/server/testgame/TestGame/Levels/Function/L07_Injective.lean b/server/testgame/TestGame/Levels/Function/L07_Injective.lean
index deb49bc..cbc45a5 100644
--- a/server/testgame/TestGame/Levels/Function/L07_Injective.lean
+++ b/server/testgame/TestGame/Levels/Function/L07_Injective.lean
@@ -9,16 +9,30 @@ Title ""
Introduction
"
+Ihr läuft durch verschiedenste Leere Gänge des Funktionentempels.
+
+**Du**: Wenn wir wüssten, dass nur ein möglicher Weg hierhin führt, könnten wir
+ausschliessen, dass wir im Kreis laufen.
+
+Plötzlich begegnet ihr einem älteren Wesen mit Fakel. Auf die Frage antwortet es mit
"
open Set Function
-def f3 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+Statement "" : Injective (fun (n : ℤ) ↦ n + 3) := by
+ intro a b
+ simp
-#eval (f3 + f3) 2
+NewDefinitions Injective
-example : ¬ f3.Injective := by
- unfold Injective
- push_neg
- use 2
- use 3
- simp
+Hint : Injective (fun (n : ℤ) ↦ n + 3) =>
+"**Robo**: `Injective` ist als `∀ \{a b : U}, f a = f b → a = b`
+definiert, also kannst du mit `intro` anfangen.
+"
+
+Hint (a b : ℤ) : (fun n => n + 3) a = (fun n => n + 3) b → a = b =>
+"**Du**: Kann man das wohl vereinfachen?"
+
+Hint (a b : ℤ) (hab : (fun n => n + 3) a = (fun n => n + 3) b) : a = b =>
+"**Robot**: Jetzt musst du wohl `{hab}` vereinfachen."
+
+Conclusion "**Du** Woa das war ja einfach!"
diff --git a/server/testgame/TestGame/Levels/Function/L08_Injective.lean b/server/testgame/TestGame/Levels/Function/L08_Injective.lean
index edc30a4..614ab80 100644
--- a/server/testgame/TestGame/Levels/Function/L08_Injective.lean
+++ b/server/testgame/TestGame/Levels/Function/L08_Injective.lean
@@ -3,17 +3,74 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 6
+Level 7
-Title ""
+Title "Injektive"
Introduction
"
+Weiterirrend kommt ihr an eine Verzweigung.
+
+**Robo**: Sieht beides gleich aus.
+
+Ein paar Schritte in den linken Korridor hinein seht ihr gekritzel an der Wand:
+
+```
+def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+```
+
+**Du**: Hier haben wir eine stückweis definierte Funktion
+
+$$
+f(n) = \\begin{cases}
+ n^2 & \\text{falls } n \\text{ gerade} \\\\
+ n+1 & \\text{andernfalls.}
+\\end{cases}
+$$
+
+
+Darunter steht in leicht leuchtender Schrift:
+"
+
+namespace FunctionLvl7
+
+open Function
+
+def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
+
+Statement "" : ¬ (f + f).Injective := by
+ unfold Injective
+ push_neg
+ use 2
+ use 3
+ simp
+
+Hint : ¬ (Injective (f + f)) =>
+"
+**Robo**: Das ist sicher ein Hinweis.
+
+**Du**: Aber `¬ Injective` sagt mir nichts…
+
+**Robo**: Könntest du etwas mit `¬ ∀` anfangen? Dann könntest du ja `Injektive` zuerst öffnen.
+
+**Du**: Darüber haben wir doch mal was gelernt…
+"
+
+HiddenHint : ¬ (Injective (f + f)) =>
+"
+**Robo**: Das war `push_neg`.
+"
+
+Hint : ∃ a b, (f + f) a = (f + f) b ∧ a ≠ b =>
+"**Du** Jetzt muss ich einfach ein Gegenbeispiel nennen, oder?
+
+**Robo** Genau! Welche beiden Zahlen möchtest du denn verwenden?"
+
+Conclusion
+"
+Als ihr das Problem gelöst habt, erschleicht euch ein starkes
+Gefühl, dass dies der falsche Weg ist.
+Also geht ihr zurück und nehmt die rechte Gabelung.
"
-Statement
-""
- : (fun (n : ℤ) ↦ n + 1).Injective := by
- intro a b hab
- simp at hab
- assumption
+end FunctionLvl7
diff --git a/server/testgame/TestGame/Levels/Function/L09_Surjective.lean b/server/testgame/TestGame/Levels/Function/L09_Surjective.lean
index 8a67873..dcb6222 100644
--- a/server/testgame/TestGame/Levels/Function/L09_Surjective.lean
+++ b/server/testgame/TestGame/Levels/Function/L09_Surjective.lean
@@ -3,7 +3,7 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 7
+Level 8
Title "Surjektive"
diff --git a/server/testgame/TestGame/Levels/Function/L10_Bijective.lean b/server/testgame/TestGame/Levels/Function/L10_Bijective.lean
index 1b372cb..4190785 100644
--- a/server/testgame/TestGame/Levels/Function/L10_Bijective.lean
+++ b/server/testgame/TestGame/Levels/Function/L10_Bijective.lean
@@ -3,7 +3,7 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 8
+Level 9
Title ""
diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean
index 9c69a80..4c211af 100644
--- a/server/testgame/TestGame/Levels/Implication.lean
+++ b/server/testgame/TestGame/Levels/Implication.lean
@@ -14,3 +14,17 @@ import TestGame.Levels.Implication.L12_Summary
Game "TestGame"
World "Implication"
Title "Aussagenlogik 2"
+
+Introduction
+"
+Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die ebenfalls
+beide bewohnt zu sein scheinen.
+
+**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
+aber niemand von den Einwohnern...
+
+**Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
+erzählen…
+
+Und damit leitet Robo den Landeanflug ein.
+"
diff --git a/server/testgame/TestGame/Levels/Proposition.lean b/server/testgame/TestGame/Levels/Proposition.lean
index 52058b7..bf6ec84 100644
--- a/server/testgame/TestGame/Levels/Proposition.lean
+++ b/server/testgame/TestGame/Levels/Proposition.lean
@@ -16,3 +16,24 @@ import TestGame.Levels.Proposition.L13_Summary
Game "TestGame"
World "Proposition"
Title "Aussagenlogik 1"
+
+Introduction "
+Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
+bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
+Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
+
+Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
+sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
+seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
+herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
+keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
+
+Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
+überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
+exklusiv in einem Dir fremden Dialekt, den sie Leansch [liːnʃ] nennen.
+
+Zum Glück hat Robo mit Dir das Universum gewechselt.
+Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir
+in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leansch gelernt.
+Und das ist Gold wert.
+"
diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
index 0e5788a..81f412d 100644
--- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
@@ -9,28 +9,9 @@ Title "Automatisierung"
Introduction
"
-Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
-bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
-Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
+Gerade seid Ihr auf Königin *Logisindes* Planeten. Sie kommt ohne Umschweife zum Punkt:
-Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
-sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
-seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
-herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
-keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
-
-Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
-überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
-exklusiv in einem Dir fremden Dialekt, den sie Leanish [liːnɪʃ] nennen.
-
-Zum Glück hat Robo mit Dir das Universum gewechselt.
-Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leanish gelernt. Und das ist Gold wert.
-
-----
-
-Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum Punkt:
-
-**Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
+**Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
Und sie kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung.
Dazwischen sollst Du offenbar einen Beweis eintragen.
@@ -44,7 +25,9 @@ Statement ""
Hint (A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
- "**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint sie: `A`, `B` und `C` sind irgendwelche Aussagen (*propositions*). Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
+ "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
+ `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
+ Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
@@ -59,7 +42,9 @@ Hint (A B C : Prop) :
Conclusion
"
-**Logisinde** (etwas konsterniert) Ja, das ist streng genommen richtig. Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt! Meine Untertanen verstehen `tauto` nicht. Da müsst Ihr Euch schon etwas mehr anstrengen.
+**Logisinde** (etwas konsterniert) Ja, das ist streng genommen richtig.
+Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt!
+Meine Untertanen verstehen `tauto` nicht. Da müsst Ihr Euch schon etwas mehr anstrengen.
"
NewTactics tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index a519591..9b723b3 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -8,7 +8,8 @@ Title "Aller Anfang ist... ein Einzeiler?"
Introduction
"
-In der Zwischenzeit hat bereits sich eine lange Schlange Untertanen gebildet, die gern ihren Fragen stellen würden. Logisinde winkt den ersten nach vorn. Er räuspert sich.
+In der Zwischenzeit hat bereits sich eine lange Schlange Untertanen gebildet, die gern ihren
+Fragen stellen würden. Logisinde winkt den ersten nach vorn. Er räuspert sich.
**Untertan** Warum ist $42 = 42$?
@@ -21,7 +22,8 @@ Statement "" :
rfl
Hint : 42 = 42 => "
-**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`.
+**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist.
+Probier mal `rfl`.
"
Conclusion
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index 169583c..c019f3f 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -16,13 +16,15 @@ Statement ""
assumption
Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
-**Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl.
+**Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl.
-**Du** Warum schreibt er dann nicht `n ∈ ℕ`??
+**Du** Warum schreibt er dann nicht `{n} ∈ ℕ`??
-**Robo** Weil das hier alles komische Typen sind … Ich kann Dir das später mal in Ruhe erklären. Jetzt will ich erst einmal die Frage entschlüsseln.
+**Robo** Weil das hier alles komische Typen sind … Ich kann Dir das später mal in Ruhe erklären.
+Jetzt will ich erst einmal die Frage entschlüsseln.
-**Robo** Also, `h₁`, `h₂`, `h₃` sind einfach nur Namen für verschiedene Annahmen, und zwar für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
+**Robo** Also, `{h₁}`, `{h₂}`, `{h₃}` sind einfach nur Namen für verschiedene Annahmen, und zwar
+für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
**Du** Aber das war doch gerade eine der Annahmen.
@@ -35,7 +37,8 @@ Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
Conclusion
"
-**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf zerbrochen habe!
+**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf
+zerbrochen habe!
"
NewTactics assumption
diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
index 1db00a7..714ca94 100644
--- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
@@ -17,20 +17,21 @@ Statement ""
assumption
Hint (A : Prop) (hA : A) : A => "
-**Robo** Hier bedeutet `A : Prop` wieder, dass `A` irgendeine Aussage ist.
- Und `hA` ist eine Name für die Annahme, dass `A` wahr ist.
+**Robo** Hier bedeutet `{A} : Prop` wieder, dass `{A}` irgendeine Aussage ist.
+ Und `{hA}` ist eine Name für die Annahme, dass `{A}` wahr ist.
-**Du** Und unter dieser Annahme sollen wir jetzt `A` beweisen?
+**Du** Und unter dieser Annahme sollen wir jetzt `{A}` beweisen?
**Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder?
"
HiddenHint (A : Prop) (hA : A) : A =>
-"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. Also wird `asumption` auch wieder funktionieren."
+"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
+Also wird `asumption` auch wieder funktionieren."
Conclusion
"
-**Untertan** Das ging ja schnell. Super! Vielen Dank.
+**Untertan** Das ging ja schnell. Super! Vielen Dank.
"
NewTactics assumption
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index 09e2ddf..97de4d3 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -16,7 +16,8 @@ True := by
trivial
Hint : True => "
-**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist.
+**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
+bedingungslos wahr ist.
**Du** Und was genau ist dann zu beweisen?
@@ -27,9 +28,11 @@ Conclusion
"
**Schelm** Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid …
-**Du** (zu Robo)** Können wir nicht einfach immer dieses `trivial` verwenden? Wie in einer Mathe-Vorlesung?
+**Du** *(zu Robo)* Können wir nicht einfach immer dieses `trivial` verwenden?
+Wie in einer Mathe-Vorlesung?
-**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung. Das funktioniert nur in einer Handvoll Situationen.
+**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung.
+Das funktioniert nur in einer Handvoll Situationen.
"
NewTactics trivial
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 3c5c77f..3800549 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -16,7 +16,8 @@ Statement "" :
trivial
Hint : ¬False => "
- **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist `¬A` falsch, und umgekehrt.
+ **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
+ wahr ist, dann ist `¬A` falsch, und umgekehrt.
**Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
index 519b018..151e025 100644
--- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
@@ -13,25 +13,27 @@ Introduction
Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
"
-Statement
-"Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`.
-Zeige, dass daraus $A$ folgt."
+Statement ""
(A : Prop) (h : False) : A := by
contradiction
Hint (A : Prop) (h : False) : A =>
"
-**Du** Wenn ich das jetzt richtig lese, ist `A` eine Aussage, und wir haben außerdem eine Annahme names `h`, die besagt …
+**Du** Wenn ich das jetzt richtig lese, ist `{A}` eine Aussage, und wir haben außerdem eine
+Annahme names `{h}`, die besagt …
**Robo** … die besagt, dass `False` gilt.
**Du** Ich dachte, `False` gilt nie?
-**Robo** Ja, genau. Die Annahme ist `False`, also falsch. Und aus einer falschen Annahme kann man bekanntlich alles beweisen! Insbesondere die gesuchte Aussage `A`.
+**Robo** Ja, genau. Die Annahme ist `False`, also falsch.
+Und aus einer falschen Annahme kann man bekanntlich alles beweisen!
+Insbesondere die gesuchte Aussage `{A}`.
**Du** Und wie erkläre ich das jetzt diesem Formalosophen?
-**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`.
+**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen
+Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`.
"
Conclusion
@@ -39,7 +41,8 @@ Conclusion
**Du** War das jetzt ein Widerspruchsbeweis?
-**Robo** Nein, nein, ein Widerspruchsbeweis sieht anders aus. Das Argument hier war: wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
+**Robo** Nein, nein, ein Widerspruchsbeweis sieht anders aus. Das Argument hier war:
+ wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
"
NewTactics contradiction
diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
index 0eee982..f26a6f7 100644
--- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
@@ -21,7 +21,7 @@ Statement ""
Hint (n : ℕ) (h : n ≠ n) : n = 37 =>
"
-**Du** Ist `n ≠ n` nicht auch ein Widerspruch?
+**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
**Robo** Probiers mal!
"
@@ -30,9 +30,11 @@ Conclusion
"
**Du** Ja, scheint funktioniert zu haben.
-**Du** Aber irgendwie kommt mir das immer noch ein wenig suspekt vor. Jetzt habe ich bewiesen, dass eine beliebige natürliche Zahl gleich 37 ist?
+**Du** Aber irgendwie kommt mir das immer noch ein wenig suspekt vor.
+Jetzt habe ich bewiesen, dass eine beliebige natürliche Zahl gleich 37 ist?
-**Robo** Nein, nicht doch. Nur eine beliebige Zahl, die ungleich sich selbst ist, ist gleich 37. Und gleich 38, und gleich 39, …
+**Robo** Nein, nicht doch. Nur eine beliebige Zahl, die ungleich sich selbst ist, ist gleich 37.
+Und gleich 38, und gleich 39, …
**Du** Ok, ok, verstehe.
"
diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
index e43bf5f..7b197fa 100644
--- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
@@ -16,17 +16,21 @@ Auftritt dritter Querulant.
"
Statement ""
- (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by
+ (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
contradiction
-Hint (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 =>
+Hint (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 =>
"
**Du** Wieder ein Widerspruch in den Annahmen?
+
+**Robo** Ich sehe, du hast langsam den Dreh raus.
"
Conclusion
"
-**Robo** Gut gemacht. Bei dieser Frage ist auch ein bisschen offensichtlicher, worin der Widerspruch besteht: Die Annahme `n ≠ 10` ist genau die Negation von `n = 10`. Man muss `≠` immer als `¬(· = ·)` lesen.
+**Robo** Gut gemacht. Bei dieser Frage ist auch ein bisschen offensichtlicher,
+worin der Widerspruch besteht: Die Annahme `n ≠ 10` ist genau die Negation von `n = 10`.
+Man muss `≠` immer als `¬(· = ·)` lesen.
"
NewTactics contradiction
diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
index cd12ca7..b406dd7 100644
--- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
@@ -11,7 +11,8 @@ Title "Und"
Introduction
"
-Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht. Er legt sie uns vor, setzt sich hin, und häkelt.
+Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht.
+Er legt sie uns vor, setzt sich hin, und häkelt.
"
Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
constructor
@@ -20,18 +21,27 @@ Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B =>
"
-**Du**: Also, wir haben zwei Annahmen: `A` gilt, und `B` gilt. Auch. Und beweisen sollen wir … `A und B` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung. Kann ich nicht wieder `trivial` sagen?
+**Du**: Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt. Auch. Und beweisen sollen wir
+dass `{A} und {B}` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung.
+Kann ich nicht wieder `trivial` sagen?
-**Robo** Nee, diesmal wird das nicht funktionieren. Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
+**Robo** Nee, diesmal wird das nicht funktionieren.
+Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
**Du** Du meinst, `destructor`??
-**Robo** Nein, `constructor`. Ist verwirrend, ich weiß, aber so nennen die das hier.
+**Robo** Nein, `constructor`. Ich weiß das ist verwirrend,
+aber die nennen das hier so weil man die Aussage aus mehreren Teilen
+konstruieren kann.
"
HiddenHint (A : Prop) (hA : A) : A =>
"
-**Robo** Schau mal, das ist Zauberpapier. Jetzt haben wir auf einmal zwei Beweisziele: `A` und `B`. Ich glaube, Du weißt schon, wie man die jeweils erreicht. Die Ziele stehen ja jeweils in den *Annahmen*.
+**Robo** Schau mal, das ist Zauberpapier.
+Jetzt haben wir auf einmal zwei Beweisziele.
+Hier ist dast Ziel `{A}`.
+Ich glaube, Du weißt schon, wie man die jeweils erreicht.
+Die Ziele stehen ja jeweils in den *Annahmen*.
"
Conclusion
@@ -40,7 +50,8 @@ Conclusion
Ihm scheinen diese Fragen inzwischen Spaß zu machen.
-**Robo** Meinst Du, dieser Hebel, an dem \"Editor mode\" steht, ist echt? Oder ist der nur gemalt? Probier mal!
+**Robo** Meinst Du, dieser Hebel, an dem \"Editor mode\" steht, ist echt?
+Oder ist der nur gemalt? Probier mal!
"
NewTactics constructor
diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
index 8c042f3..4e60cbe 100644
--- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
@@ -22,12 +22,13 @@ Statement ""
Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => "
**Du** Jetzt müssen wir wohl die Annahme de-konstruieren.
-**Robo** Ja, genau. Das geht am einfachsten mit `rcases h with ⟨h₁, h₂⟩`.
+**Robo** Ja, genau. Das geht am einfachsten mit `rcases {h} with ⟨h₁, h₂⟩`.
**Du** Moment, wie schreib ich *das* denn hier auf?
**Robo** Die bleiden Klammern schreibst Du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`.
- Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen für `h₁` und `h₂`, zum Beispiel `rcases h with ⟨hA, hBC⟩`
+Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen
+für `h₁` und `h₂`, zum Beispiel `rcases {h} with ⟨hA, hBC⟩`
"
Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B =>
@@ -42,7 +43,8 @@ HiddenHint (A : Prop) (hA : A) : A =>
Conclusion
"
-**Robo** Du hättest übrigens auch direkt schreiben können `rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`.
+**Robo** Du hättest das übrigens auch direkt verschachtelt schreiben können:
+`rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`.
"
NewTactics rcases
diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
index 7d6ced3..7ed54e8 100644
--- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
@@ -16,7 +16,7 @@ Der nächste bitte …
"
Statement
-"Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$."
+""
(A B : Prop) (hA : A) : A ∨ (¬ B) := by
left
assumption
@@ -25,16 +25,18 @@ Hint (A B : Prop) (hA : A) : A ∨ (¬ B) =>
"
**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
-**Robo** Nein, viel einfacher. Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
+**Robo** Nein, viel einfacher. Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich
+einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
-**Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde? Ich will natürlich `A` beweisen!
+**Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde?
+Ich will natürlich `{A}` beweisen!
-**Robo** Mit `left` bzw. `right'. Ist doch logisch, oder?
+**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?
"
-Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
+Hint (A B : Prop) (hA : A) : ¬ B =>
"
-**Robo** Wusst gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
+**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
"
Conclusion
diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
index 919f127..2541f0d 100644
--- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
@@ -2,7 +2,7 @@ import TestGame.Metadata
import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight
---set_option tactic.hygienic false
+set_option tactic.hygienic false
--set_option autoImplicit false
@@ -18,38 +18,64 @@ Introduction
Der nächste bitte …
"
-Statement
-"Angenommen \"$A$ oder ($A$ und $B$)\" wahr ist, zeige, dass $A$ wahr ist."
- (A B : Prop) (h : A ∨ (A ∧ B)) : A := by
+Statement ""
+ (A B : Prop) (h : (A ∧ B) ∨ A) : A := by
rcases h with h | h
- assumption
rcases h with ⟨h₁, h₂⟩
assumption
+ assumption
-Hint (A B : Prop) (h : A ∨ (A ∧ B)) : A =>
+Hint (A B : Prop) (h :(A ∧ B) ∨ A) : A =>
"
-**Du** Ja klar, erst ein Und im Ziel, dann ein Und in der Annahme, dann ein Oder im Ziel, und jetzt noch ein Oder in der Annahme. Ich glaube den ganzen Circus hier langsam nicht mehr. Die haben sich doch abgesprochen!
+**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
+wie die Klammern gesetzt sind. Irre…
+
+**Du** Ah ich sehe, also `({A} ∧ {B}) ∨ {A}`!
-**Robo** Lass ihnen doch ihren Spaß. Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten weiterfliegen.
+**Du** Ich glaube den ganzen Zircus hier langsam nicht mehr:
+Zuerst ein \"Und\" im Ziel, dann \"Und\" in der Annahme, dann \"Oder\" im Ziel und jetzt
+\"Oder\" in der Annahme, die haben sich doch abgesprochen!
+
+**Robo** Lass ihnen doch ihren Spaß.
+Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten weiterfliegen.
**Du** Also, wieder `rcases …`?
-**Robo** Ja, aber diesmal nicht `rcases h with ⟨h₁, h₂⟩`, sondern `rcases h with h | h`.
+**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`.
"
+-- -- TODO: This also triggers later under the assumptions
+-- -- `(A : Prop) (B : Prop) (h₁ : A) (h₂ : B) : A`
+-- -- Could we do something about that?
+-- Hint (A : Prop) (B : Prop) (h : A) : A =>
+-- "
+-- **Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
+-- Einmal unter Annahme der linken Seite `{A}`,
+-- und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
+-- sei wahr.
+-- "
+
Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"
-**Robo** Jetzt musst Du Dein Ziel zweimal beweisen: Einmal unter der Annahme `A`, und einmal unter der Annahme `A ∨ B`.
+**Robo**
+Jetzt musst Du Dein Ziel zweimal beweisen:
+Einmal unter Annahme der linken Seite `{A} ∨ {B}`,
+und einmal unter Annahme der rechten Seite `{A}`.
+Hier haben nehmen wir an, die linke Seite
+sei wahr.
"
HiddenHint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"
-**Robo** Wie man mit einem Und in den Annahmen umgeht, weißt Du doch schon: `rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`.
+**Robo** Wie man mit einem Und in den Annahmen umgeht, weißt Du doch schon:
+`rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`.
"
Conclusion
-"**Du** Ok, das scheint ihn zufriedenzustellen. One to go … Kannst Du mir vorher noch einmal kurz alles Leanish zusammenfassen, das Du mir bis hierher beigebracht hast?
+"**Du** Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele…
+Kannst Du mir vorher noch einmal kurz alles Leansch zusammenfassen,
+das Du mir bis hierher beigebracht hast?
-Robo straht überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
+Robo strahlt überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
**Robo** Na klar, schau her!
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index d5d7826..eb689d2 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -41,7 +41,7 @@ Statement ""
assumption
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
"**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
@@ -60,7 +60,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
-- TODO: Hint nur Anhand der Annahmen?
@@ -71,7 +71,7 @@ Conclusion
"
**Robo** Bravo! Jetzt aber nichts wie weg hier, bevor sich eine neue Schlange bildet!
-Logisinde ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
+Königin *Logisinde* ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
"
NewTactics left right assumption constructor rcases rfl contradiction trivial
diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean
index c98339c..8bd7a6c 100644
--- a/server/testgame/TestGame/TacticDocs.lean
+++ b/server/testgame/TestGame/TacticDocs.lean
@@ -115,6 +115,13 @@ TacticDoc simp_rw
TODO
"
+TacticDoc by_cases
+"
+## Beschreibung
+
+TODO
+"
+
TacticDoc apply
"
## Beschreibung