From 420f913e6939d59cf4cc2643015389760f98fc85 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 19 Jan 2023 12:01:59 +0100 Subject: [PATCH] reorganise world Implication --- server/testgame/TestGame.lean | 28 +--- server/testgame/TestGame/LemmaDocs.lean | 48 ++++++- .../testgame/TestGame/Levels/Implication.lean | 12 ++ .../Levels/Implication/L01_Intro.lean | 40 ++++++ .../Levels/Implication/L02_Revert.lean | 42 ++++++ .../L03_Apply.lean} | 19 ++- .../L04_Apply.lean} | 10 +- .../L05_Apply.lean} | 19 ++- .../L06_Iff.lean} | 15 +- .../TestGame/Levels/Implication/L07_Rw.lean | 74 ++++++++++ .../TestGame/Levels/Implication/L08_Iff.lean | 44 ++++++ .../L09_Iff.lean} | 20 ++- .../Levels/Implication/L10_Apply.lean | 55 ++++++++ .../TestGame/Levels/Implication/L11_Rw.lean | 39 ++++++ .../Levels/Implication/L12_Summary.lean | 81 +++++++++++ .../L08_Contrapose.lean | 2 +- .../Levels/{Logic => LeftOvers}/L09_Or.lean | 0 .../L14_NotNot.lean} | 0 .../{Logic => LeftOvers}/Lxx_Tauto.lean | 0 .../Levels/{Logic => LeftOvers}/Lxx_Tfae.lean | 0 server/testgame/TestGame/Levels/Level1.lean | 28 ---- server/testgame/TestGame/Levels/Level2.lean | 38 ------ server/testgame/TestGame/Levels/Level3.lean | 83 ------------ server/testgame/TestGame/Levels/Level4.lean | 64 --------- server/testgame/TestGame/Levels/Level5.lean | 128 ------------------ .../TestGame/Levels/Logic/L02_Rfl.lean | 27 ---- .../TestGame/Levels/Logic/L06_Iff.lean | 44 ------ .../TestGame/Levels/Logic/L06c_Iff.lean | 44 ------ .../TestGame/Levels/Negation/L04_Contra.lean | 35 ----- .../testgame/TestGame/Levels/Predicate.lean | 1 + .../{Naturals => Predicate}/L01_Ring.lean | 13 +- .../TestGame/Levels/Predicate/L02_Rfl.lean | 31 +++++ .../{Naturals => Predicate}/L02_Ring.lean | 0 .../{Naturals => Predicate}/L03_Exists.lean | 0 .../{Naturals => Predicate}/L04_Forall.lean | 0 .../{Logic => Predicate}/L04_Rewrite.lean | 0 .../{Logic => Predicate}/L04b_Rewrite.lean | 0 .../{Negation => Predicate}/L09_PushNeg.lean | 0 .../TestGame/Levels/Proposition/L01_Rfl.lean | 10 +- .../Levels/Proposition/L02_Assumption.lean | 5 +- .../Levels/Proposition/L03_Assumption.lean | 4 +- .../TestGame/Levels/Proposition/L04_True.lean | 4 +- .../TestGame/Levels/Proposition/L05_Not.lean | 4 +- .../Levels/Proposition/L06_False.lean | 6 +- .../Levels/Proposition/L07_ContraNotEq.lean | 2 +- .../Levels/Proposition/L08_Contra.lean | 4 +- .../TestGame/Levels/Proposition/L09_And.lean | 2 +- .../TestGame/Levels/Proposition/L10_And.lean | 6 +- .../TestGame/Levels/Proposition/L11_Or.lean | 2 +- .../TestGame/Levels/Proposition/L12_Or.lean | 8 +- .../TestGame/Levels/Proposition/L13_Or.lean | 18 +-- .../Levels/Proposition/L14_Summary.lean | 30 ++-- .../{Negation => Proving}/L03_Contra.lean | 0 .../{Negation => Proving}/L06_ByContra.lean | 0 .../{Negation => Proving}/L07_Contrapose.lean | 0 55 files changed, 573 insertions(+), 616 deletions(-) create mode 100644 server/testgame/TestGame/Levels/Implication.lean create mode 100644 server/testgame/TestGame/Levels/Implication/L01_Intro.lean create mode 100644 server/testgame/TestGame/Levels/Implication/L02_Revert.lean rename server/testgame/TestGame/Levels/{Logic/L05_Apply.lean => Implication/L03_Apply.lean} (57%) rename server/testgame/TestGame/Levels/{Logic/L05c_Apply.lean => Implication/L04_Apply.lean} (75%) rename server/testgame/TestGame/Levels/{Logic/L05b_Apply.lean => Implication/L05_Apply.lean} (66%) rename server/testgame/TestGame/Levels/{Logic/L06b_Iff.lean => Implication/L06_Iff.lean} (62%) create mode 100644 server/testgame/TestGame/Levels/Implication/L07_Rw.lean create mode 100644 server/testgame/TestGame/Levels/Implication/L08_Iff.lean rename server/testgame/TestGame/Levels/{Logic/L06d_Iff.lean => Implication/L09_Iff.lean} (54%) create mode 100644 server/testgame/TestGame/Levels/Implication/L10_Apply.lean create mode 100644 server/testgame/TestGame/Levels/Implication/L11_Rw.lean create mode 100644 server/testgame/TestGame/Levels/Implication/L12_Summary.lean rename server/testgame/TestGame/Levels/{Negation => LeftOvers}/L08_Contrapose.lean (98%) rename server/testgame/TestGame/Levels/{Logic => LeftOvers}/L09_Or.lean (100%) rename server/testgame/TestGame/Levels/{Negation/L05_Not.lean => LeftOvers/L14_NotNot.lean} (100%) rename server/testgame/TestGame/Levels/{Logic => LeftOvers}/Lxx_Tauto.lean (100%) rename server/testgame/TestGame/Levels/{Logic => LeftOvers}/Lxx_Tfae.lean (100%) delete mode 100644 server/testgame/TestGame/Levels/Level1.lean delete mode 100644 server/testgame/TestGame/Levels/Level2.lean delete mode 100644 server/testgame/TestGame/Levels/Level3.lean delete mode 100644 server/testgame/TestGame/Levels/Level4.lean delete mode 100644 server/testgame/TestGame/Levels/Level5.lean delete mode 100644 server/testgame/TestGame/Levels/Logic/L02_Rfl.lean delete mode 100644 server/testgame/TestGame/Levels/Logic/L06_Iff.lean delete mode 100644 server/testgame/TestGame/Levels/Logic/L06c_Iff.lean delete mode 100644 server/testgame/TestGame/Levels/Negation/L04_Contra.lean create mode 100644 server/testgame/TestGame/Levels/Predicate.lean rename server/testgame/TestGame/Levels/{Naturals => Predicate}/L01_Ring.lean (57%) create mode 100644 server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean rename server/testgame/TestGame/Levels/{Naturals => Predicate}/L02_Ring.lean (100%) rename server/testgame/TestGame/Levels/{Naturals => Predicate}/L03_Exists.lean (100%) rename server/testgame/TestGame/Levels/{Naturals => Predicate}/L04_Forall.lean (100%) rename server/testgame/TestGame/Levels/{Logic => Predicate}/L04_Rewrite.lean (100%) rename server/testgame/TestGame/Levels/{Logic => Predicate}/L04b_Rewrite.lean (100%) rename server/testgame/TestGame/Levels/{Negation => Predicate}/L09_PushNeg.lean (100%) rename server/testgame/TestGame/Levels/{Negation => Proving}/L03_Contra.lean (100%) rename server/testgame/TestGame/Levels/{Negation => Proving}/L06_ByContra.lean (100%) rename server/testgame/TestGame/Levels/{Negation => Proving}/L07_Contrapose.lean (100%) diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index 1fee9e5..140e2db 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -1,32 +1,8 @@ import TestGame.Metadata -import TestGame.Levels.Logic.L02_Rfl -import TestGame.Levels.Logic.L04_Rewrite -import TestGame.Levels.Logic.L04b_Rewrite -import TestGame.Levels.Logic.L05_Apply -import TestGame.Levels.Logic.L05b_Apply -import TestGame.Levels.Logic.L05c_Apply -import TestGame.Levels.Logic.L06_Iff -import TestGame.Levels.Logic.L06b_Iff -import TestGame.Levels.Logic.L06c_Iff -import TestGame.Levels.Logic.L06d_Iff -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.Naturals.L31_Sum -import TestGame.Levels.Naturals.L32_Induction -import TestGame.Levels.Naturals.L33_Prime -import TestGame.Levels.Naturals.L34_ExistsUnique -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 import TestGame.Levels.Proposition - +import TestGame.Levels.Implication +import TestGame.Levels.Predicate Game "TestGame" diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index 8c169f3..5ac61a6 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -1,5 +1,48 @@ import GameServer.Commands --- import TestGame.MyNat + +-- Wird im Level "Implication 11" ohne Beweis angenommen. +LemmaDoc not_not as not_not in "Logic" +" +### Aussage + +`¬¬A ↔ A` + +### Annahmen + +`(A : Prop)` +" + +-- Wird im Level "Implication 10" ohne Beweis angenommen. +LemmaDoc not_or_of_imp as not_or_of_imp in "Logic" +" +### Aussage + +`¬A ∨ B` + +### Annahmen + +`(A B : Prop)`\\ +`(h : A → B)` +" + +-- Wird im Level "Implication 12" bewiesen. +LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic" +" +### Aussage + +`(A → B) ↔ ¬A ∨ B` + +### Annahmen + +`(A B : Prop)` +" + + + + + + + LemmaDoc zero_add as zero_add in "Addition" "This lemma says `∀ a : ℕ, 0 + a = a`." @@ -13,9 +56,6 @@ LemmaDoc add_succ as add_succ in "Addition" LemmaSet addition : "Addition lemmas" := zero_add add_zero -LemmaDoc not_not as not_not in "Logic" -"`∀ (A : Prop), ¬¬A ↔ A`." - LemmaDoc not_forall as not_forall in "Logic" "`∀ (A : Prop), ¬(∀ x, A) ↔ ∃x, (¬A)`." diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean new file mode 100644 index 0000000..bb0f73c --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication.lean @@ -0,0 +1,12 @@ +import TestGame.Levels.Implication.L01_Intro +import TestGame.Levels.Implication.L02_Revert +import TestGame.Levels.Implication.L03_Apply +import TestGame.Levels.Implication.L04_Apply +import TestGame.Levels.Implication.L05_Apply +import TestGame.Levels.Implication.L06_Iff +import TestGame.Levels.Implication.L07_Rw +import TestGame.Levels.Implication.L08_Iff +import TestGame.Levels.Implication.L09_Iff +import TestGame.Levels.Implication.L10_Apply +import TestGame.Levels.Implication.L11_Rw +import TestGame.Levels.Implication.L12_Summary diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean new file mode 100644 index 0000000..5ef9e51 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean @@ -0,0 +1,40 @@ +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Implication" +Level 1 + +Title "Intro" + +Introduction +" +## Implikationen + +In diesem Kapitel lernst du Implikation ($\\Rightarrow$) und Genau-dann-wenn +($\\Leftrightarrow$) kennen. +Dazu lernst du, wie man bereits bewiesene Sätze verwendet. + +Seien `(A B : Prop)` zwei logische Aussagen. Eine Implikation $A \\Rightarrow B$ schreibt +man in Lean als `A → B` (`\\to`). + +Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit +`intro ha` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen. +" + +Statement + "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr." + (A B : Prop) (hb : B) : A → (A ∧ B) := by + intro hA + constructor + assumption + assumption + +Hint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) => +"Mit `intro ha` kann man annehmen, dass $A$ wahr ist. danach muss man $A \\land B$ zeigen." + +Message (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) => +"Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden." + +Tactics intro constructor assumption diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean new file mode 100644 index 0000000..8838cf4 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean @@ -0,0 +1,42 @@ +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Implication" +Level 2 + +Title "Revert" + +Introduction +" +Mit `intro` kann man also eine Implikation aus dem Goal entfernen, indem man +die Implikationsprämisse zu den *Annahmen* hinzufügt: + +``` +example : A → B := + [Beweis] +``` + +wird zu + +``` +example (ha : A) : B := + [Beweis] +``` + +Seltener kann auch die andere Richtung nützlich sein. Mit `revert ha` kann man die Annahme +`ha` entfernen und als Implikationsprämisse vor's Goal hängen. +" + +Statement +"Angenommen $A$ ist eine wahre Aussage und man hat eine Implikation $A \\Rightarrow B$, zeige +dass $B$ wahr ist." + (A B : Prop) (ha : A) (h : A → B) : B := by + revert ha + assumption + +Hint (A : Prop) (B : Prop) (ha : A) (h : A → B): B => +"Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen." + +Tactics revert assumption diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean similarity index 57% rename from server/testgame/TestGame/Levels/Logic/L05_Apply.lean rename to server/testgame/TestGame/Levels/Implication/L03_Apply.lean index 0e23401..73c4a2b 100644 --- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean @@ -5,21 +5,18 @@ Game "TestGame" World "Implication" Level 3 -Title "Implikation" +Title "Apply" Introduction -"Als nächstes widmen wir uns der Implikation $A \\Rightarrow B$. -Mit zwei logischen Aussagen `(A : Prop) (B : Prop)` schreibt man eine Implikation -als `A → B` (`\\to`). +" +`revert` ist aber nur selten der richtige Weg. -Wenn man als Goal $B$ beweisen möchte und eine Impikation `(g : A → B)` -hat, kann man mit `apply g` diese -anwenden, worauf das zu beweisende Goal $A$ wird. Auf Papier würde man an der Stelle -folgendes zu schreiben: \"Es genügt $A$ zu zeigen, denn $A \\Rightarrow B$\". - -*Bemerke:* Das ist der selbe Pfeil, der später auch für Funktionen wie `ℕ → ℕ` gebraucht -wird, deshalb heisst er `\\to`." +Im vorigen Beispiel würde man besser die Implikation $A \\Rightarrow B$ *anwenden*, also +sagen \"Es genügt $A$ zu zeigen, denn $A \\Rightarrow B$\" und danach $A$ beweisen. +Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die Konsequenz +(also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen. +" Statement "Seien $A, B$ logische Aussagen, wobei $A$ wahr ist und $A \\Rightarrow B$. diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean similarity index 75% rename from server/testgame/TestGame/Levels/Logic/L05c_Apply.lean rename to server/testgame/TestGame/Levels/Implication/L04_Apply.lean index 34c9b36..cd49a9b 100644 --- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean @@ -4,14 +4,14 @@ set_option tactic.hygienic false Game "TestGame" World "Implication" -Level 1 +Level 4 Title "Implikation" Introduction " -Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit -`intro hA` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen. +Hier eine Übung zu Implikationen. +Fast immer ist es der richtige Weg, wenn du mit `intro` anfängst. " Statement @@ -22,7 +22,7 @@ Statement apply f assumption -Message (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C => +Hint (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C => "Mit `intro hA` kann man annehmen, dass $A$ wahr ist. danach muss man $B$ zeigen." Message (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C => @@ -32,4 +32,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C = "Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende diese mit `apply` an." -Tactics intro apply assumption +Tactics intro apply assumption revert diff --git a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean similarity index 66% rename from server/testgame/TestGame/Levels/Logic/L05b_Apply.lean rename to server/testgame/TestGame/Levels/Implication/L05_Apply.lean index 18aea93..4bb684e 100644 --- a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean @@ -2,13 +2,13 @@ import TestGame.Metadata Game "TestGame" World "Implication" -Level 4 +Level 5 Title "Implikation" Introduction " -Angenommen man hat folgende Implikationen +Noch eine Übung: Angenommen man hat folgende Implikationen: $$ \\begin{CD} A @>{f}>> B @<{g}<< C \\\\ @@ -16,18 +16,23 @@ $$ D @>{i}>> E @>{k}>> F \\end{CD} $$ -und weiss, dass Aussage $A$ wahr ist. " Statement - "Beweise Aussage $F$." - (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E) - (i : D → E) (k : E → F) (m : C → F) : F := by + "Beweise $A \\Rightarrow F$." + (A B C D E F : Prop) (f : A → B) (g : C → B) (h : B → E) + (i : D → E) (k : E → F) (m : C → F) : A → F := by + intro ha apply k apply h apply f assumption +Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) + (f : A → B) (g : C → B) (h : B → E) + (i : D → E) (k : E → F) (m : C → F) : A → F => +"Wieder ist es schlau, mit `intro` anzufangen." + Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : C → F) : F => @@ -43,6 +48,6 @@ Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) (i : D → E) (k : E → F) (m : C → F) : D => "Sackgasse. Probier doch einen anderen Weg." -Tactics apply assumption +Tactics apply assumption revert intro -- https://www.jmilne.org/not/Mamscd.pdf diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean similarity index 62% rename from server/testgame/TestGame/Levels/Logic/L06b_Iff.lean rename to server/testgame/TestGame/Levels/Implication/L06_Iff.lean index eba81b5..b845c60 100644 --- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean @@ -2,17 +2,20 @@ import TestGame.Metadata Game "TestGame" World "Implication" -Level 5 +Level 6 Title "Genau dann wenn" Introduction " -Ein $A \\iff B$ besteht intern aus zwei Implikationen, $\\textrm{mp} : A \\Rightarrow B$ -und $\\textrm{mpr} : B \\Rightarrow A$. +Genau-dann-wenn, $A \\Leftrightarrow B$, wird als `A ↔ B` (`\\iff`) geschrieben. +`A ↔ B` ist eine Struktur (ähnlich wie das logische UND), die aus zwei Teilen besteht: -Wenn man ein `A ↔ B` zeigen will (im Goal), kann man dieses mit `constructor` in die -Einzelteile zerlegen. +- `mp`: die Implikation $A \\Rightarrow B$. +- `mpr`: die Implikation $B \\Rightarrow A$. + +Hat man ein $\\Leftrightarrow$ im Goal, nimmt man dieses ebenfalls mit der Taktik +`constructor` auseinander und zeigt dann beide Richtungen einzeln. " Statement @@ -22,7 +25,7 @@ Statement assumption assumption -Message (A : Prop) (B : Prop) : A ↔ B => +Hint (A : Prop) (B : Prop) : A ↔ B => "Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen." Hint (A : Prop) (B : Prop) (h : A → B) : A → B => diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean new file mode 100644 index 0000000..81d44e3 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean @@ -0,0 +1,74 @@ +import TestGame.Metadata + +import Init.Data.ToString +-- #check List UInt8 + +Game "TestGame" +World "Implication" +Level 7 + +Title "Genau dann wenn" + +Introduction +" +Hat man ein `(h : A ↔ B)` in den Annahmen, hat man die gleichen beiden Optionen wie beim +logischen UND plus noch eine neue: + +1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen + direkt auswählen. +2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei + separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)` +3. **Mit** `rw [h]` **kann man im Goal `A` durch `B` ersetzen.** + +Wir widmen uns zuerst `rw`. Dies steht für \"rewrite\". Da $A$ und $B$ logisch äquivalent +sind, kann man beliebig das eine mit dem anderen vertauschen. +`rw [h]` ersetzt $A$ durch $B$. +Dabei gibt es noch einige Tricks: + +- `rw [← h]` ersetzt umgekehrt $B$ durch $A$ (`\\l`, kleines L). +- `rw [h, g]` ist das gleiche wie `rw [h]` gefolgt von `rw [g]`. +" + +Statement + "Zeige dass `B ↔ C`." + (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by + rw [h₁] + rw [←h₂] + assumption + +Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C => +"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`. +Probiers doch mit `rw [h₁]`." + +Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : A ↔ C => +"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`. +Probiers doch mit `rw [h₁]`." + +Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D => +"Man kann auch rückwärts umschreiben: +`rw [←h₂]` ersetzt man im Goal `B` durch `a` (`\\l`, also ein kleines L)" + +Hint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B => +"Schau mal durch die Annahmen durch." + + +-- These should not be necessary if they don't use `rw [] at`. +Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ C) : B ↔ C => +"Auch eine Möglichkeit... Kannst du das Goal so umschreiben, +dass es mit einer Annahme übereinstimmt?" + +Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : B ↔ D) : B ↔ C => +"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?" + +Message (A : Prop) (B : Prop) (h : B ↔ A) : A ↔ B => +"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `A ↔ A` umschreibst, kann man es mit +`rfl` beweisen (rsp. das passiert automatisch.)" + +Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : D ↔ A) : B ↔ C => +"Das ist nicht der optimale Weg..." + +Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : A ↔ D) : B ↔ C => +"Das ist nicht der optimale Weg..." + + +Tactics rw assumption diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean new file mode 100644 index 0000000..bc566d9 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean @@ -0,0 +1,44 @@ +import TestGame.Metadata + +set_option tactic.hygienic false + +Game "TestGame" +World "Implication" +Level 8 + +Title "Genau dann wenn" + +Introduction +" +Nun schauen wir uns Option 1) an, die du schon von UND kennst: + +1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen + direkt auswählen. + +`h.mp` und `h.mpr` (oder `h.1` und `h.2`) sind die einzelnen Implikationen, und du kannst +mit denen ensprechend arbeiten. Insbesondere kannst du mit `apply h.mp` die Implikation +$A \\Rightarrow B$ anwenden, wenn das Goal $B$ ist. + +*(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.)* +" + +Statement +"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$." + (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by + intro hA + apply g + apply h.mp + assumption + +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C => +"Fange wie immer mit `intro` an." + +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C => +"Wie im Implikationen-Level kannst du nun `apply` verwenden." + +Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B => +"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden." + +Conclusion "Im nächsten Level findest du die zweite Option." + +Tactics apply assumption diff --git a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean similarity index 54% rename from server/testgame/TestGame/Levels/Logic/L06d_Iff.lean rename to server/testgame/TestGame/Levels/Implication/L09_Iff.lean index 27e713a..48b95e1 100644 --- a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean @@ -4,38 +4,36 @@ import Mathlib.Tactic.Cases Game "TestGame" World "Implication" -Level 8 +Level 9 Title "Genau dann wenn" Introduction " -Als zweite Option, kann man eine Annahme `(h : A ↔ B)` in zwei neue Annahmen -`(h₁ : A → B)` und `(h₂ : B → A)` aufteilen. +Und noch die letzte Option: -2.) Mit `rcases h` teilt man die Annahme `h` auf. - -(Mit `rcases h with ⟨h₁, h₂⟩` (`\\<`, `\\>`) kann man zudem die neuen Annahmen benennen.) +2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei + separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)` +Als letzte Option kannst du `rcases h with ⟨h₁, h₂⟩` auch auf eine Annahme `(h : A ↔ B)` +anwenden, genau wie du dies bei einer Annahme `(h' : A ∧ B)` gemacht hast. " Statement - "Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$." +"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$." (A B : Prop) : (A ↔ B) → (A → B) := by intro h rcases h assumption -Message (A : Prop) (B : Prop) : (A ↔ B) → A → B => +Hint (A : Prop) (B : Prop) : (A ↔ B) → A → B => "Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist." -Message (A : Prop) (B : Prop) (h : A ↔ B): A → B => +Hint (A : Prop) (B : Prop) (h : A ↔ B) : A → B => "Mit `rcases h with ⟨h₁, h₂⟩` kannst du jetzt die Annahme `(h : A ↔ B)` zerlegen." Conclusion " -Note: In der Mathematik definieren wir oft Strukturen als Tupels, z.B. \"Sei (G, +) eine Gruppe\". -In Lean brauchen wir dafür immer die Klammern von oben: `⟨_, _⟩`. " Tactics intro apply rcases assumption diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean new file mode 100644 index 0000000..da84543 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean @@ -0,0 +1,55 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Cases +import Mathlib + +Game "TestGame" +World "Implication" +Level 10 + +Title "Lemmas" + +Introduction +" +Bewiesene Resultate möchte man in späteren Aufgaben als Sätze wieder verwenden. + +In Lean sind das Lemmas und Theoreme (wobei es keinen Unterschied zwischen `lemma` und `theorem` +gibt). + +Links in der Bibliothek findest du bekannte Lemmas. Wenn das Goal mit der Aussage des Lemmas +übereinstimmt, kannst du es mit `apply [Lemma-Name]` anwenden, wie du das mit Implikationen auch +machst. + +Zum Beispiel gibt es ein Lemma, das sagt, dass wenn +$A \\Rightarrow B$ dann $(\\neg A \\lor B)$: + +``` +lemma not_or_of_imp : (A B : Prop) (h : A → B) : + ¬A ∨ B := by + ... +``` + +Wenn also dein Goal `¬A ∨ B` ist, kannst du mit `apply not_or_of_imp` dieses +Lemma anwenden. Danach musst du noch alle Annahmen zeigen. +" + +Statement +"Benutze `not_or_of_imp` um zu zeigen, dass $\\neg A \\lor A$ wahr ist." + (A : Prop) : ¬A ∨ A := by + apply not_or_of_imp + intro + assumption + +Hint (A : Prop) : ¬A ∨ A => +"Das Lemma wendest du mit `apply not_or_of_imp` an." + +Hint (A : Prop) : A → A => +"Wie immer, `intro` ist dein Freund." + +Conclusion +" +" + +Tactics apply left right assumption + +Lemmas not_or_of_imp diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean new file mode 100644 index 0000000..6370dc9 --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean @@ -0,0 +1,39 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.Cases +import Mathlib.Logic.Basic + +Game "TestGame" +World "Implication" +Level 11 + +Title "Lemmas" + +Introduction +" +Wenn die Aussage eines Lemmas eine Äquivalenz ist, kann man dieses auch mit `rw` brauchen, +wie du es von Äquivalenzen kennst. + +Ein wichtiges Lemma ist dass $\\neg(\\neg A))$ und $A$ äquivalent sind: + +``` +lemma not_not (A : Prop) : ¬¬A ↔ A := by + ... +``` + +Mit `rw [not_not]` sucht Lean also im Goal ein Term `¬¬(·)` und entfernt dort das `¬¬`. +" + +Statement +"Zeige, dass $A ∨ (¬¬B) ∧ C$ und $A ∨ B ∧ C$ äquivalent sind." + (A B C : Prop) : A ∨ (¬¬B) ∧ C ↔ A ∨ B ∧ C := by + rw [not_not] + +Conclusion +" +`rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet. +" + +Tactics rw + +Lemmas not_not not_or_of_imp diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean new file mode 100644 index 0000000..5bfdb3e --- /dev/null +++ b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean @@ -0,0 +1,81 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight +import Mathlib + +set_option tactic.hygienic false + +Game "TestGame" +World "Implication" +Level 12 + +Title "Zusammenfassung" + +Introduction +" +Damit bist du am Ende der zweiten Lektion angekommen. +Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine +Abschlussaufgabe. + +## Notationen / Begriffe + +| | Beschreibung | +|:--------------|:---------------------------------------------------------| +| → | Eine Implikation. | +| ↔ | Genau-dann-wenn / Äquivalenz. | +| `lemma` | Ein Resultat mit einem Namen. | +| `theorem` | Das gleiche wie ein Lemma. | +| `example` | Wie ein Lemma aber ohne Namen (nicht weiter verwendbar.) | + +## Taktiken + +| | Taktik | Beispiel | +|:----|:--------------------------|:-------------------------------------------------------| +| 8 | `intro` | Für eine Implikation im Goal. | +| 9 | `revert` | Umkehrung von `intro`. | +| 10 | `apply` | Wendet eine Implikation auf das Goal an. | +| 10ᵇ | `apply` | Wendet ein Lemma an. | +| 11 | `rw` | Umschreiben zweier äquivalenter Aussagen. | +| 11ᵇ | `rw` | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. | + + +Als Abschlussübung kannst du folgende Äquivalenz zeigen: +" + +Statement imp_iff_not_or +"$A \\Rightarrow B$ ist äquivalent zu $\\neg A \\lor B$." + (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by + constructor + apply not_or_of_imp + intro h ha + rcases h with h | h + contradiction + assumption + +Hint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B => +"Eine Äquivalenz im Goal geht man immer mit `constructor` an." + +Hint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B => +"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet." + +Hint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B => +"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet." + +Hint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) => +"Eine Implikation geht man fast immer mit `intro h` an." + +Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => +"Nochmals `intro`." + +Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) => +"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen." + +Hint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B => +"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen." + +Hint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B => +"Findest du einen Widerspruch?" + +Tactics rfl assumption trivial left right constructor rcases + +Lemmas not_not not_or_of_imp diff --git a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean b/server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean similarity index 98% rename from server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean rename to server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean index f03e3fd..a8c1ce5 100644 --- a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean +++ b/server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean @@ -8,7 +8,7 @@ import TestGame.ToBePorted Game "TestGame" World "Implication" -Level 2 +Level 102 Title "Kontraposition" diff --git a/server/testgame/TestGame/Levels/Logic/L09_Or.lean b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean similarity index 100% rename from server/testgame/TestGame/Levels/Logic/L09_Or.lean rename to server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean diff --git a/server/testgame/TestGame/Levels/Negation/L05_Not.lean b/server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean similarity index 100% rename from server/testgame/TestGame/Levels/Negation/L05_Not.lean rename to server/testgame/TestGame/Levels/LeftOvers/L14_NotNot.lean diff --git a/server/testgame/TestGame/Levels/Logic/Lxx_Tauto.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Tauto.lean similarity index 100% rename from server/testgame/TestGame/Levels/Logic/Lxx_Tauto.lean rename to server/testgame/TestGame/Levels/LeftOvers/Lxx_Tauto.lean diff --git a/server/testgame/TestGame/Levels/Logic/Lxx_Tfae.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Tfae.lean similarity index 100% rename from server/testgame/TestGame/Levels/Logic/Lxx_Tfae.lean rename to server/testgame/TestGame/Levels/LeftOvers/Lxx_Tfae.lean diff --git a/server/testgame/TestGame/Levels/Level1.lean b/server/testgame/TestGame/Levels/Level1.lean deleted file mode 100644 index 6ec5eac..0000000 --- a/server/testgame/TestGame/Levels/Level1.lean +++ /dev/null @@ -1,28 +0,0 @@ -import TestGame.Metadata - -Game "TestGame" -World "Old" -Level 1 - -Title "The reflexivity spell" - -Introduction -" -Let's learn a first spell: the `rfl` spell. `rfl` stands for \"reflexivity\", which is a fancy -way of saying that it will prove any goal of the form `A = A`. It doesn't matter how -complicated `A` is, all that matters is that the left hand side is *exactly equal* to the -right hand side (a computer scientist would say \"definitionally equal\"). I really mean -\"press the same buttons on your computer in the same order\" equal. -For example, `x * y + z = x * y + z` can be proved by `rfl`, but `x + y = y + x` cannot. -This is a very low level spell, but you need to start somewhere. - -After closing this message, type rfl in the invocation zone and hit Enter or click -the \"Cast spell\" button. -" - -Statement "" (x y z : ℕ) : x * y + z = x * y + z := by -rfl - -Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button." - -Tactics rfl diff --git a/server/testgame/TestGame/Levels/Level2.lean b/server/testgame/TestGame/Levels/Level2.lean deleted file mode 100644 index 9fd39b1..0000000 --- a/server/testgame/TestGame/Levels/Level2.lean +++ /dev/null @@ -1,38 +0,0 @@ -import TestGame.Metadata - -Game "TestGame" -World "Old" -Level 2 - -Title "The rewriting spell" - -Introduction -" -The rewrite spell is the way to \"substitute in\" the value -of an expression. In general, if you have a hypothesis of the form `A = B`, and your -goal mentions the left hand side `A` somewhere, then -the `rewrite` tactic will replace the `A` in your goal with a `B`. - -The documentation for `rewrite` just appeared in your spell book. -Play around with the menus and see what is there currently. -More information will appear as you progress. - -Take a look in the top right box at what we have. -The variables $x$ and $y$ are natural numbers, and we have -an assumption `h` that $y = x + 7$. Our goal -is to prove that $2y=2(x+7)$. This goal is obvious -- we just -substitute in $y = x+7$ and we're done. In Lean, we do -this substitution using the `rewrite` spell. This spell takes a list of equalities -or equivalences so you can cast `rewrite [h]`. -" - -Statement "" (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by - rewrite [h] - rfl - -Message (x : ℕ) (y : ℕ) (h : y = x + 7) : 2*(x + 7) = 2*(x + 7) => -"Great! Now the goal should be easy to reach using the `rfl` spell." - -Conclusion "Congratulations for completing your second level!" - -Tactics rfl rewrite diff --git a/server/testgame/TestGame/Levels/Level3.lean b/server/testgame/TestGame/Levels/Level3.lean deleted file mode 100644 index 7318367..0000000 --- a/server/testgame/TestGame/Levels/Level3.lean +++ /dev/null @@ -1,83 +0,0 @@ -import TestGame.Metadata - -Game "TestGame" -World "Old" -Level 3 - -Title "Peano's axioms" - -Introduction -" -The team that salvaged the type `ℕ` of natural numbers actually got us three things: - - * a term `0 : ℕ`, interpreted as the number zero. - * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after $n$\". - * The principle of mathematical induction. - -These are essentially the axioms isolated by Peano which uniquely characterise -the natural numbers (we also need recursion, but we can ignore it for now). -The first axiom says that $0$ is a natural number. The second says that there -is a `succ` function which eats a number and spits out the number after it, -so $\\operatorname{succ}(0)=1$, $\\operatorname{succ}(1)=2$ and so on. - -Peano's last axiom is the principle of mathematical induction. This is a deeper -fact. It says that if we have infinitely many true/false statements $P(0)$, $P(1)$, -$P(2)$ and so on, and if $P(0)$ is true, and if for every natural number $d$ -we know that $P(d)$ implies $P(\\operatorname{succ}(d))$, then $P(n)$ must be true for every -natural number $n$. It's like saying that if you have a long line of dominoes, and if -you knock the first one down, and if you know that if a domino falls down then the one -after it will fall down too, then you can deduce that all the dominos will fall down. -One can also think of it as saying that every natural number -can be built by starting at `0` and then applying `succ` a finite number of times. - -Peano's insights were firstly that these axioms completely characterise -the natural numbers, and secondly that these axioms alone can be used to build -a whole bunch of other structure on the natural numbers, for example -addition, multiplication and so on. - -This game is all about seeing how far these axioms of Peano can take us. - -Let's practice our use of the `rewrite` tactic in the following example. -Our hypothesis `h` is a proof that `succ(a) = b` and we want to prove that -`succ(succ(a))=succ(b)`. In words, we're going to prove that if -`b` is the number after `a` then `succ(b)` is the number after `succ(a)`. -Note that the system drops brackets when they're not -necessary, so `succ b` just means `succ(b)`. - -Now here's a tricky question. Knowing that our goal is `succ (succ a) = succ b`, -and our assumption is `h : succ a = b`, then what will the goal change -to when we type - -`rewrite [h]` - -and hit enter? Remember that `rewrite [h]` will -look for the *left* hand side of `h` in the goal, and will replace it with -the *right* hand side. Try and figure out how the goal will change, and -then try it. -" - -Statement "" (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by - rewrite [h] - rfl - -Message (a : ℕ) (b : ℕ) (h : succ a = b) : succ b = succ b => -" -Look: Lean changed `succ a` into `b`, so the goal became `succ b = succ b`. -That goal is of the form `X = X`, so you know what to do. -" - - -Conclusion "Congratulations for completing the third level! -You may be wondering whether we could have just substituted in the definition of `b` -and proved the goal that way. To do that, we would want to replace the right hand -side of `h` with the left hand side. You do this in Lean by writing `rewrite [<- h]`. You get the -left-arrow by typing `\\l` and then a space; note that this is a small letter L, -not a number 1. You can just edit your proof and try it. - -You may also be wondering why we keep writing `succ(b)` instead of `b+1`. This -is because we haven't defined addition yet! On the next level, the final level -of the tutorial, we will introduce addition, and then -we'll be ready to enter Addition World. -" - -Tactics rfl rewrite diff --git a/server/testgame/TestGame/Levels/Level4.lean b/server/testgame/TestGame/Levels/Level4.lean deleted file mode 100644 index 81ac34e..0000000 --- a/server/testgame/TestGame/Levels/Level4.lean +++ /dev/null @@ -1,64 +0,0 @@ -import TestGame.Metadata - -Game "TestGame" -World "Old" -Level 4 - -Title "Addition" - -Introduction -" -Peano defined addition `a + b` by induction on `b`, or, -more precisely, by *recursion* on `b`. He first explained how to add 0 to a number: -this is the base case. - -* `add_zero (a : ℕ) : a + 0 = a` - -We will call this theorem `add_zero`. It has just appeared in your inventory! -Mathematicians sometimes call it \"Lemma 2.1\" or \"Hypothesis P6\" or something. But -computer scientists call it `add_zero` because it tells you -what the answer to \"$x$ add zero\" is. It's a *much* better name than \"Lemma 2.1\". -Even better, we can use the rewrite tactic with `add_zero`. -If you ever see `x + 0` in your goal, `rewrite [add_zero]` will simplify it to `x`. -This is because `add_zero` is a proof that `x + 0 = x` (more precisely, -`add_zero x` is a proof that `x + 0 = x` but Lean can figure out the `x` from the context). - -Now here's the inductive step. If you know how to add `d` to `a`, then -Peano tells you how to add `succ(d)` to `a`. It looks like this: - -* `add_succ (a d : ℕ) : a + succ(d) = succ (a + d)` - -What's going on here is that we assume `a + d` is already -defined, and we define `a + succ(d)` to be the number after it. -This is also in your inventory now -- `add_succ` tells you -how to add a successor to something. If you ever see `... + succ ...` -in your goal, you should be able to use `rewrite [add_succ]` to make -progress. Here is a simple example where we shall see both. Let's prove -that $x$ add the number after $0$ is the number after $x$. - -Observe that the goal mentions `... + succ ...`. So type - -`rewrite [add_succ]` - -and hit enter; see the goal change. -" - -Statement "" (a : ℕ ) : a + succ 0 = succ a := by - rewrite [add_succ] - rewrite [add_zero] - rfl - -Message (a : ℕ) : succ (a + 0) = succ a => " -Do you see that the goal now mentions ` ... + 0 ...`? So type - -`rewrite [add_zero]` - -and try to finish the level alone from there. -" - -Conclusion "Congratulations for completing your fourth level! This is the end of the tutorial part -of the game. Serious things start in the next level." - -Tactics rfl rewrite - -Lemmas add_succ add_zero diff --git a/server/testgame/TestGame/Levels/Level5.lean b/server/testgame/TestGame/Levels/Level5.lean deleted file mode 100644 index c919ea7..0000000 --- a/server/testgame/TestGame/Levels/Level5.lean +++ /dev/null @@ -1,128 +0,0 @@ -import TestGame.Metadata -import TestGame.Tactics - -Game "TestGame" -World "Old" -Level 5 - -Title "The induction_on spell" - -Introduction -" -Welcome to Addition World. If you've done all four levels in tutorial world -and know about `rewrite` and `rfl`, then you're in the right place. Here's -a reminder of the things you're now equipped with which we'll need in this world. - -## Data: - - * a type called `ℕ` - * a term `0 : ℕ`, interpreted as the number zero. - * a function `succ : ℕ → ℕ`, with `succ n` interpreted as \"the number after `n`\". - * Usual numerical notation 0,1,2 etc (although 2 onwards will be of no use to us until much later ;-) ). - * Addition (with notation `a + b`). - -## Theorems: - - * `add_zero (a : ℕ) : a + 0 = a`. Use with `rewrite [add_zero]`. - * `add_succ (a b : ℕ) : a + succ(b) = succ(a + b)`. Use with `rewrite [add_succ]`. - * The principle of mathematical induction. Use with `induction_on` (see below) - - -## Spells: - - * `rfl` : proves goals of the form `X = X` - * `rewrite [h]` : if h is a proof of `A = B`, changes all A's in the goal to B's. - * `induction_on n with d hd` : we're going to learn this right now. - -# Important thing: - -This is a *really* good time to check you understand about the spell book and the inventory on -the left. Eveything you need is collected in those lists. They -will prove invaluable as the number of theorems we prove gets bigger. On the other hand, -we only need to learn one more spell to really start going places, so let's learn about -that spell right now. - -OK so let's see induction in action. We're going to prove - - `zero_add (n : ℕ) : 0 + n = n`. - -That is: for all natural numbers $n$, $0+n=n$. Wait $-$ what is going on here? -Didn't we already prove that adding zero to $n$ gave us $n$? -No we didn't! We proved $n + 0 = n$, and that proof was called `add_zero`. We're now -trying to establish `zero_add`, the proof that $0 + n = n$. But aren't these two theorems -the same? No they're not! It is *true* that `x + y = y + x`, but we haven't -*proved* it yet, and in fact we will need both `add_zero` and `zero_add` in order -to prove this. In fact `x + y = y + x` is the boss level for addition world, -and `induction_on` is the only other spell you'll need to beat it. - -Now `add_zero` is one of Peano's axioms, so we don't need to prove it, we already have it -(indeed, if you've opened the Addition World theorem statements on the left, you can even see it). -To prove `0 + n = n` we need to use induction on $n$. While we're here, -note that `zero_add` is about zero add something, and `add_zero` is about something add zero. -The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`. - -Start by casting `induction_on n`. -" - -Statement "" (n : ℕ) : 0 + n = n := by - sorry - -- induction_on n - -- rewrite [add_zero] - -- rfl - -- rewrite [add_succ] - -- rewrite [ind_hyp] - -- rfl - -Message : (0 : ℕ) + 0 = 0 => " -We now have *two goals!* The -induction spell has generated for us a base case with `n = 0` (the goal at the top) -and an inductive step (the goal underneath). The golden rule: **spells operate on the current goal** -- -the goal at the top. So let's just worry about that top goal now, the base case `0 + 0 = 0`. - -Remember that `add_zero` (the proof we have already) is the proof of `x + 0 = x` -(for any $x$) so we can try - -`rewrite [add_zero]` - -What do you think the goal will change to? Remember to just keep -focussing on the top goal, ignore the other one for now, it's not changing -and we're not working on it. -" - -Message (n : ℕ) (ind_hyp: 0 + n = n) : 0 + succ n = succ n => -" -Great! You solved the base case. We are now be back down -to one goal -- the inductive step. - -We have a fixed natural number `n`, and the inductive hypothesis `ind_hyp : 0 + n = n` -saying that we have a proof of `0 + n = n`. -Our goal is to prove `0 + succ n = succ n`. In words, we're showing that -if the lemma is true for `n`, then it's also true for the number after `n`. -That's the inductive step. Once we've proved this inductive step, we will have proved -`zero_add` by the principle of mathematical induction. - -To prove our goal, we need to use `add_succ`. We know that `add_succ 0 n` -is the result that `0 + succ n = succ (0 + n)`, so the first thing -we need to do is to replace the left hand side `0 + succ n` of our -goal with the right hand side. We do this with the `rewrite` spell. You can write - -`rewrite [add_succ]` - -(or even `rewrite [add_succ 0 n]` if you want to give Lean all the inputs instead of making it -figure them out itself). -" - -Message (n : ℕ) (ind_hyp: 0 + n = n) : succ (0 + n) = succ n => -"Well-done! We're almost there. It's time to use our induction hypothesis. -Cast - -`rewrite [ind_hyp]` - -and finish by yourself. -" - -Conclusion "Congratulations for completing your first inductive proof!" - -Tactics rfl rewrite induction_on - -Lemmas add_succ add_zero diff --git a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean deleted file mode 100644 index 00ccd81..0000000 --- a/server/testgame/TestGame/Levels/Logic/L02_Rfl.lean +++ /dev/null @@ -1,27 +0,0 @@ -import TestGame.Metadata - -Game "TestGame" -World "Predicate" -Level 6 - -Title "Definitionally equal" - -Introduction -" -**Vorsicht:** `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich -definiert sind, auch wenn diese unterschiedlich dargestellt werden. Das kann anfänglich -zu Verwirrung führen. - -So ist `2` als `1 + 1` definiert, deshalb funktioniert `rfl` auch hier. -" - -Statement "Zeige dass $1 + 1$ zwei ist." : 1 + 1 = 2 := by - rfl - -Conclusion -" -**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl` -aufzurufen, deshalb brauchst du das nur noch selten. -" - -Tactics rfl diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean deleted file mode 100644 index 460259a..0000000 --- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean +++ /dev/null @@ -1,44 +0,0 @@ -import TestGame.Metadata - -import Init.Data.ToString --- #check List UInt8 - -Game "TestGame" -World "Implication" -Level 6 - -Title "Genau dann wenn" - -Introduction -" -Genau-dann-wenn, $A \\iff B$, wird als `A ↔ B (`\\iff`) geschrieben. - -Als erstes kann man mit `rw` Annahmen der Form `(h : A ↔ B)` genau gleich wie Gleichungen -`(h : a = b)` benützen, um das Goal umzuschreiben. - -Hier also nochmals die Gleiche Aufgabe wie zuvor, -aber diesmal mit Iff-Statements von Aussagen anstatt -Gleichungen von natürlichen Zahlen. -" - -Statement - "Zeige dass `B ↔ C`." - (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by - rw [h₁] - rw [←h₂] - assumption - -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C => -"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`. -Probiers doch mit `rw [h₁]`." - -Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D => -"Zur Erinnerung: Man kann auch rückwärts umschreiben: `h₂` sagt `A ↔ b` mit -`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)" - -Hint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B => -"Schau mal durch die Annahmen durch." - - - -Tactics rw assumption diff --git a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean deleted file mode 100644 index 5ef58b6..0000000 --- a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean +++ /dev/null @@ -1,44 +0,0 @@ -import TestGame.Metadata - -set_option tactic.hygienic false - -Game "TestGame" -World "Implication" -Level 7 - -Title "Genau dann wenn" - -Introduction -" -Wenn man eine Annahme `(h : A ↔ B)` hat, kann man auch davon die beiden einzelnen -Implikationen $\\textrm{mp} : A \\Rightarrow B$ und $\\textrm{mpr} : B \\Rightarrow A$ -brauchen. - -Dazu gibt es zwei Methoden: - -1.) `h.mp` (oder `h.1`) und `h.mpr` (oder `h.2`) sind direkt die einzelnen Richtungen. -Man kann also z.B. mit `apply h.mp` die Implikation `A → B` auf ein Goal `B` anwenden. - -(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.) -" - -Statement - "Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$." - (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by - intro hA - apply g - apply h.mp - assumption - -Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C => -"Zuerst kannst du wieder `intro` benützen um die Implikation anzugehen." - -Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C => -"Der nächste Schritt kommt auch noch aus dem Implikationen-Level." - -Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B => -"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden." - -Conclusion "Im nächsten Level findest du die zweite Option." - -Tactics apply assumption diff --git a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean deleted file mode 100644 index 70ca34e..0000000 --- a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean +++ /dev/null @@ -1,35 +0,0 @@ -import TestGame.Metadata -import Std.Tactic.RCases -import Mathlib.Tactic.LeftRight - -Game "TestGame" -World "Predicate" -Level 2 - -Title "Widerspruch" - -Introduction -" -Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form -`A ≠ A` (`\\ne`) hat, oder Aussagen der Form -`A = B` hat, wo Lean weiss, dass `A` und `B` unterschiedlich sind, wie zum Beispiel `0 = 1` in `ℕ`. - -*Bemerkung:* `X ≠ Y` muss man als `¬ (X = Y)` lesen, und auch so behandeln. -" - -Statement - "Angenommen man hat $a = b = c$ und $a \\ne c$ natürliche Zahlen $a, b, c$. - Zeige, dass man daraus jede beliebige Aussage beweisen kann." - (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 => - "Benütze `rw [...] at ...` um zwei Aussagen zu bekommen die genau das Gegenteil - aussagen." - -Hint (A : Prop) (a : ℕ) (b : ℕ) (g₁ : a = b) (h : a ≠ b) : A => - "`X ≠ Y` muss man als `¬ (X = Y)` lesen. Deshalb findet `contradiction` hier direkt - einen Widerspruch." - -Tactics contradiction diff --git a/server/testgame/TestGame/Levels/Predicate.lean b/server/testgame/TestGame/Levels/Predicate.lean new file mode 100644 index 0000000..80f8942 --- /dev/null +++ b/server/testgame/TestGame/Levels/Predicate.lean @@ -0,0 +1 @@ +import TestGame.Levels.Predicate.L01_Ring diff --git a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean similarity index 57% rename from server/testgame/TestGame/Levels/Naturals/L01_Ring.lean rename to server/testgame/TestGame/Levels/Predicate/L01_Ring.lean index 175ce1d..21696e0 100644 --- a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean +++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean @@ -11,11 +11,14 @@ Title "Natürliche Zahlen" Introduction " -Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon begegnet. Dabei haben wir -gesehen, dass explizite Gleichungen wie `2 + 3 * 5 = 17` implementationsbedingt -bereits mit `rfl` bewiesen werden können. +Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon kurz begegnet. -Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen. +Gleichungen, die nur die Operationen `+, -, *, ^` und Variablen enthalten, kann Lean mit der +Taktik `ring` beweisen. + +Diese Taktik funktioniert nicht nur über den natürlichen Zahlen, +sondern auch in (kommutativen) Gruppen, Ringen, und Körpern. Sie heisst `ring`, weil sie für Ringe +entwickelt wurde. " Statement @@ -23,7 +26,7 @@ Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring -Message (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 => +Hint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 => "`ring` übernimmt den ganzen Spaß." Conclusion diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean new file mode 100644 index 0000000..3cedce1 --- /dev/null +++ b/server/testgame/TestGame/Levels/Predicate/L02_Rfl.lean @@ -0,0 +1,31 @@ +import TestGame.Metadata + +Game "TestGame" +World "Predicate" +Level 6 + +Title "Definitionally equal" + +Introduction +" +Als kleine Nebenbemerkung: + +Auf Grund der Implementation in Lean brauchst du die Taktik `ring` gar nicht, wenn +du Gleichungen über `ℕ` hast, die keine Variablen enthalten: + +So ist zum Beispiel `2` als `1 + 1` definiert, deshalb kannst du $1 + 1 = 2$ einfach mit +`rfl` beweisen. +" + +Statement +"Zeige dass $1 + 1$ zwei ist." : + 1 + 1 = 2 := by + rfl + +Conclusion +" +**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl` +aufzurufen, deshalb brauchst du das nur noch selten. +" + +Tactics rfl diff --git a/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L02_Ring.lean similarity index 100% rename from server/testgame/TestGame/Levels/Naturals/L02_Ring.lean rename to server/testgame/TestGame/Levels/Predicate/L02_Ring.lean diff --git a/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L03_Exists.lean similarity index 100% rename from server/testgame/TestGame/Levels/Naturals/L03_Exists.lean rename to server/testgame/TestGame/Levels/Predicate/L03_Exists.lean diff --git a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L04_Forall.lean similarity index 100% rename from server/testgame/TestGame/Levels/Naturals/L04_Forall.lean rename to server/testgame/TestGame/Levels/Predicate/L04_Forall.lean diff --git a/server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean similarity index 100% rename from server/testgame/TestGame/Levels/Logic/L04_Rewrite.lean rename to server/testgame/TestGame/Levels/Predicate/L04_Rewrite.lean diff --git a/server/testgame/TestGame/Levels/Logic/L04b_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L04b_Rewrite.lean similarity index 100% rename from server/testgame/TestGame/Levels/Logic/L04b_Rewrite.lean rename to server/testgame/TestGame/Levels/Predicate/L04b_Rewrite.lean diff --git a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean similarity index 100% rename from server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean rename to server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 808c982..2db30d2 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -22,15 +22,17 @@ Seite. Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\". -Deine erste Taktik ist `rfl`, welche dazu da ist, ein Goal der Form $X = X$ zu schliessen. +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 ⏎. " -Statement "Zeige $ 42 = 42 $." : 42 = 42 := by +Statement +"Zeige $ 42 = 42 $." : 42 = 42 := by rfl -Message : 42 = 42 => -"Die Taktik `rfl` beweist ein Goal der Form `X = X`." +-- Message : 42 = 42 => +-- "Die Taktik `rfl` beweist ein Goal der Form `X = X`." Hint : 42 = 42 => "Man schreibt eine Taktik pro Zeile, also gib `rfl` ein und geh mit Enter ⏎ auf eine neue Zeile." diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index 16a8840..9927e91 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -22,13 +22,14 @@ Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` be " Statement - "Angenommen $1 < n$. dann ist $1 < n$." +"Angenommen $1 < n$. dann ist $1 < n$." (n : ℕ) (h : 1 < n) : 1 < n := by assumption -Message (n : ℕ) (h : 1 < n) : 1 < n => +Hint (n : ℕ) (h : 1 < n) : 1 < n => "`assumption` sucht nach einer Annahme, die dem Goal entspricht." + Conclusion "" Tactics assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index be6614b..b7edbfe 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -17,8 +17,8 @@ Mit einer Annahme `(hA : A)` nimmt man an, dass $A$ wahr ist: " Statement - "Sei $A$ eine logische Aussage und sei `hA` ein Beweis für $A$. - Zeige, dass $A$ wahr ist." +"Sei $A$ eine logische Aussage und sei `hA` ein Beweis für $A$. +Zeige, dass $A$ wahr ist." (A : Prop) (hA : A) : A := by assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index c562672..aa2a619 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -26,7 +26,9 @@ Wir können `True` aus dem nichts mit der Taktik `trivial` beweisen. aber manchmal ist sie nützlich.* " -Statement "" : True := by +Statement +"Zeige, dass die logische Aussage `True` immer wahr ist." : +True := by trivial Conclusion "" diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index 9ac5361..fd47af5 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -14,7 +14,9 @@ geschrieben `¬A` (`\\not`), gegenteilig falsch oder wahr. Da die Aussage `False` nie wahr ist, ist die Aussage `¬False` immer wahr, genau wie `True`. " -Statement "Zeige dass die Aussage `¬False` immer wahr ist." : ¬False := by +Statement +"Zeige dass die Aussage `¬False` immer wahr ist." : + ¬False := by trivial Conclusion "" diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 46c70a0..7dfecdd 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -18,12 +18,12 @@ Der erste Widerspruch, den `contradiction` erkennt, ist ein Beweis von `False`. " Statement - "Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`. - Zeige, dass daraus $A$ folgt." +"Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`. +Zeige, dass daraus $A$ folgt." (A : Prop) (h : False) : A := by contradiction -Message (A : Prop) (h : False) : A => +Hint (A : Prop) (h : False) : A => "Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen, unabhängig davon, was das Goal ist." diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index 165a871..deb195a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -18,7 +18,7 @@ Zweitens kann `contradiction` auch aus Annahmen der Form `a ≠ a` einen Widersp " Statement - "Sei $n$ eine natürliche Zahl die ungleich sich selbst ist. Dann ist $n = 37$." +"Sei $n$ eine natürliche Zahl die ungleich sich selbst ist. Dann ist $n = 37$." (n : ℕ) (h : n ≠ n) : n = 37 := by contradiction diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index 9679f58..5165426 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -20,8 +20,8 @@ Da `≠` als `¬(· = ·)` gelesen wird, gilt dasselbe für Annahmen `(h : a = b " Statement - "Sei $n$ eine natürliche Zahl die sowohl gleich als auch ungleich `10` ist. - Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)" +"Sei $n$ eine natürliche Zahl die sowohl gleich als auch ungleich `10` ist. +Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)" (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by contradiction diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 0a2ba1b..f11ec9c 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -26,7 +26,7 @@ Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by assumption assumption -Message (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => +Hint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => "`constructor` zerlegt die Struktur in Einzelteile." Hint (A : Prop) (hA : A) : A => diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 914fa1b..6688905 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -26,9 +26,9 @@ Statement "Benutze `rcases` um das UND in `(h : A ∧ (B ∧ C))` zu zerlegen un rcases h with ⟨_, ⟨g , _⟩⟩ assumption -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => - "Du kannst mit `rcases` auch verschachtelt mehrere Strukturen in einem Schritt zerlegen: - `rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`." +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => +"Du kannst mit `rcases` auch verschachtelt mehrere Strukturen in einem Schritt zerlegen: +`rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`." Hint (A : Prop) (hA : A) : A => "Du hast einen Beweis dafür in den *Annahmen*." diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index 39461b8..e088bbb 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -19,7 +19,7 @@ welche Seite man beweisen möchte. " Statement - "Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$." +"Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$." (A B : Prop) (hA : A) : A ∨ (¬ B) := by left assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index a773a7e..3e3e04a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -24,17 +24,21 @@ wir in beiden Fälle (linke oder rechte Seite wahr) diese Seite wieder `h` nenne Der Unterschied ist, dass man beim UND eine Annahme in zwei Einzelteile zerlegt (mit `⟨h₁, h₂⟩`). Beim ODER hingegen, kriegt man stattdessen zwei *Goals*, nämlich eines wo man annimmt, die linke Seite sei wahr und eines wo man annimmt, rechts sei wahr. + +*Notiz:* UND hat stärkere Bindung als ODER, und beide binden rechts, d.h. +`A ∨ B ∧ C` wird als `A ∨ (B ∧ C)` gelesen. Zudem binden beide nach rechts, +also `A ∨ B ∨ C` ist `A ∨ (B ∨ C)`. " Statement - "Angenommen \"$A$ oder ($A$ und $B$)\" wahr ist, zeige, dass $A$ wahr ist." +"Angenommen \"$A$ oder ($A$ und $B$)\" wahr ist, zeige, dass $A$ wahr ist." (A B : Prop) (h : A ∨ (A ∧ B)) : A := by rcases h with h | h assumption rcases h with ⟨h₁, h₂⟩ assumption -Message (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A => +Hint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A => "Als erstes kannst du das ODER in den Annahmen mit `rcases h with h | h` zerlegen." Message (A : Prop) (B : Prop) (h : A ∧ B) : A => diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Or.lean b/server/testgame/TestGame/Levels/Proposition/L13_Or.lean index bf1489d..0bc998f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Or.lean @@ -24,8 +24,8 @@ umzugehen um folgende Aussage zu beweisen. -- Note: The other direction would need arguing by cases. Statement - "Angenommen $A \\lor (B \\land C)$ ist wahr, zeige dass - $(A \\lor B) \\land (A \\lor C)$ wahr ist." +"Angenommen $A \\lor (B \\land C)$ ist wahr, zeige dass +$(A \\lor B) \\land (A \\lor C)$ wahr ist." (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by constructor rcases h with h | h @@ -41,26 +41,26 @@ Statement right assumption -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => +Hint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => "Das `∧` im Goal kann mit `constructor` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => "Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) => +Hint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) => "Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." -- TODO: Message nur Anhand der Annahmen? diff --git a/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean index f505185..2b8896e 100644 --- a/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L14_Summary.lean @@ -37,34 +37,30 @@ eingeführt wurden. | `(ha : A)` | Ein Beweis, dass die logische Aussage `(A : Prop)` wahr ist. | | `(h : A ∧ B)` | Eine Annahme, die den Namen `h` bekommen hat. | | `⟨·,·⟩` | Schreibweise für Struktur mit mehreren Feldern (kommt später im Detail). | +| `h.1, h.2, …` | Die einzelnen Felder der Stuktur. Auch `h.[Name des Feldes]` | -Im weiteren haben wir gesehen, wie wir in Lean Aufgaben/Sätze formulieren : + +Im weiteren haben wir gesehen, wie wir in Lean Aufgaben formulieren : ``` example [Annahmen] : [Aussage] := by [Beweis] - -lemma [Name] [Annahmen] : [Aussage] := by - [Beweis] ``` -Der Unterschied ist lediglich, dass Lemmas einen Namen haben und darum später -wiederverwendet werden können (siehe spätere Kapitel). \"Examples\" kriegen keinen Namen. - ## Taktiken Für die Beweise haben wir verschiedene Taktiken kennengelernt. -| | Taktik | Beispiel | -|:--|:--------------------------|:--------------------------------------------------| -| 1 | `rfl` | Beweist `A = A`. | -| 2 | `assumption` | Sucht das Goal in den Annahmen. | -| 3 | `contradiction` | Sucht einen Widerspruch. | -| 4 | `trivial` | Kombiniert die obigen drei Taktiken (und mehr). | -| 5 | `constructor` | Teilt ein UND im Goal auf. | -| 6 | `left`/`right` | Beweist eine Seite eines ODER im Goal. | -| 7ᵃ | `rcases h with ⟨h₁, h₂⟩` | Teilt ein UND in den Annahmen auf. | -| 7ᵇ | `rcases h with h \\| h` | Teilt ein ODER in den Annahmen in zwei Fälle auf. | +| | Taktik | Beispiel | +|:---|:--------------------------|:--------------------------------------------------| +| 1 | `rfl` | Beweist `A = A`. | +| 2 | `assumption` | Sucht das Goal in den Annahmen. | +| 3 | `contradiction` | Sucht einen Widerspruch. | +| 4 | `trivial` | Kombiniert die obigen drei Taktiken (und mehr). | +| 5 | `constructor` | Teilt ein UND im Goal auf. | +| 6 | `left`/`right` | Beweist eine Seite eines ODER im Goal. | +| 7ᵃ | `rcases h with ⟨h₁, h₂⟩` | Teilt ein UND in den Annahmen auf. | +| 7ᵇ | `rcases h with h \\| h` | Teilt ein ODER in den Annahmen in zwei Fälle auf. | Zum Schluss gibt es noch eine kleine Übungsaufgabe: diff --git a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean b/server/testgame/TestGame/Levels/Proving/L03_Contra.lean similarity index 100% rename from server/testgame/TestGame/Levels/Negation/L03_Contra.lean rename to server/testgame/TestGame/Levels/Proving/L03_Contra.lean diff --git a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean b/server/testgame/TestGame/Levels/Proving/L06_ByContra.lean similarity index 100% rename from server/testgame/TestGame/Levels/Negation/L06_ByContra.lean rename to server/testgame/TestGame/Levels/Proving/L06_ByContra.lean diff --git a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean b/server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean similarity index 100% rename from server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean rename to server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean