From 90540b158f0be71cb2dfc05e21a9c482701f4c05 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 23 Jan 2023 11:06:23 +0100 Subject: [PATCH] new levels. --- server/testgame/TestGame.lean | 5 +- .../TestGame/Levels/Contradiction.lean | 6 ++ .../Levels/Contradiction/L01_Have.lean | 67 +++++++++++++++ .../Levels/Contradiction/L02_Suffices.lean | 65 +++++++++++++++ .../Levels/Contradiction/L03_ByContra.lean | 55 +++++++++++++ .../Levels/Contradiction/L04_ByContra.lean | 49 +++++++++++ .../Levels/Contradiction/L05_Contrapose.lean | 65 +++++++++++++++ .../Levels/Contradiction/L06_Summary.lean | 76 +++++++++++++++++ .../Levels/LeftOvers/L08_Contrapose.lean | 37 --------- .../TestGame/Levels/LeftOvers/Playground.lean | 18 +++++ .../TestGame/Levels/Naturals/L31_Sum.lean | 22 ++--- .../Levels/Predicate/L09_Summary.lean | 9 +-- server/testgame/TestGame/Levels/Proving.lean | 1 - .../TestGame/Levels/Proving/L01_Contra.lean | 51 ------------ .../TestGame/Levels/Proving/L06_ByContra.lean | 81 ------------------- .../Levels/Proving/L07_Contrapose.lean | 50 ------------ server/testgame/TestGame/TacticDocs.lean | 15 ++-- 17 files changed, 427 insertions(+), 245 deletions(-) create mode 100644 server/testgame/TestGame/Levels/Contradiction.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L01_Have.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean create mode 100644 server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean delete mode 100644 server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean create mode 100644 server/testgame/TestGame/Levels/LeftOvers/Playground.lean delete mode 100644 server/testgame/TestGame/Levels/Proving.lean delete mode 100644 server/testgame/TestGame/Levels/Proving/L01_Contra.lean delete mode 100644 server/testgame/TestGame/Levels/Proving/L06_ByContra.lean delete mode 100644 server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean index 1d65d39..efe6e43 100644 --- a/server/testgame/TestGame.lean +++ b/server/testgame/TestGame.lean @@ -3,7 +3,7 @@ import TestGame.Metadata import TestGame.Levels.Proposition import TestGame.Levels.Implication import TestGame.Levels.Predicate -import TestGame.Levels.Proving +import TestGame.Levels.Contradiction import TestGame.Levels.Prime import TestGame.Levels.Naturals.L31_Sum @@ -63,7 +63,6 @@ Conclusion "There is nothing else so far. Thanks for rescuing natural numbers!" -Path Proposition → Implication → Predicate → Proving +Path Proposition → Implication → Predicate → Contradiction Path Predicate → Prime - Path Predicate → Nat2 diff --git a/server/testgame/TestGame/Levels/Contradiction.lean b/server/testgame/TestGame/Levels/Contradiction.lean new file mode 100644 index 0000000..b62ccb7 --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction.lean @@ -0,0 +1,6 @@ +import TestGame.Levels.Contradiction.L01_Have +import TestGame.Levels.Contradiction.L02_Suffices +import TestGame.Levels.Contradiction.L03_ByContra +import TestGame.Levels.Contradiction.L04_ByContra +import TestGame.Levels.Contradiction.L05_Contrapose +import TestGame.Levels.Contradiction.L06_Summary diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean new file mode 100644 index 0000000..8bd514a --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean @@ -0,0 +1,67 @@ +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 1 + +Title "Have" + +Introduction +" +Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein +Zwischenresultat beweisen, welches wir dann benützen können. + +Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen, +dass man anschliessen beweisen muss. + +Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst +du mit +``` +have g : ¬ B +apply h +assumption +``` +eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme, +bevor du dann mit dem Beweis forfährst. +" + +Statement + "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass + $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt." + (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by + rcases g with ⟨h₁, h₂⟩ + have h₃ : ¬ B + apply h + assumption + contradiction + +Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. +" + +Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +" Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\" + + In Lean : + + ``` + have k : ¬ B + [Beweis von k] + ``` +" + +example (n : ℕ) : n.succ + 2 = n + 3 := by +ring_nf + +Conclusion "" + +Tactics contradiction rcases haveₓ assumption apply + +Lemmas Even Odd not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean new file mode 100644 index 0000000..6b977d9 --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean @@ -0,0 +1,65 @@ +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 2 + +Title "Suffices" + +Introduction +" +Die Taktik `suffices` funktioniert genau gleich wie `have`, +vertauscht aber die beiden Beweisblöcke: + +``` +suffices h : [Aussage] +[Beweis des Goals (mithilfe von h)] +[Beweis der Aussage h] +``` +Auf Deutsch entspricht `suffices h : [Aussage]` dem Ausdruck +\"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\" + +Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so, +dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe +`suffices` schöner gewesen: + +" + +Statement + "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass + $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt." + (A B : Prop) (h : A → ¬ B) (g : A ∧ B) : False := by + rcases g with ⟨h₁, h₂⟩ + suffices k : ¬ B + contradiction + apply h + assumption + +Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A ∧ B) : False => +" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen. +" + +Message (A : Prop) (B : Prop) (h : A → ¬ B) (g : A) (f : B) : False => +" Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\" + + In Lean : + + ``` + suffices k : ¬ B + contradiction + [...] + ``` +" + +Conclusion "" + +Tactics contradiction apply assumption rcases sufficesₓ + +Lemmas Even Odd not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean new file mode 100644 index 0000000..d88106c --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean @@ -0,0 +1,55 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring +import Mathlib + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 3 + +Title "Per Widerspruch" + +Introduction +" +Eine sehr nützliche Beweismethode ist per Widerspruch. + +Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen +sucht, und damit jegliches beweisen kann. + +Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle +Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt. + +Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung +steht: +" + +Statement +"Angenommen $B$ ist falsch und es gilt $A \\Rightarrow B$. Zeige, dass $A$ falsch sein +muss." + (A B : Prop) (h : A → B) (b : ¬ B) : ¬ A := by + by_contra a + suffices b : B + contradiction + apply h + assumption + + +Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) : ¬ A => +"`by_contra h` nimmt das Gegenteil des Goal als Annahme `(h : A)` und setzt das +Goal auf `False`." + +Message (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => +"Jetzt kannst du mit `suffices` oder `have` Fortschritt machen." + +Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => +"Zum Beispiel `suffices hb : B`." + + +Conclusion "" + +Tactics by_contra sufficesₓ haveₓ contradiction apply assumption diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean new file mode 100644 index 0000000..0c41219 --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean @@ -0,0 +1,49 @@ +import TestGame.Metadata +import Std.Tactic.RCases +import Mathlib.Tactic.LeftRight +import Mathlib.Tactic.Contrapose +import Mathlib.Tactic.Use +import Mathlib.Tactic.Ring +import Mathlib + +import TestGame.ToBePorted + +Game "TestGame" +World "Contradiction" +Level 4 + +Title "Per Widerspruch" + +Introduction +" +Als Übung zu `by_contra` und dem bisher gelernten, zeige folgendes Lemma welches +wir für die Kontraposition brauchen werden: +" + +Statement not_imp_not +"$A \\Rightarrow B$ ist äquivalent zu $\\neg B \\Rightarrow \\neg A$." + (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by + constructor + intro h b + by_contra a + suffices b : B + contradiction + apply h + assumption + intro h a + by_contra b + suffices g : ¬ A + contradiction + apply h + assumption + +-- TODO: Forbidden Tactics: apply, rw +-- TODO: forbidden Lemma: not_not + +Hint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) => +"" + + +Conclusion "" + +Tactics contradiction constructor intro by_contra sufficesₓ haveₓ apply assumption diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean new file mode 100644 index 0000000..94f0ae7 --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean @@ -0,0 +1,65 @@ +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 5 + +Title "Kontraposition" + +Introduction +" +Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma + +``` +lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by + [...] +``` + +Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal +entsprechend umdreht. + +Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation +im Goal erstellt. + +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 : ℕ) (h : Odd (n ^ 2)): Odd n := by + revert h + contrapose + rw [not_odd] + rw [not_odd] + apply even_square + +Hint (n : ℕ) (h : Odd (n ^ 2)) : Odd n => +"Um `contrapose` anzuwenden, brauchen wir eine Implikation `Odd (n ^ 2) → Odd n` im +Goal. Benutze `revert h`!" + +Message (n : ℕ) : Odd (n ^ 2) → Odd n => +"Mit `contrapose` kann man die Implikation zu +`¬ (Not n) → ¬ (Odd n^2)` umkehren." + +Message (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`." + +Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden." + +Message (n : ℕ) : Even n → ¬Odd (n ^ 2) => +"rw [not_odd] muss hier zweimal angewendet werden." + +Message (n : ℕ) : Even n → Even (n ^ 2) => +"Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek." + +Tactics contrapose rw apply +Lemmas Even Odd not_even not_odd even_square diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean new file mode 100644 index 0000000..f070cae --- /dev/null +++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean @@ -0,0 +1,76 @@ +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 "Proving" +Level 6 + +Title "Contradiction" + +Introduction +" +In diesem Kapitel hast du also folgende Taktiken kennengelernt: + +| | Taktik | Beispiel | +|:------|:----------------|:-------------------------------------------------------| +| 16 | `have` | Zwischenresultat annehmen. | +| 17 | `suffices` | Zwischenresultat annehmen. | +| 18 | `by_contra` | Widerspruch. (startet einen Widerspruch) | +| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* | +| 19 | `contrapose` | Contraposition. | +| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. | + +Als Vergleich zwischen Beweisen \"per Widerspruch\" +und \"per Kontraposition\", beweise die Gleiche Aufgabe indem +du mit `by_contra` einen Widerspruch suchst. +" + +Statement + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." + (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by + by_contra g + suffices d : ¬ Odd (n ^ 2) + contradiction + rw [not_odd] at * + apply even_square + assumption + +Hint (n : ℕ) (h : Odd (n^2)) : Odd n => +"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten." + +Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False => +" +Am sinnvollsten ist es, hier einen Widerspruch zu `Odd (n^2)` zu suchen. +Dafür kannst du +``` +suffices k : ¬ Odd (n ^ 2) +contradiction +``` +benützen. +" + +Hint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False => +"Hier brauchst du nur `contradiction`." + +Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) => +"Das Zwischenresultat `¬Odd (n^2)` muss auch bewiesen werden. +Hier ist wieder das Lemma `not_Odd` hilfreich." + +Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) => +"Mit `rw [not_Odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben." + +Message (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => +"Diese Aussage hast du bereits als Lemma bewiesen." + +Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => +"Probiers mit `apply ...`" + + +Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have + +Lemmas Odd Even not_odd not_even even_square diff --git a/server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean b/server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean deleted file mode 100644 index a8c1ce5..0000000 --- a/server/testgame/TestGame/Levels/LeftOvers/L08_Contrapose.lean +++ /dev/null @@ -1,37 +0,0 @@ -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 "Implication" -Level 102 - -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 - -Hint (n : ℕ) (h : odd (n ^ 2)) : odd n => -"Benutze `revert h` um das Goal in eine Implikation umzuschreiben." - -Message (n : ℕ) : odd (n ^ 2) → odd n => -"Jetzt ist es genau das gleiche wie bei der letzten Aufgabe." - -Tactics contrapose rw apply revert -Lemmas even odd not_even not_odd even_square diff --git a/server/testgame/TestGame/Levels/LeftOvers/Playground.lean b/server/testgame/TestGame/Levels/LeftOvers/Playground.lean new file mode 100644 index 0000000..7622e0b --- /dev/null +++ b/server/testgame/TestGame/Levels/LeftOvers/Playground.lean @@ -0,0 +1,18 @@ +import TestGame.Metadata +import Mathlib + +-- -- INCORPORATED +-- example (A B : Prop) : (A → B) ↔ (¬ B → ¬A) := by +-- constructor +-- intro h nb +-- by_contra +-- have : B +-- apply h +-- assumption +-- contradiction +-- intro h a +-- by_contra +-- have : ¬ A +-- apply h +-- assumption +-- contradiction diff --git a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean index 90f0417..aaf51f0 100644 --- a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean +++ b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean @@ -1,5 +1,9 @@ +import Mathlib.Algebra.BigOperators.Basic +import Mathlib + import TestGame.Metadata -import Mathlib.Tactic.Ring + +set_option tactic.hygienic false Game "TestGame" World "Nat2" @@ -9,15 +13,13 @@ Title "Summe" Introduction " -TODO: Summe - " -Statement "" : True := by - trivial - -Conclusion -" -" +Statement +"Zeige $\\sum_{i=0}^{n} i = \\frac{n \\cdot {n+1}}{2}$" + (n : ℕ) : 2 * (∑ i : Fin (n+1), ↑i) = n * (n + 1) := by + induction' n with n hn + simp + sorry -- done in Lean3. -Tactics ring +Tactics intro constructor assumption diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean index 3125cd4..0ba22c4 100644 --- a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean +++ b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean @@ -23,13 +23,8 @@ Abschlussaufgabe. | `ℕ` | Die natürlichen Zahlen. | | `∃` | Existential-Quantifier | | `∀` | Forall-Quantifier | -| `even n` | `n` ist gerade | -| `odd n` | `n` ist ungerade | -| | | -| | | -| | | -| | | -| | | +| `Even n` | `n` ist gerade | +| `Odd n` | `n` ist ungerade | ## Taktiken diff --git a/server/testgame/TestGame/Levels/Proving.lean b/server/testgame/TestGame/Levels/Proving.lean deleted file mode 100644 index e279ac1..0000000 --- a/server/testgame/TestGame/Levels/Proving.lean +++ /dev/null @@ -1 +0,0 @@ -import TestGame.Levels.Proving.L01_Contra diff --git a/server/testgame/TestGame/Levels/Proving/L01_Contra.lean b/server/testgame/TestGame/Levels/Proving/L01_Contra.lean deleted file mode 100644 index 6b01ccb..0000000 --- a/server/testgame/TestGame/Levels/Proving/L01_Contra.lean +++ /dev/null @@ -1,51 +0,0 @@ -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 "Proving" -Level 1 - -Title "Ad absurdum" - -Introduction -" -In diesem Kapitel lernen wir die wichtigsten Beweistechniken kennen. - -Zuerst repetieren wir, dass man vorhandene Lemmas mit `rw` und `apply` benützen kann. - - - Aber, die Aussagen müssen wirklich exakte Gegenteile sein. - -Hier musst du zuerst eines der folgenden Lemmas benützen, um einer der Terme umzuschreiben. - -``` -lemma not_odd (n : ℕ): ¬ odd n ↔ even n := by - ... - -lemma not_even (n : ℕ): ¬ even n ↔ odd n := by - ... -``` -" - -Statement - "Sei $n$ eine natürliche Zahl die sowohl gerade wie auch ungerade ist. - Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)." - (n : ℕ) (h_even : Even n) (h_odd : Odd n) : n = 42 := by - rw [← not_even] at h_odd - contradiction - -Message (n : ℕ) (h_even : Even n) (h_odd : Odd n) : n = 42 => -"Schreibe zuerst eine der Aussagen mit `rw [←not_even] at h_odd` um, damit diese genaue -Gegenteile werden." - -Conclusion "" - -Tactics contradiction rw - -Lemmas Even Odd not_even not_odd diff --git a/server/testgame/TestGame/Levels/Proving/L06_ByContra.lean b/server/testgame/TestGame/Levels/Proving/L06_ByContra.lean deleted file mode 100644 index b7d77bd..0000000 --- a/server/testgame/TestGame/Levels/Proving/L06_ByContra.lean +++ /dev/null @@ -1,81 +0,0 @@ -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 "Proving" -Level 2 - -Title "Widerspruch" - -Introduction -" -Zwei wichtige Beweisformen sind per Widerspruch und per Kontraposition. Hier -schauen wir beide an und auch den Unterschied. - -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. - -**Bemerkung:** Besonders beim Beweis durch Widerspruch ist es hilfreich, wenn man -Zwischenresultate erstellen kann. -`suffices h₁ : ¬(Odd (n ^ 2))` erstellt zwei neue Goals: - -1) Ein Beweis, wieso es genügt `¬(Odd (n ^ 2))` zu zeigen (\"weil das einen Widerspruch zu -`h` bewirkt\"). -2) Einen Beweis des Zwischenresultats `suffices h₁ : ¬(Odd (n ^ 2))` - -Alternativ macht `have h₁ : ¬(Odd (n ^ 2))` genau das gleiche, vertauscht aber die -Beweise (1) und (2), so dass man zuerst `h₁` beweist, und dann den eigentlichen Beweis -fortsetzt. -" - -Statement - "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." - (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by - by_contra g - suffices d : ¬ Odd (n ^ 2) -- TODO: I don't like this - contradiction - - rw [not_odd] at g - rw [not_odd] - apply even_square - assumption - -Message (n : ℕ) (h : Odd (n^2)) : Odd n => -"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten." - -Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False => -"Nun *genügt es zu zeigen, dass* `¬Odd (n ^ 2)` wahr ist, -denn dann erhalten wir einen Widerspruch zu `h`. - -Benütze dafür `suffices h₂ : ¬Odd (n ^ 2)`. -" - -Message (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False => -"Hier musst du rechtfertigen, wieso das genügt. In unserem Fall, weil -dadurch einen Widerspruch entsteht." - -Hint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False => -"Also `contradiction`..." - -Message (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) => -"Das Zwischenresultat `¬Odd (n^2)` muss auch bewiesen werden. -Hier ist wieder das Lemma `not_Odd` hilfreich." - -Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) => -"Mit `rw [not_Odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben." - -Message (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => -"Diese Aussage hast du bereits als Lemma bewiesen." - -Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) => -"Probiers mit `apply ...`" - - -Tactics contradiction by_contra rw apply assumption -- TODO: suffices, have - -Lemmas Odd Even not_odd not_even even_square diff --git a/server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean b/server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean deleted file mode 100644 index 0523ad5..0000000 --- a/server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean +++ /dev/null @@ -1,50 +0,0 @@ -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 "Proving" -Level 3 - -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 - -Message (n : ℕ) (h : Odd (n ^ 2)) : Odd n => -"`intro` wär generell ein guter Ansatz! Aber hier wollen wir `contrapose` benützen, was eine -Implikation benötigt, deshalb ist `intro` hier der falsche Weg!" - - -Message (n : ℕ) : Odd (n ^ 2) → Odd n => -"Mit `contrapose` kann man die Implikation zu -`¬ (even n) → ¬ (even n^2)` umkehren." - -Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Du kennst bereits ein Lemma um `¬ odd ...` mit `rw` -umzuschreiben" - -Message (n : ℕ) : Even n → ¬Odd (n ^ 2) => "rw [not_odd] muss hier zweimal angewendet werden, -da rw das erste Mal `not_odd n` gebraucht hat und das zweite Mal `not_odd (n^2)` benützt." - -Message (n : ℕ) : Even n → Even (n ^ 2) => "Diese Aussage hast du bereits als Lemma bewiesen." - -Tactics contrapose rw apply -Lemmas Even Odd not_even not_odd even_square diff --git a/server/testgame/TestGame/TacticDocs.lean b/server/testgame/TestGame/TacticDocs.lean index f58a957..7e1f974 100644 --- a/server/testgame/TestGame/TacticDocs.lean +++ b/server/testgame/TestGame/TacticDocs.lean @@ -189,12 +189,19 @@ TacticDoc use TODO " +TacticDoc sufficesₓ +" +## Beschreibung +TODO +" +TacticDoc haveₓ +" +## Beschreibung - - - +TODO +" TacticDoc induction_on @@ -236,8 +243,6 @@ Prove: ``` " - - TacticDoc intro "Useful to introduce stuff"