changes to levels

2023-01-19 15:43:29 +01:00
parent 01e2b3b4a1
commit 9d1a591670
15 changed files with 187 additions and 96 deletions
@@ -1,33 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Implication"
-Level 20
-
-Title "Nicht-nicht"
-
-Introduction
-"
-Wenn man ein Nicht (`¬`) im Goal hat, will man meistens einen Widerspruch starten,
-wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form
-`¬ (¬ A)`, in welchem Fall das Lemma `not_not` nützlich ist, welches du mit
-`rw` oder `apply` benützen kannst.
-"
-
-Statement
-    "Zeige, dass $\\neg(\\neg A)$ äquivalent zu $A$ ist."
-    (A : Prop) : ¬ (¬ A) ↔ A := by
-  rw [not_not]
-
-Message (A : Prop) : ¬ (¬ A) ↔ A => "Da `not_not` ein Lemma der Form `X ↔ Y` ist,
-kannst du wahlweise `rw [not_not]` oder `apply not_not` benützen.
-
- `rw` ersetzt `¬ (¬ A)` mit `A` und schliesst dann `A ↔ A` mit `rfl`.
- `apply` hingegen funktioniert hier nur, weil das gesamte Goal
-genau mit der Aussage des Lemmas übereinstimmt.
-"
-
-Tactics rw apply
-
-Lemmas not_not
@@ -1 +1,9 @@
 import TestGame.Levels.Predicate.L01_Ring
+import TestGame.Levels.Predicate.L02_Rewrite
+import TestGame.Levels.Predicate.L03_Rewrite
+import TestGame.Levels.Predicate.L04_Ring
+import TestGame.Levels.Predicate.L05_Rfl
+import TestGame.Levels.Predicate.L06_Exists
+import TestGame.Levels.Predicate.L07_Forall
+import TestGame.Levels.Predicate.L08_PushNeg
+import TestGame.Levels.Predicate.L09_Summary
@@ -13,12 +13,15 @@ Introduction
 "
 Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon kurz begegnet.

-Gleichungen, die nur die Operationen `+, -, *, ^` und Variablen enthalten, kann Lean mit der
-Taktik `ring` beweisen.
+Gleichungen, die nur die Operationen `+, -, *, ^` (Addition, Subtraktion, Multiplikation, Potenz)
+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.
+
+(Note: Division `/` ignorieren wir hier erst einmal, weil diese auf `ℕ`
+nicht kanonisch definiert ist.)
 "

 Statement
@@ -37,3 +40,5 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
 "

 Tactics ring
