Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
eine Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
gebeten.
**Robo**: Ich glaube, das ist Spinoza, einer der ganz wenigen Asteroiden vom Type QED. Schnell. Wir müssen uns ein bisschen beeilen, sonst verpassen wir ihn.
Eine halbe Stunde später seid ihr gelandet. Sehr einladend wirkt Spinoza nicht. Seine gesamte Oberfläche ist von feinem, rötlichen Sand bedeckt.
Ein einziger, einsamer Formalosoph, der sich als Benedictus vorstellt, erwartet euch.
**Benedictus**: Schön, dass Ihr gekommen seid! Ich habe schon auf Euch gewartet!
**Du**: Hast Du auch ein paar dringende Fragen … ?
**Benedictus**: Ach nein, aus dem Alter bin ich heraus. Aber ich kann mir denken, wie es Euch auf Implis und Quantus ergangen ist. Und glaubt, mir auf den anderen Planeten wird es nicht viel besser. Aber ich kann Euch vielleicht ein bisschen vorbereiten.
**Du**: Können wir nicht einfach hier bleiben und uns ein wenig ausruhen?
Benedictus schüttelt den Kopf.
**Benedictus**: Nein. Spinoza verträgt keine drei Bewohner. Und Ihr müsst bald wieder weiter, sonst wird der Weg zu weit. Wir kommen nur alle 400 Jahre bei den Planeten vorbei.
**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
**Benedictus**: Ihr hättet natürlich auch erst das Hauptresultat und dann das Zwischenresultat beweisen können. Das könnt Ihr ja mal an dieser Aufgabe probieren, die ist ganz ähnlich.
"
-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
@ -35,29 +33,27 @@ Introduction
-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
-- `suffices` schöner gewesen:
-- "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
-- $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
Statement
"Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
$A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
(A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
brauchen. Das funktioniert genau gleich, aussert dass dann die beiden Goals vertauscht sind.
Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst Du auch `suffices`
verwenden. Das funktioniert genau gleich, außer, dass dann die beiden Beweisziele vertauscht sind.
**Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
abschliesst bevor ich `g` beweise?
abschliesst, bevor ich `g` beweise?
**Robo**: Genau! Verwendende `have` und `suffices` einfach nach gutdünken."
**Robo**: Genau!"
suffices g : ¬ B
Hint "**Robo**: Also hier beendest du den Beweis angenommen {g} sei wahr."
Hint "**Robo**: Also hier beendest Du den Beweis unter der Annahme `{g}` sei wahr."
contradiction
Hint "**Robo**: Und hier beweist du das Zwischenresultat."
Hint "**Robo**: Und hier beweist Du das Zwischenresultat."
apply h
assumption
NewTactic «suffices»
DisabledTactic «have»
Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
**Oddeus**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
Conclusion "**Benedictus**: Genau so meinte ich das. Ob Ihr nun in Zukunft `have` und `suffices` verwendet, ist reine Geschmacksfrage. Hauptsache, Ihr wisst, wie Ihr entfernte Ziele in kleinen Schritte erreicht.
*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
**Oddeus**: Ich hab's gleich. Hier ist eine Notiz meiner Gelehrter, die mir
mit solchen kryptischen Nachrichten helfen wollten.
Auf dem Pergament steht das ein Lemma mit dem Namen `not_imp_not`:
**Benedictus**: Ich habe noch eine schöne Frage zu ungeraden Quadraten für Euch. Aber vorher beweist Ihr besser noch diese Äquivalenz hier. Ich gaube, die hat sogar bei Euch einen Namen: *Kontrapositionsäquivalenz*, oder so etwas. Auf Leansch nennen wir die Äuqivalenz einfach `not_imp_not`. Ist doch viel einleuchtender, oder?
"
Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
Hint "**Du**: Ich glaube, dafür kenn ich das meiste schon."
Hint "**Du**: Ja, das habe ich tatsächlich schon einmal gesehen.
**Robo**: Ja, klar hast Du das schon einmal gesehen. Das benutzen Mathematiker doch ständig. Wenn ihnen zu $A ⇒ B$ nichts einfällt, zeigen sie stattdessen $¬B ⇒ ¬A$. Ich würde das ja statt *Kontraposition* oder `not_imp_not` eher *von_hinten_durch_die_Brust_ins_Auge* nennen. Aber gut, ich will mich nicht einmisschen.
"
Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
constructor
intro h b
by_contra a
Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
herbeiführen."
Hint "**Robo**: Ich würde wieder mit `suffices g : B` einen Widerspruch herbeiführen."
suffices b : B
contradiction
apply h
assumption
intro h a
Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruch anfangen."
Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruchsbeweis anfangen."
by_contra b
Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
suffices g : ¬ A
@ -48,4 +45,4 @@ Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
DisabledTactic rw
DisabledLemma not_not
Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"
**Oddeus**: Das ist doch klar eine Aggression uns gegenüber!
**Robo**: Wartet mal, vielleicht wollte euch eure Schwester einfach von ihren neuen
Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
**Benedictus**: Gut, hier ist die angekündigte Frage. Versucht mal einen *direkten* Beweis, ohne `contrapose`.
"
-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
@ -45,26 +38,24 @@ Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
Hint "**Oddeus**: Wie soll das den gehen?
Hint "**Robo**: Ich schlage vor, wir führen das auf das Lemma `even_square` zurück, das wir auf Quantus schon gezeigt hatten. Hier steht ja im Grunde `Odd (n^2) → Odd n`. Und unter Kontraposition ist das äquivalent zu `Even n → Even (n^2)`.
**Robo**: `contrapose` benutzt das Lemma eurer Gelehrter, `not_imp_not`. Also es wandelt
ein Goal `A → B` zu `¬B → ¬A ` um.
**Du**: Richtig. Von hinten durch die Brust … Aber warte, im Moment steht da doch gar kein `→`.
**Du**: Aber das Goal ist doch gar keine Implikation?
**Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
schieben."
**Robo**: Erinner Dich an `revert`. Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Beweissziel schieben."
revert h
Hint "*Oddeus*: Ob man jetzt wohl dieses `contrapose` benutzen kann?"
Hint "**Du**: Und jetzt kann ich dieses Kontrapositionslemma anwenden? Wie hieß das noch einmal?
**Robo**: Tatsächlich kannst auch einfach `contrapose` schreiben.
"
contrapose
Hint (hidden := true) "**Du**: Warte mal, jetzt kann man wohl `even_iff_not_odd` verwenden…"
Hint (hidden := true) "**Robo**: Vielleicht hilft jetzt `even_iff_not_odd` weiter?"
rw [← even_iff_not_odd]
rw [← even_iff_not_odd]
Hint "**Robo**: Und den Rest hast du bei *Evenine* als Lemma gezeigt!"
Hint "**Du**: Das sieht schon ganz gut aus. Jetzt kann ich tatsächlich das alte Lemma anwenden!"
apply even_square
NewTactic contrapose
DisabledTactic by_contra
Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
Ich danke euch, darauf wäre ich nie gekommen."
Conclusion "**Benedictus**: Hervorragend! Ich glaube, damit seid Ihr jetzt ganz gut gewappnet."
**Du**: Sag mal Robo, das hätte ich aber auch als Widerspruch anstatt Kontraposition
beweisen können?
**Du**: Aber hätten wir die letzte Aufgabe nicht genauso gut per Widerspruch beweisen können?
**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
Probiers doch einfach!
In diesem Kapitel hast du also folgende Taktiken kennengelernt:
**Benedictus**: Klar. Ich dachte nur, ein zweiter Widerspruchsbeweis wäre langweilig. Aber Ihr könnt die Aufgabe gern noch einmal probieren. Hier, ich gebe Sie Euch mit auf die Reise. Aber nun seht zu, dass Ihr weiterkommt!"
-- Statt mit `contrapose` `by_contra` ein Widerspruchsbeweis.
-- Probiers doch einfach!
-- In diesem Kapitel hast du also folgende Taktiken kennengelernt:
Als Vergleich zwischen Beweisen \"per Widerspruch\"
und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
du mit `by_contra` einen Widerspruch suchst.
"
-- Als Vergleich zwischen Beweisen \"per Widerspruch\"
-- und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
-- du mit `by_contra` einen Widerspruch suchst.
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
Hint "**Robo**: Fang diesmal mit `by_contra g` an!"
Hint "Sobald Ihr Euch sicher vom Gravitationsfeld des Asteroiden befreit habt, beugt Ihr Euch wieder über die Aufgabe.
**Robo**: Ok, also diesmal fangen wir mit `by_contra g` an!"
by_contra g
Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
@ -42,15 +44,15 @@ Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
DisabledTactic contrapose revert
Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
Mond gelernt haben:
Conclusion "**Robo**: Bravo! Hier ein Überblick, was uns Benediktus gezeigt hat.
Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die ebenfalls
beide bewohnt zu sein scheinen.
Zurück im Raumschiff macht ihr euch auf den Weg zu einem der beiden Monde, die ebenfalls
bewohnt zu sein scheinen.
**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
aber niemand von den Einwohnern wusste was davon...
**Du**: Ich habe immer noch das Gefühl, dass ich die Aufgabe von Königin *Logisinde* ohne `tauto` nicht hätte lösen können.
Kamen in der Aufgabe nicht auch Implikationen vor?
**Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
erzählen…
**Robo**: Vielleicht haben wir ja auf dem Mond *Implis*, den wir gerade ansteuern, Gelegenheit, noch etwas dazuzulernen. Festhalten bitte …
Und damit leitet Robo den Landeanflug ein. Implis scheint ein riesiger Tagbau zu sein auf
dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und quer.
Und damit leitet Robo den Landeanflug ein.
Implis scheint ein riesiger Tagebau zu sein.
Überall verlaufen Förderbänder, kreuz und quer, aber die meisten stehen still.
Ein schüchterner Operationsleiter erwartet Euch bereits.
**Operationsleiter**: Ihr kommt mir gerade recht! Ich habe schon gehört. Echte Mathematiker! Wisst Ihr, wir fördern hier Wahrheitswerte. Und dabei muss man höllisch aufpassen. Ein Fehler, und alles bricht zusammen. Aber ich bin sehr vorsichtig. Ich sage immer: Lieber Stillstand als Untergang!
Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
**Operationsleiter**: Sagt mal, könnt ihr mir hier weiterhelfen?
**Operationsleiter**: Hier, zum Beispiel:
"
Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
Hint "**Du**: Einen Moment, das ist eine Implikation (`\\to`),
also `A` impliziert `A und B`, soweit so gut, also eine Tautologie.
Hint "
**Operationsleiter:** Die Arbeiten meinen, das wäre so richtig und wir würden das dringend brauchen. Aber keiner kann es mir beweisen.
**Robo**: Du hast recht, eigentlich könnte man `tauto` sagen,
aber das scheinen die hier tauto nicht zu verstehen.
Implikationen kannst du aber mit `intro h` angehen."
**Du**: Einen Moment. Das ist ja gerade so eine Implikation (`\\to`). Wir nehmen an, dass `{B}` gilt, und wollen zeigen, dass dann gilt `{A}` impliziert `{A} und {B}`. Ja, klar! Natürlich stimmt das.
Der Operationsleiter sieht Dich erwartungsvoll an.
**Du** *(leise zu Robo)*: Soll ich ihm `tauto` aufschreiben?
**Robo** *(leise zurück)*: So wie der aussieht, fürchte ich, das wird er auch nicht verstehen.
Schreib den Beweis lieber aus.
*Du**: Aber wie denn? Ich glaube, ich würde als erstes gern so etwas sagen wie 'Nehmen wir also an, `{A}` gilt …'
**Robo**: Ja, gute Idee. Wähle dazu für Deine Annahme einfach einen Namen, zum Beispiel `{h}`, und schreib `intro {h}`."
intro hA
Hint "**Du**: Jetzt habe ich also angenommen, dass `A` wahr ist und muss `A ∧ B` zeigen,
das kennen wir ja schon."
Hint "**Du**: OK. Jetzt habe ich also sowohl `{A}` als auch `{B}` in meinen Annahmen und muss `{A} ∧ {B}` zeigen.
**Robo**: Genau. Und wie das geht, weißt Du ja schon."
"Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
"Der Operationsleiter holt aus einem Container einen Stapel Papier hervor.
**Operationsleiter:** Hier hat sich echt einiges angesammelt. Wäre echt super, wenn Ihr mir noch ein bisschen helfen könntet.
Er übergibt Euch das oberste Blatt."
Statement (A B : Prop) (ha : A) (h : A → B) : B := by
Hint "**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
Hint "**Operationsleiter:** Das ist von einem Kollegen.
**Robo**: Oh, das hab ich schon einmal irgendwo gelesen. Warte mal … Richtig! Das war damals, als ich Wikipedia gecrawlt habe: `Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen …`
**Du**: Das wirkt etwas unnatürlich.
**Du**: Robo! Gefragt ist ein Beweis und kein historischer Aufsatz! Oder komme ich hier etwa mit `mopo` oder so etwas weiter?
**Robo**: Schon, ja. Aber als Tool kann das manchmal nützlich sein."
**Robo**: Ok, nein, sorry. `mopo` gibt es nicht. Probier lieber `revert {ha}`."
revert ha
assumption
Hint "**Du**: Aha. `revert` ist qausi `intro` rückwärts.
Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
**Robo:** Genau. `intro` nimmt die Prämisse aus einer Implikation `{A} \\to {B}` im Beweisziel und macht daraus eine Annahme. `revert` nimmt umgekehrt eine Annahme und setzt sie als Implikationsprämisse vor das Beweisziel. Aber nun mach schon fertig."
assumption
Daraufhin lächelt der Fragende nur vorahnend."
Conclusion "Der Operationsleiter nimmt erfreut Eure Lösung entgegen, und greift zum Telefon."
Selbstsicher folgt ihr den Anweisungen und geht nach draußen zum
defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
$$
\\begin{CD}
A @>{f}>> B @<{g}<< C \\\\
@. @V{h}VV @V{m}VV \\\\
D @>{i}>> E @>{k}>> F \\\\
@A{m}AA @A{n}AA @V{p}VV \\\\
G @<{q}<< H @>{r}>> I
\\end{CD}
$$
Die nächste Seite sieht ein bisschen komplizierter aus. Damit Ihr nicht die Übersicht verliert, fasst Robo sofort die verschiedenen Implikationen in einem Diagramm zusammen.
$$
\\begin{CD}
A @>{f}>> B @<{g}<< C \\\\
@. @V{h}VV @V{m}VV \\\\
D @>{i}>> E @>{k}>> F \\\\
@A{m}AA @A{n}AA @V{p}VV \\\\
G @<{q}<< H @>{r}>> I
\\end{CD}
$$
"
Statement
(A B C D E F G H I : Prop)
(f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
(n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
**Robo**: Und dann fängst du am besten wieder mit `intro` an."
**Robo**: Dann fängst du am besten wieder mit `intro` an."
intro ha
Branch
apply r
Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
apply p
apply k
apply h
Branch
apply g
Hint "**Robo**: Nah, da stimmt doch was nicht…"
Hint "**Robo**: Nah, da stimmt doch was nicht…"
apply f
assumption
Conclusion
"Mit einem lauten Ratteln springen die Förderbänder wieder an.
**Operationsleiter**: Vielen Dank euch! Kommt ich geb euch eine Führung und stell euch den
Technikern hier vor."
"Der Operationsleiter bedankt sich wieder artig. Er drückt wieder auf ein paar Knöpfe, und mit einem lauten Ratteln springen mehrere Förderbänder gleichzeitig wieder an."
Als erstes kommt ihr in einen kleinen Raum mit ganz vielen Bildschirmen.
Ein junges Wesen dreht sich auf dem Stuhl um, und sagt:
**Mitarbeiter**: Oh hallo! Schaut euch mal das hier an!
**Operationsleiter:** Wir hatten auch mal ein paar Förderbänder, die in beide Richtungen laufen konnten. Die hatte ich vorsichtshalber alle abgestellt, weil in den neusten Handbüchern von solchen Doppelbändern abgeraten wird. Aber vielleicht sind sie ja unter bestimmten Voraussetzungen doch sicher? Was meint Ihr zu diesem Fall?
"
Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
Hint "**Robo**: Das ist ein genau-dann-wenn Pfeil: `\\iff`. Er besteht aus zwei Teilen:
`A ↔ B` ist als `⟨A → B, B → A⟩` definiert.
Hint "**Robo**: `→` ist natürlich Leansch für `$\iff$`.
Die Aussage `A ↔ B` besteht also aus zwei Teilen; sie ist als `⟨A → B, B → A⟩` definiert.
**Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
**Robo**: Genau. Entsprechend kannst du hier auch mit `constructor` anfangen."
**Robo**: Genau. Entsprechend kannst Du auch hier mit `constructor` anfangen."
constructor
Hint "**Du**: Ah und die beiden hab ich schon in den Annahmen."
Hint "**Du**: Ah, und die beiden Teile habe ich schon in den Annahmen."
assumption
assumption
Conclusion
"
**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheißen,
hier bei `(h : A ↔ B)` heißen sie `h.mp` und `h.mpr`.
**Operationsleiter**: Ok, das leuchtet mir ein.
**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
**Robo** *(zu Dir)*: Übrigens, so wie bei `(h : A ∧ B)` die beiden Teile `h.left` und `h.right` heißen,
heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`.
**Operationsleiter**: \"Modulo Ponens\" ist ein lokaler Begriff hier,
aber das ist doch nicht wichtig.
**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
**Robo**: Und das \"r\" in `mpr` stünde für \"reverse\" weil's die Rückrichtung ist.
**Robo**: `mp` steht für Modus Ponens`. Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen … Ach nee, das wolltest Du ja nicht hören. Das \"r\" in `mpr` steht für \"reverse\", weil's die Rückrichtung ist.
Noch während der Koch wieder zu seiner Suppe geht, kommt sein erster Gehilfe hervor.
**Operationsleiter**: Ah, die nächste Seite ist auch von diesem Kollegen. Aber da ist noch eine Notiz bei. Wir hatten hierfür schon einmal einen Beweis, aber den mochte er nicht. Er wollte einen Beweis, der weder `rw` noch `apply` verwendet!!
**Gehilfe**: Ich hab gestern noch was anderes gehört, könnt ihr mir da auch helfen?
Aber ich versteh nicht ganz was ihr meinem Chef erklärt habt.
Er holt tief Luft und seuft.
**Operationsleiter**: Ich glaube, der stellt sich immer viel dümmer, als er ist. Aber meint Ihr, Ihr schafft das?
"
Statement (A B : Prop) : (A ↔ B) → (A → B) := by
Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
Hint (hidden := true) "**Robo**: Genau, das war `intro`."
intro h
Hint "**Du**: Also ich kenn `rw [h]` und `apply h.mp`, aber das will er wohl nicht hören.
Hint "**Du**: Also, ich kenne `rw [h]` und `apply h.mp`, aber das wollten wir ja diesmal vermeiden.
**Robo**: Was du machen könntest ist mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
**Robo**: Was Du machen könntest, ist, mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
Teile aufteilen."
Branch
intro a
Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benützen, aber der
Gehilfe will, dass du zwingend eine dritte Variante benützt. Geh doch einen
Schritt zurück so dass das Goal `A → B` ist."
Hint "**Robo**: Hier müsstest Du jetzt `rw [←h]` oder `apply h.mp` benutzen.
Geh lieber einen Schritt zurück, sodass das Goal `A → B` ist."
rcases h with ⟨mp, mpr⟩
Hint (hidden := true) "**Du**: Ah und jetzt ist das Resultat in den Annahmen."
Hint (hidden := true) "**Du**: Ah, und jetzt ist das Beweisziel in den Annahmen."
assumption
Conclusion
"
**Gehilfe**: Ah danke! Und jetzt versteh ich auch die Zusammenhänge!
**Operationsleiter**: Perfekt, das sollte reichen!
Der Arbeitskollegin der Mechanikerin, der die ganze Zeit gespannt zugehört hat, dreht sich zu
euch.
Er ist offensichtlich interessiert and existierenden Resultaten zu sein, aber offenbar
kann er nicht viel mit `apply` anfangen.
Er hat aber folgendes Resultat bereit:
**Operationsleiter**: Wieder etwas für den Kollegen …. Und er wollte wieder einen Beweise ohne `apply`. Ich sehe hier auch, dass ich mir schon einmal etwas hierzu notiert hatte. Richtig, es gibt da dieses Lemma:
```
lemma not_not (A : Prop) : ¬¬A ↔ A
```
und stellt euch folgende Frage:
**Operationsleiter**: Schafft Ihr das damit?
"
Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
@ -33,17 +26,16 @@ Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B
Hint "**Du**: Häh, wieso hat das jetzt 2 von 3 der `¬¬` umgeschrieben?
**Robo**: `rw` schreibt nur das erste um, das es findet, also `¬¬C`. Aber weil dieses
mehrmals vorkommt, werden die alle ersetzt…
mehrmals vorkommt, werden die alle ersetzt…
**Du**: Ah, und `¬¬B` ist was anderes, also brauch ich das Lemma nochmals."
**Du**: Ah, und `¬¬B` ist etwas anderes, also brauche ich das Lemma nochmals."
rw [not_not]
Conclusion
"
**Du**: Ah und wir sind fertig…?
**Du**: Wir sind schon fertig …?
**Robo**: Ja, `rw` versucht immer anschliessend `rfl` aufzurufen, und das hat hier
funktioniert.
**Robo**: Ja, `rw` versucht immer anschließend `rfl` aufzurufen, und das hat hier funktioniert.
**Operationsleiter**: Damit endet unsere Führung langsam. Bevor ihr weitergeht
habe ich noch ein Problem, an dem ich mir die Zähne ausbeisse. Wir haben die
Herleitung eines unserer Programme `imp_iff_not_or` verloren, und wissen nicht mehr
ob es einwandfrei funktioniert.
**Operationsleiter**: Ihr habt mir wirklich so geholfen! Hier ist das letzte Problem. Das habe ich von meinem Vorgänger geerbt. Er hat behauptet, wenn wir das lösen können, dann läuft hier wieder alles. Aber es sah mir immer viel zu schwierig aus, um es überhaupt zu versuchen. Wollt Ihr es einmal probieren?
**Du**: Nah gut, mal sehen. Robo, was hab ich denn alles hier gelernt?
**Du**: Klar, zeig her! Robo, kannst Du mir vielleicht auch noch einmal so eine nette Zusammenfassung anzeigen, was ich theoretisch in den letzten fünf Minuten gelernt habe?
**Robo**: Hier ist die Übersicht:
**Robo**: Hier ist die Übersicht:
## Notationen / Begriffe
@ -44,34 +41,35 @@ ob es einwandfrei funktioniert.
Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
constructor
Hint "**Du**: Das sieht kompliziert aus…
Hint "**Du** *(flüsternd)*: Ist das nicht die Definition von `→`?
**Robo** *(flüsternd)*: Ja, aber die Richtung kennst du ja schon also Lemma,
wend doch einfach das an."
**Robo** *(flüsternd)*: Könnte man so sehen. Aber auf Leansch ist das bloß eine Äquivalenz.
So oder so kennst du ja eine Richtung schon als Lemma.
Also wende das doch einfach an."
apply not_or_of_imp
Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma?
**Robo**: Leider nicht. Da musst du manuell ran."
Hint (hidden := true) "**Robo**: Na Implikationen fangst du immer mit `intro` an."
**Robo**: Leider nicht. Da musst Du manuell ran."
Hint (hidden := true) "**Robo**: Na Implikationen gehst Du immer mit `intro` an."
intro h
intro ha
Hint (hidden := true) "**Robo**: Ich wür mal die Annahme `h` mit `rcases` aufteilen."
Hint (hidden := true) "**Robo**: Ich würde mal die Annahme `h` mit `rcases` aufteilen."
rcases h with h | h
contradiction
assumption
DisabledTactic tauto
Conclusion "**Operationsleiter**: Damit gehen unsere Wege auseinander. Da fällt mir ein, seit
ihr auf dem Weg zu unserem Schwestermond?
Conclusion "**Operationsleiter**: Das ist ja fantastisch! Tausend Dank! Dann will ich Euch auch gar nicht länger aufhalten.
Ihr wollt bestimmt weiter zu Quantus, unserem Schestermond, oder?
**Du**: Könnten wir sein…
**Du**: Ehm, vielleicht …
**Operationsleiter**: Ich hab hier einen Brief für *Evenine*, könntet ihr diesen mit euch führen?
**Operationsleiter**: Dann habe ich noch eine letzte Bitte. Ich habe hier noch ein Päckchen für die Königin von Quantus! Auch schon von meinem Vorgänger geerbt. Die Post will es nicht annehmen, weil ich die Adresse nicht weiß. Könntet Ihr es vielleicht zu ihr mitnehmen?
**Du**: Klar! Robo, halt den mal.
**Du**: Klar! Robo, halt mal.
Robo nimmt den Brief und lässt ihn irgendwo in seinem Innern verschwinden. Dabei bemerkt er
den besorgten Blick des Operationsleiters.
Robo nimmt das Päckchen und lässt es irgendwo in seinem Innern verschwinden.
Introduction "Eure Reise geht weiter zum zweiten Mond. Dieser ist etwas grösser und
komplett mit buschartigen Pflanzen überwachsen. Der Landeanflug sit etwas kniffliger,
aber offenbar kann Robo nicht nur Lean übersetzen, sondern auch mit maschineller Genauigkeit
navigieren.
Introduction "Auf dem Schwestermond Quantus erwartet Euch bereits ein großer Ansammlung von Formalosopheninnen. Sie reden alle wild durcheinander und Ihr habt Probleme, Euch überhaupt Gehör zu verschaffen. Robo produziert schließlich ein lautes Gong-Geräusch, das sie kurzzeitig zur Ruhe bringt.
Ihr werdet sofort empfangen und man führt euch zur lokalen Machthaberin.
Ihr kommt an verschiedensten riesigen Büschen vorbei, die offensichtlich innen Ausgehöhlt sind
und so als Wände für Behausungen der Wesen hier dienen.
**Du**: Wir haben einen Brief für Eure Königin. Könntet Ihr uns zu Eurer Königin führen?
Man führt euch in einen der Büsche. Nun entdecksts du dass das Blätterdach künstlich verstärkt ist,
offensichtlich um Regen abzuweisen.
**Alle** *(im Chor)*: Wir sind schon alle hier!
Vor euch steht eine Frau, die euch als Machthabering *Evenine* vorgestellt wird."
**Du**: Ok. Und wer von Euch ist die Königin?
Nun herrscht betretenes Schweigen. Alle zucken mit den Schultern.
**Du**: Habt Ihr überhaupt eine Königin?
**Alle** *(im Chor)*: Ja, ja. Wir haben eine Königen, wir haben eine Königen.
**Robo** *(zu Dir)*: Ich fasse mal zusammen. Es existiert eine Königen, aber keiner weiß, wer sie ist …
**Du**: Ist das nicht ein Widerspruch?
**Robo**: Fragst Du, Du als Mathematiker? Nein, das ist kein Widerspruch. Das ist einfach eine „reine Existenzaussage“.
Du bist Dir nicht ganz sicher, wie ernst er das meint.
**Du**: Dann ich schlage vor, wir übergeben das Päckchen einfach an *alle* Bewohner. Dann haben wir es ja insbesondere der Königin übergeben.
**Du** *(in die Menge*): Wir haben Euch ein Päckchen von Implis gebracht. Hier, das ist für Euch.
Robo spuckt es aus, wirft es in die Menge, und die Formalosophinnen reißen es auf. Darin befinden sich ein paar loser Seiten, die sie sofort eingehend studieren.
Zwei Minuten später liegen die Seiten wieder bei Euch. Es sind wieder mathematische Probleme. Und die Formalosophinnen wollen sehen, wie Ihr sie löst.
Müde ruht ihr euch in eurer Bleibe aus. Du schaust doch eine Lücke in den Blättern vielen
kleinen Vögeln bei der Nahrungssuche zu.
Beim nächsten Problem bekommt ihr ausnahmsweise Hilfe vom Publikum.
**Du**: Sag mal Robo, ich hab vorhin ein Kind überhört, dass seinem Spielgefährten erklärt hat,
folgendes sei mit `rfl` zu beweisen:
**Alle**: `rfl`, `rfl`, …
"
Statement : 1 + 1 = 2 := by
Hint "**Du**: Wieso nicht `ring`?
**Robo**: Klar, `ring` geht auch und ist intuitiver.
Für `rfl` kommt es darauf an, wie die Sachen genau definiert sind: `1 + 1` ist als
`(0.succ).succ` definiert und `2` halt ebenfalls.
"
**Robo**: Klar, `ring` würde normalerweise auch funktioneren. Aber ich würde mich hier dem Mehrheitswillen beugen …"
rfl
OnlyTactic rfl
Conclusion
"
**Du**: Dann war das mehr Glück?
**Robo**: Der Grund, warum hier ausnahmsweise auch mal `rfl` funktioniert hat, ist, dass auf beiden Seiten tatsächlich *per Definition* dasselbe steht. Das soll heißen, wenn man links in `1 + 1` die Definition von `1` und `+ 1` einsetzt, und rechts die Definition von `2`, dann erhält man *buchstäblich* dasselbe (nämlich `(0.succ).succ`).
**Robo**: Das ist eine Art die Welt zu sehen…
**Du**: Na schön. Muss ich mir jetzt diese Definition von `2` merken?
Am nächsten Tag erklärt euch *Evenine*, dass es auf dem Mond zwei Gruppierungen gibt,
ihre und die ihres Halbbruders *Oddeus*. Die Mottos sind
Ihr habt nun alle Fragen aus dem königlichen Päckchen beantwortet, und die Formalosophinnen applaudieren. Dann wollen Sie aber auch noch ein paar Fragen stellen, aber sie können sich nicht einigen, welche.
Ihr heute abwechselnd die Rufe „Even“ und „Odd“ aus der Menge heraus. Deshalb zeigt Dir Robo vorsichtshalber schon einmal die entsprechenden Definitionen an:
```
def Even (n : ℕ) : Prop := ∃ r, n = r + r
@ -29,18 +29,20 @@ und
def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
```
**Evenine**: Hier, ich zeige euch mal etwas was man bei uns machen kann:
Schließlich taucht von irgendwo aus der Menge folgendes Papier auf:
"
Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
Hint "**Robo**: Du kannst Dir mit `unfold Even` auch hier auf dem Papier die Definition sehen."
Branch
unfold Even
Hint "Rob**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst was los ist."
Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
dass ein `r` existiert so dass `r + r = n`. Am besten
öffnest du diese Definition mit `unfold Even at *` einmal, dann siehst du besser, was los ist. "
Hint "Robo**: Am besten machst Du auch noch `unfold Even at h`, damit Du verstehst, was los ist."
Hint "**Robo**: Wie Du oben siehst, ist `Even n` dadurch definiert,
dass ein `r` existiert so dass `r + r = n` ist. Am besten
öffnest du diese Definition mit `unfold Even at *` einmal.
Dann siehst Du besser, was los ist. "
unfold Even at *
Hint "**Du**: Also von `{h}` weiss ich jetzt dass ein `r` existiert, so dass `r + r = n`…
Hint "**Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = n` …
**Robo**: Mit `rcases h with ⟨r, hr⟩` kannst du dieses `r` tatsächlich einführen."
rcases h with ⟨r, hr⟩
@ -48,18 +50,18 @@ Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
**Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
dir leider nicht sagen, welche Zahl passt.
Dir leider nicht sagen, welche Zahl passt.
"
Branch
rw [hr]
Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
Hint "**Robo**: Das geht auch, jetzt musst Du aber wirklich `use` verwenden."
use 2 * r ^ 2
ring
use 2 * r ^ 2
Hint "**Du**: Ah und jetzt `ring`!
Hint "**Du**: Ah, und jetzt `ring`!
**Robo**: Aber zuerst must du noch mit
`rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiss."
**Robo**: Aber zuerst musst Du noch mit
`rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiß."
rw [hr]
ring
@ -70,4 +72,4 @@ Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
Hint "**Du**: Also ich kann mal das `¬` durch die Quantifier hindurchschieben.
**Robo**: `push_neg` macht genau das!
Hint "**Du**: Ich würde gern diese Negation `¬` am Quantor vorbeischieben.
**Robo**: Intern braucht das zwei Lemmas
**Robo**: `push_neg` macht genau das! Oder Du könntest `rw` mit den folgenden Lemmas verwenden:
```
not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)
not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)
```
die du natürlich auch mit `rw` gebrauchen könntest."
"
Branch
unfold Odd
push_neg
Hint "**Robo**: Der Weg ist etwas schwieriger. Ich würde nochmals zurück und schauen,
dass du irgendwann `¬Odd` kriegst, was du dann mit `rw [←even_iff_not_odd]`
zu `Even` umwandeln.
kannst."
Hint "**Robo**: Dieser Lösungsweg scheint mir etwas zu schwierig.
Ich würde nochmal zurückgehen und schauen,
dass Du irgendwie `¬Odd` erhältst.
Das kannst Du dann mit `rw [←even_iff_not_odd]`
zu `Even` umwandeln."
push_neg
intro n
Hint "**Robo**: Welche Zahl du jetzt mit `use` brauchst, danach wirst du vermutlich das
Lemma `←even_iff_not_odd` brauchen.
Hint "**Robo**: Jetzt brauchst Du eine Zahl mit `use`, und danach vermutlich das Lemma `←even_iff_not_odd` brauchen.
**Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` machen?
**Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` anwenden?
**Robo**: Ne, `rw` kann nicht innerhalb von Quantifiern umschreiben.
**Robo**: Nee, `rw` kann nicht innerhalb von Quantoren umschreiben.
**Du**: Aber wie würde ich das machen?
**Robo**: Zeig ich dir später, die Wache wird schon ganz ungeduldig!
Im Moment würde ich zuerst mit `use` eine richtige Zahl angeben, und danach umschreiben."
**Robo**: Zeig ich dir später, nicht hier vor großem Publikum.
Ich würde jetzt lieber mit `use` eine richtige Zahl angeben, und danach umschreiben."
Branch
use n + 2
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
Branch
use n + 4
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
use n
Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
Hint "**Robo**: Gute Wahl! Jetzt kannst Du `←even_iff_not_odd` verwenden."
rw [←even_iff_not_odd]
unfold Even
use n
--ring
Conclusion "Damit werdet ihr eingelassen.
Conclusion "Die Formalosophinnen sind ganz begeistert.
Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
**Du**: Kann uns hier irgendjemand vielleicht ein bisschen Orientierung im Formaloversum geben?
**Alle**: Ja, ja.
**Robo**: Entweder wir suchen direkt diesen *Oddeus*, oder wir schauen uns einmal um. Die Wahl
ist deine!
**Du**: Wer denn?
**Du**: Kannst du mir nochmals einen Überblick geben, was wir gelernt haben?
Die Frage war wieder zu konkret. Betretenes Schweigen.
**Robo**:
**Robo**: Lass nur. Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da drüben. Und bevor Du fragst – hier ist wieder ein Überblick, was Du auf diesem Planeten gelernt hast.
Jon Eugster
2 years ago
committed by
GitHub