more levels

2022-12-05 11:40:44 +01:00
parent 4acd791fd7
commit cde0e95c1e
19 changed files with 515 additions and 29 deletions
@@ -2,13 +2,13 @@ import TestGame.Metadata
 import Std.Tactic.RCases
 import Mathlib.Tactic.LeftRight

-set_option tactic.hygienic false
+--set_option tactic.hygienic false

 Game "TestGame"
 World "TestWorld"
 Level 15

-Title "Oder"
+Title "Oder - Bonus"

 Introduction
 "
@@ -21,38 +21,32 @@ wo man annimmt, dass entweder die linke oder rechte Seite von `h` war ist.
 Diese Annahme benennt man dann mit `rcases h with hA | hB`.
 "

-Statement and_or_imp
-  "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
-    (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
-  rcases h with h₁ | h₂
+Statement
+    (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by
+  rcases h with ⟨ha, hb⟩ | (h | h)
  left
-  rcases h₁ with ⟨x, y⟩
+  constructor
+  assumption
  assumption
  right
-  constructor
-  apply h₂
+  right
  assumption
+  right
+  left
  assumption

-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
-"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`. Der `|` signalisiert
-dass `h₁` und `h2` die Namen der neuen Annahmen in den verschiedenen Fällen sind."
-
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
-"Ein ODER im Goal kann mit `left` oder `right` angegangen werden."
-
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B =>
-"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen.
-Der Konstruktor `⟨⟩` signalisiert hier, dass dann nur ein Goal aber zwei neu benannte
-Annahmen erhält."
-
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C =>
-"Sackgasse."
-
-Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
-"Hmmm..."
-
-Message (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
-"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
+Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) =>
+"Man kann hier entweder in mehren Schritten `rcases` anwenden:
+```
+  rcases h with h₁ | h₂
+  rcases h₁ with ⟨hA, hB⟩
+  [...]
+  rcases h₂ with h | h
+```
+oder man kann dies in einem Schritt verschachteln:
+```
+rcases h with ⟨ha, hb⟩ | (h | h)
+```
+"

 Tactics left right assumption constructor rcases
@@ -0,0 +1,52 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "TestWorld"
+Level 16
+
+Title "Oder"
+
+Introduction
+"
+Übung macht den Meister...
+"
+
+Statement and_or_imp
+  "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen."
+    (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by
+  rcases h with h₁ | h₂
+  left
+  rcases h₁ with ⟨x, y⟩
+  assumption
+  right
+  constructor
+  apply h₂
+  assumption
+  assumption
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B ∨ (A → C)) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER in den Annahmen teilt man mit `rcases h with h₁ | h₂`. Der `|` signalisiert
+dass `h₁` und `h2` die Namen der neuen Annahmen in den verschiedenen Fällen sind."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B ∨ (C ∧ A) =>
+"Ein ODER im Goal kann mit `left` oder `right` angegangen werden."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) (hA : A) : B =>
+"Ein UND in den Annahmen kann man mit `rcases h with ⟨h₁, h₂⟩` aufteilen.
+Der Konstruktor `⟨⟩` signalisiert hier, dass dann nur ein Goal aber zwei neu benannte
+Annahmen erhält."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C =>
+"Sackgasse."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
+"Hmmm..."
+
+Message (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
+"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
+
+Tactics left right assumption constructor rcases
@@ -0,0 +1 @@
+-- tauto is not implemented yet... duper?
@@ -0,0 +1 @@
+-- not implemented yet
@@ -0,0 +1,39 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+
+-- TODOs:
+-- Natural numbers
+-- even / odd
+-- prime
+-- `ring`
+-- sum
+-- induction
+
+--set_option tactic.hygienic false
+
+Game "TestGame"
+World "Nat"
+Level 1
+
+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.
+
+Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen.
+"
+
+Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+  ring
+
+Conclusion
+"
+Die Taktik heisst übrigens `ring` weil sie dafür entwickelt wurde, Gleichungen in einem abstrakten
+Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
+(erst `ℤ` ist ein Ring).
+"
+
+Tactics ring
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+Game "TestGame"
+World "Contradiction"
+Level 1
+
+Title "Widerspruch"
+
+Introduction
+"
+Ein wichtiges Konzept ist die Verneinung und damit einhergehend die Kontraposition
+und der Widerspruch (Kontradiktion).
+
+Als allererstes der Widerspruch.
+
+Wenn man in den Annahmen einen Widerspruch hat, kann man mit `contradiction` den Beweis
+schliessen, denn ein Widerspruch beweist alles.
+
+Der einfachste Widerspruch ist wenn man einen Beweis von `false` hat:
+"
+
+Statement
+  "Ein Widerspruch impliziert alles."
+    (A : Prop) (h : false) : A := by
+  contradiction
+
+Tactics contradiction
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+Game "TestGame"
+World "Contradiction"
+Level 2
+
+Title "Widerspruch"
+
+Introduction
+"
+Ähnlich siehts aus, wenn man Annahmen hat, die direkte Negierung voneinander sind,
+also `(h : A)` und `(g : ¬ A)`. (`\\not`)
+"
+
+Statement
+  "Ein Widerspruch impliziert alles."
+    (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by
+  contradiction
+
+Conclusion
+"
+Detail: `¬ A` ist übrigens als `A → false` implementiert, was aussagt, dass
+\"falls `A` wahr ist, impliziert das `false` und damit einen Widerspruch\".
+"
+-- TODO: Oder doch ganz entfernen?
+
+Tactics contradiction
@@ -0,0 +1,31 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+Game "TestGame"
+World "Contradiction"
+Level 3
+
+Title "Widerspruch"
+
+Introduction
+"
+Im weiteren kann man auch Widersprüche erhalten, wenn man Annahmen der Form
+`A = B` hat, wo Lean weiss, dass `A und `B` unterschiedlich sind, z.B. `0 = 1` in `ℕ`
+oder auch Annahmen der Form `A ≠ A` (`\\ne`).
+"
+
+Statement
+  "Ein Widerspruch impliziert alles."
+    (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by
+  rw [g₁] at h
+  contradiction
+
+Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A =>
+  "Recap: `rw [...] at h` hilft dir hier."
+
+Message (A : Prop) (a : ℕ) (b : ℕ) (c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : b ≠ c) : A =>
+  "`b ≠ c` muss man als `¬ (b = c)` lesen. Deshalb findet `contradiction` hier direkt
+  einen Widerspruch."
+
+Tactics contradiction
@@ -0,0 +1,20 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Contradiction"
+Level 4
+
+Title "Widerspruch"
+
+Introduction
+"
+"
+
+
+Statement
+    (A : Prop) : A := by
+  by_contradiction
+
+
+Tactics contradiction
@@ -0,0 +1,20 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Contradiction"
+Level 5
+
+Title "Widerspruch"
+
+Introduction
+"
+"
+
+
+Statement
+    (A : Prop) : A := by
+  not_not
+
+
+Tactics contradiction
@@ -0,0 +1,20 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Contradiction"
+Level 6
+
+Title "Widerspruch"
+
+Introduction
+"
+"
+
+
+Statement
+    (A : Prop) : A := by
+  pushNeg
+
+
+Tactics contradiction
@@ -0,0 +1,23 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+
+Game "TestGame"
+World "Contradiction"
+Level 7
+
+Title "Kontraposition"
+
+Introduction
+"
+Im Gegensatz zum Widerspruch, wo
+"
+
+Statement
+  "Ein Widerspruch impliziert alles."
+    (A B : Prop) (h : ¬ B → ¬ A) (hA : A) : B := by
+  revert hA
+  contrapose
+  assumption
+
+Tactics contradiction
@@ -0,0 +1,26 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+
+Game "TestGame"
+World "Contradiction"
+Level 8
+
+Title "Kontraposition"
+
+Introduction
+"
+Im Gegensatz zum Widerspruch, wo
+"
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+
+-- Statement
+--   "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
+--     (n : ℕ) (h : odd n ^ 2) : odd n := by
+--   byContradiction g
+--   rw [not_odd] at g
+--   ...
+--   contradiction
+
+Tactics contradiction
@@ -0,0 +1,27 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+
+Game "TestGame"
+World "Contradiction"
+Level 9
+
+Title "Kontraposition"
+
+Introduction
+"
+Im Gegensatz zum Widerspruch, wo
+"
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+
+-- Statement
+--   "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
+--     (n : ℕ) (h : odd n ^ 2) : odd n := by
+--   revert h
+--   contrapose
+--   rw [not_odd]
+--   intro
+--   trivial (?)
+
+Tactics contradiction
@@ -0,0 +1,4 @@
+- `trivial` uses a bunch of other tactics:
+  (contradiction, assumption, rfl, decide, True.intro, And.intro)
+  so it's maybe not a good candidate to introduce at the beginning of the level.
+- Ringschluss (tfae) is not in mathlib4 yet.
@@ -0,0 +1,68 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+
+Game "TestGame"
+World "Quantors"
+Level 9
+
+Title "Kontraposition"
+
+Introduction
+"
+Häufig enthalten logische Aussagen die Quantoren \"für alle `x`\" und
+\"es existiert ein `x`, so dass\". In Lean schreibt man diese wie in der Mathe
+mit den Zeichen `∀` und `∃` (`\\forall`, `\\exists`):
+
+Beide können mehrere Variablen annehmen: `∃ (x : ℕ) (y : ℕ), x ^ 3 = 2 * y + 1` ist das selbe
+wie `∃ (x : ℕ), (∃ (y : ℕ), x ^ 3 = 2 * y + 1)`.
+
+Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
+ein `x` erhalten, dass die Aussage erfüllt.
+
+Bei einem Exists-Statement im Goal kann man mit `use` das Element angeben, dass dieses `∃ x,`
+erfüllt.
+"
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+def even (a : ℕ) : Prop := ∃ r, a = r + r
+def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1
+
+Statement (n : ℕ) (h : even n) : even (n ^ 2) := by
+  unfold even at *
+  rcases h with ⟨x, hx⟩
+  use 2 * x ^ 2
+  rw [hx]
+  ring
+
+-- TODO: Server PANIC because of the `even`.
+--
+-- Message (n : ℕ) (h : even n) : even (n ^ 2) =>
+-- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
+-- `unfold even at *` ersetzen.
+-- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
+-- genau gleich, wenn du das `unfold` rauslöscht."
+
+Message (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
+"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
+ein `x` erhalten, dass die Aussage erfüllt."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
+"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
+die Aussage erfüllen soll."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r =>
+"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
+die Aussage erfüllen soll."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
+"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu
+`x + x` umschreiben..."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
+"Die Taktik `ring` löst solche Gleichungen."
+
+Tactics unfold rcases use rw ring
@@ -0,0 +1,57 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+
+Game "TestGame"
+World "Quantors"
+Level 9
+
+Title "Kontraposition"
+
+Introduction
+"
+Bei einem `∀ x,` im Goal kann man mit `intro x` annehmen, dass man ein solches `x` hat.
+
+Ein `(h : ∀ x, _)` in den Annahmen kann ....
+"
+
+-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
+def even (a : ℕ) : Prop := ∃ r, a = r + r
+def odd (a : ℕ) : Prop := ∃ k, a = 2*k + 1
+
+Statement : ∀ (x : ℕ), 1 = x ^ 2 → 1 = x := by
+  intro x h
+
+
+
+-- TODO: Server PANIC because of the `even`.
+--
+-- Message (n : ℕ) (h : even n) : even (n ^ 2) =>
+-- "Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
+-- `unfold even at *` ersetzen.
+-- Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
+-- genau gleich, wenn du das `unfold` rauslöscht."
+
+Message (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
+"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
+ein `x` erhalten, dass die Aussage erfüllt."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
+"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
+die Aussage erfüllen soll."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r =>
+"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
+die Aussage erfüllen soll."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
+"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu
+`x + x` umschreiben..."
+
+Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
+"Die Taktik `ring` löst solche Gleichungen."
+
+Tactics unfold rcases use rw ring
@@ -0,0 +1,22 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+
+Game "TestGame"
+World "Contradiction"
+Level 3
+
+Title "Widerspruch"
+
+Introduction
+"
+Ähnlich siehts aus, wenn man Annahmen hat, die direkte Negierung voneinander sind,
+also `(h : A)` und `(g : ¬ A)`.
+"
+
+Statement
+  "Ein Widerspruch impliziert alles."
+    (A : Prop) (n : ℕ) (h : ∃ x, 2 * x = n) (g : ¬ (∃ x, 2 * x = n)) : A := by
+  contradiction
+
+Tactics contradiction
@@ -117,10 +117,33 @@ TacticDoc right
 TODO
 "

+TacticDoc contradiction
+"
+## Beschreibung

+TODO
+"

+TacticDoc ring
+"
+## Beschreibung

+TODO
+"

+TacticDoc unfold
+"
+## Beschreibung
+
+TODO
+"
+
+TacticDoc use
+"
+## Beschreibung
+
+TODO
+"