phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

bump mathlib and use Even/Odd.

Browse Source
This commit is contained in:
Jon Eugster
2023-01-20 11:42:01 +01:00
parent 6e0469d3bf
commit d2be90a8a0
12 changed files with 84 additions and 102 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/testgame/TestGame.lean
+3
View File
@@ -4,6 +4,7 @@ import TestGame.Levels.Proposition
import TestGame.Levels.Implication
import TestGame.Levels.Predicate
import TestGame.Levels.Proving
import TestGame.Levels.Prime
import TestGame.Levels.Naturals.L31_Sum
@@ -63,4 +64,6 @@ Conclusion
Path Proposition → Implication → Predicate → Proving
Path Predicate → Prime
Path Predicate → Nat2
server/testgame/TestGame/LemmaDocs.lean
+3 -10
View File
@@ -37,13 +37,6 @@ LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic"
`(A B : Prop)`
"
LemmaDoc zero_add as zero_add in "Addition"
"This lemma says `∀ a : ℕ, 0 + a = a`."
@@ -62,13 +55,13 @@ LemmaDoc not_forall as not_forall in "Logic"
LemmaDoc not_exists as not_exists in "Logic"
"`∀ (A : Prop), ¬(∃ x, A) ↔ ∀x, (¬A)`."
LemmaDoc even as even in "Nat"
LemmaDoc Even as Even in "Nat"
"
`even n` ist definiert als `∃ r, a = 2 * r`.
Die Definition kann man mit `unfold even at *` einsetzen.
"
LemmaDoc odd as odd in "Nat"
LemmaDoc Odd as Odd in "Nat"
"
`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
Die Definition kann man mit `unfold odd at *` einsetzen.
@@ -85,7 +78,7 @@ LemmaDoc even_square as even_square in "Nat"
LemmaSet natural : "Natürliche Zahlen" :=
even odd not_odd not_even
Even Odd not_odd not_even
LemmaSet logic : "Logik" :=
not_not not_forall not_exists
server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
+10 -10
View File
@@ -4,7 +4,7 @@ import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.Use
import Mathlib.Tactic.Ring
import TestGame.ToBePorted
import Mathlib.Algebra.Parity
Game "TestGame"
World "Predicate"
@@ -16,17 +16,17 @@ 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
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 = 2 * 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.
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)`.
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
@@ -35,14 +35,14 @@ Hierzu gibt es 3 wichtige Taktiken:
Statement even_square
"Wenn $n$ gerade ist, dann ist $n^2$ gerade."
(n : ℕ) (h : even n) : even (n ^ 2) := by
unfold even at *
(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) =>
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
@@ -68,4 +68,4 @@ Message (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^
"Die Taktik `ring` löst solche Gleichungen."
Tactics unfold rcases use rw ring
Lemmas even odd
Lemmas Even Odd
server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
+6 -5
View File
@@ -4,7 +4,8 @@ import Mathlib.Tactic.Contrapose
import Mathlib.Tactic.Use
import Mathlib.Tactic.Ring
import TestGame.ToBePorted
import Mathlib.Algebra.Parity
import Mathlib
Game "TestGame"
World "Predicate"
@@ -33,16 +34,16 @@ TODO: 1-2 Aufgaben mehr.
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
ungerade." : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
intro x h
unfold even at h
unfold odd
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) =>
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 : ℕ) → `"
server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
+9 -8
View File
@@ -2,6 +2,8 @@ import TestGame.Metadata
import Mathlib.Tactic.PushNeg
import Mathlib
import Mathlib.Algebra.Parity
import TestGame.ToBePorted
Game "TestGame"
@@ -25,31 +27,30 @@ Das braucht intern die Lemmas
Statement
"Es existiert keine natürliche Zahl $n$, sodass $n + k$ immer ungerade ist.":
¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
push_neg
intro n
use n
rw [not_odd]
unfold even
unfold Even
use n
ring
Message : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) =>
Message : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) =>
"`push_neg` schiebt die Negierung an den Quantoren vorbei."
Message (n : ℕ) : (∃ k, ¬odd (n + k)) =>
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) =>
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) =>
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."
@@ -63,4 +64,4 @@ Conclusion ""
Tactics push_neg intro use rw unfold ring
Lemmas even odd not_even not_odd not_exists not_forall
Lemmas Even Odd not_even not_odd not_exists not_forall
server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
+1 -1
View File
@@ -57,4 +57,4 @@ Conclusion ""
Tactics push_neg intro use rw unfold ring
Lemmas even odd not_even not_odd not_exists not_forall
Lemmas Even Odd not_even not_odd not_exists not_forall
server/testgame/TestGame/Levels/Prime/L01_Prime.lean
+17 -29
View File
@@ -1,4 +1,6 @@
import TestGame.Metadata
import Mathlib.Data.Nat.Prime
import Std.Tactic.RCases
import Mathlib.Tactic.LeftRight
import Mathlib.Tactic.Contrapose
@@ -8,44 +10,30 @@ import Mathlib.Tactic.Ring
import TestGame.ToBePorted
Game "TestGame"
World "Proving"
World "Prime"
Level 1
Title "Ad absurdum"
Title "Primzahlen"
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."
"TODO"
(n : ℕ) : ∃! (n : ℕ), Nat.Prime n ∧ Even n := by
use (2 : ℕ)
constructor
simp only [true_and]
use 1
intro y
rintro ⟨h₁, h₂⟩
rw [← Nat.Prime.even_iff]
assumption
assumption
Conclusion ""
Tactics contradiction rw
Tactics
Lemmas even odd not_even not_odd
Lemmas
server/testgame/TestGame/Levels/Proving/L01_Contra.lean
+3 -3
View File
@@ -36,11 +36,11 @@ 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
(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 =>
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."
@@ -48,4 +48,4 @@ Conclusion ""
Tactics contradiction rw
Lemmas even odd not_even not_odd
Lemmas Even Odd not_even not_odd
server/testgame/TestGame/Levels/Proving/L06_ByContra.lean
+20 -20
View File
@@ -22,22 +22,22 @@ 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:
`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
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))`
2) Einen Beweis des Zwischenresultats `suffices h₁ : ¬(Odd (n ^ 2))`
Alternativ macht `have h₁ : ¬(odd (n ^ 2))` genau das gleiche, vertauscht aber die
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
(n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
by_contra g
suffices d : ¬ odd (n ^ 2) -- TODO: I don't like this
suffices d : ¬ Odd (n ^ 2) -- TODO: I don't like this
contradiction
rw [not_odd] at g
@@ -45,37 +45,37 @@ Statement
apply even_square
assumption
Message (n : ℕ) (h : odd (n^2)) : odd n =>
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,
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)`.
Benütze dafür `suffices h₂ : ¬Odd (n ^ 2)`.
"
Message (n : ℕ) (g : ¬ odd (n^2)) (h : odd (n^2)) : False =>
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 =>
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."
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."
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) =>
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) =>
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
Lemmas Odd Even not_odd not_even even_square
server/testgame/TestGame/Levels/Proving/L07_Contrapose.lean
+7 -7
View File
@@ -23,28 +23,28 @@ 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
(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 =>
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 =>
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`
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,
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."
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
Lemmas Even Odd not_even not_odd even_square
server/testgame/TestGame/ToBePorted.lean
+4 -8
View File
@@ -1,16 +1,12 @@
import Mathlib
-- TODO: `even`/`odd` sind in Algebra.Parity. Not ported yet
def even (a : ℕ) : Prop := ∃ r, a = 2 * r
def odd (a : ℕ) : Prop := ∃ k, a = 2 * k + 1
lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by sorry
lemma not_odd {n : ℕ} : ¬ odd n ↔ even n := by sorry
lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by sorry
lemma not_even {n : ℕ} : ¬ even n ↔ odd n := by sorry
lemma even_square (n : ℕ) : even n → even (n ^ 2) := by
lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
intro ⟨x, hx⟩
unfold even at *
unfold Even at *
use 2 * x ^ 2
rw [hx]
ring
server/testgame/lake-manifest.json
+1 -1
View File
@@ -28,7 +28,7 @@
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "1771130ddfb56ca04da3296cf3693a9e58eb00c6",
"rev": "8176e5d663db861cccf6fed6db2f9e5669fe6c5b",
"name": "mathlib",
"inputRev?": "master"}},
{"git":