|
|
|
|
@ -6,6 +6,8 @@ import Mathlib.Tactic.Ring
|
|
|
|
|
|
|
|
|
|
import Mathlib.Algebra.Parity
|
|
|
|
|
|
|
|
|
|
set_option tactic.hygienic false
|
|
|
|
|
|
|
|
|
|
Game "TestGame"
|
|
|
|
|
World "Predicate"
|
|
|
|
|
Level 6
|
|
|
|
|
@ -14,58 +16,58 @@ Title "Gerade/Ungerade"
|
|
|
|
|
|
|
|
|
|
Introduction
|
|
|
|
|
"
|
|
|
|
|
Gerade/ungerade werden in Lean wie folgt definiert:
|
|
|
|
|
Am nächsten Tag erklärt euch *Evenine*, dass es auf dem Mond zwei Gruppierungen gibt,
|
|
|
|
|
ihre und die ihres Halbbruders *Oddeus*. Die Mottos sind
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
def Even (n : ℕ) : Prop := ∃ r, n = r + r
|
|
|
|
|
def Odd (n : ℕ) : Prop := ∃ r, n = r + r + 1
|
|
|
|
|
```
|
|
|
|
|
Also dadurch, dass ein `(r : ℕ)` existiert sodass `n = r + 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
|
|
|
|
|
und
|
|
|
|
|
|
|
|
|
|
```
|
|
|
|
|
def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
|
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
Hint (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."
|
|
|
|
|
**Evenine**: Hier, ich zeige euch mal etwas was man bei uns machen kann:
|
|
|
|
|
"
|
|
|
|
|
|
|
|
|
|
Hint (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."
|
|
|
|
|
Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
|
|
|
|
|
Branch
|
|
|
|
|
unfold Even
|
|
|
|
|
Hint "Rob**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst was los ist."
|
|
|
|
|
Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
|
|
|
|
|
dass ein `r` existiert so dass `r + r = n`. Am besten
|
|
|
|
|
öffnest du diese Definition mit `unfold Even at *` einmal, dann siehst du besser, was los ist. "
|
|
|
|
|
unfold Even at *
|
|
|
|
|
Hint "**Du**: Also von `{h}` weiss ich jetzt dass ein `r` existiert, so dass `r + r = n`…
|
|
|
|
|
|
|
|
|
|
Hint (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."
|
|
|
|
|
**Robo**: Mit `rcases h with ⟨r, hr⟩` kannst du dieses `r` tatsächlich einführen."
|
|
|
|
|
rcases h with ⟨r, hr⟩
|
|
|
|
|
Hint "**Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = n^2`?
|
|
|
|
|
|
|
|
|
|
Hint (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."
|
|
|
|
|
**Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
|
|
|
|
|
Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
|
|
|
|
|
dir leider nicht sagen, welche Zahl passt.
|
|
|
|
|
"
|
|
|
|
|
Branch
|
|
|
|
|
rw [hr]
|
|
|
|
|
Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
|
|
|
|
|
use 2 * r ^ 2
|
|
|
|
|
ring
|
|
|
|
|
use 2 * r ^ 2
|
|
|
|
|
Hint "**Du**: Ah und jetzt `ring`!
|
|
|
|
|
|
|
|
|
|
Hint (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..."
|
|
|
|
|
**Robo**: Aber zuerst must du noch mit
|
|
|
|
|
`rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiss."
|
|
|
|
|
rw [hr]
|
|
|
|
|
ring
|
|
|
|
|
|
|
|
|
|
Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
|
|
|
|
|
"Die Taktik `ring` löst solche Gleichungen."
|
|
|
|
|
-- TODO: [Comment] For me the expected behaviour of `(strict := true)` would
|
|
|
|
|
-- be that it distinguishes between the defEq states while `(strict := false)`
|
|
|
|
|
-- would show the hint regardless of a `unfold Even`.
|
|
|
|
|
|
|
|
|
|
NewTactic unfold rcases use rw ring
|
|
|
|
|
NewTactic unfold use
|
|
|
|
|
NewDefinition Even Odd
|
|
|
|
|
|
|
|
|
|
Conclusion "**Evenine**: Seht ihr?"
|
|
|
|
|
|
Jon Eugster
2 years ago