levels: Function

server/testgame/TestGame.lean

@@ -36,6 +36,7 @@ Path LeanStuff → SetTheory → SetTheory2 → SetFunction
 
 Path Predicate → Prime → Induction
 Path Sum → Inequality → Induction
+Path Inequality → LeanStuff
 
 Path SetTheory2 → Numbers
 Path Module → Basis → Module2

server/testgame/TestGame/Levels/Function.lean

@@ -1,13 +1,23 @@
 import TestGame.Levels.Function.L01_Function
 import TestGame.Levels.Function.L02_Let
-import TestGame.Levels.Function.L03_Composition
+import TestGame.Levels.Function.L03_Piecewise
-import TestGame.Levels.Function.L06_Piecewise
+import TestGame.Levels.Function.L04_Injective
-import TestGame.Levels.Function.L07_Injective
+import TestGame.Levels.Function.L05_Injective
-import TestGame.Levels.Function.L07'_Injective
+import TestGame.Levels.Function.L06_Injective
-import TestGame.Levels.Function.L08_Injective
+import TestGame.Levels.Function.L07_Surjective
-import TestGame.Levels.Function.L09_Surjective
+import TestGame.Levels.Function.L08_Bijective
-import TestGame.Levels.Function.L10_Bijective
+import TestGame.Levels.Function.L09_Inverse
 
 Game "TestGame"
 World "Function"
 Title "Abbildungen"
+
+Introduction "
+Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf
+eine Insel komplett mit Wasser bedeckt zu sein scheint.
+
+Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,
+vereinzelte aus Lehm.
+
+Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt.
+"

server/testgame/TestGame/Levels/Function/L01_Function.lean

@@ -5,31 +5,59 @@ Game "TestGame"
 World "Function"
 Level 1
 
-Title ""
+Title "Anonyme Funktionen"
 
 Introduction
 "
-Funktionen werden in Lean mit `ℕ → ℕ` geschrieben (`\\to`), also dem gleichen
+Auf die Frage hin, ob sie von einem Bibliothek wisse, erzählt euch das kleine Mädchen,
-Pfeil wie Implikationen.
+dass es auf der Insel nur einen gäbe, aber sie bedrängt euch so mit einer Frage,
-
+dass sie euch gar nicht sagt, wo dieser zu finden sei.
-Eine abstrakte Funktion ist ein entsprechendes Element `(f : ℕ → ℕ)` oder `(g : ℕ → ℝ)`.
-Dies sagt aber gar nichts darüber, wie `f` tatsächlich definiert ist.
-
-Hat man eine Funktion `(f : A → B)` und ein Element `(x : A)` dann ist `f x` der
-Bildpunkt in `B`. In Lean braucht man also keine Klammern um $f(x)$ zu schreiben.
-
-Eplizite, anonyme Funktionen kann man mit dem Syntax `fun (n : ℕ) ↦ n ^ 2` definieren
-(entweder `↦` (`\\map`) oder `=>` als Pfeil in der Mitte).
 "
 
-Statement
+Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by
-"Zeige, dass es eine Funktion $\\mathbb{N} \\to \\mathbb{Z}$ gibt, für die $f(x) < x$ gilt."
-    : ∃ f : ℕ → ℤ, ∀ x, f x < x := by
   use (fun x ↦ x - 1)
   simp
 
-Hint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
+Hint : ∃ f : ℤ → ℤ, ∀ x, f x < x =>
 "
