From af3afc3a947a47991f36d3f9153fe146b60e420e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 13 Feb 2023 17:48:11 +0100 Subject: [PATCH] levels --- server/testgame/TestGame.lean | 6 +- .../Levels/Contradiction/L01_Have.lean | 11 +-- .../Levels/Contradiction/L02_Suffices.lean | 13 +-- .../Levels/Contradiction/L03_ByContra.lean | 2 +- .../Levels/Contradiction/L04_ByContra.lean | 2 +- server/testgame/TestGame/Levels/Function.lean | 9 +- .../Levels/Function/L01_Function.lean | 29 +++++++ .../TestGame/Levels/Function/L01_xxx.lean | 26 ------ .../TestGame/Levels/Function/L02_Let.lean | 59 +++++++++++++ .../Levels/Function/L03_Composition.lean | 20 +++++ .../Levels/Function/L06_Piecewise.lean | 27 ++++++ .../Levels/Function/L07_Injective.lean | 24 ++++++ .../Levels/Function/L08_Injective.lean | 19 +++++ .../Levels/Function/L09_Surjective.lean | 19 +++++ .../Levels/Function/L10_Bijective.lean | 23 ++++++ .../testgame/TestGame/Levels/LeanStuff.lean | 4 +- .../TestGame/Levels/LeanStuff/L01_Type.lean | 42 ++++++++++ .../TestGame/Levels/LeanStuff/L01_xxx.lean | 33 +++++++- .../Levels/LeanStuff/L02_Universe.lean | 37 +++++++++ .../LeanStuff/L03_ImplicitArguments.lean | 57 +++++++++++++ server/testgame/TestGame/Levels/Numbers.lean | 2 + .../TestGame/Levels/Numbers/L01_PNat.lean | 82 +++++++++++++++++++ .../TestGame/Levels/Numbers/L02_PNat.lean | 24 ++++++ .../TestGame/Levels/Proposition/L09_And.lean | 2 +- .../TestGame/Levels/Proposition/L10_And.lean | 2 +- .../testgame/TestGame/Levels/SetFunction.lean | 5 +- .../Levels/SetFunction/L01_Image.lean | 65 +++++++++++++++ .../TestGame/Levels/SetFunction/L01_xxx.lean | 24 ------ .../Levels/SetFunction/L02_Preimage.lean | 21 +++++ .../Levels/SetFunction/L03_Range.lean | 21 +++++ .../Levels/SetFunction/L04_ImageUnion.lean | 18 ++++ server/testgame/TestGame/TacticDocs.lean | 4 +- 32 files changed, 658 insertions(+), 74 deletions(-) create mode 100644 server/testgame/TestGame/Levels/Function/L01_Function.lean delete mode 100644 server/testgame/TestGame/Levels/Function/L01_xxx.lean create mode 100644 server/testgame/TestGame/Levels/Function/L02_Let.lean create mode 100644 server/testgame/TestGame/Levels/Function/L03_Composition.lean create mode 100644 server/testgame/TestGame/Levels/Function/L06_Piecewise.lean create mode 100644 server/testgame/TestGame/Levels/Function/L07_Injective.lean create mode 100644 server/testgame/TestGame/Levels/Function/L08_Injective.lean create mode 100644 server/testgame/TestGame/Levels/Function/L09_Surjective.lean create mode 100644 server/testgame/TestGame/Levels/Function/L10_Bijective.lean create mode 100644 server/testgame/TestGame/Levels/LeanStuff/L01_Type.lean create mode 100644 server/testgame/TestGame/Levels/LeanStuff/L02_Universe.lean create mode 100644 server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean create mode 100644 server/testgame/TestGame/Levels/Numbers.lean create mode 100644 server/testgame/TestGame/Levels/Numbers/L01_PNat.lean create mode 100644 server/testgame/TestGame/Levels/Numbers/L02_PNat.lean create mode 100644 server/testgame/TestGame/Levels/SetFunction/L01_Image.lean delete mode 100644 server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean create mode 100644 server/testgame/TestGame/Levels/SetFunction/L02_Preimage.lean create mode 100644 server/testgame/TestGame/Levels/SetFunction/L03_Range.lean create mode 100644 server/testgame/TestGame/Levels/SetFunction/L04_ImageUnion.lean diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index c4742bf..dcab229 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -7,6 +7,8 @@ import TestGame.Levels.Contradiction import TestGame.Levels.Prime import TestGame.Levels.Induction +import TestGame.Levels.Numbers + import TestGame.Levels.LeanStuff import TestGame.Levels.SetTheory import TestGame.Levels.Function @@ -39,9 +41,9 @@ Conclusion Path Proposition → Implication → Predicate → Prime -Path Predicate → Contradiction → LeanStuff → SetTheory → SetFunction +Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 → SetFunction Path Predicate → Induction → LeanStuff → Function → SetFunction -Path SetTheory → SetTheory2 +Path SetTheory2 → Numbers MakeGame diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean index b4b4ddf..3aea102 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean @@ -35,18 +35,18 @@ bevor du dann mit dem Beweis forfährst. Statement "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt." - (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by - rcases g with ⟨h₁, h₂⟩ + (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by + rcases k with ⟨h₁, h₂⟩ have h₃ : ¬ B apply h assumption contradiction -Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False => " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. " -Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False => " Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\" @@ -63,6 +63,7 @@ have k : ¬ B Conclusion "" -NewTactics contradiction rcases haveₓ assumption apply +NewTactics «have» +DisabledTactics «suffices» NewLemmas Even Odd not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean index 4f36b7a..f6d02cb 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean @@ -23,7 +23,7 @@ suffices h : [Aussage] [Beweis des Goals (mithilfe von h)] [Beweis der Aussage h] ``` -Auf Deutsch entspricht `suffices h : [Aussage]` dem Ausdruck +Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\" Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so, @@ -35,18 +35,18 @@ dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Statement "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt." - (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by - rcases g with ⟨h₁, h₂⟩ + (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by + rcases k with ⟨h₁, h₂⟩ suffices k : ¬ B contradiction apply h assumption -Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False => " Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. " -Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False => " Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\" In Lean : @@ -60,6 +60,7 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => Conclusion "" -NewTactics contradiction apply assumption rcases sufficesₓ +NewTactics «suffices» +DisabledTactics «have» NewLemmas Even Odd not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean index 50a5246..ebd0351 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean @@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => Conclusion "" -NewTactics by_contra sufficesₓ haveₓ contradiction apply assumption +NewTactics by_contra contradiction apply assumption diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean index d3cbe73..c67c016 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean @@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) => Conclusion "" -NewTactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption +NewTactics contradiction constructor intro by_contra apply assumption diff --git a/server/testgame/TestGame/Levels/Function.lean b/server/testgame/TestGame/Levels/Function.lean index 1472ed1..b5f0bb8 100644 --- a/server/testgame/TestGame/Levels/Function.lean +++ b/server/testgame/TestGame/Levels/Function.lean @@ -1,4 +1,11 @@ -import TestGame.Levels.Function.L01_xxx +import TestGame.Levels.Function.L01_Function +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.L08_Injective +import TestGame.Levels.Function.L09_Surjective +import TestGame.Levels.Function.L10_Bijective Game "TestGame" World "Function" diff --git a/server/testgame/TestGame/Levels/Function/L01_Function.lean b/server/testgame/TestGame/Levels/Function/L01_Function.lean new file mode 100644 index 0000000..3c3a1cd --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L01_Function.lean @@ -0,0 +1,29 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 1 + +Title "" + +Introduction +" +Funktionen werden in Lean mit `ℕ → ℕ` geschrieben (`\\to`), also dem gleichen +Pfeil wie Implikationen. + +Eine abstrakte Funktion ist ein entsprechendes Element `(f : ℕ → ℕ)` oder `(g : ℕ → ℝ)`. +Dies sagt aber gar nichts darüber, wie `f` tatsächlich definiert ist. + +Hat man eine Funktion `(f : A → B)` und ein Element `(x : A)` dann ist `f x` der +Bildpunkt in `B`. In Lean braucht man also keine Klammern um $f(x)$ zu schreiben. + +Eplizite, anonyme Funktionen kann man mit dem Syntax `fun (n : ℕ) ↦ n ^ 2` definieren +(entweder `↦` (`\\map`) oder `=>` als Pfeil in der Mitte). +" + +Statement +"Zeige, dass es eine Funktion $\\mathbb{N} \\to \\mathbb{Z}$ gibt, für die $f(x) < x$ gilt." + : ∃ f : ℕ → ℤ, ∀ x, f x < x := by + use (fun x ↦ x - 1) + simp diff --git a/server/testgame/TestGame/Levels/Function/L01_xxx.lean b/server/testgame/TestGame/Levels/Function/L01_xxx.lean deleted file mode 100644 index 4048f5a..0000000 --- a/server/testgame/TestGame/Levels/Function/L01_xxx.lean +++ /dev/null @@ -1,26 +0,0 @@ -import TestGame.Metadata - -import Mathlib - -set_option tactic.hygienic false - -Game "TestGame" -World "Function" -Level 1 - -Title "Abbildungen" - -Introduction -" -In diesem Kapitel lernen wir mit Abbildungen/Funktionen umzugehen. - -Funktionen auf `ℕ`. - -" - -Statement - "TODO" - : True := by - trivial - -NewTactics rw diff --git a/server/testgame/TestGame/Levels/Function/L02_Let.lean b/server/testgame/TestGame/Levels/Function/L02_Let.lean new file mode 100644 index 0000000..6601c7a --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L02_Let.lean @@ -0,0 +1,59 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 2 + +Title "" + +Introduction +" +Ausserhalb eines Beweises kann man Funktionen mit `def` +(anstatt `lemma`/`example`/`theorem`) definieren: + +``` +def f (x : ℚ) : ℚ := 1 / (1 + x^2) + +def f : ℚ → ℚ := fun x ↦ 1 / (1 + x^2) +``` + +(die beiden Varianten sind äquivalent.) + +Um eine anonyme Funktion `fun x ↦ 1 / (1 + x^2)` innerhalb eines Beweis einem Namen +zuzuordnen, benützt man `let`: + +``` +let f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2 +``` + +Die Taktiken `let` und `have` sind fast gleich, mit einem wichtigen Unterschied. Mit + +``` +have f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2 +``` + +vergisst Lean sofort wie `f` konstruiert wurde, und weiss nur noch dass es eine Funktion +`(f : ℕ → ℕ)` gibt. Mit `let` kann Lean jederzeit auf die Definition von `f` zugreifen. +" + +def f (x : ℤ) : ℤ := (x + 1) ^ 2 + +Statement +" +Given the function +``` +def f (x : ℤ) : ℤ := (x + 1) ^ 2 +``` +show that $f(x) = x^2 + 2x + 1$. + +" + : ∀ x, f x = x ^ 2 + 2 * x + 1 := by + intro x + unfold f + ring + +Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 => +"If your function has been defined with a `def` then usually you need to use `unfold f` to +help Lean replacing it with it's definition (alternatively `sim [f]` +oder `rw [f]` funktionieren auch)." diff --git a/server/testgame/TestGame/Levels/Function/L03_Composition.lean b/server/testgame/TestGame/Levels/Function/L03_Composition.lean new file mode 100644 index 0000000..2f64c34 --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L03_Composition.lean @@ -0,0 +1,20 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 3 + +Title "" + +Introduction +" +Komposition von Funktionen kann als `g ∘ f` geschrieben werden. + +TODO +" + +Statement +"TODO: Find an exercise." + (U S T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x) := by + trivial diff --git a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean new file mode 100644 index 0000000..d79413f --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean @@ -0,0 +1,27 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 4 + +Title "" + +Introduction +" +" + +open Set + +def f2 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1 + +#eval (f2 + f2) 2 + +#check range f2 + +Statement +"" + : True := by + trivial + +#check Set.piecewise 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..deb49bc --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L07_Injective.lean @@ -0,0 +1,24 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 5 + +Title "" + +Introduction +" +" +open Set Function + +def f3 : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1 + +#eval (f3 + f3) 2 + +example : ¬ f3.Injective := by + unfold Injective + push_neg + use 2 + use 3 + simp diff --git a/server/testgame/TestGame/Levels/Function/L08_Injective.lean b/server/testgame/TestGame/Levels/Function/L08_Injective.lean new file mode 100644 index 0000000..edc30a4 --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L08_Injective.lean @@ -0,0 +1,19 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 6 + +Title "" + +Introduction +" +" + +Statement +"" + : (fun (n : ℤ) ↦ n + 1).Injective := by + intro a b hab + simp at hab + assumption diff --git a/server/testgame/TestGame/Levels/Function/L09_Surjective.lean b/server/testgame/TestGame/Levels/Function/L09_Surjective.lean new file mode 100644 index 0000000..8a67873 --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L09_Surjective.lean @@ -0,0 +1,19 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 7 + +Title "Surjektive" + +Introduction +" +" + +Statement +"" +: (fun (n : ℤ) ↦ n + 1).Surjective := by + intro y + use y-1 + simp diff --git a/server/testgame/TestGame/Levels/Function/L10_Bijective.lean b/server/testgame/TestGame/Levels/Function/L10_Bijective.lean new file mode 100644 index 0000000..1b372cb --- /dev/null +++ b/server/testgame/TestGame/Levels/Function/L10_Bijective.lean @@ -0,0 +1,23 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Function" +Level 8 + +Title "" + +Introduction +" +" + +Statement +"" + : (fun (n : ℤ) ↦ n + 1).Bijective := by + constructor + intro a b hab + simp at hab + assumption + intro y + use y-1 + simp diff --git a/server/testgame/TestGame/Levels/LeanStuff.lean b/server/testgame/TestGame/Levels/LeanStuff.lean index 22db2b6..4b56380 100644 --- a/server/testgame/TestGame/Levels/LeanStuff.lean +++ b/server/testgame/TestGame/Levels/LeanStuff.lean @@ -1,4 +1,6 @@ -import TestGame.Levels.LeanStuff.L01_xxx +import TestGame.Levels.LeanStuff.L01_Type +import TestGame.Levels.LeanStuff.L02_Universe +import TestGame.Levels.LeanStuff.L03_ImplicitArguments Game "TestGame" World "LeanStuff" diff --git a/server/testgame/TestGame/Levels/LeanStuff/L01_Type.lean b/server/testgame/TestGame/Levels/LeanStuff/L01_Type.lean new file mode 100644 index 0000000..027228e --- /dev/null +++ b/server/testgame/TestGame/Levels/LeanStuff/L01_Type.lean @@ -0,0 +1,42 @@ +import TestGame.Metadata + +import Mathlib + +set_option tactic.hygienic false + +Game "TestGame" +World "LeanStuff" +Level 1 + +Title "Typen" + +Introduction +" +Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen solltest. + +Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas +verstehst wie Lean manche Sachen macht. + +Als erstes geht es um Typen. + +Oft sieht man Argumente von der Form `(U : Type)` was heisst \"sei $U$ ein Typ.\" +Als Mathematiker kann man sich Typen ein bisschen wie Mengen vorstellen, in dem Sinn +dass sie die Grundlage der Mathematik bilden: Alles sind Typen. + +Zum Beispiel ist `ℕ` der Typ der natürlichen Zahlen, `Prop` der Typ der logischen +Aussagen, und ein Ring ist ein Typ `(R : Type)` zusammen mit einer Instanz `[Ring R]`, +die sagt, dass auf diesem Typ eine Ringstruktur besteht. + +**Achtung**: Wie du aber gleich sehen wirst sind Typen und Mengen in Lean komplett +unterschiedliche Sachen! (Und Mengen nehmen in Lean nicht die fundamentale Funktion +ein, die sie in der Mathe innehaben.) +" + +Statement +"" + (R : Type) [CommRing R] (a b : R) : a + b = b + a := by + ring + +Hint (R : Type) (h : CommRing R) (a : R) (b : R) : a + b = b + a => +"Die Taktik `ring` funktioniert in jedem Typen, +der mindestens eine Instanz `[Ring R]` hat." diff --git a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean index f46dbdb..a3a520d 100644 --- a/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean +++ b/server/testgame/TestGame/Levels/LeanStuff/L01_xxx.lean @@ -17,10 +17,36 @@ Dieses Kapitel führt ein paar Lean-spezifische Sachen ein, die du wissen sollte Mathematisch haben diese Sachen keinen Inhalt, aber es ist wichtig, dass du etwas verstehst wie Lean manche Sachen macht. +Als erstes geht es um implizite und explizite Argumente von Lemmas. **Explizite Argumente** +schreibt man mit runden Klammern `()`, **impliziete Argumente** mit geschweiften `{}`. -- Implizite und explizite Argumente. -- Types +Als implizit werden alle Argumente markiert, die Lean selbständig aus dem Kontext +erschliessen und einfüllen kann. +Als Beispiel hier zweimal das gleiche Lemma, einmal ohne impliziten Argumenten und einmal mit +``` +lemma not_or_of_imp' (A B : Prop) (h : A → B) : ¬A ∨ B := sorry + +lemma not_or_of_imp {A B : Prop} (h : A → B) : ¬A ∨ B := sorry +``` + +Hat man nun `g : C → D` dann braucht man diese Lemmas mit +`have := not_or_of_imp g` oder `have := not_or_of_imp' C D g`. + +Wie man sieht erschliesst Lean die impliziten Argumente automatisch und es wäre deshalb +unnötig, diese jedes Mal explizit angeben zu müssen. + +TODO +(Trick mit `@not_or_of_imp` kann man sagen, dass man **alle** Argumente angeben möchte und mir +`not_or_of_imp g (B := D)` könnte man ein spezifisches implizites Argument spezifizieren. +Wenn man diese Tricks braucht, heisst das aber meistens, das etwas nicht optimal definiert +ist.) + +TODO +Zudem gibt es noch Argumente in eckigen Klammern `[]`. Dies sind auch implizite +Argumente, die aber von der **Instance Resolution** gefüllt werden sollen. Dies +wird später kommen, aber ein typisches Beispiel ist `(S : Type _) [ring S]` was Lean +sagt, es soll suchen gehen, ob es weiss, dass `S` ein Ring ist. " open Set @@ -30,3 +56,6 @@ Statement trivial NewTactics rw + +#check not_not +#check not_or_of_imp diff --git a/server/testgame/TestGame/Levels/LeanStuff/L02_Universe.lean b/server/testgame/TestGame/Levels/LeanStuff/L02_Universe.lean new file mode 100644 index 0000000..2dcd62e --- /dev/null +++ b/server/testgame/TestGame/Levels/LeanStuff/L02_Universe.lean @@ -0,0 +1,37 @@ +import TestGame.Metadata + +import Mathlib + +set_option tactic.hygienic false + +Game "TestGame" +World "LeanStuff" +Level 2 + +Title "Universen" + +Introduction +" +In der Mathematik stösst man manchmal an Mengentheoretische Grenzen, und so auch in Lean. + +Klassisch ist bekannt dass die \"Menge aller Mengen\" nicht existieren kann. + +Falls man an diese Grenzen stösst (z.B. in der Mengenlehre oder Kategorientheorie) hat Lean +Universen bereit: `Type` ist eigentlich `Type 0` und es gibt auch `Type 1, Type 2, ...` + +Deshalb sieht man oft in Lean-Code `(R : Type _)` wenn es keine mengentheoretischen +Probleme gibt (`_` ist ein Platzhalter) oder `universe u` am Anfang und dann `(R : Type u)` +falls man diese mengentheoretischen Probleme kontrollieren muss. + +In der Praxis kommt man aber relativ weit, wenn man sich erst mal nicht mit Universen +beschäftigt, und lediglich weiss, dass es sowas gibt. +" + +Statement +"TODO" + (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by + ring + +Hint (R : Type _) (h : CommRing R) (a : R) (b : R) : a + b = b + a => +"Die Taktik `ring` funktioniert in jedem Typen, +der mindestens eine Instanz `[Ring R]` hat." diff --git a/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean b/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean new file mode 100644 index 0000000..4310b5e --- /dev/null +++ b/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean @@ -0,0 +1,57 @@ +import TestGame.Metadata + +import Mathlib + +set_option tactic.hygienic false + +Game "TestGame" +World "LeanStuff" +Level 3 + +Title "Implizite Argumente" + +Introduction +" + +Auch wichtiger Syntax ist der Unterschied zwischen +impliziten und expliziten Argumenten von Lemmas. **Explizite Argumente** +schreibt man mit runden Klammern `()`, **impliziete Argumente** mit geschweiften `{}`. + +Als implizit werden alle Argumente markiert, die Lean selbständig aus dem Kontext +erschliessen und einfüllen kann. + +Als Beispiel hier zweimal das gleiche Lemma, einmal ohne impliziten Argumenten und einmal mit +``` +lemma not_or_of_imp' (A B : Prop) (h : A → B) : ¬A ∨ B := sorry + +lemma not_or_of_imp {A B : Prop} (h : A → B) : ¬A ∨ B := sorry +``` + +Hat man nun `g : C → D` dann braucht man diese Lemmas mit +`have := not_or_of_imp g` oder `have := not_or_of_imp' C D g`. + +Wie man sieht erschliesst Lean die impliziten Argumente automatisch und es wäre deshalb +unnötig, diese jedes Mal explizit angeben zu müssen. + +TODO +(Trick mit `@not_or_of_imp` kann man sagen, dass man **alle** Argumente angeben möchte und mir +`not_or_of_imp g (B := D)` könnte man ein spezifisches implizites Argument spezifizieren. +Wenn man diese Tricks braucht, heisst das aber meistens, das etwas nicht optimal definiert +ist.) + + +Nebenbemerkung: Es gibt auch noch implizite **Klassen-Elemente** mit eckigen Klammern `[]` +wie zum Beispiel `[CommRing R]` im vorigen Beispiel. Diese werden später behandelt, +und sagen Lean, dass es für dieses Argument eine **Instanz** suchen gehen soll. Diese +Instanzen werden mehrheitlich dafür verwendet, mathematische Strukturen auf Typen zu +definieren, aber das kommt alles später. +" + +Statement +"TODO" + (R S : Type _) [CommRing R] (a b : R) : a + b = b + a := by + ring + +Hint (R : Type _) (h : CommRing R) (a : R) (b : R) : a + b = b + a => +"Die Taktik `ring` funktioniert in jedem Typen, +der mindestens eine Instanz `[Ring R]` hat." diff --git a/server/testgame/TestGame/Levels/Numbers.lean b/server/testgame/TestGame/Levels/Numbers.lean new file mode 100644 index 0000000..622c5a4 --- /dev/null +++ b/server/testgame/TestGame/Levels/Numbers.lean @@ -0,0 +1,2 @@ +import TestGame.Levels.Numbers.L01_PNat +import TestGame.Levels.Numbers.L02_PNat diff --git a/server/testgame/TestGame/Levels/Numbers/L01_PNat.lean b/server/testgame/TestGame/Levels/Numbers/L01_PNat.lean new file mode 100644 index 0000000..fa1a217 --- /dev/null +++ b/server/testgame/TestGame/Levels/Numbers/L01_PNat.lean @@ -0,0 +1,82 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Numbers" +Level 1 + +Title "" + +Introduction +" +-- Level name : Positive natürliche Zahlen + +import data.pnat.basic + +/- +In diesem Level lernst du neben `ℕ` weitere Arten von +Zahlen kennen: `ℕ+`,`ℤ`, `ℚ`, `ℝ`, `ℂ`. + +Manchmal sieht man in der Literatur Diskussionen, ob die natürlichen Zahlen jetzt bei `0` oder `1` +anfangen, wobei zumindest in der formalisierten Mathematik (z.B. ZFC-Mengenlehre) +eigentlich immer `ℕ = {0, 1, 2, 3, …}` definiert wird. + +So ist auch in Lean `1` als `0.succ` und `2 = 1.succ = 0.succ.succ` definiert und +Lean hat eine separate Notation `ℕ+` (oder `pnat`) für alle *positiven* natürlichen Zahlen. + +Dies ist als Sub-Typ von `ℕ` definiert: +`def pnat := {n : ℕ // 0 < n}` + +ein Element `(p : ℕ+)` besteht also aus einer natürlichen Zahl `(p.val : ℕ)` +(oder auch `p.1`, wobei `p.val` bevorzugt ist) sowie einem Beweis, dass diese positiv ist, +`p.property` (oder `p.2`). + +Solche Strukturen mit mehr als einem Feld kann man in Lean mit dem anonymen Konstruktor `⟨_, _⟩` +erstellen, wie du schon einmal beim `∃` gesehen hast: `(⟨n, h⟩ : ℕ+)` +" + +Statement +"" + (a : ℕ+) : (a : ℕ) ≠ 0 := by + apply ne_of_gt + rcases a with ⟨a, ha⟩ + assumption + + +-- -/ + +-- /- Hint : a.property +-- `have ha := a.property` speichert die `ℕ+`-Eigenschaft dass `0 < a.val` +-- gilt als neue Variable. +-- -/ + +-- /- Hint : ne_of_lt/ne_of_gt +-- `a < b → a ≠ b` +-- oder +-- `a < b → b ≠ a` + +-- alternativ kannst du auch mit `symmetry` ein symmetrischen Goal drehen. +-- -/ + +-- /- Lemma : no-side-bar +-- Beweise. +-- -/ +-- example (a : ℕ+) : (a : ℕ) ≠ 0 := +-- begin +-- have ha := a.property, +-- symmetry, +-- apply ne_of_lt, +-- exact ha, +-- end + +-- /- Axiom : ne_of_lt +-- `a < b → a ≠ b`. +-- -/ + +-- /- Axiom : ne_of_gt +-- `a < b → b ≠ a`. +-- -/ + +-- /- Tactic : symmetry +-- Dreht ein symmetrisches Goal wie `A = B`, `A ≠ B`, `A ↔ B`, ... +-- -/ diff --git a/server/testgame/TestGame/Levels/Numbers/L02_PNat.lean b/server/testgame/TestGame/Levels/Numbers/L02_PNat.lean new file mode 100644 index 0000000..bca2e8f --- /dev/null +++ b/server/testgame/TestGame/Levels/Numbers/L02_PNat.lean @@ -0,0 +1,24 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "Numbers" +Level 2 + +Title "" + +Introduction +" + Das Lemma, das du gerade bewiesen hast, findest du als `pnat.ne_zero` +" + +Statement +"" + (a b : ℕ+) : (a : ℕ) * b ≠ 0 := by + by_contra h + rw [Nat.mul_eq_zero] at h + cases h + have := PNat.ne_zero a + contradiction + have := PNat.ne_zero b + contradiction diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 9aa3f37..638227d 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -32,7 +32,7 @@ HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => HiddenHint (A : Prop) (hA : A) : A => "Du hast einen Beweis dafür in den *Annahmen*." -NewTactics constructor assumption +NewTactics constructor DisabledTactics tauto -- Statement diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 6579ff7..3237428 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -33,7 +33,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => HiddenHint (A : Prop) (hA : A) : A => "Du hast einen Beweis dafür in den *Annahmen*." -NewTactics constructor assumption +NewTactics rcases DisabledTactics tauto -- Statement diff --git a/server/testgame/TestGame/Levels/SetFunction.lean b/server/testgame/TestGame/Levels/SetFunction.lean index ef3c09a..bf9cfbc 100644 --- a/server/testgame/TestGame/Levels/SetFunction.lean +++ b/server/testgame/TestGame/Levels/SetFunction.lean @@ -1,4 +1,7 @@ -import TestGame.Levels.SetFunction.L01_xxx +import TestGame.Levels.SetFunction.L01_Image +import TestGame.Levels.SetFunction.L02_Preimage +import TestGame.Levels.SetFunction.L03_Range +import TestGame.Levels.SetFunction.L04_ImageUnion Game "TestGame" World "SetFunction" diff --git a/server/testgame/TestGame/Levels/SetFunction/L01_Image.lean b/server/testgame/TestGame/Levels/SetFunction/L01_Image.lean new file mode 100644 index 0000000..1bfede9 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetFunction/L01_Image.lean @@ -0,0 +1,65 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "SetFunction" +Level 1 + +Title "" + +open Set + +Introduction +" +Wenn man mit Abildungen auf Mengen arbeitet, muss man in Lean etwas aufpassen, um +die Typen (z.B. `(U : Type _)`) und Mengen von diesen Typen (z.B. `(S : Set U)`) +zu unterscheiden. + +Abbildungen sind prinzipiell immer auf Typen definiert. Wenn eine Funktion nicht +auf dem ganzen Typen definiert ist, hat man prinzipiell zwei Optionen: + +1. Nach dem Motto \"Chunk in, chunk out\" werden in der Mathlib Funktionen +oft einfach auf irgendwas gesetzt wenn sie nicht definiert sind, so gibt `1 / 0` in `ℕ` +einfach `0`. Dies funktioniert, weil dann alle relevanten Theoreme, die von `x / n` +handeln, dann Annahmen der Form `(h : n ≠ 0)` haben. +2. Man kann auch Funktionen auf *Subtypen* definieren, also z.B. auf `ℕ+`. + + +" + + +-- /- Image of Union -/ +-- lemma image_unionₓ + +Statement +"" + (S T : Set ℕ) (f : ℕ → ℕ) : (f '' S) ∪ (f '' T) = f '' (S ∪ T) := by + ext i + rw [mem_union] + simp_rw [mem_image] + constructor + intro h + rcases h with ⟨x, hx, hx'⟩ | ⟨x, hx, hx'⟩ + use x + constructor + apply mem_union_left + assumption + assumption + use x + constructor + apply mem_union_right + assumption + assumption + rintro ⟨x, hx, hx'⟩ + rw [mem_union] at hx + rcases hx with hx | hx + left + use x + constructor + assumption + assumption + right + use x + constructor + assumption + assumption diff --git a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean b/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean deleted file mode 100644 index b2bf693..0000000 --- a/server/testgame/TestGame/Levels/SetFunction/L01_xxx.lean +++ /dev/null @@ -1,24 +0,0 @@ -import TestGame.Metadata - -import Mathlib - -set_option tactic.hygienic false - -Game "TestGame" -World "SetFunction" -Level 1 - -Title "Abbildungen" - -Introduction -" -Fortsetzung: Funktionen auf Mengen. - -" - -Statement - "TODO" - : True := by - trivial - -NewTactics rw diff --git a/server/testgame/TestGame/Levels/SetFunction/L02_Preimage.lean b/server/testgame/TestGame/Levels/SetFunction/L02_Preimage.lean new file mode 100644 index 0000000..b94e605 --- /dev/null +++ b/server/testgame/TestGame/Levels/SetFunction/L02_Preimage.lean @@ -0,0 +1,21 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "SetFunction" +Level 2 + +Title "" + +Introduction +" +" + +Statement +"" + (U : Set ℕ) (f : ℕ → ℕ) : U ⊆ f ⁻¹' (f '' U) := by + intro x hx + use x + constructor + assumption + rfl diff --git a/server/testgame/TestGame/Levels/SetFunction/L03_Range.lean b/server/testgame/TestGame/Levels/SetFunction/L03_Range.lean new file mode 100644 index 0000000..21d2ccc --- /dev/null +++ b/server/testgame/TestGame/Levels/SetFunction/L03_Range.lean @@ -0,0 +1,21 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "SetFunction" +Level 3 + +Title "" + +Introduction +" +" + +Statement +"" + (U : Set ℕ) (f : ℕ → ℕ) : U ⊆ f ⁻¹' (f '' U) := by + intro x hx + use x + constructor + assumption + rfl diff --git a/server/testgame/TestGame/Levels/SetFunction/L04_ImageUnion.lean b/server/testgame/TestGame/Levels/SetFunction/L04_ImageUnion.lean new file mode 100644 index 0000000..7bfcfca --- /dev/null +++ b/server/testgame/TestGame/Levels/SetFunction/L04_ImageUnion.lean @@ -0,0 +1,18 @@ +import TestGame.Metadata +import Mathlib + +Game "TestGame" +World "SetFunction" +Level 4 + +Title "" + +Introduction +" +" + +Statement +"" + (I U V : Type _) (f : U → V) (N : I → Set V) : + f ⁻¹' (⋃ (i : I), N i) = ⋃ i, f ⁻¹' (N i) := by + simp diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean index 4dc6b45..b1adad1 100644 --- a/server/testgame/TestGame/TacticDocs.lean +++ b/server/testgame/TestGame/TacticDocs.lean @@ -208,14 +208,14 @@ TacticDoc use TODO " -TacticDoc sufficesₓ +TacticDoc «suffices» " ## Beschreibung TODO " -TacticDoc haveₓ +TacticDoc «have» " ## Beschreibung