wip

2022-11-28 17:48:45 +01:00
parent 5cb0ff4ccf
commit e43a2e2e9f
9 changed files with 334 additions and 86 deletions
@@ -48,11 +48,12 @@ 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" sig:declSig val:declVal : command => do
+elab "Statement" name:ident ? 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))
  modifyCurLevel fun level => pure {level with goal := sig}
+-- TODO: Do something with the lemma name.

 /-- Define the conclusion of the current game or current level if some
 building a level. -/
@@ -131,6 +132,10 @@ local elab "Message'" decls:mydecl* ":" goal:term "=>" msg:str : command => do
 macro "Message" decls:mydecl* ":" goal:term "=>" msg:str : command => do
  `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg)

+/-- Declare a hint in reaction to a given tactic state in the current level. -/
+macro "Hint" decls:mydecl* ":" goal:term "=>" msg:str : command => do
+  `(set_option linter.unusedVariables false in Message' $decls* : $goal => $msg)
+  -- TODO: implement me?

 /-! ## Tactics -/

@@ -0,0 +1,10 @@
+{
+  "editor.insertSpaces": true,
+  "editor.tabSize": 2,
+  "editor.rulers" : [100],
+  "files.encoding": "utf8",
+  "files.eol": "\n",
+  "files.insertFinalNewline": true,
+  "files.trimFinalNewlines": true,
+  "files.trimTrailingWhitespace": true
+}
@@ -0,0 +1,35 @@
+import TestGame.Metadata
+
+Game "Introduction"
+World "Tactic"
+Level 1
+
+Title "Aller Anfang ist... ein Einzeiler?"
+
+Introduction
+"
+Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
+unterstützt und verifiziert schreiben kann.
+
+Ein Beweis besteht in Lean aus verschiedenen **Taktiken**, welche ungefähr einem
+logischen Schritt entsprechen, den man auf Papier aufschreiben würde.
+
+Rechts im **Infoview** siehst den Status des aktuellen Beweis.
+Du siehst ein oder mehrere offene **Goals** (mit einem `⊢` davor), die du noch zeigen musst.
+Wenn du eine Taktik hinschreibst, dann versucht Lean diesen Schritt beim
+ersten offenen Goal zu machen.
+Wenn der Beweis komplett ist, erscheint \"goals accomplished\".
+"
+
+Statement : 42 = 42 := by
+  rfl
+
+Message : 42 = 42 =>
+"Die erste Taktik ist `rfl`, die ein Goal von der Form `A = A` beweist."
+
+Hint : 42 = 42 =>
+"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein gefolgt von ENTER."
+
+Conclusion "Bravo!"
+
+Tactics rfl
@@ -0,0 +1,28 @@
+import TestGame.Metadata
+
+Game "Introduction"
+World "Tactic"
+Level 2
+
+Title "Definitionally equal"
+
+Introduction
+"
+Achtung: `refl` 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.
+
+Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab.
+"
+
+Statement : 1 + 1 = 2 := by
+  rfl
+
+Conclusion
+"
+Im weiteren führen die meisten anderen Taktiken `refl` automatisch am Ende aus,
+deshalb musst du dieses häufig gar nicht mehr schreiben.
+"
+
+Tactics rfl
@@ -0,0 +1,57 @@
+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
@@ -0,0 +1,56 @@
+import TestGame.Metadata
+
+Game "Introduction"
+World "Tactic"
+Level 4
+
+Title "Rewrite"
+
+Introduction
+"
+Oft sind aber die Annahmen nicht genau das, was man zeigen will, sondern helfen einem
+nur, dorthin zu kommen.
+
+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₁]
+  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."
+
+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
@@ -0,0 +1,59 @@
+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
@@ -4,29 +4,100 @@ import TestGame.Tactics

 TacticDoc rfl
 "
-## Summary
+## Beschreibung

-`rfl` proves goals of the form `X = X`.
+`rfl` beweist ein Goal der Form `X = X`.

-## Details
+## Detail

-The `rfl` tactic will close any goal of the form `A = B`
-where `A` and `B` are *exactly the same thing*.
+`rfl` beweist jedes Goal `A = B` wenn `A` und `B` genau das gleiche sind.
+Wichtig ist nicht, ob diese im Infoview gleich aussehen, sondern ob sie in
+Lean gleich definiert sind.

