level update
This commit is contained in:
Jon Eugster
@@ -11,23 +11,30 @@ 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* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment am Beweisen
|
||||
bist. Falls es mehrere Subgoals gibt, werden alle weiteren darunter unter **Further Goals**
|
||||
aufgelistet, diese musst du dann später auch noch zeigen.
|
||||
|
||||
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\".
|
||||
Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie
|
||||
man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen,
|
||||
andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken *Links* an der
|
||||
Seite.
|
||||
|
||||
Wenn der Beweis komplett ist, erscheint \"Level Completed! 🎉\".
|
||||
|
||||
Deine erste Taktik ist `rfl`, welche dazu da ist, ein Goal der Form `X = X` zu schliessen.
|
||||
Gib die Taktik ein gefolgt von Enter ⏎.
|
||||
"
|
||||
|
||||
Statement "Zeige $ 42 = 42 $." : 42 = 42 := by
|
||||
rfl
|
||||
|
||||
Message : 42 = 42 =>
|
||||
"Die erste Taktik ist `rfl`, die ein Goal von der Form `A = A` beweist."
|
||||
"Die Taktik `rfl` beweist ein Goal der Form `X = X`."
|
||||
|
||||
Hint : 42 = 42 =>
|
||||
"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein gefolgt von ENTER."
|
||||
"Man schreibt eine Taktik pro Zeile, also gib 'rfl' ein und geh mit Enter ⏎ auf eine neue Zeile."
|
||||
|
||||
Conclusion "Bravo!"
|
||||
|
||||
Tactics rfl
|
||||
|
||||
@@ -8,22 +8,20 @@ Title "Definitionally equal"
|
||||
|
||||
Introduction
|
||||
"
|
||||
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.
|
||||
**Vorsicht:** `rfl` kann auch Gleichungen beweisen, wenn die beiden Terme Lean-intern gleich
|
||||
definiert sind, auch wenn diese unterschiedlich dargestellt werden. Das kann anfänglich
|
||||
zu Verwirrung führen.
|
||||
|
||||
Das kann anfänglich verwirrend sein und das Verhalten hängt von der Lean-Implementation ab.
|
||||
So sind `2` definiert als `1 + 1`, deshalb funktioniert `rfl` auch hier.
|
||||
"
|
||||
|
||||
Statement "Zeige dass eins plus eins zwei ist." : 1 + 1 = 2 := by
|
||||
Statement "Zeige dass $1 + 1$ zwei ist." : 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.
|
||||
**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl`
|
||||
aufzurufen, deshalb brauchst du das nur noch selten.
|
||||
"
|
||||
|
||||
Tactics rfl
|
||||
Lemmas zero_add
|
||||
|
||||
@@ -8,13 +8,14 @@ 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
|
||||
Um Aussagen zu formulieren brauchen wir Annahmen. Das sind zum einen Objekte, wie \"sei `n` eine
|
||||
natürliche Zahl\", und Annahmen über diese Objekte, von denen wir wissen, dass sie wahr sind.
|
||||
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`.
|
||||
zuerst eine natürliche Zahl `n` und eine Annahme dass `1 < n` (die Annahme kriegt
|
||||
den Namen `h`).
|
||||
|
||||
Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
|
||||
"
|
||||
@@ -24,6 +25,9 @@ Statement triviale_angelegenheit
|
||||
(n : ℕ) (h : 1 < n) : 1 < n := by
|
||||
assumption
|
||||
|
||||
Message (n : ℕ) (h : 1 < n) : 1 < n =>
|
||||
"`assumption` sucht nach einer Annahme, die dem Goal entspricht."
|
||||
|
||||
Conclusion ""
|
||||
|
||||
Tactics assumption
|
||||
|
||||
@@ -9,18 +9,22 @@ 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`.
|
||||
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 sozusagen ein Beweis von `A`.
|
||||
"
|
||||
|
||||
-- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben?
|
||||
Statement mehr_triviales
|
||||
"Sei $ A $ eine logische Aussage und sei `hA` ein Beweis für $A$.
|
||||
Zeige, dass $ A $ wahr ist."
|
||||
(A : Prop) (hA : A) : A := by
|
||||
assumption
|
||||
|
||||
Hint (A : Prop) (hA : A) : A =>
|
||||
"Auch hier kann `assumption` den Beweis von `A` finden."
|
||||
|
||||
Conclusion ""
|
||||
|
||||
Tactics assumption
|
||||
|
||||
@@ -12,39 +12,41 @@ Introduction
|
||||
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,
|
||||
kann man die Taktik `rw` (steht für 'rewrite') brauchen um im Goal
|
||||
das eine durch das andere zu ersetzen.
|
||||
Wenn man eine Annahme `(h : X = Y)` hat,
|
||||
kann die Taktik `rw [h]` im Goal `X` durch `Y` ersetzen.
|
||||
(`rw` steht für *rewrite*)
|
||||
|
||||
"
|
||||
|
||||
Statement umschreiben
|
||||
"
|
||||
Angenommen man hat die Gleichheiten
|
||||
`a = b`, `a = d`, `c = d`.
|
||||
Zeige dass `b = c`.
|
||||
"
|
||||
"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."
|
||||
|
||||
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
|
||||
"Die kleinen Zahlen `h₁ h₂ h₃` werden in Lean oft verwendet und man tippt 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."
|
||||
Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
|
||||
"Im Goal kommt `c` vor und `h₁` sagt `c = d`.
|
||||
Probiers doch mit `rw [h₁]`."
|
||||
|
||||
-- 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."
|
||||
Message (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
|
||||
" Man kann auch rückwärts umschreiben: `h₂` sagt `a = b` mit
|
||||
`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
|
||||
|
||||
Hint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
|
||||
"Schau mal durch die Annahmen durch."
|
||||
|
||||
|
||||
-- -- 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."
|
||||
|
||||
@@ -8,7 +8,9 @@ Level 6
|
||||
Title "Implikation"
|
||||
|
||||
Introduction
|
||||
"
|
||||
"Als nächstes widmen wir uns der Implikation &A \\Rightarrow B&. TODO
|
||||
|
||||
Logische Aussagen `(A : Prop)`, `(B : Prop)`
|
||||
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`.
|
||||
@@ -18,8 +20,7 @@ Logische Aussagen können einander implizieren. Wir kennen hauptsächlich zwei Z
|
||||
|
||||
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`\".
|
||||
"
|
||||
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`.
|
||||
@@ -32,5 +33,4 @@ Message (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
|
||||
"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch `A` zeigen,
|
||||
dafür hast du bereits einen Beweis in den Annahmen."
|
||||
|
||||
Tactics apply
|
||||
Tactics assumption
|
||||
Tactics apply assumption
|
||||
|
||||
Reference in New Issue
Block a user