From 01199c379312423ab05155fbb538fb2b2c40f8c7 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Tue, 7 Mar 2023 17:13:32 +0100
Subject: [PATCH] levels Function

---
 server/testgame/TestGame/LemmaDocs.lean       | 37 +++++++++
 server/testgame/TestGame/Levels/Function.lean |  1 +
 .../Levels/Function/L06_Piecewise.lean        |  5 +-
 .../Levels/Function/L07'_Injective.lean       | 79 +++++++++++++++++++
 .../Levels/Function/L07_Injective.lean        | 30 +++++--
 .../Levels/Function/L08_Injective.lean        | 73 +++++++++++++++--
 .../Levels/Function/L09_Surjective.lean       |  2 +-
 .../Levels/Function/L10_Bijective.lean        |  2 +-
 8 files changed, 210 insertions(+), 19 deletions(-)
 create mode 100644 server/testgame/TestGame/Levels/Function/L07'_Injective.lean

diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index a03f990..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`"
 
@@ -141,3 +169,12 @@ 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/L06_Piecewise.lean b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
index 4a793b8..97bbfcd 100644
--- a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
+++ b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
@@ -171,6 +171,9 @@ geschrieben hast."
 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."
-#check Set.piecewise
+
+Conclusion
+"Zufrieden tauschen die beiden Wächter ihren Platz und geben so dabei den
+Durchgang frei."
 
 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 ""