From 87f943a08cc9b2c2ef549fbab342959263219565 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 6 Dec 2022 19:33:29 +0100 Subject: [PATCH 1/2] levels: negation, nat-basics --- server/testgame/TestGame.lean | 14 ++++ server/testgame/TestGame/HelperTools.lean | 11 +++ server/testgame/TestGame/LemmaDocs.lean | 32 +++++++++ .../TestGame/Levels/LeftOvers/Lxx_Prime.lean | 61 ++++++++++++++++ .../Levels/LeftOvers/xx_Functions.lean | 25 +++++++ .../TestGame/Levels/Logic/L08b_Or.lean | 3 + .../Naturals/{L01_Nat.lean => L01_Ring.lean} | 0 .../Naturals/{L02_Nat.lean => L02_Ring.lean} | 0 .../{L03_Nat.lean => L03_Exists.lean} | 8 +-- .../TestGame/Levels/Naturals/L04_Forall.lean | 38 ++++++++++ .../TestGame/Levels/Negation/L01_False.lean | 2 +- .../TestGame/Levels/Negation/L02_Contra.lean | 9 ++- .../TestGame/Levels/Negation/L03_Contra.lean | 32 ++++++--- .../TestGame/Levels/Negation/L04_Contra.lean | 21 ++++-- .../TestGame/Levels/Negation/L05_Not.lean | 13 ++-- .../Levels/Negation/L06_ByContra.lean | 48 +++++++++++++ .../TestGame/Levels/Negation/L06_PushNeg.lean | 20 ------ .../Levels/Negation/L07_Contrapose.lean | 33 +++++++++ .../Levels/Negation/L07_Contraposition.lean | 23 ------- .../TestGame/Levels/Negation/L08_Contra.lean | 26 ------- .../Levels/Negation/L08_Contrapose.lean | 32 +++++++++ .../Levels/Negation/L09_Contraposition.lean | 27 -------- .../TestGame/Levels/Negation/L09_PushNeg.lean | 36 ++++++++++ .../TestGame/Levels/Quantors/L01_Exists.lean | 69 ------------------- .../TestGame/Levels/Quantors/L02_Forall.lean | 39 ----------- .../TestGame/Levels/Quantors/TMP.lean | 22 ------ server/testgame/TestGame/TacticDocs.lean | 37 ++++++++++ server/testgame/TestGame/ToBePorted.lean | 16 +++++ server/testgame/lakefile.lean | 8 ++- 29 files changed, 443 insertions(+), 262 deletions(-) create mode 100644 server/testgame/TestGame/HelperTools.lean create mode 100644 server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean create mode 100644 server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean rename server/testgame/TestGame/Levels/Naturals/{L01_Nat.lean => L01_Ring.lean} (100%) rename server/testgame/TestGame/Levels/Naturals/{L02_Nat.lean => L02_Ring.lean} (100%) rename server/testgame/TestGame/Levels/Naturals/{L03_Nat.lean => L03_Exists.lean} (92%) create mode 100644 server/testgame/TestGame/Levels/Naturals/L04_Forall.lean create mode 100644 server/testgame/TestGame/Levels/Negation/L06_ByContra.lean delete mode 100644 server/testgame/TestGame/Levels/Negation/L06_PushNeg.lean create mode 100644 server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean delete mode 100644 server/testgame/TestGame/Levels/Negation/L07_Contraposition.lean delete mode 100644 server/testgame/TestGame/Levels/Negation/L08_Contra.lean create mode 100644 server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean delete mode 100644 server/testgame/TestGame/Levels/Negation/L09_Contraposition.lean create mode 100644 server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean delete mode 100644 server/testgame/TestGame/Levels/Quantors/L01_Exists.lean delete mode 100644 server/testgame/TestGame/Levels/Quantors/L02_Forall.lean delete mode 100644 server/testgame/TestGame/Levels/Quantors/TMP.lean create mode 100644 server/testgame/TestGame/ToBePorted.lean diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index e6cd5fe..65a60a7 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -14,3 +14,17 @@ import TestGame.Levels.Logic.L06d_Iff import TestGame.Levels.Logic.L07_And import TestGame.Levels.Logic.L08_Or import TestGame.Levels.Logic.L08b_Or +import TestGame.Levels.Logic.L08c_Or +import TestGame.Levels.Naturals.L01_Ring +import TestGame.Levels.Naturals.L02_Ring +import TestGame.Levels.Naturals.L03_Exists +import TestGame.Levels.Naturals.L04_Forall +import TestGame.Levels.Negation.L01_False +import TestGame.Levels.Negation.L02_Contra +import TestGame.Levels.Negation.L03_Contra +import TestGame.Levels.Negation.L04_Contra +import TestGame.Levels.Negation.L05_Not +import TestGame.Levels.Negation.L06_ByContra +import TestGame.Levels.Negation.L07_Contrapose +import TestGame.Levels.Negation.L08_Contrapose +import TestGame.Levels.Negation.L09_PushNeg diff --git a/server/testgame/TestGame/HelperTools.lean b/server/testgame/TestGame/HelperTools.lean new file mode 100644 index 0000000..b61ca25 --- /dev/null +++ b/server/testgame/TestGame/HelperTools.lean @@ -0,0 +1,11 @@ +import Lean + +-- show all available options +instance : ToString Lean.OptionDecl where + toString a := toString a.defValue ++ ", [" ++ toString a.group ++ "]: " ++ toString a.descr + +def showOptions : IO Unit := do + let a <- Lean.getOptionDeclsArray + IO.println f! "{a}" + +#eval showOptions diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index b12744f..123fed1 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -12,3 +12,35 @@ import GameServer.Commands -- LemmaSet addition : "Addition lemmas" := -- zero_add add_zero + +LemmaDoc not_not as not_not in "Logic" +"`∀ (A : Prop), ¬¬A ↔ A`." + + + + + +LemmaDoc even as even in "Nat" +" +`even n` ist definiert als `∃ r, a = 2 * r`. +Die Definition kann man mit `unfold even at *` einsetzen. +" + +LemmaDoc odd as odd in "Nat" +" +`odd n` ist definiert als `∃ r, a = 2 * r + 1`. +Die Definition kann man mit `unfold odd at *` einsetzen. +" + +LemmaDoc not_odd as not_odd in "Nat" +"`¬ (odd n) ↔ even n`" + +LemmaDoc not_even as not_even in "Nat" +"`¬ (even n) ↔ odd n`" + +LemmaDoc even_square as even_square in "Nat" +"`∀ (n : ℕ), even n → even (n ^ 2)`" + + +LemmaSet natural : "Natürliche Zahlen" := +even odd not_odd not_even diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean new file mode 100644 index 0000000..a2a8c77 --- /dev/null +++ b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean @@ -0,0 +1,61 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet +def even (a : ℕ) : Prop := ∃ r, a = 2 * r +def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1 + +lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry + +lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry + +lemma even_square (n : ℕ) : even n → even (n ^ 2) := by + intro ⟨x, hx⟩ + unfold even at * + use 2 * x ^ 2 + rw [hx] + ring + +def prime (n : ℕ) : Prop := (2 ≤ n) ∧ ∀ a b, n = a * b → a = 1 ∨ b = 1 + +Game "TestGame" +World "Nat" +Level 4 + +Title "Für alle" + +Introduction +" +Eine Primzahl könnte man folgendermassen implementieren: +``` +def prime (p : ℕ) : Prop := (2 ≤ p) ∧ (∀ a b, p = a * b → a = 1 ∨ b = 1) +``` +Also, eine Zahl `p` ungleich `0` oder `1`, für die gilt wenn `a * b = p` dann ist +entweder `a` oder `b` eins. + +(Tatsächlich ist eine Primzahl dann etwas genereller definiert, aber dazu mehr später.) + + + + +" + +Statement + "Wenn `n * m` eine Primzahl ist, dann ist einer der beiden Faktoren eins." + (p n m : ℕ) (h : prime p) (h₂ : p = m * n) : n = 1 ∨ m = 1 := by + unfold prime at h + rcases h with ⟨l, r⟩ + apply r + rw [h₂] + ring + + + +Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) => +"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie +`(x : ℕ) → `" + +Tactics ring intro unfold diff --git a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean new file mode 100644 index 0000000..84c8044 --- /dev/null +++ b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean @@ -0,0 +1,25 @@ +import TestGame.Metadata +import Mathlib.Tactic.Ring + +Game "TestGame" +World "Function" +Level 1 + +Title "Funktionen" + +Introduction +" +Funktionen werden in Lean als `(f : ℕ → ℕ)` geschrieben (`\\to`), also mit dem gleichen +Pfeil wie Implikationen. Entsprechend kann man Implikationen und Funktionen genau +gleich behandeln. + +" + +Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by + let g := fun (x : ℕ) ↦ 0 + use g + simp + +Conclusion "" + +Tactics use simp diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean index dafbd4a..10b5aff 100644 --- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean @@ -4,6 +4,9 @@ import Mathlib.Tactic.LeftRight --set_option tactic.hygienic false +--set_option autoImplicit false + + Game "TestGame" World "TestWorld" Level 15 diff --git a/server/testgame/TestGame/Levels/Naturals/L01_Nat.lean b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean similarity index 100% rename from server/testgame/TestGame/Levels/Naturals/L01_Nat.lean rename to server/testgame/TestGame/Levels/Naturals/L01_Ring.lean diff --git a/server/testgame/TestGame/Levels/Naturals/L02_Nat.lean b/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean similarity index 100% rename from server/testgame/TestGame/Levels/Naturals/L02_Nat.lean rename to server/testgame/TestGame/Levels/Naturals/L02_Ring.lean diff --git a/server/testgame/TestGame/Levels/Naturals/L03_Nat.lean b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean similarity index 92% rename from server/testgame/TestGame/Levels/Naturals/L03_Nat.lean rename to server/testgame/TestGame/Levels/Naturals/L03_Exists.lean index 14dcee1..df0b272 100644 --- a/server/testgame/TestGame/Levels/Naturals/L03_Nat.lean +++ b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean @@ -4,6 +4,7 @@ import Mathlib.Tactic.Contrapose import Mathlib.Tactic.Use import Mathlib.Tactic.Ring +import TestGame.ToBePorted Game "TestGame" World "Nat" @@ -32,12 +33,7 @@ Hierzu gibt es 3 wichtige Taktiken: soll. Das macht man mit `use y` " --- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet -def even (a : ℕ) : Prop := ∃ r, a = 2 * r - -def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1 - -Statement (n : ℕ) (h : even n) : even (n ^ 2) := by +Statement even_square (n : ℕ) (h : even n) : even (n ^ 2) := by unfold even at * rcases h with ⟨x, hx⟩ use 2 * x ^ 2 diff --git a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean new file mode 100644 index 0000000..7175f1d --- /dev/null +++ b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean @@ -0,0 +1,38 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted + +Game "TestGame" +World "Nat" +Level 4 + +Title "Für alle" + +Introduction +" +Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`). + +Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`. +" + +Statement : ∀ (x : ℕ), (even x) → odd (1 + x) := by + intro x h + unfold even at h + unfold odd + rcases h with ⟨y, hy⟩ + use y + rw [hy] + ring + +Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) => +"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie +`(x : ℕ) → `" + +Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle +praktisch gleich. Mehr dazu später." + +Tactics ring intro unfold diff --git a/server/testgame/TestGame/Levels/Negation/L01_False.lean b/server/testgame/TestGame/Levels/Negation/L01_False.lean index 187e454..a2ca589 100644 --- a/server/testgame/TestGame/Levels/Negation/L01_False.lean +++ b/server/testgame/TestGame/Levels/Negation/L01_False.lean @@ -6,7 +6,7 @@ Game "TestGame" World "Contradiction" Level 1 -Title "Widerspruch" +Title "Widerspruch beweist alles." Introduction " diff --git a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean index e06756f..6a844ea 100644 --- a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean @@ -2,11 +2,13 @@ import TestGame.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight +import TestGame.ToBePorted + Game "TestGame" World "Contradiction" Level 2 -Title "Widerspruch" +Title "Ad absurdum" Introduction " @@ -16,14 +18,11 @@ also `(h : A)` und `(g : ¬ A)`. (`\\not`) Statement "Ein Widerspruch impliziert alles." - (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by + (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by contradiction Conclusion " -Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass -\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\". " --- TODO: Oder doch ganz entfernen? Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean index 8ca41cc..a7ad661 100644 --- a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean @@ -1,31 +1,41 @@ import TestGame.Metadata import Std.Tactic.RCases import Mathlib.Tactic.LeftRight +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted Game "TestGame" World "Contradiction" Level 3 -Title "Widerspruch" +Title "Ad absurdum" Introduction " -Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form -`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ` -oder auch Annahmen der Form `A ≠ A` (`\\ne`). +Aber, die Aussagen müssen wirklich exakte Gegenteile sein. + +Hier musst du zuerst eines der Lemmas `not_odd : ¬ odd n ↔ even n` oder +`not_even : ¬ even n ↔ odd n` benützen, um einer der Terme umzuschreiben. " Statement "Ein Widerspruch impliziert alles." - (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by - rw [g₁] at h + (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by + rw [← not_even] at h₂ contradiction -Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A => - "Recap: `rw [...] at h` hilft dir hier." +Message (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 => +"Schreibe zuerst eine der Aussagen mit `rw [←not_even] at h₂` um, damit diese genaue +Gegenteile sind." -Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A => - "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt - einen Widerspruch." +Conclusion +" +Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass +\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\". +" +-- TODO: Oder doch ganz entfernen? Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean index a55200b..992f977 100644 --- a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean @@ -1,20 +1,31 @@ import TestGame.Metadata -import Mathlib +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight Game "TestGame" World "Contradiction" Level 4 -Title "Widerspruch" +Title "Ad absurdum" Introduction " +Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form +`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ` +oder auch Annahmen der Form `A ≠ A` (`\\ne`). " - Statement - (A : Prop) : A := by - by_contradiction + "Ein Widerspruch impliziert alles." + (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by + rw [g₁] at h + contradiction + +Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A => + "Recap: `rw [...] at h` hilft dir hier." +Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A => + "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt + einen Widerspruch." Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L05_Not.lean b/server/testgame/TestGame/Levels/Negation/L05_Not.lean index 0bbd75a..bf1012d 100644 --- a/server/testgame/TestGame/Levels/Negation/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Negation/L05_Not.lean @@ -5,16 +5,19 @@ Game "TestGame" World "Contradiction" Level 5 -Title "Widerspruch" +Title "Nicht-nicht" Introduction " +Wenn man ein Nicht (`¬`) im Goal hat, will man meistens einen Widerspruch starten, +wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form +`¬ (¬ A)`, in welchem Fall das Lemma `not_not` nützlich ist. " - Statement - (A : Prop) : A := by - not_not + (A : Prop) : ¬ (¬ A) ↔ A := by + rw [not_not] +Tactics rw -Tactics contradiction +Lemmas not_not diff --git a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean new file mode 100644 index 0000000..4cfd4e2 --- /dev/null +++ b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean @@ -0,0 +1,48 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 6 + +Title "Widerspruch" + +Introduction +" +Um einen Beweis per Widerspruch zu führen, kann man mit `by_contra h` annehmen, +dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen. +" + +Statement + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." + (n : ℕ) (h : odd (n ^ 2)) : odd n := by + by_contra g + rw [not_odd] at g + + suffices ¬ odd (n ^ 2) by contradiction -- TODO: I don't like this + + rw [not_odd] + apply even_square + assumption + +Message : false => +"Es gibt mehrere Möglichkeiten, wie man nach einem `by_contra` weitergeht. + +Hier wollen wir einen Widerspruch zu `h` machen. Wir machen das mit +`suffices ¬ odd (n ^ 2) by contradiction`, worauf man dann nur noch `¬ odd (n ^ 2)` +zeigen muss." + +Hint (n : ℕ) : ¬ (odd (n ^ 2)) => +"Das Lemma `not_odd` ist hilfreich." + +Message (n: ℕ) (h : odd (n ^ 2)) (g : even n) : even (n ^ 2) => +"Das haben wir schon gezeigt. Mit `apply even_square` kannst du das Lemma anwenden." + +Tactics contradiction by_contra rw apply assumption -- TODO: suffices + +Lemmas odd even not_odd not_even even_square diff --git a/server/testgame/TestGame/Levels/Negation/L06_PushNeg.lean b/server/testgame/TestGame/Levels/Negation/L06_PushNeg.lean deleted file mode 100644 index 3885f61..0000000 --- a/server/testgame/TestGame/Levels/Negation/L06_PushNeg.lean +++ /dev/null @@ -1,20 +0,0 @@ -import TestGame.Metadata -import Mathlib - -Game "TestGame" -World "Contradiction" -Level 6 - -Title "Widerspruch" - -Introduction -" -" - - -Statement - (A : Prop) : A := by - pushNeg - - -Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean new file mode 100644 index 0000000..f273736 --- /dev/null +++ b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean @@ -0,0 +1,33 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 7 + +Title "Kontraposition" + +Introduction +" +Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen. +Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)` +logisch equivalent sind. + +Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden. +" + +Statement + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." + (n : ℕ) : odd (n ^ 2) → odd n := by + contrapose + rw [not_odd] + rw [not_odd] + apply even_square + +Tactics contrapose rw apply +Lemmas even odd not_even not_odd even_square diff --git a/server/testgame/TestGame/Levels/Negation/L07_Contraposition.lean b/server/testgame/TestGame/Levels/Negation/L07_Contraposition.lean deleted file mode 100644 index 5685e9a..0000000 --- a/server/testgame/TestGame/Levels/Negation/L07_Contraposition.lean +++ /dev/null @@ -1,23 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose - -Game "TestGame" -World "Contradiction" -Level 7 - -Title "Kontraposition" - -Introduction -" -Im Gegensatz zum Widerspruch, wo -" - -Statement - "Ein Widerspruch impliziert alles." - (A B : Prop) (h : ¬ B → ¬ A) (hA : A) : B := by - revert hA - contrapose - assumption - -Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L08_Contra.lean b/server/testgame/TestGame/Levels/Negation/L08_Contra.lean deleted file mode 100644 index 778c547..0000000 --- a/server/testgame/TestGame/Levels/Negation/L08_Contra.lean +++ /dev/null @@ -1,26 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose - -Game "TestGame" -World "Contradiction" -Level 8 - -Title "Kontraposition" - -Introduction -" -Im Gegensatz zum Widerspruch, wo -" - --- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet - --- Statement --- "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." --- (n : ℕ) (h : odd n ^ 2) : odd n := by --- byContradiction g --- rw [not_odd] at g --- ... --- contradiction - -Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean new file mode 100644 index 0000000..50b458f --- /dev/null +++ b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean @@ -0,0 +1,32 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 8 + +Title "Kontraposition" + +Introduction +" +Lean Trick: Wenn das Goal nicht bereits eine Implikation ist, sondern man eine Annahme `h` hat, die +Man gerne für die Kontraposition benützen würde, kann man mit `revert h` diese als +Implikationsannahme ins Goal schreiben. +" + +Statement + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." + (n : ℕ) (h : odd (n ^ 2)): odd n := by + revert h + contrapose + rw [not_odd] + rw [not_odd] + apply even_square + +Tactics contrapose rw apply revert +Lemmas even odd not_even not_odd even_square diff --git a/server/testgame/TestGame/Levels/Negation/L09_Contraposition.lean b/server/testgame/TestGame/Levels/Negation/L09_Contraposition.lean deleted file mode 100644 index c1aab61..0000000 --- a/server/testgame/TestGame/Levels/Negation/L09_Contraposition.lean +++ /dev/null @@ -1,27 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose - -Game "TestGame" -World "Contradiction" -Level 9 - -Title "Kontraposition" - -Introduction -" -Im Gegensatz zum Widerspruch, wo -" - --- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet - --- Statement --- "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." --- (n : ℕ) (h : odd n ^ 2) : odd n := by --- revert h --- contrapose --- rw [not_odd] --- intro --- trivial (?) - -Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean new file mode 100644 index 0000000..c759ba1 --- /dev/null +++ b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean @@ -0,0 +1,36 @@ +import TestGame.Metadata +import Mathlib.Tactic.PushNeg +import Mathlib + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 9 + +Title "PushNeg" + +Introduction +" +Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man +mit `push_neg` das `¬` durch den Quantor hindurchschieben. +" + +Statement + "Es existiert keine natürliche Zahl, die grösser als alle anderen." + : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by + push_neg + intro n + use 3*n + 6 + rw [not_odd] + unfold even + use 2*n + 3 + ring + +Message (n : ℕ) : (Exists fun k ↦ ¬odd (n + k)) => +"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutz `use ...` +mit der richtigen Zahl." + +Conclusion "" + +Tactics push_neg intro use rw unfold ring diff --git a/server/testgame/TestGame/Levels/Quantors/L01_Exists.lean b/server/testgame/TestGame/Levels/Quantors/L01_Exists.lean deleted file mode 100644 index a5bfdef..0000000 --- a/server/testgame/TestGame/Levels/Quantors/L01_Exists.lean +++ /dev/null @@ -1,69 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - - -Game "TestGame" -World "Quantors" -Level 9 - -Title "Kontraposition" - -Introduction -" -Häufig enthalten logische Aussagen die Quantoren \"für alle `x`\" und -\"es existiert ein `x`, so dass\". In Lean schreibt man diese wie in der Mathe -mit den Zeichen `∀` und `∃` (`\\forall`, `\\exists`): - -Beide können mehrere Variablen annehmen: `∃ (x : ℕ) (y : ℕ), x ^ 3 = 2 * y + 1` ist das selbe -wie `∃ (x : ℕ), (∃ (y : ℕ), x ^ 3 = 2 * y + 1)`. - -Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und -ein `x` erhalten, dass die Aussage erfüllt. - -Bei einem Exists-Statement im Goal kann man mit `use` das Element angeben, dass dieses `∃ x,` -erfüllt. -" - --- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet -def even (a : ℕ) : Prop := ∃ r, a = r + r - -def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1 - -Statement (n : ℕ) (h : even n) : even (n ^ 2) := by - unfold even at * - rcases h with ⟨x, hx⟩ - use 2 * x ^ 2 - rw [hx] - ring - --- TODO: Server PANIC because of the `even`. --- --- Message (n : ℕ) (h : even n) : even (n ^ 2) => --- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder --- `unfold even at *` ersetzen. --- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert --- genau gleich, wenn du das `unfold` rauslöscht." - -Message (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r => -"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und -ein `x` erhalten, dass die Aussage erfüllt." - -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r => -"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass -die Aussage erfüllen soll." - -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r => -"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass -die Aussage erfüllen soll." - -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => -"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu -`x + x` umschreiben..." - -Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => -"Die Taktik `ring` löst solche Gleichungen." - -Tactics unfold rcases use rw ring diff --git a/server/testgame/TestGame/Levels/Quantors/L02_Forall.lean b/server/testgame/TestGame/Levels/Quantors/L02_Forall.lean deleted file mode 100644 index e32f996..0000000 --- a/server/testgame/TestGame/Levels/Quantors/L02_Forall.lean +++ /dev/null @@ -1,39 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.Contrapose -import Mathlib.Tactic.Use -import Mathlib.Tactic.Ring - - -Game "TestGame" -World "Quantors" -Level 9 - -Title "Kontraposition" - -Introduction -" -Bei einem `∀ x,` im Goal kann man mit `intro x` annehmen, dass man ein solches `x` hat. - -Ein `(h : ∀ x, _)` in den Annahmen kann .... -" - --- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet -def even (a : ℕ) : Prop := ∃ r, a = r + r -def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1 - -Statement : ∀ (x : ℕ), even x → even (x + 2) := by - intro x h - unfold even at * - rcases h with ⟨y, hy⟩ - use y + 1 - rw [hy] - ring - --- Message (n : ℕ) (h : even n) : even (n ^ 2) => --- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder --- `unfold even at *` ersetzen. --- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert --- genau gleich, wenn du das `unfold` rauslöscht." - -Tactics unfold rcases use rw ring intro diff --git a/server/testgame/TestGame/Levels/Quantors/TMP.lean b/server/testgame/TestGame/Levels/Quantors/TMP.lean deleted file mode 100644 index b5c0931..0000000 --- a/server/testgame/TestGame/Levels/Quantors/TMP.lean +++ /dev/null @@ -1,22 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight - -Game "TestGame" -World "Contradiction" -Level 3 - -Title "Widerspruch" - -Introduction -" -Ähnlich siehts aus, wenn man Annahmen hat, die direkte Negierung voneinander sind, -also `(h : A)` und `(g : ¬ A)`. -" - -Statement - "Ein Widerspruch impliziert alles." - (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by - contradiction - -Tactics contradiction diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean index bf4919a..dfbcafc 100644 --- a/server/testgame/TestGame/TacticDocs.lean +++ b/server/testgame/TestGame/TacticDocs.lean @@ -117,6 +117,13 @@ TacticDoc right TODO " +TacticDoc simp +" +## Beschreibung + +TODO +" + TacticDoc contradiction " ## Beschreibung @@ -124,6 +131,36 @@ TacticDoc contradiction TODO " +TacticDoc push_neg +" +## Beschreibung + +TODO +" + + +TacticDoc contrapose +" +## Beschreibung + +TODO +" + +TacticDoc revert +" +## Beschreibung + +TODO +" + + +TacticDoc by_contra +" +## Beschreibung + +TODO +" + TacticDoc ring " ## Beschreibung diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean new file mode 100644 index 0000000..9a7172a --- /dev/null +++ b/server/testgame/TestGame/ToBePorted.lean @@ -0,0 +1,16 @@ +import Mathlib + +-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet +def even (a : ℕ) : Prop := ∃ r, a = 2 * r +def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1 + +lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry + +lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry + +lemma even_square (n : ℕ) : even n → even (n ^ 2) := by + intro ⟨x, hx⟩ + unfold even at * + use 2 * x ^ 2 + rw [hx] + ring diff --git a/server/testgame/lakefile.lean b/server/testgame/lakefile.lean index 4f93e12..c63997f 100644 --- a/server/testgame/lakefile.lean +++ b/server/testgame/lakefile.lean @@ -6,10 +6,12 @@ require GameServer from ".."/"leanserver" require mathlib from git "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350" -set_option tactic.hygienic false -set_option autoImplicit false +--set_option tactic.hygienic false +--set_option autoImplicit false package TestGame @[default_target] -lean_lib TestGame +lean_lib TestGame { + moreLeanArgs := #["-DautoImplicit=false"] +} From 8de1eea5488c083688a859cca79066eb5a63e7d7 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 6 Dec 2022 19:38:10 +0100 Subject: [PATCH 2/2] Update README.md --- README.md | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 28332ca..fdcc460 100644 --- a/README.md +++ b/README.md @@ -8,6 +8,8 @@ The project is currently mostly copied from Patrick Massot's [NNG4](https://gith Building this requires a [npm](https://www.npmjs.com/) toolchain. After cloning the repository you should run `npm install` to pull in all dependencies. For development and experimentation, you can run `npm start` that will perform a non-optimized build and then run a local webserver on port 3000. +### Progress +This is a work in progress. In the future there are plans to host a server managing different public learning games for Lean4, but for now the target is to provide the first games (in German and eventually English) by April 2023. ## NPM Scripts @@ -23,4 +25,4 @@ On the server side, the command will set up a docker image containing the Lean s ## Security Providing the use access to a Lean instance running on the server is a severe security risk. That is why we start the Lean server in a Docker container -secured by [gVisor](https://gvisor.dev/). \ No newline at end of file +secured by [gVisor](https://gvisor.dev/).