-Benütze eine anonyme Funktion `use (fun n ↦ _)` wobei `_` durch einen Ausdruck ersetzt
+**Robo**: `f : ℤ → ℤ` ist die Notation für eine Funktion und `f x` ist diese Funktion
-werden muss, so dass die Aussage erfüllt wird.
+angewendet auf ein Element `(x : ℤ)`.
+
+**Du**: War `→` nicht eben noch eine Implikation?
+
+**Robo**: Doch, die brauchen das gleiche Zeichen für beides.
+
+**Du**: Dann ist `f : ℤ → ℤ` also einfach abstrakt irgendeine Funktion,
+wie definier ich aber jetzt konkret eine Abbildungsvorschrift?
+
+**Robo**: Man kennt hier eine Notation für eine anonyme Funktion:
+`fun (x : ℤ) ↦ x ^ 2` ist
+
+$$
+\\begin\{aligned}
+  f : \\mathbb\{ℤ} &\\to \\mathbb\{ℤ} \\\\
+  x &\\mapsto x ^ 2
+\\end\{aligned}
+$$
+
+**Robo**: PS, `↦` ist `\\mapsto`. Aber man kann auch stattdessen `=>` benützen.
+"
+
+HiddenHint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
+"
+**Du**: Ja aber was mach ich damit?
+
+**Robo**: Wie immer gehst du ein `∃` mit `use …` an.
+"
+
+-- TODO: Why does this not show?
+HiddenHint : ∀ (x : ℤ), (fun (y : ℤ) => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+HiddenHint (x : ℤ) : (fun y => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+Conclusion "Das Mädchen wird kurz ruhig, dann beginnt es zu lächeln und zeigt strahlend
+in eine Richtung. Ihr folgt ihrem Finger und euch fällt in weiter ferne eine pompöse Struktur
+auf einem flachen Hügel auf.
 "

server/testgame/TestGame/Levels/Function/L02_Let.lean

@@ -5,72 +5,78 @@ Game "TestGame"
 World "Function"
 Level 2
 
-Title ""
+Title "let"
 
 Introduction
 "
-Ausserhalb eines Beweises kann man Funktionen mit `def`
+Ihr macht euch auf Richtung Bibliothek entlang kleiner Pfade zwischen verschiedenster Behausungen.
-(anstatt `lemma`/`example`/`theorem`) definieren:
+
+**Du**: Sag mal, ich weiss jetzt dass ich eine Funktion als `fun x ↦ x - 1` definieren kann,
+aber wie kann ich der einen Namen geben?
+
+**Robo**: Wenn jemand hier eine Funktion definiert, werden die dir
+`def f (x : ℤ) : ℤ := x - 1` oder `def f : ℤ → ℤ := (fun x ↦ x - 1)` geben.
+
+**Du**: Und das bedeutet beides das gleiche?
+
+**Robo**: Praktisch, ja. Aber! Wenn du eine Funktion in einer Aufgabe benennen willst,
+schreibst du `let f := fun (x : ℤ) ↦ x - 1`!
+
+**Du**: Und was ist der Unterschied?
+
+**Robo**: Deines mit `let` ist für innerhalb von einem Beweis, das andere mit `def`
+ist für ausserhalb von einem Beweis. Hier, ich geb dir mal eine Aufgabe:
 
 ```
-def f (x : ℚ) : ℚ := 1 / (1 + x^2)
+def f (x : ℤ) : ℤ := (x + 4)
-
-def f : ℚ → ℚ := fun x ↦ 1 / (1 + x^2)
 ```
-
+und:
-(die beiden Varianten sind äquivalent.)
-
-Um eine anonyme Funktion `fun x ↦ 1 / (1 + x^2)` **innerhalb** eines Beweis einem Namen
-zuzuordnen, benützt man `let`:
-
-```
-let f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
-```
-
-`def` und `let` funktionieren also fast gleich wie `lemma`/`example`/`theorem` und `have` mit
-einem wichtigen Unterschied:
-
-```
-have f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
-let f₂ : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
-```
-
-`have` vergisst sofort den \"Beweis\", das heisst, Lean weiss dann nur, dass es eine
-Funktion `(f : ℕ → ℕ)` gibt, aber nicht, wie diese definiert ist. `let` hingegen speichert
-die Definition der Funktion.
-
-Manchmal muss man Definitionen (von einem `def` oder `let` Statement) mit `unfold` einsetzen.
 "
 
-def f (x : ℤ) : ℤ := (x + 1) ^ 2
+def f (x : ℤ) : ℤ := (x + 4)
 
-Statement
+Statement "" (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by
-"
+  let g := fun (x : ℤ) ↦ x - 3
-Given the function
+  use g
-```
+  simp
-def f (x : ℤ) : ℤ := (x + 1) ^ 2
-```
-show that $f(x) = x^2 + 2x + 1$.
-
-"
-    : ∀ x, f x = x ^ 2 + 2 * x + 1 := by
-  intro x
   unfold f
   ring
 
 NewTactic «let»
-OnlyTactic «let» intro unfold ring
+NewLemma Function.comp_apply
 
-HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 =>
+Hint (x : ℤ) : ∃ g, (g ∘ f) x = x + 1 =>
-"Fang zuerst wie immer mit `intro x` an."
+"**Du**: Ist `g ∘ f` Komposition von Funktionen?
 
-Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
+**Robo**: Richtig! Das schreibt man mit `\\comp`.
-"
-Definitionen muss man manchmal manuell einsetzen um den Taktiken zu helfen.
 
-Das macht man mit `unfold f` (oder alternativ mit `rw [f]`).
+  **Du** Und hier könnte ich also zuerst
+`let g := fun (x : ℤ) ↦ _` definieren, anstatt direkt
+`use fun (x : ℤ) ↦ _`?
+
+**Robo**: Genau! Das ist zwar praktisch das gleiche, aber kann manchmal nützlich sein.
 "
 
-HiddenHint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
+-- TODO: Make some hints work here
-"
+Hint (x : ℤ) : ((fun (x : ℤ) ↦ x - 3) ∘ f) x = x + 1 =>
-Nachdem die Definition von `f` eingesetzt ist, übernimmt `ring` den Rest"
+"**Robo**: Manchmal must du nachhelfen und Funktionen mit `unfold f` öffnen, manchmal nicht.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO : Make this work
+Hint (x : ℤ) (g := (fun (x : ℤ) ↦ x - 3)) : (g ∘ f) x = x + 1 =>
+"**Robo**: `(g ∘ f) x` ist per Definition `g (f x)`, aber mit
+`rw [Function.comp_apply]` kann man das explizit umschreiben, aber `simp` kennt das
+Lemma auch."
+
+Hint (x : ℤ) : f x - 3 = x + 1 =>
+"**Robo**: Manchmal must du nachhelfen und Definitionen mit `unfold f` öffnen, mamchmal klappts
+ohne.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO: Block simp-Lemma
+
+Conclusion "**Du**: Dann verstehst du etwas Mathe?
+
+**Robo**: Ich hatte ja keine Ahnung ob die generierte Aufgabe beweisbar ist…
+
+Und damit erreicht ihr den Hügel mit der Bibliothek."

server/testgame/TestGame/Levels/Function/L03_Composition.lean

@@ -1,22 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Function"
-Level 3
-
-Title ""
-
-Introduction
-"
-Komposition von Funktionen kann als `g ∘ f` geschrieben werden.
-
-TODO
-"
-
-Statement
-"TODO: Find an exercise."
-    (U T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x)  := by
-  simp only [Function.comp_apply]
-
-NewLemma Function.comp_apply

server/testgame/TestGame/Levels/Function/L03_Piecewise.lean

@@ -3,13 +3,14 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 4
+Level 3
 
-Title ""
+Title "Komposition"
 
 Introduction
 "
-Du kommst an eine Tür mit zwei Wächtern. Der eine hat ein Schild
+Endlich kommt ihr zur Bibliothek. Komischerweise stehen an der Tür
+zwei Wächtern. Der eine zeigt euch ein Blatt mit
 
 ```
 def f : ℚ → ℚ := fun x ↦ 5 * x
@@ -21,11 +22,9 @@ der andere eines mit
 def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
 ```
 
-Auf der Tür steht groß:
+und gibt Dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
 "
 
-example (P : Prop) [Decidable P] (a b : ℕ) (h : P) : ite P a b = a := if_pos h
-
 open Set
 
 namespace LevelFunction4
@@ -33,11 +32,6 @@ 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
@@ -72,6 +66,7 @@ Hint : f ∘ g = g ∘ f =>
 dann für dieses.
 "
 
+-- TODO : This does not trigger.
 -- 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 =>
@@ -92,12 +87,15 @@ 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`.
+eine neue Annahme `0 ≤ f x`.
+
+**Du**: Also `have h₂ : _`?
 "
 
 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,
+**Du**: Mit den beiden Annahmen sagt die Definition von `g` ja z.B.
+`(if 0 ≤ x then _)` wobei ich weiss dass `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

server/testgame/TestGame/Levels/Function/L04_Injective.lean

@@ -3,13 +3,13 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 5
+Level 4
 
 Title ""
 
 Introduction
 "
-Ihr läuft durch verschiedenste Leere Gänge des Funktionentempels.
+Ihr läuft durch verschiedenste Gänge der Bibliothek, allesamt mit Büchern entlang der Wände.
 
 **Du**: Wenn wir wüssten, dass nur ein möglicher Weg hierhin führt, könnten wir
 ausschliessen, dass wir im Kreis laufen.

server/testgame/TestGame/Levels/Function/L05_Injective.lean

@@ -5,7 +5,7 @@ set_option tactic.hygienic false
 
 Game "TestGame"
 World "Function"
-Level 6
+Level 5
 
 Title ""
 
@@ -76,4 +76,4 @@ Hint (a b : ℤ) (h : a ^ 3 + (a + 3) = b ^ 3 + (b + 3)) : a = b =>
 
 Conclusion "**Du**: Danke vielmals!
 
-Und ihr läst das Wesen mit im Gang stehen weiter über Injectivität nachdenkend."
+Und damit lässt das Wesen mitten im Gang stehen, wo es weiter über Injektivität nachdenkt."

server/testgame/TestGame/Levels/Function/L06_Injective.lean

@@ -3,7 +3,7 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 7
+Level 6
 
 Title "Injektive"
 
@@ -13,13 +13,13 @@ 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:
+Ein paar Schritte in den linken Korridor hinein seht ihr auf dem Boden ein Blatt mit Gekritzel:
 
 ```
 def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
 ```
 
-**Du**: Hier haben wir eine stückweis definierte Funktion
+**Du**: Hier haben wir wieder eine stückweise Funktion
 
 $$
 f(n) = \\begin{cases}

server/testgame/TestGame/Levels/Function/L07_Surjective.lean

@@ -3,7 +3,7 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 8
+Level 7
 
 Title "Surjektive"
 

server/testgame/TestGame/Levels/Function/L08_Bijective.lean

@@ -3,7 +3,7 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 9
+Level 8
 
 Title ""
 
@@ -26,7 +26,7 @@ Statement "" : Bijective (fun (n : ℤ) ↦ n + 1) := by
   simp
 
 Hint : Bijective (fun (n : ℤ) ↦ n + 1) =>
-"**Robo** *(flüsternd)**: `Bijectve f` ist als `Injective f ∧ Surjective f` definiert.
+"**Robo** *(flüsternd)*: `Bijectve f` ist als `Injective f ∧ Surjective f` definiert.
 
 **Du**: Dann ist das ja ganz simpel!
 "

server/testgame/TestGame/Levels/Function/L09_Inverse.lean

@@ -3,7 +3,7 @@ import Mathlib
 
 Game "TestGame"
 World "Function"
-Level 10
+Level 9
 
 Title "Inverse"
 
@@ -19,6 +19,7 @@ aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
 
 open Function
 
+--TODO: This is a really hard proof
 Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
     Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
   constructor
@@ -53,7 +54,7 @@ Hint {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ Rig
 ich ja schon."
 
 Conclusion
-"Endlich entkommt ihr dem Tempel.
+"Endlich entkommt ihr der Bibliothek.
 
 **Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!