more levels. lake-packages

2022-12-06 11:14:24 +01:00
parent 80e1c6f5e0
commit b61ffb4499
11 changed files with 166 additions and 85 deletions
@@ -1,5 +1,5 @@
 node_modules
 client/dist
 server/build
-**/lean_packages/
+**/lake-packages/

@@ -17,37 +17,34 @@ kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
 das eine durch das andere zu ersetzen.
 "

-Statement (A : Prop) (hA : A) : A := by
+Statement umschreiben
+    "
+    Angenommen man hat die Gleichheiten
+    `a = b`, `a = d`, `c = d`.
+    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

-- Statement umschreiben
--     "
--     Angenommen man hat die Gleichheiten
--     `a = b`, `a = d`, `c = d`.
--     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
+-- Gleich am Anfang anzeigen.
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
+"Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
+`c` im Goal mit `d` ersetzen."

-- -- Gleich am Anfang anzeigen.
-- Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-- "Wenn man eine Annahme `(h₁ : c = d)` hat, kann man mit `rw [h₁]` (oder `rewrite [h₁]`) das erste
-- `c` im Goal mit `d` ersetzen."
+Hint (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 schreibt diese mit
+`\\1`, `\\2`, `\\3`, …"

-- Hint (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 schreibt diese mit
-- `\\1`, `\\2`, `\\3`, …"
+Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
+"Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
+`(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."

-- Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-- "Mit `rw [← h₂]` (`\\l`, also klein L wie \"left\") kann man eine Hypotheses
-- `(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."
-
-- -- TODO: Muss ich das wirklich mehrmals auflisten?
-- Message (x : ℕ) : x = x =>
-- "Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-- anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
+-- TODO: Muss ich das wirklich mehrmals auflisten?
+Message (x : ℕ) : x = x =>
+"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
+anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."

 Conclusion "Übrigens, mit `rw [h₁] at h₂` kann man auch eine andere Annahme umschreiben
 anstatt dem Goal."
@@ -1,5 +1,8 @@
 import TestGame.Metadata

+import Init.Data.ToString
+#check List UInt8
+
 Game "TestGame"
 World "TestWorld"
 Level 9
@@ -2,7 +2,7 @@ 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"
@@ -0,0 +1,21 @@
+import TestGame.Metadata
+import Mathlib.Tactic.Ring
+
+Game "TestGame"
+World "Nat"
+Level 2
+
+Title "Natürliche Zahlen"
+
+Introduction
+"
+Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden.
+"
+
+Statement (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
+  rw [h]
+  ring
+
+Conclusion ""
+
+Tactics ring
@@ -0,0 +1,74 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+
+Game "TestGame"
+World "Nat"
+Level 3
+
+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`
+"
+
+-- 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
+
+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 = 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
@@ -1,57 +0,0 @@
-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
@@ -29,6 +29,7 @@ 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
@@ -0,0 +1,39 @@
+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 : ℕ), even x → even (x + 2) := by
+  intro x h
+  unfold even at *
+  rcases h with ⟨y, hy⟩
+  use y + 1
+  rw [hy]
+  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."
+
+Tactics unfold rcases use rw ring intro
@@ -6,6 +6,9 @@ require GameServer from ".."/"leanserver"
 require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"@"9b15aa6f091a623f992d6fff76167864794ce350"

+set_option tactic.hygienic false
+set_option autoImplicit false
+
 package TestGame

@[default_target]