From 404f346920cc760a4d1882438d9444a54a6a4bbb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 2 Feb 2023 14:44:58 +0100 Subject: [PATCH] set theory levels --- server/testgame/TestGame.lean | 21 +- server/testgame/TestGame/LemmaDocs.lean | 20 ++ .../Levels/Contradiction/L03_ByContra.lean | 4 +- .../Levels/Induction/L10_Bernoulli.lean | 3 +- .../TestGame/Levels/Induction/T00_Sum.lean | 25 ++ .../Levels/Induction/T01_Induction.lean | 24 ++ .../Levels/Induction/T02_Induction.lean | 24 ++ .../Levels/Induction/T03_SumComm.lean | 34 +++ .../testgame/TestGame/Levels/Proposition.lean | 1 + .../Levels/Proposition/L00_Tauto.lean | 51 ++++ .../TestGame/Levels/Proposition/L01_Rfl.lean | 20 +- .../Levels/Proposition/L02_Assumption.lean | 2 +- .../Levels/Proposition/L03_Assumption.lean | 2 +- .../TestGame/Levels/Proposition/L04_True.lean | 2 +- .../TestGame/Levels/Proposition/L05_Not.lean | 2 +- .../Levels/Proposition/L06_False.lean | 2 +- .../Levels/Proposition/L07_ContraNotEq.lean | 2 +- .../Levels/Proposition/L08_Contra.lean | 2 +- .../TestGame/Levels/Proposition/L09_And.lean | 2 +- .../TestGame/Levels/Proposition/L10_And.lean | 2 +- .../TestGame/Levels/Proposition/L11_Or.lean | 2 +- .../TestGame/Levels/Proposition/L12_Or.lean | 2 +- .../Levels/Proposition/L13_Summary.lean | 2 +- .../testgame/TestGame/Levels/SetTheory.lean | 25 +- .../TestGame/Levels/SetTheory/L01_Univ.lean | 42 +++ .../TestGame/Levels/SetTheory/L02_Empty.lean | 29 ++ .../TestGame/Levels/SetTheory/L03_Subset.lean | 45 ++++ .../Levels/SetTheory/L04_SubsetEmpty.lean | 61 +++++ .../TestGame/Levels/SetTheory/L05_Empty.lean | 52 ++++ .../Levels/SetTheory/L06_Nonempty.lean | 35 +++ .../Levels/SetTheory/L07_UnionInter.lean | 31 +++ .../Levels/SetTheory/L08_UnionInter.lean | 35 +++ .../Levels/SetTheory/L09_Complement.lean | 35 +++ .../TestGame/Levels/SetTheory/L10_Morgan.lean | 58 ++++ .../Levels/SetTheory/L11_SSubset.lean | 38 +++ .../TestGame/Levels/SetTheory/L12_Insert.lean | 37 +++ .../TestGame/Levels/SetTheory/L13_Insert.lean | 39 +++ .../TestGame/Levels/SetTheory/L14_SetOf.lean | 37 +++ .../Levels/SetTheory/L15_Powerset.lean | 42 +++ .../Levels/SetTheory/L16_Disjoint.lean | 41 +++ .../TestGame/Levels/SetTheory/L17_SetOf.lean | 39 +++ .../TestGame/Levels/SetTheory/L18_SetOf.lean | 33 +++ .../Levels/SetTheory/L19_Subtype.lean | 28 ++ .../Levels/SetTheory/L20_UnionInter.lean | 27 ++ .../Levels/SetTheory/L21_Summary.lean | 28 ++ .../Levels/SetTheory/PowersetPlayground.lean | 109 ++++++++ .../TestGame/Levels/SetTheory/T01_Set.lean | 250 ++++++++++++++++++ .../TestGame/Levels/SetTheory/T04_xx.lean | 96 +++++++ server/testgame/TestGame/TacticDocs.lean | 13 + server/testgame/TestGame/ToBePorted.lean | 70 +++++ server/testgame/lake-manifest.json | 10 +- server/testgame/lakefile.lean | 3 + 52 files changed, 1602 insertions(+), 37 deletions(-) create mode 100644 server/testgame/TestGame/Levels/Induction/T00_Sum.lean create mode 100644 server/testgame/TestGame/Levels/Induction/T01_Induction.lean create mode 100644 server/testgame/TestGame/Levels/Induction/T02_Induction.lean create mode 100644 server/testgame/TestGame/Levels/Induction/T03_SumComm.lean create mode 100644 server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean create mode 100644 server/testgame/TestGame/Levels/SetTheory/T04_xx.lean diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index ed7652c..246233a 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -17,10 +17,25 @@ import TestGame.Levels.SetFunction Game "TestGame" Title "Lean 4 game" Introduction -"Work in progress. +" +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. " Conclusion -"There is nothing else so far. Thanks for rescuing natural numbers!" +"Fertig!" Path Proposition → Implication → Predicate → Contradiction → LeanStuff @@ -28,3 +43,5 @@ Path Proposition → Implication → Predicate → Contradiction → LeanStuff Path Predicate → Induction → LeanStuff → Function → SetFunction Path LeanStuff → SetTheory → SetFunction + +Path SetTheory → SetTheory2 diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index c419646..0ad6627 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -77,6 +77,26 @@ LemmaDoc even_square as even_square in "Nat" "`∀ (n : ℕ), even n → even (n ^ 2)`" + + +LemmaDoc mem_univ as mem_univ in "Set" +"x ∈ @univ α" + +LemmaDoc not_mem_empty as not_mem_empty +"" + +LemmaDoc empty_subset as empty_subset in "Set" +"" + +LemmaDoc Subset.antisymm_iff as Subset.antisymm_iff in "Set" +"" + + + + + + + LemmaSet natural : "Natürliche Zahlen" := Even Odd not_odd not_even diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean index 3b4551b..17fadbf 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean @@ -31,11 +31,11 @@ steht: Statement "Angenommen $B$ ist falsch und es gilt $A \\Rightarrow B$. Zeige, dass $A$ falsch sein muss." - (A B : Prop) (h : A → B) (b : ¬ B) : ¬ A := by + (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by by_contra a suffices b : B contradiction - apply h + apply g assumption diff --git a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean index 20d6ed8..8828b15 100644 --- a/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean +++ b/server/testgame/TestGame/Levels/Induction/L10_Bernoulli.lean @@ -28,8 +28,7 @@ example (n : ℕ) : (∑ i : Fin (n + 1), ↑(2 * i - 1)) = n ^ 2 := by induction' n with n hn simp - - +#check Finset.sum_comm Statement "Zeige $\\sum_{i = 0}^n i = \\frac{n ⬝ (n + 1)}{2}$." diff --git a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean new file mode 100644 index 0000000..f6b3b58 --- /dev/null +++ b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean @@ -0,0 +1,25 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring +import Mathlib + +import TestGame.ToBePorted + +Game "TestGame" +World "Induction" +Level 3 + +Title "Induktion" + +Introduction +" +" + + +Statement +"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i^3)^2$." + (n : ℕ) : (∑ i : Fin (n + 1), (i : ℕ)^3) = (∑ i : Fin (n + 1), (i : ℕ))^2 := by + induction n + simp + sorry + +Tactics ring diff --git a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean new file mode 100644 index 0000000..2197ebe --- /dev/null +++ b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean @@ -0,0 +1,24 @@ +import Mathlib.Algebra.BigOperators.Basic +import Mathlib + +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Induction" +Level 2 + +Title "endliche Summe" + +Introduction +" +2^n > n^2 für n ≥ 5 +" + +Statement +"2^n > n^2 für n ≥ 5" + (n : ℕ) : True := by + sorry + +Tactics rw simp ring diff --git a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean new file mode 100644 index 0000000..cc0d2dd --- /dev/null +++ b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean @@ -0,0 +1,24 @@ +import Mathlib.Algebra.BigOperators.Basic +import Mathlib + +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Induction" +Level 2 + +Title "endliche Summe" + +Introduction +" +n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n +" + +Statement +"n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n" + (n : ℤ) : True := by + sorry + +Tactics rw simp ring diff --git a/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean new file mode 100644 index 0000000..f23163b --- /dev/null +++ b/server/testgame/TestGame/Levels/Induction/T03_SumComm.lean @@ -0,0 +1,34 @@ + +import Mathlib.Algebra.BigOperators.Basic +import Mathlib + +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Induction" +Level 1 + +Title "Simp" + +Introduction +" +" + +Statement +"" + (n : ℕ) : True := by + trivial + +Tactics simp + + +-- Σ_i Σ_j ... = Σ_j Σ_i ... +-- rw [sum_comm] +example : ¬ ∀ (x : ℕ), x ≥ 10 := by + push_neg + use 5 + simp + +¬ ∀ (...) ↔ ∃ (¬ ...) diff --git a/server/testgame/TestGame/Levels/Proposition.lean b/server/testgame/TestGame/Levels/Proposition.lean index 9e1b736..52058b7 100644 --- a/server/testgame/TestGame/Levels/Proposition.lean +++ b/server/testgame/TestGame/Levels/Proposition.lean @@ -1,3 +1,4 @@ +import TestGame.Levels.Proposition.L00_Tauto import TestGame.Levels.Proposition.L01_Rfl import TestGame.Levels.Proposition.L02_Assumption import TestGame.Levels.Proposition.L03_Assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean new file mode 100644 index 0000000..5824a91 --- /dev/null +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -0,0 +1,51 @@ +import TestGame.Metadata +import Mathlib.Tactic.Tauto + +Game "TestGame" +World "Proposition" +Level 1 + +Title "Atomatisierung" + +Introduction +" +Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer +unterstützt und verifiziert schreiben kann. + +*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am beweisen +bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals** +aufgelistet, diese musst du dann später auch noch zeigen. + +Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie +man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen, +andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der +Seite. + +Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\". + +Als erstes ein kleiner Preview, dass Lean auch vieles automatisch kann. So gibt es eine +Taktik `tauto`, die alle wahren Aussagen der Prädikaten-Logik beweisen kann. + +Dieses Beispiel würde von Hand etwas Zeit in Anspruch nehmen. Lean ist da viel schneller. + +Gib also `tauto` gefolgt von Enter ⏎ ein um deinen ersten automatisierten Beweis zu führen! +" + +Statement +"Zeige dass folgende Aussage wahr ist: + +$$ + \\neg ((\\neg B\\textrm{ oder }\\neg C) \\textrm{ oder } (A \\Rightarrow B)) \\Rightarrow + (\\neg A \\textrm{ oder } B) \\textrm{ und } \\neg (B \\textrm{ und } C) +$$ +" + (A B C : Prop) : + ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by + tauto + +HiddenHint (A : Prop) (B : Prop) (C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => +"Man schreibt eine Taktik pro Zeile, also gib `tauto` ein und geh mit Enter ⏎ auf eine neue Zeile." + +Conclusion "" + +Tactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 3e82469..2171491 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -2,29 +2,17 @@ import TestGame.Metadata Game "TestGame" World "Proposition" -Level 1 +Level 2 Title "Aller Anfang ist... ein Einzeiler?" Introduction " -Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer -unterstützt und verifiziert schreiben kann. - -*Rechts* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am beweisen -bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals** -aufgelistet, diese musst du dann später auch noch zeigen. - -Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie -man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen, -andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der -Seite. - -Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\". +Jetzt gehen wir aber einen Schritt zurück und lernen, wie man konkret mit Lean arbeitet, +damit du verstehst, was `tauto` hinter der Kulisse macht. Deine erste Taktik ist `rfl` (für \"reflexivity\"), welche dazu da ist, -ein Goal der Form $X = X$ zu schliessen. -Gib die Taktik ein gefolgt von Enter ⏎. +ein Goal der Form $X = X$ zu schließen. " Statement diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index 0bb2704..21fb31f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -2,7 +2,7 @@ import TestGame.Metadata Game "TestGame" World "Proposition" -Level 2 +Level 3 Title "Annahmen" diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index 9ffd29d..bb038f2 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -3,7 +3,7 @@ import Mathlib.Data.Nat.Basic -- TODO Game "TestGame" World "Proposition" -Level 3 +Level 4 Title "Logische Aussagen" diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index aa2a619..bbbac31 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -2,7 +2,7 @@ import TestGame.Metadata Game "TestGame" World "Proposition" -Level 4 +Level 5 Title "True/False" diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index fd47af5..0aaf9df 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -2,7 +2,7 @@ import TestGame.Metadata Game "TestGame" World "Proposition" -Level 5 +Level 6 Title "Not" diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 34cd0ac..990f282 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -4,7 +4,7 @@ import Mathlib.Tactic.LeftRight Game "TestGame" World "Proposition" -Level 6 +Level 7 Title "Widerspruch beweist alles." diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index deb195a..286dbc1 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -6,7 +6,7 @@ import TestGame.ToBePorted Game "TestGame" World "Proposition" -Level 7 +Level 8 Title "Widerspruch" diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index 5165426..e2ee09f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -6,7 +6,7 @@ import TestGame.ToBePorted Game "TestGame" World "Proposition" -Level 8 +Level 9 Title "Widerspruch" diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 3fe50d0..f33a175 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -5,7 +5,7 @@ set_option tactic.hygienic false Game "TestGame" World "Proposition" -Level 9 +Level 10 Title "Und" diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 461217f..fe85f6a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -5,7 +5,7 @@ set_option tactic.hygienic false Game "TestGame" World "Proposition" -Level 10 +Level 11 Title "Und" diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index 59a4e53..62d5147 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -6,7 +6,7 @@ import Mathlib.Tactic.LeftRight Game "TestGame" World "Proposition" -Level 11 +Level 12 Title "Oder" diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index 8bbb033..984d6a6 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -9,7 +9,7 @@ import Mathlib.Tactic.LeftRight Game "TestGame" World "Proposition" -Level 12 +Level 13 Title "Oder" diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index d0342bf..b05193a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -6,7 +6,7 @@ set_option tactic.hygienic false Game "TestGame" World "Proposition" -Level 13 +Level 14 Title "Zusammenfassung" diff --git a/server/testgame/TestGame/Levels/SetTheory.lean b/server/testgame/TestGame/Levels/SetTheory.lean index 88ec2ec..d1a3ed0 100644 --- a/server/testgame/TestGame/Levels/SetTheory.lean +++ b/server/testgame/TestGame/Levels/SetTheory.lean @@ -1,5 +1,28 @@ -import TestGame.Levels.SetTheory.T01_Set +import TestGame.Levels.SetTheory.L01_Univ +import TestGame.Levels.SetTheory.L02_Empty +import TestGame.Levels.SetTheory.L03_Subset +import TestGame.Levels.SetTheory.L04_SubsetEmpty +import TestGame.Levels.SetTheory.L05_Empty +import TestGame.Levels.SetTheory.L06_Nonempty +import TestGame.Levels.SetTheory.L07_UnionInter +import TestGame.Levels.SetTheory.L08_UnionInter +import TestGame.Levels.SetTheory.L09_Complement +import TestGame.Levels.SetTheory.L10_Morgan +import TestGame.Levels.SetTheory.L11_SSubset +import TestGame.Levels.SetTheory.L12_Insert +import TestGame.Levels.SetTheory.L13_Insert +import TestGame.Levels.SetTheory.L14_SetOf +import TestGame.Levels.SetTheory.L15_Powerset +import TestGame.Levels.SetTheory.L16_Disjoint +import TestGame.Levels.SetTheory.L17_SetOf +import TestGame.Levels.SetTheory.L18_SetOf +import TestGame.Levels.SetTheory.L19_Subtype + Game "TestGame" World "SetTheory" Title "Mengenlehre" + +Game "TestGame" +World "SetTheory2" +Title "Mehr Mengenlehre" diff --git a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean new file mode 100644 index 0000000..eb240e9 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean @@ -0,0 +1,42 @@ +import TestGame.Metadata + +import Mathlib.Init.Set +import Mathlib.Tactic.Tauto + +set_option tactic.hygienic false +set_option autoImplicit false + +Game "TestGame" +World "SetTheory" +Level 1 + +Title "Mengen" + +Introduction +" +In diesem Kapitel schauen wir uns Mengen an. + +Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst, +alle Elemente in einer Menge haben den gleichen Typ. + +Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine +Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben. + +Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus +`X`. `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied +zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht +austauschbar! + +Um zu beweisen, dass etwas in `univ` ist, kannst du verschiedenste deiner Taktiken anwenden, +zum Beispiel `tauto`. +" + +open Set + +Statement mem_univ + "4 ist ein Element der Menge aller natürlichen Zahlen." {A : Type _} (x : A) : + x ∈ (univ : Set A) := by + trivial + -- tauto + +Tactics tauto trivial diff --git a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean new file mode 100644 index 0000000..3c0c548 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean @@ -0,0 +1,29 @@ +import TestGame.Metadata + +import Mathlib.Init.Set +import Mathlib.Tactic.Tauto + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 2 + +Title "leere Menge" + +Introduction +" +Gleich wie bei `univ` gibt es leere Mengen `∅` von verschiedenen Typen. +So ist `(∅ : Set ℕ)` in Lean nicht das gleiche wie `(∅ : Set ℤ)`. (`\\empty`) + +Zudem hat die Verneinung `¬ (x ∈ A)` die Notation `x ∉ A` (`\\nin`), gleich wie bei `=` and `≠`. + +Um zu zeigen, dass etwas nicht in der leeren Menge ist, kannst du wieder `tauto` verwenden. +" + +open Set + +Statement not_mem_empty + "Kein Element ist in der leeren Menge enthalten." {A : Type _} (x : A) : + x ∉ (∅ : Set A) := by + tauto diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean new file mode 100644 index 0000000..483a8d3 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean @@ -0,0 +1,45 @@ +import TestGame.Metadata + +import Mathlib.Init.Set +import Mathlib.Tactic.Tauto + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 3 + +Title "Teilmengen" + +Introduction +" +Hat man zwei Mengen `(A B : Set ℕ)` kann man fragen, ob diese Teilmengen +voneinander sind: `A ⊆ B` (`\\sub`/`\\ss`) ist die Notation für Teilmengen, die auch gleich +sein können. + +`A ⊆ B` ist als `∀ x, x ∈ A → x ∈ B` definiert, das heisst, ein `⊆` kann immer auch mit `intro x hx` +angegangen werden. + +Die Taktik `tauto` macht das automatisch, aber um dies zu lernen ist `tauto` hier deaktiviert. +Benutze also `intro`: +" + +namespace MySet + +open Set + +theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by + trivial + +theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by + tauto + +Statement subset_empty_iff +"." (A : Set ℕ) : A ⊆ univ := by + intro h hA + apply mem_univ -- or `trivial`. + +Tactics intro trivial apply +-- blocked: tauto simp + +end MySet diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean new file mode 100644 index 0000000..1307805 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean @@ -0,0 +1,61 @@ +import TestGame.Metadata +import TestGame.Levels.SetTheory.L03_Subset + +import Mathlib.Init.Set +import Mathlib.Tactic.Tauto + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 4 + +Title "Teilmengen" + +Introduction +" +Ein zentrales Lemma ist `Subset.antisymm_iff` welches folgendes sagt: + +``` +A = B ↔ A ⊆ B ∧ B ⊆ A +``` + +Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei Ungleichungen +aufteilen. +" + +namespace MySet + +open Set + +-- 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 +"Die einzige Teilmenge der leeren Menge ist die leere Menge." + {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 + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset + +end MySet diff --git a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean new file mode 100644 index 0000000..40260ab --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean @@ -0,0 +1,52 @@ +import TestGame.Metadata +import TestGame.Levels.SetTheory.L04_SubsetEmpty + +--import Mathlib.Data.Set.Basic +import Mathlib.Init.Set +import Mathlib.Tactic.Tauto +import Mathlib.Tactic.PushNeg + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 5 + +Title "Nonempty" + +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: +" + +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 + rw [←subset_empty_iff] + rfl -- This is quite a miracle :) + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset + +end MySet diff --git a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean new file mode 100644 index 0000000..55585e8 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean @@ -0,0 +1,35 @@ +import TestGame.Metadata +import TestGame.Levels.SetTheory.L05_Empty + +import Mathlib.Data.Set.Basic + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 6 + +Title "Nonempty" + +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: +" + +open Set + +Statement nonempty_iff_ne_empty +"" + {A : Type _} (s : Set A) : + s.Nonempty ↔ s ≠ ∅ := by + rw [Set.Nonempty] + rw [ne_eq, eq_empty_iff_forall_not_mem] + push_neg + rfl + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean new file mode 100644 index 0000000..9bd7bf9 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean @@ -0,0 +1,31 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 7 + +Title "Schnittmenge und Vereinigung" + +Introduction +" +Die klassischen Mengenoperationen sind +Schnittmenge `∩` (`\\inter`), Vereinigung `∪` (`\\union`) und +Differenz `\\` (`\\\\`). + +Die Taktik `simp` kann triviale Aussagen with Vereinigung mit der +leeren Menge vereinfachen. +" + +open Set + +Statement +"" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by + simp + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean new file mode 100644 index 0000000..918313d --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean @@ -0,0 +1,35 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 8 + +Title "Schnittmenge und Vereinigung" + +Introduction +" +Ansonsten gibt es jegliche Lemmas in + +`import Mathlib.Data.Set.Basic` + +die beim Umgang mit diesen Operationen weiterhelfen. Schaue in der Bibliothek auf +der Seite nach Lemmas, die dir hier weiterhelfen! +" + +open Set + +Statement +"" + (A B : Set ℕ) : univ \ (A ∩ B) = (univ \ A) ∪ (univ \ B) ∪ (A \ B) := by + rw [diff_inter] + rw [union_assoc] + rw [←union_diff_distrib] + rw [univ_union] + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean new file mode 100644 index 0000000..bef711c --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean @@ -0,0 +1,35 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +Game "TestGame" +World "SetTheory" +Level 9 + +Title "Komplement" + +Introduction +" +Das Komplement einer Menge wird als `Aᶜ` (`\\^c`) geschrieben. Wichtige Lemmas +sind `not_mem_compl_iff` und `compl_eq_univ_diff`. +" + +open Set + +#check not_mem_compl_iff +#check compl_eq_univ_diff + +Statement +"" + (A : Set ℕ) (h : Aᶜ ⊆ A) : A = univ := by + apply Subset.antisymm + simp only [subset_univ] + intros x hx + by_cases h4 : x ∈ Aᶜ + exact mem_of_subset_of_mem h h4 + rw [←not_mem_compl_iff] + exact h4 + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean new file mode 100644 index 0000000..556d3c5 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean @@ -0,0 +1,58 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +Game "TestGame" +World "SetTheory" +Level 10 + +Title "Morgansche Regeln" + +Introduction +" +Die De-Morgan'schen Regeln sagen `(A ∪ B)ᶜ = Aᶜ ∩ Bᶜ` +und `(A ∩ B)ᶜ = Aᶜ ∪ Bᶜ` sind in Lean als + +`compl_union` und `compl_inter`. + + +Zudem gibt es die Lemmas `mem_compl_iff : x ∈ Aᶜ ↔ x ∉ A` und +`not_mem_compl_iff`, mit welchen +man die de-Morganschen Regeln einfach selber beweisen könnten. + + +Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster +Lemmas in `import Mathlib.Data.Set`. + +Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft +wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu +brauchen: + +- `rw [lemma_A, lemma_B]`: führt jedes Lemma genau einmal aus in der Reihenfolge. +- `simp_rw [lemma_A, lemma_B]` : führt jedes Lemma in Reihenfolge so oft aus wie möglich. +- `simp only [lemma_A, lemma_B]` : sucht eine Kombination der beiden Lemmas, ohne bestimmte + Reihenfolge. +- `simp [lemma_A, lemma_B]` : Braucht die beiden Lemmas und alle simp-Lemmas. +" + +open Set + +#check compl_union +#check compl_inter +#check mem_compl_iff + +Statement +"" + (A B C : Set ℕ) : (A \ B)ᶜ ∩ (C \ B)ᶜ = ((univ \ A) \ C) ∪ (univ \ Bᶜ) := by + rw [←compl_union] + rw [←union_diff_distrib] + rw [diff_diff] + simp_rw [←compl_eq_univ_diff] + rw [←compl_inter] + rw [diff_eq_compl_inter] + rw [inter_comm] + +Tactics constructor intro rw assumption rcases simp tauto trivial + +-- TODOs +-- Lemmas compl_union compl_inter mem_compl_iff diff --git a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean new file mode 100644 index 0000000..dfae8fd --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean @@ -0,0 +1,38 @@ +import TestGame.Metadata +import Mathlib.Data.Set.Basic + +Game "TestGame" +World "SetTheory" +Level 11 + +Title "Strikte Teilmenge" + +Introduction +" +Strikte Teilmengen sind in Lean eher selten, aber wir schauen sie hier +trotzdem kurz an : `A ⊂ B` (`\\ssub`) bedeutet `(A ⊆ B) ∧ (¬B ⊆ A)`. +Entsprechend, kann man die gleichen Methoden wie beim UND benützen +(`rcases`/`constructor`). + +Zudem kann man mit `rw [ssubset_def]` explizit die Definition einsetzen. + +Note: `rw [subset_def]` macht das gleiche für `⊆`. +" + +--open Set + +Statement +"" + (A B : Set ℕ) (h : A ⊂ B) : ∃ x, x ∈ B \ A := by + cases' h with h₁ h₂ + rw [Set.subset_def] at h₂ + rw [not_forall] at h₂ + cases' h₂ with x hx + use x + rw [not_imp] at hx + rw [Set.mem_diff] + exact hx + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean new file mode 100644 index 0000000..2501949 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean @@ -0,0 +1,37 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +Game "TestGame" +World "SetTheory" +Level 12 + +Title "Konkrete Mengen" + +Introduction +" +Nun schauen wir uns konkrete Mengen an. Man schreibt diese mit +geschweiften Klammern: `{0, 4, 117, 3}`. Meistens muss man +den Typ explizit angeben, weil lein nicht weiss, ob man mit `Set` (Mengen) +oder `Finset` (endliche Mengen) arbeiten möchte: `({4, 9} : Set ℕ)`. + +`Finset` schauen wir uns später an. + +Um mit expliziten Mengen zu arbeiten, ist die Implementationsweise wichtig. + +Intern ist eine Menge `{0, 9, 5, 2}` iterativ als Vereinigung von +Singletons definiert: `{0} ∪ ( {9} ∪ ( {5} ∪ {2} ))`. + +Die folgende Aufgabe ist entsprechend mit `rfl` lösbar. +" + +open Set + +Statement +"Die Menge $\\{4, 9\\}}$ ist per Definition \\{4}\\cup\\{9\\}." : + ({4, 9} : Set ℕ) = Set.insert 4 {9} := by + rfl + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean new file mode 100644 index 0000000..dde8c82 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean @@ -0,0 +1,39 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic + +Game "TestGame" +World "SetTheory" +Level 13 + +Title "Konkrete Mengen" + +Introduction +" +Um zu überprüfen, dass gewisse Elemente in +konkreten Mengen enthalten sind, gibt es nicht direkt eine Taktik, aber ein +einfaches Rezept: + +``` +simp_rw [mem_insert_iff, mem_singleton_iff] at * +``` + +vereinfacht Aussagen der Form `6 ∈ { 0, 6, 1}` zu `(6 = 0) ∨ (6 = 6) ∨ (6 = 1)`, +und dann kann `tauto` diese Aussage beweisen. + +Bei `⊆` kann man wie schon vorher zuerst mit `intro x hx` die Definition +auseinandernehmen und dann gleich vorgehen. + +" + +open Set + +Statement +"" : + ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by + intro x hx + simp_rw [mem_insert_iff, mem_singleton_iff] at * + tauto + +Tactics simp_rw intro tauto rw +--Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean new file mode 100644 index 0000000..68974a9 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean @@ -0,0 +1,37 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib.Tactic.Ring + +Game "TestGame" +World "SetTheory2" +Level 1 + +Title "Mengen mit Konditionen" + +Introduction +" +Eine wichtige mathematische Notation ist Teilmengen zu erstellen, +die gewissen Bedingungen unterliegen. + +`{n : ℕ | Odd n}` ist die Menge aller natürlichen Zahlen, die ungerade sind. +Diese Konstruktion hat in Lean den Namen `setOf` + +Um zu beweisen, dass ein Element in einer Teilmenge mit Bedingungen ist, braucht +man `rw [mem_setOf]`. Danach muss man zeigen, dass die Bedinung für +dieses Element erfüllt ist. +" + +open Set + +Statement +"" : + 3 ∈ {n : ℕ | Odd n} := by + rw [mem_setOf] + use 1 + ring + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean new file mode 100644 index 0000000..b0e2484 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean @@ -0,0 +1,42 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted + +Game "TestGame" +World "SetTheory2" +Level 2 + +Title "Potenzmenge" + +Introduction +" +Eine andere wichtige Menge ist die Potenzmenge einer Menge, welche als +`𝒫 A` geschrieben wird (`\\powerset`). Diese ist als `{S | S ⊆ A}` definiert, also +alle Mengen, die in $A$ enthalten sind. + +Eines der wichtigsten Lemmas ist `mem_powerset_iff: x ∈ 𝒫 s ↔ x ⊆ s` welches +im Grunde die Definition einsetzt. +" + +open Set + +Statement +"" (X Y : Set ℕ): + 𝒫 X ∪ 𝒫 Y ⊆ 𝒫 (X ∪ Y) := by + intro A hA + rw [mem_union] at hA + simp_rw [mem_powerset_iff] at * + rcases hA with hA | hA + apply subset_union_of_subset_left + assumption + apply subset_union_of_subset_right + assumption + + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean new file mode 100644 index 0000000..8fe48f8 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean @@ -0,0 +1,41 @@ +import TestGame.Metadata + +import Mathlib +import Mathlib.Algebra.Parity +import Mathlib.Tactic.Ring + +Game "TestGame" +World "SetTheory2" +Level 3 + +Title "" + +Introduction +" +Um anzunehmen, dass zwei Mengen disjunkt sind schreibt man +`Disjoint S T`, welches dadurch definiert ist das die +einzige gemeinsame Teilmenge die leere Menge ist, +also etwa `A ⊆ S → A ⊆ T → A ⊆ ∅`. + +Beachte, dass `Disjoint` in Lean genereller definiert ist als +für Mengen, deshalb siehst du die Symbole +`≤` anstatt `⊆` und `⊥` anstatt `∅`, aber diese bedeuten genau +das gleiche. +" + +open Set + +Statement +"" : + ¬Disjoint ({n : ℤ | ∃ k, n = 2 * k} : Set ℤ) ({3, 5, 6, 9, 11} : Set ℤ) := by + unfold Disjoint + rw [not_forall] -- why not `push_neg`? + use {6} + simp + use 3 + ring + + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean new file mode 100644 index 0000000..e3449fd --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean @@ -0,0 +1,39 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib + +Game "TestGame" +World "SetTheory2" +Level 4 + +Title "" + +Introduction +" +" + +open Set + +Statement +"" : + {2, 7} ⊆ {n : ℕ | n = 2 ∨ (n ≤ 10 ∧ Odd n)} := by + rw [setOf_or, setOf_and] + intro x hx + rw [mem_union, mem_inter_iff] + simp_rw [mem_setOf, mem_insert_iff, mem_singleton_iff] at * + rcases hx with hx | hx + left + assumption + right + constructor + linarith + use 3 + rw [hx] + ring + + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean new file mode 100644 index 0000000..110e17b --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean @@ -0,0 +1,33 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib + +Game "TestGame" +World "SetTheory2" +Level 5 + +Title "" + +Introduction +" +Zu der Teilmengen-Schreibweise (`SetOf`) gibt es noch zwei spezielle +Syntax, die abundzu auftreten. + +Der erste ist `{ x ∈ S | 0 ≤ x}` ( für z.B `(S : Set ℤ)`), +welcher eine Abkürzung für `{ x : ℤ | x ∈ S ∧ 0 ≤ x}` ist. +Entsprechend hilft auch hier `setOf_and`. + +" + +open Set + +Statement +"" (S : Set ℤ) : + { x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by + library_search + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean new file mode 100644 index 0000000..65e8e32 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean @@ -0,0 +1,28 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib.Tactic.Ring + +Game "TestGame" +World "SetTheory2" +Level 6 + +Title "" + +Introduction +" +" + +open Set + +Statement +"" : + 3 ∈ {n : ℕ | Odd n} := by + rw [mem_setOf] + use 1 + ring + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean new file mode 100644 index 0000000..a081429 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean @@ -0,0 +1,27 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib + +Game "TestGame" +World "SetTheory2" +Level 7 + +Title "" + +Introduction +" +Wir haben bereits `∪` und `∩` kennengelernt. Von beiden gibt es auch eine Version für Familien +von Mengen: $\\bigcup_i A_ i$ und $\\bigcap_j B_ j$. + +" + +open Set + +Statement +"" : True := sorry + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean new file mode 100644 index 0000000..e4c74d3 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean @@ -0,0 +1,28 @@ +import TestGame.Metadata + +import Mathlib.Data.Set.Basic +import Mathlib.Algebra.Parity +import Mathlib.Tactic.Ring + +Game "TestGame" +World "SetTheory" +Level 21 + +Title "" + +Introduction +" +" + +open Set + +Statement +"" : + 3 ∈ {n : ℕ | Odd n} := by + rw [mem_setOf] + use 1 + ring + +Tactics constructor intro rw assumption rcases simp tauto trivial + +Lemmas Subset.antisymm_iff empty_subset diff --git a/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean b/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean new file mode 100644 index 0000000..44fd72b --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean @@ -0,0 +1,109 @@ +import Mathlib + +open Set + +namespace Finset + +theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) : + Finset.powerset {x} = {∅, {x}} := by + ext y + rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton] + +end Finset + +/- The powerset of a singleton contains only `∅` and the singleton. -/ +theorem powerset_singleton {U : Type _} (x : U) : + 𝒫 ({x} : Set U) = {∅, {x}} := by + ext y + rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff] + +theorem subset_insert_iff_of_not_mem {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s) + : s ⊆ insert a t ↔ s ⊆ t := by + constructor + · intro g y hy + specialize g hy + rw [mem_insert_iff] at g + rcases g with g | g + · rw [g] at hy + contradiction + · assumption + · intro g y hy + specialize g hy + exact mem_insert_of_mem _ g + +theorem subset_insert_iff_of_not_mem' {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s) + (g : s ⊆ t) : s ⊆ insert a t := by + intro y hy + specialize g hy + exact mem_insert_of_mem _ g + +lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by + simp_rw [mem_powerset_iff] + constructor + · intro h + by_cases hs : x ∈ S + · right + use S \ {x} + rw [insert_diff_singleton, insert_eq_of_mem hs, diff_singleton_subset_iff] + exact ⟨h, rfl⟩ + · left + exact (subset_insert_iff_of_not_mem hs).mp h + · intro h + rcases h with h | ⟨B, h₁, h₂⟩ + · exact le_trans h (subset_insert x A) + · rw [←h₂] + exact insert_subset_insert h₁ + +lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by + rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] + +lemma powerset_insert {U : Type _} (A : Set U) (x : U) : + 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by + ext y + rw [mem_powerset_insert_iff, mem_union, mem_image] + + + + + +example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by + rw [union_insert, singleton_union] + simp only [insert_comm, ←insert_emptyc_eq] + +example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by + simp_rw [powerset_insert, powerset_singleton] + simp only [image_insert_eq, union_insert, image_singleton, union_singleton] + simp only [insert_comm, ←insert_emptyc_eq] + +-- This one is much slower, but it still works +example : powerset {0, 1, 2, 4} = + {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2}, + {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by + simp_rw [powerset_insert, powerset_singleton] + simp only [image_insert_eq, union_insert, image_singleton, union_singleton] + simp only [insert_comm, ←insert_emptyc_eq] + +example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by + simp only [] + +example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by + rw [Subset.antisymm_iff] + constructor <;> + intro A hA <;> + simp_rw [mem_insert_iff, mem_singleton_iff] at * + · rw [pair_comm 2 0, insert_comm 5 3] + tauto + · rw [pair_comm 0 2, insert_comm 3 5] + tauto + +-- A trick to compare two concrete sets. +example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by + simp only [insert_comm, ←insert_emptyc_eq] + +example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by + simp only + +-- Trick: +-- attribute [default_instance] Set.instSingletonSet diff --git a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean index b597a12..a63620d 100644 --- a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean +++ b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean @@ -1,5 +1,15 @@ import TestGame.Metadata +import Mathlib.Order.SymmDiff +import Mathlib.Logic.Function.Iterate +import Mathlib.Tactic.Use +import Mathlib.Tactic.SolveByElim +import Mathlib.Tactic.Tauto +import Mathlib.Tactic.ByContra +import Mathlib.Tactic.Lift +import Mathlib.Data.Set.Basic +import Mathlib.Data.Finset.Powerset +import Mathlib.Tactic.LibrarySearch import Mathlib set_option tactic.hygienic false @@ -45,3 +55,243 @@ Statement rw [Set.univ_union] Tactics rw + + +example : 4 ∈ (univ : Set ℕ) := by + trivial + +example (A : Set ℕ) : 4 ∉ (∅ : Set ℕ) := by + trivial + +example (A : Set ℕ) : A ⊆ univ := by + intro x h + trivial + +-- -- subset_empty_iff +-- example {s : Set α} : 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 + +-- -- eq_empty_iff_forall_not_mem +-- example {s : Set α} : s = ∅ ↔ ∀ x, x ∉ s := by +-- rw [←subset_empty_iff] +-- rfl + +-- -- nonempty_iff_ne_empty +-- example (X : Type _) (s : Set X) : Set.Nonempty s ↔ s ≠ ∅ := by +-- rw [Set.Nonempty] +-- rw [ne_eq, eq_empty_iff_forall_not_mem] +-- push_neg +-- rfl + + +-- example (A B : ℝ): A = B ↔ A ≤ B ∧ B ≤ A := by library_search + +namespace Finset + +theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) : + Finset.powerset {x} = {∅, {x}} := by + ext y + rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton] + +end Finset + +/- The powerset of a singleton contains only `∅` and the singleton. -/ +theorem powerset_singleton {U : Type _} (x : U) : + 𝒫 ({x} : Set U) = {∅, {x}} := by + ext y + rw [mem_powerset_iff, subset_singleton_iff_eq] + rw [mem_insert_iff, mem_singleton_iff] + + +lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by + rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] + +-- lemma powerset_insert {U : Type _} (A : Set U) (x : U) : +-- 𝒫 (insert x A) = 𝒫 A ∪ ({B : Set U | B \ {x} ∈ 𝒫 A}) := by +-- sorry + +theorem subset_insert_iff_of_not_mem {U : Type _ }{s t : Set U} (h : a ∉ s) : s ⊆ insert a t ↔ s ⊆ t := by + rw [subset_insert_iff, erase_eq_of_not_mem h] + +lemma mem_powerset_insert_iff₂ {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by + simp_rw [mem_powerset_iff] + constructor + · intro h + by_cases hs : x ∈ S + · sorry + · left + rw [Finset.subset_insert_iff_of_not_mem] + · intro h + rcases h with h | ⟨B, h₁, h₂⟩ + · exact le_trans h (subset_insert x A) + · rw [←h₂] + exact insert_subset_insert h₁ + +lemma powerset_insert {U : Type _} (A : Set U) (x : U) : + 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by + rw [Subset.antisymm_iff] + constructor <;> + intro B hB <;> + simp_rw [mem_powerset_insert_iff₂, mem_union, mem_image] at hB ⊢ <;> + assumption + + +example : powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by + simp_rw [powerset_insert, powerset_singleton, Finset.powerset_insert, Finset.powerset_singleton] + simp only [image_insert_eq, union_insert, image_singleton, union_singleton] + simp only [insert_comm, ←insert_emptyc_eq] + +example [DecidableEq ℕ] : Finset.powerset {0, 1} = {∅, {0}, {1}, {0, 1}} := by + repeat' rw [@ Finset.powerset_insert ℕ] + repeat' rw [@Finset.powerset_singleton ℕ] + --simp only [image_insert_eq, union_insert, image_singleton, union_singleton] + + +example : powerset {0, 1, 2, 4} = + {∅, {0}, {1}, {0, 1}, {2}, {1, 2}, {0, 2}, {0, 1, 2}, + {4}, {0, 4}, {1, 4}, {0, 1, 4}, {2, 4}, {1, 2, 4}, {0, 2, 4}, {0, 1, 2, 4}} := by + simp_rw [powerset_insert, powerset_singleton] + simp_rw [image_insert_eq, image_singleton] + + + +example : Finset.powerset ({0, 1} : Finset ℕ) = {{0, 1}, ∅, {1}, {0}} := by + have h : Finset.powerset ({0, 1} : Finset ℕ) = {∅, {0}, {1}, {0, 1}} + rfl + rw [h] + simp only [] + + +example : ({∅, {0}, {1}, {0, 1}} : Finset (Finset ℕ)) = {∅, {1}, {0}, {0, 1}} := by + simp only [] + + + +lemma subset_of_subset_diff {U : Type _} (A B C : Set U) (h : A ⊆ B \ C) : A ⊆ B := + fun _ hx => mem_of_mem_diff (h hx) + +lemma subset_of_subset_diff' {U : Type _} (A B C : Set U) (h : A ⊆ B) : A \ C ⊆ B := + sorry + +lemma mem_powerset' {U : Type _} {A B C : Set U} + (h' : B ∈ 𝒫 C) (h : A ⊆ B) : + A ∈ 𝒫 C := by + rw [mem_powerset_iff] at h' ⊢ + exact le_trans h h' + +example (A B : Set ℕ) : A = B ↔ ∀ x, x ∈ A ↔ x ∈ B := by + exact ext_iff + + + +lemma NO.powerset_insert {U : Type _} (A : Set U) (x : U) : + 𝒫 (insert x A) = 𝒫 A ∪ ({insert x B | B ∈ 𝒫 A}) := by + ext y + rw [mem_powerset_insert_iff] + constructor + · intro h + rw [mem_union, mem_setOf] + by_cases hx : x ∈ y + · right + use y \ {x} + constructor + · assumption + · rw [insert_diff_singleton, insert_eq_of_mem hx] + · left + rw [diff_singleton_eq_self hx] at h + assumption + · intro h + rw [mem_union, mem_setOf] at h + rcases h with h | h + · apply mem_powerset' h + simp + · rcases h with ⟨B, hB⟩ + rw [←hB.2] + apply mem_powerset' hB.1 + simp + +-- lemma xxx {U : Type _} (x y : U): +-- ({insert x B | B ∈ {∅, }}) = {({x} : Set U), {x, y}} := by +-- sorry + +-- lemma hh {U : Type _} (A : Set U) (x : U) : +-- A \ {x} ∈ + +lemma diff_singleton_eq_iff {U : Type _} {A B : Set U} {x : U} : + A \ {x} = B ↔ A = B ∨ A = insert x B := by sorry + +lemma x1 {U : Type _} (x : U) : insert x (∅ : Set U) = {x} := by sorry + +--set_option maxHeartbeats 20000 + + +example {U : Type _} {x y : U} : ({x, y} : Set U) = {y, x} := by + exact pair_comm x y + +example {U : Type _} {A : Set U} {x y : U} : insert x (insert y A) = insert y (insert x A) := by + exact insert_comm x y A + +open Classical + +#check decide + +example : ({{0, 2}, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}} := by + rw [Subset.antisymm_iff] + constructor <;> + intro A hA <;> + simp_rw [mem_insert_iff, mem_singleton_iff] at * + · rw [pair_comm 2 0, insert_comm 5 3] + tauto + · rw [pair_comm 0 2, insert_comm 3 5] + tauto + +example (A : Set ℕ) : ({{0, 2}, A, {3, 5, 6}} : Set (Set ℕ)) = {{2, 0}, {5, 3, 6}, A} := by + simp only [insert_comm, ←insert_emptyc_eq] + + +example : ({{0, 2}, {3, 5, 6}} : Finset (Finset ℕ)) = {{2, 0}, {5, 3, 6}} := by + simp only + + + -- -- This works but does not scale well + -- ext x + -- simp_rw [powerset_insert, powerset_singleton] + -- simp_rw [mem_union, mem_setOf, mem_insert_iff, mem_singleton_iff] + -- simp_rw [diff_singleton_eq_iff, x1] + -- tauto + + + + + -- rw [Subset.antisymm_iff] + -- constructor + -- intro A hA + -- rw [mem_powerset_iff] at hA + -- simp_rw [mem_insert_iff, mem_singleton_iff] at * + + +example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by + intro a ha + simp_rw [Set.mem_insert_iff, Set.mem_singleton_iff] at * + tauto + +example : ({0} : Set ℕ) ∪ {1, 2} = {0, 2, 1} := by + rw [Subset.antisymm_iff] + intro A hA + --rw [Set.mem_insert_iff] + + + +-- Trick: +-- attribute [default_instance] Set.instSingletonSet diff --git a/server/testgame/TestGame/Levels/SetTheory/T04_xx.lean b/server/testgame/TestGame/Levels/SetTheory/T04_xx.lean new file mode 100644 index 0000000..bb8523c --- /dev/null +++ b/server/testgame/TestGame/Levels/SetTheory/T04_xx.lean @@ -0,0 +1,96 @@ +import TestGame.Metadata + +import Mathlib +import Duper.Tactic + + +import Mathlib.Order.Disjoint + +set_option tactic.hygienic false + +Game "TestGame" +World "SetTheory" +Level 4 + +Title "Mengen" + +Introduction +" +`∈ ∉ ⊆ ⊂ ⋃ ⋂` +" + +open Set + +-- open_locale cardinal + +variables {X : Type _} (x : X) (A B : Set X) + +#check A.Nonempty +#check Nonempty A +#check insert x A -- {x} ∪ A +-- #check disjoint A B -- needs Mathlib.Order.Disjoint +#check A ∆ B +#check Nontrivial A + +#check ({2} : Set ℕ) + +example : ({2} : Set ℕ) ⊆ {4, 2, 3} := by + simp only [mem_singleton_iff, mem_insert_iff, or_self, singleton_subset_iff, or_false, or_true] + +example : ({2, 3, 5} : Set ℕ) ⊆ {4, 2, 5, 7, 3} := by + intro n hn + simp only [mem_insert_iff, mem_singleton_iff] at * + tauto + +example : {2, 3, 5} ⊆ (univ : Set ℕ) := by + tauto + +example : 3 ∈ ({4, 2, 5, 7, 3} : Set ℕ) := by + tauto + +example : ({4, 9} : Set ℕ) = Set.insert 4 {9} := by + rfl + + + + +#check Finset.card + +variable (A : Finset ℕ) + +#check A.card + +-- card_union_eq +example (A B : Finset ℕ) (h : Disjoint A B) : (A ∪ B).card = A.card + B.card := by + -- Not a suitable proof for the course. + rw [← Finset.disjUnion_eq_union A B h, Finset.card_disjUnion _ _ _] + +example : ¬Disjoint {n : ℤ | ∃ k, n = 2 * k} {3, 5, 6, 9, 11} := by + rw [not_disjoint_iff] + use 6 + constructor + rw [mem_setOf_eq] + use 3 + tauto + +example : {n : ℕ | Even n ∨ Odd n} = univ := by + rw [setOf_or] + + + + +#check Set.eq_of_mem_singleton +#check {n : ℤ | ∃ k, n = 2 * k} +#check {n : ℤ // ∃ k, n = 2 * k} +#check ℤ +variables (C : Set ℤ) +#check {n ∈ C | ∃ (k : ℤ), n = 2 * k} +#check {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} +#check {x ∈ A | x = x} +#check {y | y ∈ A} +#check setOf_and +#check setOf_or +#check Disjoint C univ + +example : {n ∈ C | ∃ (k : ℤ), n = 2 * k} = {n : ℤ | n ∈ C ∧ ∃ (k : ℤ), n = 2 * k} := by + rfl diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean index 7e1f974..fd33f0d 100644 --- a/server/testgame/TestGame/TacticDocs.lean +++ b/server/testgame/TestGame/TacticDocs.lean @@ -81,6 +81,12 @@ mit Theoremen/Lemmas der Form `X = Y` TODO " +TacticDoc simp_rw +" +## Beschreibung + +TODO +" TacticDoc apply " @@ -96,6 +102,13 @@ TacticDoc constructor TODO " +TacticDoc tauto +" +## Beschreibung + +TODO +" + TacticDoc rcases " ## Beschreibung diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean index ed519cc..807087f 100644 --- a/server/testgame/TestGame/ToBePorted.lean +++ b/server/testgame/TestGame/ToBePorted.lean @@ -14,3 +14,73 @@ lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by ring theorem nat_succ (n : ℕ) : Nat.succ n = n + 1 := rfl + +section powerset + +open Set + +namespace Finset + +theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) : + Finset.powerset {x} = {∅, {x}} := by + ext y + rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton] + +end Finset + +/- The powerset of a singleton contains only `∅` and the singleton. -/ +theorem powerset_singleton {U : Type _} (x : U) : + 𝒫 ({x} : Set U) = {∅, {x}} := by + ext y + rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff] + +theorem subset_insert_iff_of_not_mem {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s) + : s ⊆ insert a t ↔ s ⊆ t := by + constructor + · intro g y hy + specialize g hy + rw [mem_insert_iff] at g + rcases g with g | g + · rw [g] at hy + contradiction + · assumption + · intro g y hy + specialize g hy + exact mem_insert_of_mem _ g + +theorem subset_insert_iff_of_not_mem' {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s) + (g : s ⊆ t) : s ⊆ insert a t := by + intro y hy + specialize g hy + exact mem_insert_of_mem _ g + +lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by + simp_rw [mem_powerset_iff] + constructor + · intro h + by_cases hs : x ∈ S + · right + use S \ {x} + rw [insert_diff_singleton, insert_eq_of_mem hs, diff_singleton_subset_iff] + exact ⟨h, rfl⟩ + · left + exact (subset_insert_iff_of_not_mem hs).mp h + · intro h + rcases h with h | ⟨B, h₁, h₂⟩ + · exact le_trans h (subset_insert x A) + · rw [←h₂] + exact insert_subset_insert h₁ + +lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) : + S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by + rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] + +lemma powerset_insert {U : Type _} (A : Set U) (x : U) : + 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by + ext y + rw [mem_powerset_insert_iff, mem_union, mem_image] + + + +end powerset diff --git a/server/testgame/lake-manifest.json b/server/testgame/lake-manifest.json index bf389c1..d5603ab 100644 --- a/server/testgame/lake-manifest.json +++ b/server/testgame/lake-manifest.json @@ -28,7 +28,7 @@ {"git": {"url": "https://github.com/leanprover-community/mathlib4.git", "subDir?": null, - "rev": "8176e5d663db861cccf6fed6db2f9e5669fe6c5b", + "rev": "98bc5f26ea463d9583f601c84518c95643c0ea14", "name": "mathlib", "inputRev?": "master"}}, {"git": @@ -59,6 +59,12 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "5770b609aeae209cb80ac74655ee8c750c12aabd", + "rev": "04b3c9831e0c141713a70e68af7e40973ec9a1ff", "name": "std", + "inputRev?": "main"}}, + {"git": + {"url": "/home/jeugster/Documents/Lean/duper", + "subDir?": null, + "rev": "d0fb397d96483c90969c725ad5ea307cc02bdf7d", + "name": "duper", "inputRev?": "main"}}]} diff --git a/server/testgame/lakefile.lean b/server/testgame/lakefile.lean index 27631d6..98ba429 100644 --- a/server/testgame/lakefile.lean +++ b/server/testgame/lakefile.lean @@ -6,6 +6,9 @@ require GameServer from ".."/"leanserver" require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"master" +require duper from git + "/home/jeugster/Documents/Lean/duper"@"main" + --set_option tactic.hygienic false --set_option autoImplicit false