reorganise world Implication
This commit is contained in:
Jon Eugster
@@ -0,0 +1,39 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib.Tactic.Ring
|
||||
|
||||
--set_option tactic.hygienic false
|
||||
|
||||
Game "TestGame"
|
||||
World "Predicate"
|
||||
Level 1
|
||||
|
||||
Title "Natürliche Zahlen"
|
||||
|
||||
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.
|
||||
|
||||
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
|
||||
"Zeige $(x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2$."
|
||||
(x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
|
||||
ring
|
||||
|
||||
Hint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 =>
|
||||
"`ring` übernimmt den ganzen Spaß."
|
||||
|
||||
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,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
|
||||
@@ -0,0 +1,30 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib.Tactic.Ring
|
||||
|
||||
Game "TestGame"
|
||||
World "Predicate"
|
||||
Level 5
|
||||
|
||||
Title "Natürliche Zahlen"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Angenommen, man hat die Gleichung $x = 2 * y + 1$, zeige
|
||||
$x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y$. "
|
||||
(x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
|
||||
rw [h]
|
||||
ring
|
||||
|
||||
Message (x : ℕ) (y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
|
||||
"Die Annahme `h` kannst du mit `rw [h]` benützen."
|
||||
|
||||
Message (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
|
||||
"Jetzt kann `ring` übernehmen."
|
||||
|
||||
Conclusion ""
|
||||
|
||||
Tactics ring rw
|
||||
@@ -0,0 +1,71 @@
|
||||
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 "Predicate"
|
||||
Level 7
|
||||
|
||||
Title "Gerade/Ungerade"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Gerade/ungerade werden in Lean wie folgt definiert:
|
||||
```
|
||||
def even (n : ℕ) : Prop := ∃ r, n = 2 * r
|
||||
def odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
|
||||
```
|
||||
Also dadurch, dass ein `(r : ℕ)` existiert sodass `n = 2 * r (+1)`.
|
||||
Beachte das Komma `,` welches die Variablen des `∃` (`\\exists`) von der Aussage trennen.
|
||||
|
||||
Hierzu gibt es 3 wichtige Taktiken:
|
||||
|
||||
1) Definitionen wie `even` kann man mit `unfold even at *` im Infoview einsetzen.
|
||||
Das ändert Lean-intern nichts und ist nur für den Benutzer. Man kann auch einen
|
||||
Term `(h : even x)` einfach so behandeln als wäre es ein Term `(h : ∃ r, x = 2 * r)`.
|
||||
2) Bei einer Annahme `(h : ∃ r, ...)` kann man mit `rcases h with ⟨y, hy⟩` ein solches `y`
|
||||
Auswählen, dass die Annahme `h` erfüllt.
|
||||
3) Bei einem `∃` im Goal muss man ein Element `y` angeben, welches diese Aussage erfüllen
|
||||
soll. Das macht man mit `use y`
|
||||
"
|
||||
|
||||
Statement even_square
|
||||
"Wenn $n$ gerade ist, dann ist $n^2$ gerade."
|
||||
(n : ℕ) (h : even n) : even (n ^ 2) := by
|
||||
unfold even at *
|
||||
rcases h with ⟨x, hx⟩
|
||||
use 2 * x ^ 2
|
||||
rw [hx]
|
||||
ring
|
||||
|
||||
Message (n : ℕ) (h : even n) : even (n ^ 2) =>
|
||||
"Wenn du die Definition von `even` nicht kennst, kannst du diese mit `unfold even` oder
|
||||
`unfold even at *` ersetzen.
|
||||
Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
|
||||
genau gleich, wenn du das `unfold` rauslöscht."
|
||||
|
||||
Message (n : ℕ) (h : ∃ r, n = 2 * r) : ∃ r, n ^ 2 = 2 * 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 = 2 * 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
|
||||
Lemmas even odd
|
||||
@@ -0,0 +1,40 @@
|
||||
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 "Predicate"
|
||||
Level 8
|
||||
|
||||
Title "Für alle"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
|
||||
|
||||
Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
|
||||
"
|
||||
|
||||
Statement
|
||||
" Für alle natürlichen Zahlen $x$ gilt, falls $x$ gerade ist, dann ist $x + 1$
|
||||
ungerade." : ∀ (x : ℕ), (even x) → odd (1 + x) := by
|
||||
intro x h
|
||||
unfold even at h
|
||||
unfold odd
|
||||
rcases h with ⟨y, hy⟩
|
||||
use y
|
||||
rw [hy]
|
||||
ring
|
||||
|
||||
Message (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even (n + 1) =>
|
||||
"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
|
||||
`(x : ℕ) → `"
|
||||
|
||||
Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
|
||||
praktisch gleich. Mehr dazu später."
|
||||
|
||||
Tactics ring intro unfold
|
||||
@@ -0,0 +1,50 @@
|
||||
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
|
||||
@@ -0,0 +1,39 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib
|
||||
|
||||
Game "TestGame"
|
||||
World "Predicate"
|
||||
Level 4
|
||||
|
||||
Title "Rewrite"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Mit `rw` kann man nicht nur das Goal sondern auch andere Annahmen umschreiben:
|
||||
|
||||
Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
|
||||
`g` das `X` durch `Y`.
|
||||
"
|
||||
|
||||
Statement umschreiben
|
||||
"Angenommen man hat die Gleichheiten
|
||||
|
||||
$$
|
||||
\\begin{aligned} a &= b \\\\ a + a ^ 2 &= b + 1 \\end{aligned}
|
||||
$$
|
||||
|
||||
Zeige dass $b + b ^ 2 = b + 1$."
|
||||
(a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
|
||||
rw [h] at g
|
||||
assumption
|
||||
|
||||
Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 =>
|
||||
"`rw [ ... ] at g` schreibt die Annahme `g` um."
|
||||
|
||||
Message (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 =>
|
||||
"Sackgasse. probiers doch mit `rw [h] at g` stattdessen."
|
||||
|
||||
Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
|
||||
dem Goal umschreiben."
|
||||
|
||||
Tactics assumption rw
|
||||
@@ -0,0 +1,66 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib.Tactic.PushNeg
|
||||
import Mathlib
|
||||
|
||||
import TestGame.ToBePorted
|
||||
|
||||
Game "TestGame"
|
||||
World "Predicate"
|
||||
Level 9
|
||||
|
||||
Title "PushNeg"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
|
||||
mit `push_neg` das `¬` durch den Quantor hindurchschieben.
|
||||
|
||||
Das braucht intern die Lemmas
|
||||
|
||||
- `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
|
||||
- `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
|
||||
|
||||
(welche man auch mit `rw` explizit benutzen könnte.)
|
||||
"
|
||||
|
||||
Statement
|
||||
"Es existiert keine natürliche Zahl $n$, sodass $n + k$ immer ungerade ist.":
|
||||
¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
|
||||
push_neg
|
||||
intro n
|
||||
use n
|
||||
rw [not_odd]
|
||||
unfold even
|
||||
use n
|
||||
ring
|
||||
|
||||
Message : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) =>
|
||||
"`push_neg` schiebt die Negierung an den Quantoren vorbei."
|
||||
|
||||
|
||||
Message (n : ℕ) : (∃ k, ¬odd (n + k)) =>
|
||||
"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutze `use`
|
||||
mit der richtigen Zahl."
|
||||
|
||||
|
||||
Hint (n : ℕ) : ¬odd (n + n) =>
|
||||
"Du kennst ein Lemma um mit `¬odd` umzugehen."
|
||||
|
||||
-- Hint (n : ℕ) (k : ℕ) : ¬odd (n + k) =>
|
||||
-- "Du kennst ein Lemma um mit `¬odd` umzugehen."
|
||||
|
||||
Hint (n : ℕ) : even (n + n) =>
|
||||
"`unfold even` hilft, anzuschauen, was hinter `even` steckt.
|
||||
|
||||
Danach musst du wieder mit `use r` ein `(r : ℕ)` angeben, dass du benützen möchtest."
|
||||
|
||||
-- Hint (n : ℕ) (k : ℕ) : even (n + k) =>
|
||||
-- "`unfold even` hilft hier weiter."
|
||||
|
||||
Message (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
|
||||
|
||||
Conclusion ""
|
||||
|
||||
Tactics push_neg intro use rw unfold ring
|
||||
|
||||
Lemmas even odd not_even not_odd not_exists not_forall
|
||||
Reference in New Issue
Block a user