-### Example:
-If it looks like this in the top right hand box:
+## Beispiel
+`rfl` kann folgenes Goal beweisen:
+```
+Objects
+  a b c : ℕ
+Prove:
+  (a + b) * c = (a + b) * c
+```
+
+`rfl` kann auch folgendes beweisen:
+```
+Objects
+  n : ℕ
+Prove:
+  1 + 1 = 2
+```
+denn Lean liest dies intern als `0.succ.succ = 0.succ.succ`.
+"
+
+TacticDoc assumption
+"
+## Beschreibung
+
+`assumption` sucht nach einer Annahme, die genau dem Goal entspricht.
+
+## Beispiel
+Wenn das Goal wie folgt aussieht:
 ```
 Objects
  a b c d : ℕ
+  h : a + b = c
+  g : a * b = 16
+  t : c = 12
 Prove:
-  (a + b) * (c + d) = (a + b) * (c + d)
+  a + b = c
 ```

-then
+dann findet `assumption` die Annahme `h`und schliesst den Beweis.
+"
+
+TacticDoc rewrite
+"
+## Beschreibung
+
+Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+"
+
+TacticDoc rw
+"
+## Beschreibung
+
+Wenn man eine Annahme `(h : X = Y)` hat, kann man mit
+`rw [h]` alle `X` im Goal durch `Y` ersetzen.
+
+## Detail
+- `rw [←h]` wendet `h` rückwärts an und ersetzt alle `Y` durch `X`.
+- `rw [h, g, ←f]`: Man kann auch mehrere `rw` zusammenfassen.
+- `rw [h] at h₂` ersetzt alle `X` in `h₂` zu `Y` (anstatt im Goal).
+
+`rw` funktioniert gleichermassen mit Annahmen `(h : X = Y)` also auch
+mit Theoremen/Lemmas der Form `X = Y`
+
+## Beispiel
+
+TODO
+"
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

-`rfl`

-will close the goal and solve the level."

 TacticDoc induction_on
 "
@@ -67,82 +138,9 @@ Prove:
 ```
 "

-TacticDoc rewrite
-"
-## Summary

-If `h` is a proof of `X = Y`, then `rewrite [h],` will change
-all `X`s in the goal to `Y`s. Variants: `rewrite [<- h]` (changes
-`Y` to `X`) and
-`rewrite [h] at h2` (changes `X` to `Y` in hypothesis `h2` instead
-of the goal).
-
-## Details
-
-The `rewrite` tactic is a way to do \"substituting in\". There
-are two distinct situations where use this tactics.
-
-1) If `h : A = B` is a hypothesis (i.e., a proof of `A = B`)
-in your local context (the box in the top right)
-and if your goal contains one or more `A`s, then `rewrite h`
-will change them all to `B`'s. 
-
-2) The `rewrite` tactic will also work with proofs of theorems
-which are equalities (look for them in the inventory).
-For example, if your inventory contains `add_zero x : x + 0 = x`, 
-then `rewrite [add_zero]` will change `x + 0` into `x` in your goal 
-(or fail with an error if Lean cannot find `x + 0` in the goal).
-
-Important note: if `h` is not a proof of the form `A = B`
-or `A ↔ B` (for example if `h` is a function, an implication,
-or perhaps even a proposition itself rather than its proof),
-then `rewrite` is not the tactic you want to use. For example,
-`rewrite [P = Q]` is never correct: `P = Q` is the true-false
-statement itself, not the proof.
-If `h : P = Q` is its proof, then `rewrite [h]` will work.
-
-Pro tip 1: If `h : A = B` and you want to change
-`B`s to `A`s instead, try `rewrite [<- h]` (get the arrow with `\\l` and
-note that this is a small letter L, not a number 1).
-
-### Example:
-If it looks like this in the top right hand box:
-```
-Objects
-  x y : ℕ
-Assumptions  
-  h : x = y + y
-Prove:
-  succ (x + 0) = succ (y + y)
-```
-
-then
-
-`rewrite [add_zero]`
-
-will change the goal into `succ x = succ (y + y)`, and then
-
-`rewrite [h]`
-
-will change the goal into `succ (y + y) = succ (y + y)`, which
-can be solved with `rfl,`.
-
-### Example: 
-You can use `rewrite` to change a hypothesis as well. 
-For example, if your local context looks like this:
-```
-Objects
-  x y : ℕ
-Assumptions
-  h1 : x = y + 3
-  h2 : 2 * y = x
-Prove:
-  y = 3
-```
-then `rewrite [h1] at h2` will turn `h2` into `h2 : 2 * y = y + 3`.
-"

 TacticDoc intro
 "Useful to introduce stuff"

-TacticSet basics := rfl induction_on intro rewrite
+TacticSet basics := rfl induction_on intro rewrite