+
+#eval 4 / 6
@@ -0,0 +1,70 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Predicate"
+Level 2
+
+Title "Rewrite"
+
+Introduction
+"
+Wir haben gesehen, dass man mit `rw` Äquivalenzen wie `A ↔ B` brauchen kann, um im Goal
+$A$ durch $B$ zu ersetzen.
+
+Genau gleich kann man auch Gleichungen `a = b` mit `rw` verwenden.
+"
+
+Statement umschreiben
+"Angenommen man hat die Gleichheiten
+
+$$
+\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
+$$
+
+Zeige dass $b = c$."
+(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rw [h₁]
+  rw [←h₂]
+  assumption
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (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 : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (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₁]`."
+
+Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
+" 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 : ℕ) (b : ℕ) (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 : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (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 : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (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 : ℕ) (b : ℕ) (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 : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c =>
+"das ist nicht der optimale Weg..."
+
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c =>
+"das ist nicht der optimale Weg..."
+
+
+
+Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
+
+Tactics assumption rw
@@ -3,13 +3,14 @@ import Mathlib

 Game "TestGame"
 World "Predicate"
-Level 4
+Level 3

 Title "Rewrite"

 Introduction
 "
-Mit `rw` kann man nicht nur das Goal sondern auch andere Annahmen umschreiben:
+Als Übung erinnern wir daran, dass man mit `rw [h] at g` auch in anderen Annahmen umschreiben
+kann:

 Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
 `g` das `X` durch `Y`.
@@ -1,50 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Predicate"
-Level 3
-
-Title "Rewrite"
-
-Introduction
-"
-Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern man braucht
-mehrere Schritte im Beweis.
-
-Wenn man eine Annahme `(h : X = Y)` hat,
-kann die Taktik `rw [h]` im Goal $X$ durch $Y$ ersetzen.
-(`rw` steht für *rewrite*)
-"
-
-Statement umschreiben
-"Angenommen man hat die Gleichheiten
-
-$$
-\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
-$$
-
-Zeige dass $b = c$."
-(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
-  rw [h₁]
-  rw [←h₂]
-  assumption
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man tippt diese mit
-`\\1`, `\\2`, `\\3`, …"
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (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₁]`."
-
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-" 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 : ℕ) (b : ℕ) (h : a = b) : a = b =>
-"Schau mal durch die Annahmen durch."
-
-Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
-
-Tactics assumption rw
@@ -3,13 +3,16 @@ import Mathlib.Tactic.Ring

 Game "TestGame"
 World "Predicate"
-Level 5
+Level 4

 Title "Natürliche Zahlen"

 Introduction
 "
-Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
+Oft braucht man eine Kombination von `rw` und `ring` um Gleichungen zu lösen.
+
+Zuerst setzt man mit `rw` die vorhandenen Annahmen ein, und sobald die beiden Seiten
+einer Gleichung im Goal rechnerisch gleich sind, kan `ring` dies beweisen.
 "

 Statement
@@ -2,7 +2,7 @@ import TestGame.Metadata

 Game "TestGame"
 World "Predicate"
-Level 6
+Level 5

 Title "Definitionally equal"

@@ -8,7 +8,7 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Predicate"
-Level 7
+Level 6

 Title "Gerade/Ungerade"

@@ -8,7 +8,7 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Predicate"
-Level 8
+Level 7

 Title "Für alle"

@@ -16,7 +16,19 @@ Introduction
 "
 Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).

+Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
+
+Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
+auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
+
+Also folgende Annahme und Lemma sind genau :
+- `(le_square : ∀ (n : ℕ), n ≤ n^2)`
+- `lemma le_square (n : ℕ) : n ≤ n^2`
+
 Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
+
+
+TODO: 1-2 Aufgaben mehr.
 "

 Statement
@@ -6,7 +6,7 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Predicate"
-Level 9
+Level 8

 Title "PushNeg"

@@ -0,0 +1,60 @@
+import TestGame.Metadata
+import Mathlib.Tactic.PushNeg
+import Mathlib
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Predicate"
+Level 9
+
+Title "Zusammenfassung"
+
+Introduction
+"
+Damit bist du am Ende der dritten Lektion angekommen.
+Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
+Abschlussaufgabe.
+
+## Notationen / Begriffe
+
+|               | Beschreibung                |
+|:--------------|:----------------------------|
+| `ℕ`           | Die natürlichen Zahlen.     |
+| `∃`           | Existential-Quantifier      |
+| `∀`           | Forall-Quantifier           |
+| `even n`      | `n` ist gerade              |
+| `odd n`       | `n` ist ungerade            |
+|               |                             |
+|               |                             |
+|               |                             |
+|               |                             |
+|               |                             |
+
+
+## Taktiken
+
+|       | Taktik                    | Beispiel                                               |
+|:------|:--------------------------|:-------------------------------------------------------|
+| *11ᶜ* | `rw`                      | Umschreiben mit Gleichungen.                           |
+| 12    | `ring`                    | Löst Gleichungen mit `+, -, *, ^`.                     |
+| 13    | `unfold`                  | Setzt visuell die Bedeutung einer Definition ein.      |
+| 14    | `use`                     | Um ein `∃` im Goal anzugehen.                          |
+| *7ᶜ*  | `rcases h with ⟨x, hx⟩`   | Um ein `∃` in den Annahmen zu zerlegen.                |
+| *8ᵇ*  | `intro`                   | Um ein `∀` im Goal anzugehen.                          |
+| 15    | `push_neg`                | Für `¬∃` und `¬∀` im Goal.                             |
+
+Als Abschlussübung kannst du folgende Äquivalenz zeigen:
+
+"
+
+Statement
+    "TODO":
+    True := by
+  trivial
+
+Conclusion ""
+
+Tactics push_neg intro use rw unfold ring
+
+Lemmas even odd not_even not_odd not_exists not_forall
@@ -0,0 +1 @@
+import TestGame.Levels.Prime.L01_Prime
@@ -14,10 +14,24 @@ Level 1
 Title "Ad absurdum"

 Introduction
-"Aber, die Aussagen müssen wirklich exakte Gegenteile sein.
+"
+In diesem Kapitel lernen wir die wichtigsten Beweistechniken kennen.

-Hier musst du zuerst eines der Lemmas `(not_odd : ¬ odd n ↔ even n)` oder
-`(not_even : ¬ even n ↔ odd n)` benützen, um einer der Terme umzuschreiben."
+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.