From 4ae7e0eab652580db6f81adbcdcabf73162ea1bb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 29 Mar 2023 15:37:21 +0200 Subject: [PATCH] levels --- server/adam/Adam.lean | 27 ++++ server/adam/Adam/DefinitionDocs.lean | 87 ++++++++++++ server/adam/Adam/LemmaDocs.lean | 132 ++++++------------ .../adam/Adam/Levels/Implication/L06_Iff.lean | 4 +- .../Levels/SetTheory/L04_SubsetEmpty.lean | 31 ++-- .../adam/Adam/Levels/SetTheory/L05_Empty.lean | 24 +--- .../Adam/Levels/SetTheory/L06_Nonempty.lean | 8 +- .../Adam/Levels/SetTheory/L08_UnionInter.lean | 1 + server/adam/Adam/Metadata.lean | 1 + 9 files changed, 179 insertions(+), 136 deletions(-) create mode 100644 server/adam/Adam/DefinitionDocs.lean diff --git a/server/adam/Adam.lean b/server/adam/Adam.lean index 2f5351d..39fd5ae 100644 --- a/server/adam/Adam.lean +++ b/server/adam/Adam.lean @@ -23,6 +23,33 @@ Game "Adam" Title "Lean 4 game" Introduction " + +# Game Over oder QED? + +Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du Computer-gestütztes +Beweisen. Das Interface ist anfangs etwas vereinfacht, der \"Editor Mode\" funktioniert aber +ziemlich gleich wie wenn du später Lean im VSCode benützt. + +Rechts siehst du eine Übersicht der Welt dieses Spiels. Jeder Planet hat mehrere Levels, +die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden dann grün. + +Klicke auf die erste Welt \"Aussagenlogik 1\" um deine Reise zu starten. + +### Spielstand + +Dein Spielstand wird lokal in deinem Browser als \"site data\" gespeichert. +Solltest du diese löschen, verlierst du deinen Spielstand! Du kannst aber jederzeit jeden +Level spielen, auch wenn frühere Levels nicht grün sind. + +(oft werden *Site data & Cookies* zusammen gelöscht). + +### Kontakt + +Wenn du Bugs findest, schreib doch ein Email oder erstelle einen +[Issue auf Github](https://github.com/leanprover-community/lean4game/issues). + +Jon Eugster, jon.eugster@hhu.de + " Conclusion diff --git a/server/adam/Adam/DefinitionDocs.lean b/server/adam/Adam/DefinitionDocs.lean new file mode 100644 index 0000000..173e4c2 --- /dev/null +++ b/server/adam/Adam/DefinitionDocs.lean @@ -0,0 +1,87 @@ +import GameServer.Commands + +/-! ## Definitions -/ + +DefinitionDoc Even as "Even" +" +`even n` ist definiert als `∃ r, a = 2 * r`. +Die Definition kann man mit `unfold even at *` einsetzen. +## Eigenschaften + +* Mathlib Doc: [#Even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Even)" + +DefinitionDoc Odd as "Odd" +" +`odd n` ist definiert als `∃ r, a = 2 * r + 1`. +Die Definition kann man mit `unfold odd at *` einsetzen. + +* Mathlib Doc: [Odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd)" + +DefinitionDoc Injective as "Injective" +" +`Injective f` ist definiert als + +``` +∀ a b, f a = f b → a = b +``` +definiert. + +* Mathlib Doc: [Injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Injective)" + +DefinitionDoc Surjective as "Surjective" +" +`Surjective f` ist definiert als + +``` +∀ a, (∃ b, f a = b) +``` + +* Mathlib Doc: [Surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Surjective)" + +DefinitionDoc Bijective as "Bijective" +" + +## Eigenschaften + +* Mathlib Doc: [#Bijective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Bijective) +" + +DefinitionDoc LeftInverse as "LeftInverse" +" + +## Eigenschaften + +* Mathlib Doc: [#LeftInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.LeftInverse) +" + +DefinitionDoc RightInverse as "RightInverse" +" + +## Eigenschaften + +* Mathlib Doc: [#RightInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Logic.html#RightInverse) +" + +DefinitionDoc StrictMono as "StrictMono" +" +`StrictMono f` ist definiert als + +``` +∀ a b, a < b → f a < f b +``` + +## Eigenschaften + +* Mathlib Doc: [#StrictMono](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono) + +" + +DefinitionDoc Symbol.Subset as "⊆" " + +Auf Mengen (`Set`) ist `A ⊆ B` als `∀x, x ∈ A → x ∈ B` implementiert. +" + +DefinitionDoc Set.Nonempty as "Nonempty" " + +`A.Nonemty` ist als `∃ x, x ∈ A` definiert. +" diff --git a/server/adam/Adam/LemmaDocs.lean b/server/adam/Adam/LemmaDocs.lean index 2166bd9..2f0d34c 100644 --- a/server/adam/Adam/LemmaDocs.lean +++ b/server/adam/Adam/LemmaDocs.lean @@ -165,7 +165,7 @@ Jedes Element ist in `univ`, der Menge aller Elemente eines Typs `α`. * Mathlib Doc: [#mem_univ](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.mem_univ) " -LemmaDoc not_mem_empty as "not_mem_empty" in "Set" +LemmaDoc Set.not_mem_empty as "not_mem_empty" in "Set" " `Set.not_mem_empty {α : Type _} (x : α) : x ∉ ∅` @@ -175,11 +175,21 @@ Kein Element ist in der leeren Menge. * `simp`-Lemma: Nein * Namespace: `Set` -* Minimal Import: `Mathlib.Data.Set.Basic` * Mathlib Doc: [#not_mem_empty](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.not_mem_empty) " -LemmaDoc empty_subset as "empty_subset" in "Set" +LemmaDoc Set.subset_empty_iff as "subset_empty_iff" in "Set" +" +`Set.subset_empty_iff.{u} {α : Type u} {s : Set α} : s ⊆ ∅ ↔ s = ∅` + +## Eigenschaften + +* `simp`-Lemma: Nein +* Namespace: `Set` +* Mathlib Doc: [#empty_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.subset_empty_iff) +" + +LemmaDoc Set.empty_subset as "empty_subset" in "Set" " `Set.empty_subset {α : Type u} (s : Set α) : ∅ ⊆ s` @@ -187,11 +197,10 @@ LemmaDoc empty_subset as "empty_subset" in "Set" * `simp`-Lemma: Ja * Namespace: `Set` -* Minimal Import: `Mathlib.Data.Set.Basic` * Mathlib Doc: [#empty_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.empty_subset) " -LemmaDoc Subset.antisymm as "Subset.antisymm" in "Set" +LemmaDoc Set.Subset.antisymm as "Subset.antisymm" in "Set" " `Set.Subset.antisymm {α : Type u} {a : Set α} {b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b` @@ -212,7 +221,7 @@ für die Iff-Version. * Mathlib Doc: [#Subset.antisymm](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm) " -LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set" +LemmaDoc Set.Subset.antisymm_iff as "Subset.antisymm_iff" in "Set" " `Set.Subset.antisymm_iff {α : Type u} {a : Set α} {b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a` @@ -234,6 +243,17 @@ für eine verwandte Version. * Mathlib Doc: [#Subset.antisymm_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm_iff) " +LemmaDoc Set.diff_inter as "union_assoc" in "Set" +"" + +LemmaDoc Set.union_assoc as "union_assoc" in "Set" +"" + +LemmaDoc Set.union_diff_distrib as "union_diff_distrib" in "Set" +"" + +LemmaDoc Set.univ_union as "univ_union" in "Set" +"" LemmaDoc Nat.prime_def_lt'' as "prime_def_lt''" in "Nat" " @@ -249,7 +269,6 @@ Die bekannte Definition einer Primmzahl in `ℕ`: Eine Zahl (`p ≥ 2`) mit gena * Mathlib Doc: [#Nat.prime_def_lt''](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html#Nat.prime_def_lt'') " - LemmaDoc Finset.sum_add_distrib as "sum_add_distrib" in "Sum" " @@ -280,6 +299,22 @@ LemmaDoc Nat.succ_eq_add_one as "succ_eq_add_one" in "Sum" * Mathlib Doc: [#succ_eq_add_one](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Basic.html#Nat.succ_eq_add_one) " +LemmaDoc ne_eq as "ne_eq" in "Logic" +" + +## Eigenschaften + +* Mathlib Doc: [#ne_eq](https://leanprover-community.github.io/mathlib4_docs/Init/SimpLemmas.html#ne_eq) +" + +LemmaDoc Set.eq_empty_iff_forall_not_mem as "eq_empty_iff_forall_not_mem" in "Sum" +" + +## Eigenschaften + +* Mathlib Doc: [#eq_empty_iff_forall_not_mem](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.eq_empty_iff_forall_not_mem) +" + LemmaDoc Nat.zero_eq as "zero_eq" in "Sum" " @@ -429,86 +464,3 @@ LemmaDoc Iff.symm as "Iff.symm" in "Logic" * Mathlib Doc: [#Iff.symm](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff.symm) " - - - -/-! ## Definitions -/ - -DefinitionDoc Even as "Even" -" -`even n` ist definiert als `∃ r, a = 2 * r`. -Die Definition kann man mit `unfold even at *` einsetzen. -## Eigenschaften - -* Mathlib Doc: [#Even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Even)" - -DefinitionDoc Odd as "Odd" -" -`odd n` ist definiert als `∃ r, a = 2 * r + 1`. -Die Definition kann man mit `unfold odd at *` einsetzen. - -* Mathlib Doc: [Odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd)" - -DefinitionDoc Injective as "Injective" -" -`Injective f` ist definiert als - -``` -∀ a b, f a = f b → a = b -``` -definiert. - -* Mathlib Doc: [Injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Injective)" - -DefinitionDoc Surjective as "Surjective" -" -`Surjective f` ist definiert als - -``` -∀ a, (∃ b, f a = b) -``` - -* Mathlib Doc: [Surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Surjective)" - -DefinitionDoc Bijective as "Bijective" -" - -## Eigenschaften - -* Mathlib Doc: [#Bijective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Bijective) -" - -DefinitionDoc LeftInverse as "LeftInverse" -" - -## Eigenschaften - -* Mathlib Doc: [#LeftInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.LeftInverse) -" - -DefinitionDoc RightInverse as "RightInverse" -" - -## Eigenschaften - -* Mathlib Doc: [#RightInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Logic.html#RightInverse) -" - -DefinitionDoc StrictMono as "StrictMono" -" -`StrictMono f` ist definiert als - -``` -∀ a b, a < b → f a < f b -``` - -## Eigenschaften - -* Mathlib Doc: [#StrictMono](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono) - -" - -DefinitionDoc Symbol.Subset as "⊆" " - -Auf Mengen (`Set`) ist `A ⊆ B` als `∀x, x ∈ A → x ∈ B` implementiert. -" diff --git a/server/adam/Adam/Levels/Implication/L06_Iff.lean b/server/adam/Adam/Levels/Implication/L06_Iff.lean index 3941d32..40602d0 100644 --- a/server/adam/Adam/Levels/Implication/L06_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L06_Iff.lean @@ -29,8 +29,8 @@ Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by Conclusion " -**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen, -hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`. +**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheißen, +hier bei `(h : A ↔ B)` heißen sie `h.mp` und `h.mpr`. **Du**: Also `h.mp` ist `A → B`? Wieso `mp`? diff --git a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean index 9889ea6..07c6ed5 100644 --- a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean +++ b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean @@ -29,21 +29,8 @@ Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei aufteilen. " -namespace MySet - open Set Subset --- Copied some lemmas from `Matlib.Data.Set.Basic` in order to not import the entire file. -theorem tmp {α : Type _} {s t : Set α} : s = t → s ⊆ t := - fun h₁ _ h₂ => by rw [← h₁] ; exact h₂ - -theorem Subset.antisymm_iff {α : Type _} {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a := - ⟨fun e => ⟨tmp e, tmp e.symm⟩, fun ⟨h₁, h₂⟩ => Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩⟩ - -@[simp] -theorem empty_subset {α : Type _} (s : Set α) : ∅ ⊆ s := - fun. - Statement subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge. @@ -53,16 +40,16 @@ Statement subset_empty_iff {A : Type _} (s : Set A) : Hint (hidden := true) "**Robo**: Fang doch einmal mit `constructor` an." constructor intro h - Hint "**Robo**: " + Hint "**Robo**: Gleichheit zwischen Mengen kann man zum Beispiel zeigen, + indem man `A ⊆ B` und `B ⊆ A` zeigt. + + Dieser Schritt ist `apply Subset.antisymm`" apply Subset.antisymm assumption - simp only [empty_subset] - intro a - rw [Subset.antisymm_iff] at a - rcases a with ⟨h₁, h₂⟩ - assumption + Hint "**Robo**: Hier ist das Lemma `empty_subset` hilfreich." + apply empty_subset + intro h + rw [h] DisabledTactic tauto -NewLemma Subset.antisymm Subset.antisymm_iff empty_subset - -end MySet +NewLemma Set.Subset.antisymm Set.Subset.antisymm_iff Set.empty_subset diff --git a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean index f284019..cc79f4c 100644 --- a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean @@ -12,39 +12,23 @@ Game "Adam" World "SetTheory" Level 5 -Title "Nonempty" +Title "Empty" Introduction " -Das Gegenteil von `A = ∅` ist `A ≠ ∅`, aber in Lean wird der Ausdruck `A.Nonempty` bevorzugt. -Dieser ist dadurch existiert, dass in `A` ein Element existiert: `∃x, x ∈ A`. - -Zeige dass die beiden Ausdrücke äquivalent sind: +Zeige folgendes Lemma, welches wir gleich brauchen werden: " -namespace MySet - open Set -theorem subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by - constructor - intro h - rw [Subset.antisymm_iff] - constructor - assumption - simp only [empty_subset] - intro a - rw [Subset.antisymm_iff] at a - rcases a with ⟨h₁, h₂⟩ - assumption Statement eq_empty_iff_forall_not_mem "" {A : Type _} (s : Set A) : s = ∅ ↔ ∀ x, x ∉ s := by + Hint "Das Lemma `subset_empty_iff` von letzter Aufgabe könnte hilfreich sein." rw [←subset_empty_iff] rfl -- This is quite a miracle :) NewTactic constructor intro rw assumption rcases simp tauto trivial - -end MySet +NewLemma Set.subset_empty_iff diff --git a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean index a55b084..34d3bd8 100644 --- a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean +++ b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean @@ -25,9 +25,13 @@ Statement nonempty_iff_ne_empty "" {A : Type _} (s : Set A) : s.Nonempty ↔ s ≠ ∅ := by - rw [Set.Nonempty] + Hint "Am besten fängst du mit `unfold Set.Nonempty` an." + unfold Set.Nonempty + Hint "Mit `ne_eq` und `eq_empty_iff_forall_not_mem` kannst du hier weiterkommen." rw [ne_eq, eq_empty_iff_forall_not_mem] + Hint (hidden := true) "`push_neg` kann hier helfen." push_neg rfl -NewTactic constructor intro rw assumption rcases simp tauto trivial +NewLemma ne_eq Set.eq_empty_iff_forall_not_mem +NewDefinition Set.Nonempty diff --git a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean index 072434b..de62fb8 100644 --- a/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean +++ b/server/adam/Adam/Levels/SetTheory/L08_UnionInter.lean @@ -31,3 +31,4 @@ Statement rw [univ_union] NewTactic constructor intro rw assumption rcases simp tauto trivial +NewLemma Set.diff_inter Set.union_assoc Set.union_diff_distrib Set.univ_union diff --git a/server/adam/Adam/Metadata.lean b/server/adam/Adam/Metadata.lean index e0f2b52..35a7bab 100644 --- a/server/adam/Adam/Metadata.lean +++ b/server/adam/Adam/Metadata.lean @@ -1,4 +1,5 @@ import GameServer.Commands import Adam.TacticDocs import Adam.LemmaDocs +import Adam.DefinitionDocs import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.