Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
**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 Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
gebeten.
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.
**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.
**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
"
"
-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
-- 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
-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
-- `suffices` schöner gewesen:
-- `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
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
(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`
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.
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
**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
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
contradiction
Hint "**Robo**: Und hier beweist du das Zwischenresultat."
Hint "**Robo**: Und hier beweist Du das Zwischenresultat."
apply h
apply h
assumption
assumption
NewTactic «suffices»
NewTactic «suffices»
DisabledTactic «have»
DisabledTactic «have»
Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
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**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
**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?
**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`:
"
"
Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
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."
Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
constructor
constructor
intro h b
intro h b
by_contra a
by_contra a
Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
Hint "**Robo**: Ich würde wieder mit `suffices g : B` einen Widerspruch herbeiführen."
herbeiführen."
suffices b : B
suffices b : B
contradiction
contradiction
apply h
apply h
assumption
assumption
intro h a
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
by_contra b
Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
suffices g : ¬ A
suffices g : ¬ A
@ -48,4 +45,4 @@ Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
DisabledTactic rw
DisabledTactic rw
DisabledLemma not_not
DisabledLemma not_not
Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"
**Benedictus**: Gut, hier ist die angekündigte Frage. Versucht mal einen *direkten* Beweis, ohne `contrapose`.
**Du**: Da steht etwas über `contrapose` hier…
**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.
"
"
-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
-- 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
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
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
**Du**: Richtig. Von hinten durch die Brust … Aber warte, im Moment steht da doch gar kein `→`.
ein Goal `A → B` zu `¬B → ¬A ` um.
**Du**: Aber das Goal ist doch gar keine Implikation?
**Robo**: Erinner Dich an `revert`. Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Beweissziel schieben."
**Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
schieben."
revert h
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
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]
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
apply even_square
NewTactic contrapose
NewTactic contrapose
DisabledTactic by_contra
DisabledTactic by_contra
Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
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
**Du**: Aber hätten wir die letzte Aufgabe nicht genauso gut per Widerspruch beweisen können?
beweisen können?
**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
**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!"
Probiers doch einfach!
In diesem Kapitel hast du also folgende Taktiken kennengelernt:
-- 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
-- Als Vergleich zwischen Beweisen \"per Widerspruch\"
du mit `by_contra` einen Widerspruch suchst.
-- und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
"
-- du mit `by_contra` einen Widerspruch suchst.
open Nat
open Nat
Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
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
by_contra g
Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
@ -42,15 +44,15 @@ Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
DisabledTactic contrapose revert
DisabledTactic contrapose revert
Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
Conclusion "**Robo**: Bravo! Hier ein Überblick, was uns Benediktus gezeigt hat.
Conclusion "Die Formalosophinnen sind ganz begeistert.
Conclusion "Die Formalosophinnen sind ganz begeistert.
Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage.
**Du**: Kannst Du mir nochmal einen neun Überblick geben?
**Du**: Kann uns hier irgendjemand vielleicht ein bisschen Orientierung im Formaloversum geben?
**Robo**:
**Alle**: Ja, ja.
**Du**: Wer denn?
Die Frage war wieder zu konkret. Betretenes Schweigen.
**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.
Marcus Zibrowius
3 years ago