From a4cb28df7b033b24d93444a4a3d43cef334ea163 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Mon, 10 Apr 2023 14:01:53 +0200
Subject: [PATCH] level

---
 server/adam/Adam/Doc/Definitions.lean         | 12 ++++
 server/adam/Adam/Levels/Inequality.lean       |  3 +-
 .../Adam/Levels/Inequality/L04_Linarith.lean  |  4 +-
 .../Inequality/L05_DrinkersParadox.lean       | 62 +++++++++++++++++++
 4 files changed, 77 insertions(+), 4 deletions(-)
 create mode 100644 server/adam/Adam/Levels/Inequality/L05_DrinkersParadox.lean

diff --git a/server/adam/Adam/Doc/Definitions.lean b/server/adam/Adam/Doc/Definitions.lean
index 17b3cae..3d4084c 100644
--- a/server/adam/Adam/Doc/Definitions.lean
+++ b/server/adam/Adam/Doc/Definitions.lean
@@ -110,3 +110,15 @@ wie andere Objekte verwenden.
 
 Note: `=>` wird in mathlib oft auch `↦` (`\\maps`) geschrieben.
 "
+
+DefinitionDoc Inhabited as "Inhabited" "
+`Inhabited U` ist eine Instanz, die aussagt, dass `U` mindestens ein Element
+enthält.
+
+Hat man eine solche Instanz, kann man immer das Element `(default : U)` verwenden.
+
+Was `default` genau ist hängt davon ab, wie `Inhabited U` bewiesen wurde. Es könnte
+also alles sein und man sollte sich nicht darauf verlassen, dass `default` eine
+bestimmte Eigenschaft hat. Z.B. ist `(default : ℕ) = 0` aber es hätte genau so gut
+als `1` oder `2` definiert werden können.
+"
diff --git a/server/adam/Adam/Levels/Inequality.lean b/server/adam/Adam/Levels/Inequality.lean
index d136814..18eb423 100644
--- a/server/adam/Adam/Levels/Inequality.lean
+++ b/server/adam/Adam/Levels/Inequality.lean
@@ -2,10 +2,11 @@ import Adam.Levels.Inequality.L01_LE
 import Adam.Levels.Inequality.L02_Pos
 import Adam.Levels.Inequality.L03_Linarith
 import Adam.Levels.Inequality.L04_Linarith
+import Adam.Levels.Inequality.L05_DrinkersParadox
 
 Game "Adam"
 World "Inequality"
-Title "Ungleichung"
+Title "Traum"
 
 Introduction "
 Später erinnerst du dich gar nicht mehr wo und wann du diese Unterhaltung hattest, geschweige
diff --git a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
index 6a8b886..c51e9c2 100644
--- a/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
+++ b/server/adam/Adam/Levels/Inequality/L04_Linarith.lean
@@ -24,6 +24,4 @@ $$
 Statement (x y : ℤ) (h₂ : 5 * y ≤ 35 - 2 * x) (h₃ : 2 * y ≤ x + 3) : y ≤ 5 := by
   linarith
 
-Conclusion "**Du**: Boah, das ist schon gar nicht schlecht.
-
-Und damit endet auch deine Erinnerung und wer weiss was du anschließend gemacht hast…"
+Conclusion "**Du**: Boah, das ist schon gar nicht schlecht."
diff --git a/server/adam/Adam/Levels/Inequality/L05_DrinkersParadox.lean b/server/adam/Adam/Levels/Inequality/L05_DrinkersParadox.lean
new file mode 100644
index 0000000..9089578
--- /dev/null
+++ b/server/adam/Adam/Levels/Inequality/L05_DrinkersParadox.lean
@@ -0,0 +1,62 @@
+import Adam.Metadata
+
+import Adam.Options.MathlibPart
+
+Game "Adam"
+World "Inequality"
+Level 5
+
+Title "Drinker's Paradox"
+
+set_option tactic.hygienic false
+
+Introduction
+"
+**weitere Person**: Jetzt aber zu einem anderen Thema. Kennt ihr eigentlich das
+Drinker-Paradoxon?
+
+**Robo**: Das ist in meinem System. *In dieser Bar gibt es eine Person, so dass
+falls diese Person jetzt am drinken ist, dann sind alle am trinken*.
+
+**weitere Person**: Genau! Könnt ihr mir das beweisen?
+"
+
+open Function
+
+Statement {People : Type} [Inhabited People] (isDrinking : People → Prop) :
+    ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by
+  Hint "**Du**: Wenn `p` eine Person ist, dann ist also `isDrinking p` eine Aussage,
+  die wahr oder falsch ist. Soweit so gut.
+  Wieso hat er aber `Inhabited People` hinzugefügt?
+
+  **Robo**: Die Aussage ist falsch, wenn die Bar leer wäre, da dann keine solche
+  Person existieren kann. Jedenfalls kannst du dadurch jederzeit `default`, oder lang
+  `(default : Person)`, schreiben, wenn du einfach irgendeine Person brauchst.
+
+  **Du**: Und wie fang ich jetzt an?
+
+  **Robo**: Du könntest eine Fallunterscheidung machen, ob die Aussage
+  `∀ (y : People), isDrinking y` wahr oder falsch ist."
+  Hint (hidden := true) "**Robo**: Schau mal `by_cases` an."
+  by_cases ∀ y, isDrinking y
+  Hint (hidden := true) "**Du**: Und wen nehm ich jetzt?
+
+  **Robo**: Wie gesagt, `default` ist eine x-beliebige Person."
+  use (default : People)
+  intro
+  assumption
+  Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen."
+  push_neg at h
+  rcases h with ⟨p, hp⟩
+  use p
+  intro hp'
+  Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?"
+  contradiction
+
+LemmaTab "Logic"
+NewDefinition Inhabited
+
+Conclusion
+"**weitere Person**: Fantastisch! Zum wohl!
+
+…und damit endet auch deine Erinnerung und wer weiss was du anschließend gemacht hast…"