first_levels

2022-11-29 17:11:17 +01:00
parent e43a2e2e9f
commit 5bf0cd9775
19 changed files with 186 additions and 167 deletions
@@ -12297,7 +12297,7 @@
    },
    "lean4web": {
      "version": "git+ssh://git@github.com/hhu-adam/lean4web.git#465694da60e2afbf7d188b41af173998ae75d915",
-      "from": "lean4web@git+https://github.com/hhu-adam/lean4web.git",
+      "from": "lean4web@github:hhu-adam/lean4web",
      "requires": {
        "@fontsource/roboto": "^4.5.8",
        "@fontsource/roboto-mono": "^4.5.8",
@@ -48,7 +48,7 @@ elab "Introduction" t:str : command => do
  | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}

 /-- Define the statement of the current level. -/
-elab "Statement" name:ident ? sig:declSig val:declVal : command => do
+elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
  let lvlIdx ← getCurLevelIdx
  let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String)
  elabCommand (← `(theorem $(mkIdent declName) $sig $val))
@@ -1,6 +1,7 @@
 import TestGame.Metadata
-import TestGame.Levels.Level1
-import TestGame.Levels.Level2
-import TestGame.Levels.Level3
-import TestGame.Levels.Level4
-import TestGame.Levels.Level5
+import TestGame.Levels.Logic.L01_Rfl
+import TestGame.Levels.Logic.L02_Rfl
+import TestGame.Levels.Logic.L03_Assumption
+import TestGame.Levels.Logic.L03b_Assumption
+import TestGame.Levels.Logic.L04_Rewrite
+import TestGame.Levels.Logic.L05_Apply
@@ -1,14 +1,14 @@
 import GameServer.Commands
-import TestGame.MyNat
+-- import TestGame.MyNat

-LemmaDoc zero_add as zero_add in "Addition"
-"This lemma says `∀ a : ℕ, 0 + a = a`."
+-- LemmaDoc zero_add as zero_add in "Addition"
+-- "This lemma says `∀ a : ℕ, 0 + a = a`."

-LemmaDoc add_zero as add_zero in "Addition"
-"This lemma says `∀ a : ℕ, a + 0 = a`."
+-- LemmaDoc add_zero as add_zero in "Addition"
+-- "This lemma says `∀ a : ℕ, a + 0 = a`."

-LemmaDoc add_succ as add_succ in "Addition"
-"This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."
+-- LemmaDoc add_succ as add_succ in "Addition"
+-- "This lemma says `∀ a b : ℕ, a + succ b = succ (a + b)`."

-LemmaSet addition : "Addition lemmas" := 
-zero_add add_zero
+-- LemmaSet addition : "Addition lemmas" :=
+-- zero_add add_zero
@@ -1,57 +0,0 @@
-import TestGame.Metadata
-
-Game "Introduction"
-World "Tactic"
-Level 3
-
-Title "Annahmen"
-
-Introduction
-"
-Um Aussagen zu formulieren braucht man Annahmen. Zum einen sind das Objekte, von denen
-eine Aussage handelt, wie zum Beispiel \"sei `n` eine natürliche Zahl\", oder
-\"seien `A`, `B` logische Aussagen\", zum anderen sind dass Annahmen wie \"angenommen
-dass `n` nicht Null ist\" oder \"angenommen `A` ist wahr\".
-
-In Lean schreibt man beides mit der gleichen Notation: `(n : ℕ)` ist eine natürliche Zahl,
-`(A B : Prop)` sind Aussagen, `(h : n ≠ 0)` ist eine Annahme, dass `n` nicht Null ist, und
-`(hA : A)` ist die Annahme, dass `A` wahr ist (`hA` ist ein Beweis von `A`).
-
-Die Annahmen kommen dann vor den Doppelpunkt.
-
-Wenn eine Annahme `h` genau dem Goal entspricht, kannst du `exact h` verwenden.
-"
-
-Statement theorem not_or (n : ℕ) (h : n = 0) : n = 0 := by
-  assumption
-
-- TODO: In Lean3 hatten wir ein Lemma-Text. Können wir den wieder haben?
-
-- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
-Statement (A : Prop) (hA : A) : A := by
-  assumption
-
-@[description "halli hallo"]
-Statement instance hallo : Hallo Nat where
-  mul_eq_add := by
-    $editor {
-    rfl
-    rw }
-  add_comm := by
-    rfl
-    apply
-
-Statement "halli hallo" instance hallo : Hallo Nat where
-  mul_eq_add := by
-    $editor {
-    rfl
-    rw }
-  add_comm := by
-    rfl
-    apply
-
-
-
-Conclusion ""
-
-Tactics assumption
@@ -1,59 +0,0 @@
-import TestGame.Metadata
-
-Game "Introduction"
-World "Tactic"
-Level 5
-
-Title "Implikation"
-
-Introduction
-"
-Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
-die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
-Aussage `A`.
-
-Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
-`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
-
-Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
-diese mit `apply h` anwenden.
-Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\".
-"
-
-Statement (A B : Prop) (hA : A) (g : A → B) : B := by
-  apply g
-  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."
-
-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."
-
-- TODO: Muss ich das wirklich mehrmals auflisten?
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = a =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = b =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : c = c =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : d = d =>
-"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."
-- TODO: Das macht es doch unmöglich mit den Messages...
-
-Tactics assumption
--Tactics rw
@@ -1,7 +1,7 @@
 import TestGame.Metadata

-Game "Introduction"
-World "Tactic"
+Game "TestGame"
+World "TestWorld"
 Level 1

 Title "Aller Anfang ist... ein Einzeiler?"
@@ -21,7 +21,7 @@ ersten offenen Goal zu machen.
 Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
 "

-Statement : 42 = 42 := by
+Statement "Zeige `42 = 42`." : 42 = 42 := by
  rfl

 Message : 42 = 42 =>
@@ -1,14 +1,14 @@
 import TestGame.Metadata

-Game "Introduction"
-World "Tactic"
+Game "TestGame"
+World "TestWorld"
 Level 2

 Title "Definitionally equal"

 Introduction
 "
-Achtung: `refl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
+Achtung: `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
 definiert sind, auch wenn diese unterschiedlich dargestellt werden.
 So sind `1 + 1` und `2` per Definition das Gleiche, da sie beide von Lean als `0.succ.succ`
 gelesen werden.
@@ -16,7 +16,7 @@ gelesen werden.
 Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab.
 "

-Statement : 1 + 1 = 2 := by
+Statement "Zeige dass eins plus eins zwei ist." : 1 + 1 = 2 := by
  rfl

 Conclusion
@@ -0,0 +1,29 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 3
+
+Title "Annahmen"
+
+Introduction
+"
+Mathematische Aussagen haben Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine
+natürliche Zahl\", oder auch wahre Aussagen über diese Objekte, wie zum Beispiel
+\"und angenommen, dass `n` strikt grösser als `1` ist\".
+
+In Lean schreibt man beides mit dem gleichen Syntax: `(n : ℕ) (h : 1 < n)` definiert
+zuerst `n` als natürliche Zahl und kreeirt eien Annahme, dass `1 < n`. Dieser Annahme geben wir
+den Namen `h`.
+
+Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
+"
+
+Statement triviale_angelegenheit
+    "Angenommen `1 < n`. dann ist `1 < n`."
+    (n : ℕ) (h : 1 < n) : 1 < n := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+import Mathlib.Data.Nat.Basic -- TODO
+
+Game "TestGame"
+World "TestWorld"
+Level 4
+
+Title "Logische Aussagen: `Prop`"
+
+Introduction
+"
+Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. Damit sagt man noch nicht,
+ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man an, dass
+`A` wahr ist: `hA` ist ein Beweis der Aussage `A`.
+"
+
+-- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
+Statement mehr_triviales
+    "
+    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
+    Zeige, dass `A` wahr ist.
+    "
+    (A : Prop) (hA : A) : A := by
+  assumption
+
+Conclusion ""
+
+Tactics assumption
@@ -1,23 +1,29 @@
 import TestGame.Metadata

-Game "Introduction"
-World "Tactic"
-Level 4
+Game "TestGame"
+World "TestWorld"
+Level 5

 Title "Rewrite"

 Introduction
 "
-Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern helfen einem
-nur, dorthin zu kommen.
+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, die sagt, dass `X` und `Y` gleich sind,
+Wenn man eine Annahme `(h : X = Y)` hat die sagt, dass `X` und `Y` gleich sind,
 kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
 das eine durch das andere zu ersetzen.
 "

-Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
-  rewrite [h₁]
+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

@@ -35,16 +41,7 @@ Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h
 `(h₂ : a = b)` rückwärts anwenden und `b` durch `a` ersetzen."

 -- TODO: Muss ich das wirklich mehrmals auflisten?
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = a =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = b =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : c = c =>
-"Der Hauptunterschied zwischen `rw` und `rewrite` ist, dass das erste automatisch versucht,
-anschliessend `rfl` anzuwenden. Bei `rewrite` musst du `rfl` explizit noch aufrufen."
-Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : d = d =>
+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."

@@ -53,4 +50,4 @@ anstatt dem Goal."
 -- TODO: Das macht es doch unmöglich mit den Messages...

 Tactics assumption
--Tactics rw
+Tactics rw
@@ -0,0 +1,33 @@
+import TestGame.Metadata
+
+Game "TestGame"
+World "TestWorld"
+Level 6
+
+Title "Implikation"
+
+Introduction
+"
+Wie wir schon gesehen haben, wir eine logische Aussage als `(A : Prop)` geschrieben, und
+die Annahme, dass `A` wahr ist als `(hA : A)`, also `hA` ist sozusagens ein Beweis der
+Aussage `A`.
+
+Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Zeichen dafür:
+`A ↔ B` (`\\iff`) bedeutet \"Genau dann wenn\" und `A → B` (`\\to`) bedeutet \"`A` impliziert `B`\".
+
+Wenn man Aussage `B` beweisen will und eine Implikationsannahme `(h : A → B)` hat, dann kann man
+diese mit `apply h` anwenden.
+Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn `A` impliziert `B`\".
+"
+
+Statement
+    "
+    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist.
+    "
+    (A B : Prop) (hA : A) (g : A → B) : B := by
+  apply g
+  assumption
+
+Tactics apply
+Tactics assumption
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "TestWorld"
+Level 1
+
+Title "Annahmen"
+
+Introduction "yadaa yadaa"
+
+class MyClass (n : ℕ) where
+
+Statement name
+"Beweise dieses Lemma."
+(n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := sorry
+  mul_assoc := sorry
+
+--@[exercise]
+instance instTest (n m : ℕ) : CommSemigroup ℕ where
+  mul := fun i j => 0
+  mul_comm := by
+    sorry
+  mul_assoc := by
+    sorry
+
+--@[exercise]
+lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+  rewrite [h₁]
+  rw [←h₂]
+  assumption
+
+
+Conclusion ""
+
+Tactics assumption
@@ -1,7 +1,8 @@
 import GameServer.Commands
-import TestGame.MyNat
+--import TestGame.MyNat
 import TestGame.TacticDocs
 import TestGame.LemmaDocs
+import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.

 Game "TestGame"

@@ -10,10 +11,10 @@ Title "The Natural Number Game"
 Introduction
 "This is a sad day for mathematics. While trying to find glorious new foundations for mathematics,
 someone removed the law of excluded middle and the axiom of choice. Unsurprisingly,
-everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage 
+everything collapsed. A brave rescue team managed to retrieve our precious axioms from the wreckage
 but now we need to rebuild all of mathematics from scratch.

-As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from 
+As a beginning mathematics wizard, you've been tasked to rebuild the theory of natural numbers from
 the axioms that Giuseppe Peano found under the collapsed tower of number theory. You've been equipped
 with a level 1 spell book. Good luck."

@@ -21,4 +22,4 @@ Conclusion
 "There is nothing else so far. Thanks for rescuing natural numbers!"

 Path w1 → w2 → w3
-Path w1 → v2 → w3
+Path w1 → v2 → w3
@@ -1,6 +1,6 @@
 axiom MyNat : Type

-notation "ℕ" => MyNat
+--notation "ℕ" => MyNat

 --axiom zero : ℕ

@@ -17,4 +17,3 @@ axiom add_zero : ∀ a : ℕ, a + 0 = a
 axiom add_succ : ∀ a b : ℕ, a + succ b = succ (a + b)

@[elab_as_elim] axiom myInduction {P : ℕ → Prop} (n : ℕ) (h₀ : P 0) (h : ∀ n, P n → P (succ n)) : P n
-
@@ -82,6 +82,12 @@ TODO
 "


+TacticDoc apply
+"
+## Beschreibung
+
+TODO
+"



@@ -1,5 +1,5 @@
 import Lean
-import TestGame.MyNat
+-- import TestGame.MyNat

 open Lean Elab Tactic

@@ -8,5 +8,5 @@ elab "swap" : tactic => do
  | g₁::g₂::t => setGoals (g₂::g₁::t)
  | _ => pure ()

-- macro "induction_on" n:ident : tactic => 
-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
+-- macro "induction_on" n:ident : tactic =>
+-- `(tactic| refine myInduction $n ?base ?inductive_step; swap; clear $n; intro $n $(mkIdent `ind_hyp); swap)
@@ -3,6 +3,9 @@ open Lake DSL

 require GameServer from ".."/"leanserver"

+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"@"b1cf06cb126ee163a7dc895c1aee17946ff20900"
+
 package TestGame

@[default_target]