Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer
unterstützt und verifiziert schreiben kann.
Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
In der *mittleren Spalte* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment
beweisen musst. Falls es mehrere Dinge zu beweisen gibt, werden alle weiteren darunter unter **Further Goals**
aufgelistet, diese musst du dann später auch noch zeigen.
Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
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 in der *rechten Spalte*.
Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
exklusiv in einem Dir fremden Dialekt, den sie Leanish [liːnɪʃ] nennen.
Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\".
Zum Glück hat Robo mit Dir das Universum gewechselt.
Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische Leuchte, die Du Dir in dieser Situation gewünscht hättest, aber es scheint, er hat irgendwo Leanish gelernt. Und das ist Gold wert.
Als erste kleine Vorschau, dass Lean auch vieles automatisch kann, gibt es eine
Taktik `tauto`, die alle wahren Aussagen der Prädikaten-Logik beweisen kann.
----
Dieses Beispiel würde von Hand etwas Zeit in Anspruch nehmen. Lean ist da viel schneller.
Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum Punkt:
Gib also `tauto` gefolgt von Enter ⏎ ein um deinen ersten automatisierten Beweis zu führen!
**Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
Und er kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung.
Dazwischen sollst Du offenbar einen Beweis eintragen.
Du siehst Robo hilflos an.
"
Statement
"Zeige dass folgende Aussage wahr ist:
$$
\\neg ((\\neg B\\textrm{ oder }\\neg C) \\textrm{ oder } (A \\Rightarrow B)) \\Rightarrow
(\\neg A \\textrm{ oder } B) \\textrm{ und } \\neg (B \\textrm{ und } C)
$$
"
(A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
tauto
Hint (A B C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
"Gib `tauto` ein und drücke Enter ⏎."
Conclusion ""
Hint
"**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint er: `A`, `B` und `C` sind irgendwelche Aussagen (*propositions*). Und mit `→` meint er ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
**Du** Ernsthaft?
**Robo** Ja. Schreib einfach `tauto`.
**Robo** Mach schon …
"
Conclusion
"
**Logisinde** (etwas konsterniert) Ja, das ist streng genommen richtig. Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt! Meine Untertanen verstehen `tauto` nicht. Da müsst Ihr Euch schon etwas mehr anstrengen.
@ -8,24 +8,27 @@ Title "Aller Anfang ist... ein Einzeiler?"
Introduction
"
Jetzt gehen wir aber einen Schritt zurück und lernen, wie man konkret mit Lean arbeitet,
damit du verstehst, was `tauto` hinter der Kulisse macht.
In der Zwischenzeit hat bereits sich eine lange Schlange Untertanen gebildet, die gern ihren Fragen stellen würden. Logisinde winkt den ersten nach vorn. Er räuspert sich.
Eine der grundlegendsten Taktiken ist `rfl` (für \"reflexivity\"), welche dazu da ist,
ein Goal der Form $X = X$ zu schließen.
**Untertan** Warum ist $42 = 42$?
Du schaust ihn fassungslos an.
Er schreibt es Dir wieder auf.
"
Statement
"Zeige$ 42 = 42 $." : 42 = 42 := by
42 = 42 := by
rfl
-- Hint : 42 = 42 =>
-- "Die Taktik `rfl` beweist ein Goal der Form `X = X`."
HiddenHint : 42 = 42 =>
"Die beiden Seiten dieser Gleichung sind identisch, also gib `rfl` ein und drücke Enter ⏎"
Hint
"
**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`.
"
Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."
Conclusion
"
**Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl …
Um spannendere Aussagen zu formulieren brauchen wir Objekte und Annahmen über diese
Objekte.
Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste nach vorne. Es ist schüchtern und schreibt bloß.
"
Hier zum Beispiel haben wir eine natürliche Zahl $n$ und eine Annahme $1 < n$, die
wir $h$ nennen.
Statement
(n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
assumption
Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen.
Hint
"
**Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl.
**Du** Warum schreibt er dann nicht `n ∈ ℕ`??
**Note:**
Wenn du den \"Editor mode\" umstellst, kannst du sehen, wie die Aufgabe in vollständigem
Lean-Code geschrieben wird. Hier sieht das wie folgt aus:
**Robo** Weil das hier alles komische Typen sind … Ich kann Dir das später mal in Ruhe erklären. Jetzt will ich erst einmal die Frage entschlüsseln.
```
example (n : ℕ) (h : 1 < n) : 1 < n := by
sorry
```
**Robo** Also, `h₁`, `h₂`, `h₃` sind einfach nur Namen für verschiedene Annahmen, und zwar für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
Also
**Du** Aber das war doch gerade eine der Annahmen.
```
example [Objekte/Annahmen] : [Aussage] := by
[Beweis]
```
"
**Robo** Ja, stimmt.
Statement
"Angenommen $1 < n$. Dann ist $1 < n$."
(n : ℕ) (h : 1 < n) : 1 < n := by
assumption
**Du** ???
HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
"`assumption` sucht nach einer Annahme, die dem Goal entspricht."
**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`.
"
Conclusion ""
Conclusion
"
**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf zerbrochen habe!
@ -10,11 +10,7 @@ Title "Widerspruch beweist alles."
Introduction
"
Die Aussage `False` ist für uns wichtiger als `True`, da ein Beweis der falschen Aussage
`False` einen Widerspruch repräsentiert.
Hat man einen Widerspruch, kann man daraus mit der Taktik `contradiction` alles beweisen.
Der erste Widerspruch, den `contradiction` erkennt, ist ein Beweis von `False`.
Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
"
Statement
@ -23,9 +19,28 @@ Zeige, dass daraus $A$ folgt."
(A : Prop) (h : False) : A := by
contradiction
HiddenHint (A : Prop) (h : False) : A =>
"Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen,
unabhängig davon, was das Goal ist."
Hint
"
**Du** Wenn ich das jetzt richtig lese, ist `A` eine Aussage, und wir haben außerdem eine Annahme names `h`, die besagt …
**Robo** … die besagt, dass `False` gilt.
**Du** Ich dachte, `False` gilt nie?
**Robo** Ja, genau. Die Annahme ist `False`, also falsch. Und aus einer falschen Annahme kann man bekanntlich alles beweisen! Insbesondere die gesuchte Aussage `A`.
**Du** Und wie erkläre ich das jetzt diesem Formalosophen?
**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`.
"
Conlusion
"Der erste Querulant ist offenbar zufrieden.
**Du** War das jetzt ein Widerspruchsbeweis?
**Robo** Nein, nein, ein Widerspruchsbeweis sieht anders aus. Das Argument hier war: wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
Drittens kann die Taktik `contradiction` auch einen Widerspruch finden,
wenn zwei Annahmen genaue Gegenteile voneinander sind.
Also z.B. `(h : A)` und `(g : ¬ A)`.
Da `≠` als `¬(· = ·)` gelesen wird, gilt dasselbe für Annahmen `(h : a = b)` und `(g : a ≠ b)`.
Auftritt dritter Querulant.
"
Statement
"Sei $n$ eine natürliche Zahl die sowohl gleich als auch ungleich `10` ist.
Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)"
(n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by
(n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by
contradiction
Hint
"
**Du** Wieder ein Widerspruch in den Annahmen?
"
Conclusion
"
**Robo** Gut gemacht. Bei dieser Frage ist auch ein bisschen offensichtlicher, worin der Widerspruch besteht: Die Annahme `n ≠ 10` ist genau die Negation von `n = 10`. Man muss `≠` immer als `¬(· = ·)` lesen.
Zusätzlich zur Verneinung (`¬`) können wir logische Aussagen auch mit UND (`∧`) und ODER (`∨`) kombinieren.
In einer Mathevorlesung würde man vielleicht `A ∧ B` als Tupel `⟨A, B⟩` definieren. In Lean
sind dies *Strukturen*. Eine Struktur hat mehrere Felder, in diesem Fall zwei,
nämlich die linke und die rechte Seite.
Will man eine Aussage `A ∧ B` beweisen (im Goal), dann kann man diese mit der Taktik
`constructor` in die einzelnen Felder aufteilen.
Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht. Er legt sie uns vor, setzt sich hin, und häkelt.
"
Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
constructor
assumption
assumption
HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B =>
"`constructor` zerlegt die Struktur in Einzelteile."
HiddenHint (A : Prop) (hA : A) : A =>
"Du hast einen Beweis dafür in den *Annahmen*."
NewTactics constructor
DisabledTactics tauto
-- Statement
-- "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
-- (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
-- constructor
-- intro h
-- rcases h with ⟨h₁, h₂⟩
-- constructor
-- assumption
-- apply h₂
-- assumption
-- intro h
-- rcases h with ⟨h₁, h₂⟩
-- constructor
-- assumption
-- intro
-- assumption
-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
-- "`↔` oder `∧` im Goal kann man mit `constructor` zerlegen."
-- Hint (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B =>
-- "Hier würdest du mit `intro` die Implikation angehen.
-- (Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf
-- das UND in der Implikationsannahme)"
-- -- if they don't use `intro ⟨_, _⟩`.
-- Hint (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B =>
-- "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen."
-- HiddenHint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
-- "Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?"
-- -- Rückrichtung
-- Hint (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) =>
-- "Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$
-- Da hilft `intro`.
-- (auch hier kann man wieder mit `intro ⟨ha, hb⟩` gleich noch die Premisse zerlegen.)"
-- -- if they don't use `intro ⟨_, _⟩`.
-- Hint (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) =>
-- "Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen."
-- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
-- "Wieder in Einzelteile zerlegen..."
Hint
"
**Du**: Also, wir haben zwei Annahmen: `A` gilt, und `B` gilt. Auch. Und beweisen sollen wir … `A und B` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung. Kann ich nicht wieder `trivial` sagen?
-- Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) =>
-- "Immer das gleiche ... noch mehr zerlegen."
**Robo** Nee, diesmal wird das nicht funktionieren. Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
-- -- Hint (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B =>
-- -- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen,
-- -- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`).
**Du** Du meinst, `destructor`??
-- -- Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht,
-- -- dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen,
-- -- dass `B` wahr ist."
**Robo** Nein, `constructor`. Ist verwirrend, ich weiß, aber so nennen die das hier.
"
HiddenHint (A : Prop) (hA : A) : A =>
"
**Robo** Schau mal, das ist Zauberpapier. Jetzt haben wir auf einmal zwei Beweisziele: `A` und `B`. Ich glaube, Du weißt schon, wie man die jeweils erreicht. Die Ziele stehen ja jeweils in den *Annahmen*.
"
Conclusion
"
**Robo** Super!
-- -- TODO
Ihm scheinen diese Fragen inzwischen Spaß zu machen.
**Robo** Meinst Du, dieser Hebel, an dem \"Editor mode\" steht, ist echt? Oder ist der nur gemalt? Probier mal!
Das logische ODER `A ∨ B` (`\\or`) funktioniert ein wenig anders als das UND.
Wenn das Goal ein `∨` ist kann man mit den Taktiken `left` oder `right` entscheiden,
welche Seite man beweisen möchte.
Der nächste bitte …
"
Statement
@ -24,11 +21,26 @@ Statement
left
assumption
HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) =>
"Entscheide dich, `right` oder `left`?"
Hint
"
**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
**Robo** Nein, viel einfacher. Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
**Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde? Ich will natürlich `A` beweisen!
**Robo** Mit `left` bzw.`right'. Ist doch logisch, oder?
"
Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
"Sackgasse. Probier's nochmals."
"
**Robo** Wusst gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
"
Conclusion
"
Auch dieser Formalosoph zieht zufrieden von dannen.
Wenn man hingegen ein ODER `(h : A ∨ B)` in den Annahmen hat, kann man dieses
ähnlich wie beim UND mit `rcases h` aufteilen.
**Wichtig:** der Syntax dafür ist `rcases h with h | h`. Das \"`h | h`\" bedeutet, dass
wir in beiden Fälle (linke oder rechte Seite wahr) diese Seite wieder `h` nennen wollen.
Der Unterschied ist, dass man beim UND eine Annahme in zwei Einzelteile zerlegt (mit `⟨h₁, h₂⟩`).
Beim ODER hingegen, kriegt man stattdessen zwei *Goals*, nämlich eines wo man annimmt,
die linke Seite sei wahr und eines wo man annimmt, rechts sei wahr.
*Notiz:* UND hat stärkere Bindung als ODER, und beide binden rechts, d.h.
`A ∨ B ∧ C` wird als `A ∨ (B ∧ C)` gelesen. Zudem binden beide nach rechts,
also `A ∨ B ∨ C` ist `A ∨ (B ∨ C)`.
Der nächste bitte …
"
Statement
@ -38,11 +26,78 @@ Statement
rcases h with ⟨h₁, h₂⟩
assumption
HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A =>
"Als erstes kannst du das ODER in den Annahmen mit `rcases h with h | h` zerlegen."
Hint
"
**Du** Ja klar, erst ein Und im Ziel, dann ein Und in der Annahme, dann ein Oder im Ziel, und jetzt noch ein Oder in der Annahme. Ich glaube den ganzen Circus hier langsam nicht mehr. Die haben sich doch abgesprochen!
**Robo** Lass ihnen doch ihren Spaß. Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten weiterfliegen.
**Du** Also, wieder `rcases …`?
**Robo** Ja, aber diesmal nicht `rcases h with ⟨h₁, h₂⟩`, sondern `rcases h with h | h`.
"
Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
"
**Robo** Jetzt musst Du Dein Ziel zweimal beweisen: Einmal unter der Annahme `A`, und einmal unter der Annahme `A ∨ B`.
"
HiddenHint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
"
**Robo** Wie man mit einem Und in den Annahmen umgeht, weißt Du doch schon: `rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`.
"
Conclusion
"**Du** Ok, das scheint ihn zufriedenzustellen. One to go … Kannst Du mir vorher noch einmal kurz alles Leanish zusammenfassen, das Du mir bis hierher beigebracht hast?
Robo straht überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` |
| Goal | `constructor` | `left`/`right` |
Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vorherigen.
"
-- Note: The other direction would need arguing by cases.
Statement
"Angenommen $A \\lor (B \\land C)$ ist wahr, zeige dass
$(A \\lor B) \\land (A \\lor C)$ wahr ist."
(A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
(A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
constructor
rcases h with h | h
left
@ -95,32 +33,49 @@ $(A \\lor B) \\land (A \\lor C)$ wahr ist."
right
assumption
Hint
"
**Robo** Wirf einfach alles drauf, was Du gelernt hast. Hier, ich bin sogar so nett und zeig Dir noch einmal die beiden vier wichtigsten Taktiken für diese Situation an.
Marcus Zibrowius
2 years ago