From 11a8352fd3f76a3bc3b5f38792aed1b153647c89 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Thu, 30 Mar 2023 11:33:16 +0200 Subject: [PATCH] =?UTF-8?q?story=20f=C3=BCr=20Contradiction=20=C3=BCberarb?= =?UTF-8?q?eiten?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- server/adam/Adam/Levels/Contradiction.lean | 21 ++++++++-- .../Adam/Levels/Contradiction/L01_Have.lean | 22 +++++------ .../Levels/Contradiction/L02_Suffices.lean | 28 ++++++-------- .../Levels/Contradiction/L03_ByContra.lean | 32 +++++----------- .../Levels/Contradiction/L04_ByContra.lean | 21 +++++----- .../Levels/Contradiction/L05_Contrapose.lean | 31 ++++++--------- .../Levels/Contradiction/L06_Summary.lean | 38 ++++++++++--------- .../Adam/Levels/Predicate/L09_PushNeg.lean | 11 +++++- 8 files changed, 99 insertions(+), 105 deletions(-) diff --git a/server/adam/Adam/Levels/Contradiction.lean b/server/adam/Adam/Levels/Contradiction.lean index a7cdde7..103085a 100644 --- a/server/adam/Adam/Levels/Contradiction.lean +++ b/server/adam/Adam/Levels/Contradiction.lean @@ -7,10 +7,23 @@ import Adam.Levels.Contradiction.L06_Summary Game "Adam" World "Contradiction" -Title "Widerspruch" +Title "Beweisstrategien" Introduction " -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. " diff --git a/server/adam/Adam/Levels/Contradiction/L01_Have.lean b/server/adam/Adam/Levels/Contradiction/L01_Have.lean index 01d4aa3..ced66a2 100644 --- a/server/adam/Adam/Levels/Contradiction/L01_Have.lean +++ b/server/adam/Adam/Levels/Contradiction/L01_Have.lean @@ -11,12 +11,11 @@ Game "Adam" World "Contradiction" Level 1 -Title "Have" +Title "Was wir haben, haben wir." Introduction " -**Oddeus**: Willkommen Reisende! Ich muss eingestehen ich bin in Gedanken noch -an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen? +**Benedictus**: Hier, schaut mal. Das habe ich für Euch vorbereitet. " -- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein @@ -36,17 +35,18 @@ an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen? -- bevor du dann mit dem Beweis forfährst. Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by - Hint "**Du**: Also als erstes Teile ich wohl mal das Und (`∧`) auf." + Hint "**Du**: Also als erstes teile ich wohl mal das Und (`∧`) auf." rcases k with ⟨h₁, h₂⟩ - Hint "**Du**: Aber jetzt… + Hint "**Du**: Und jetzt … - **Robo**: Du könntest dir ein passendes Zwischenresultat zurechtlegen, das dir hilft: - Mach mal `have g : ¬ B`!" + **Benedictus**: … solltest Du Dir ein passendes Zwischenresultat zurechtlegen. + + **Robo**: Ja! Probier mal `have g : ¬ B`!" have g : ¬ B - · Hint "**Du**: Was und jetzt hab ich einfach angenommen das sei richtig? + · Hint "**Du**: Was? Jetzt hab ich einfach angenommen, dass sei richtig? - **Robo**: Ne, jetzt musst du das zuerst beweisen bevor du es dann benützen kannst." - Hint (hidden := true) "**Robo**: `apply` scheint passend zu sein." + **Robo**: Nee, jetzt musst Du das erst noch beweisen, bevor Du es dann benutzen kannst." + Hint (hidden := true) "**Robo**: `apply` sollte helfen" apply h assumption · Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen? @@ -57,4 +57,4 @@ Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by NewTactic «have» DisabledTactic «suffices» -Conclusion "*Oddeus*: Das stimmt wohl." +Conclusion "**Benedictus**: Das sieht gut aus!" diff --git a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean index ac8f762..bb954b7 100644 --- a/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean +++ b/server/adam/Adam/Levels/Contradiction/L02_Suffices.lean @@ -11,13 +11,11 @@ Game "Adam" World "Contradiction" Level 2 -Title "Suffices" +Title "Es reicht!" Introduction " -*Oddeus*' Partner meldet sich. - -**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. -Und er führt euch durch seinen Rosengarten." diff --git a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean index 4a178bf..db3ccb9 100644 --- a/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L03_ByContra.lean @@ -12,17 +12,10 @@ Game "Adam" World "Contradiction" Level 3 -Title "Per Widerspruch" +Title "Widerspruch" Introduction -"**Oddeus**: Ich verstehe *Evenine* einfach nicht. Ich will euch auch gleich zeigen, -was sie mir letzthin geschrieben hat, aber zuerst schaut einmal unseren -wunderschönen Absurda-Tempel an! - -Damit kommt ihr vor einen sehr hohen Turm, der ausschliesslich aus Dornenranken gewachsen -scheint. - -**Oddeus**: Versteht ihr, was hier über dem Eingang steht? +"**Benedictus**: Hier ist noch eine Variante. " -- Eine sehr nützliche Beweismethode ist per Widerspruch. @@ -37,29 +30,24 @@ scheint. -- steht: Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by - Hint "**Robo**: Ein `¬` im Goal heisst häufig, dass du einen Widerspruchsbeweis führen + Hint "**Robo**: Ein `¬` im Goal heißt häufig, dass Du einen Widerspruchsbeweis führen möchtest. - **Du**: Und wie mach ich das? Mit `contradiction`? + **Du**: Und wie mache ich das? Mit `contradiction`? - **Robo**: Mit `by_contra h` fängst du einen an. Mit `contradiction` schliesst du ihn dann - später ab." + **Robo**: Mit `by_contra h` fängst Du einen Widerspruchsbeweis an. Und mit `contradiction` schließt Du ihn ab." by_contra h - Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : ¬ {A}`, und damit musst du einen - Widerspruch herbeileiten. + Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : {A}`, und damit musst Du einen Widerspruch herleiten. - Ein Methode ist, dass du jetzt mit `suffices` sagts, zu was du denn gerne den Widerspruch - haben möchtest, zum Beispiel `suffices k : B` + Du könntest zum Beispiel jetzt mit `suffices` sagten, welchen Widerspruch Du gern herleiten möchtest, etwa `suffices k : B` " suffices k : B - Hint "**Du**: Ah und jetzt kann ich einfach sagen dass sich die Anahmen `{B}` und `¬{B}` - widersprechen." + Hint "**Du**: Ah, und jetzt kann ich einfach sagen dass sich die Annahmen `{B}` und `¬{B}` sich widersprechen." contradiction - Hint "**Robo**: Und jetzt kannst du noch das Ergebnis zeigen, das zu einem Widerspruch - geführt hat." + Hint "**Robo**: Und jetzt musst Du nur noch das Zwischenresultat herleiten, dass zu diesem Widerspruch geführt hat." apply g assumption NewTactic by_contra -Conclusion "**Oddeus**: Sehr gut, kommt mit hinein!" +Conclusion "**Benedictus**: Ich sehe schon, Ihr lernt schnell!" diff --git a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean index f9530cc..a285afc 100644 --- a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean @@ -12,32 +12,29 @@ Game "Adam" World "Contradiction" Level 4 -Title "Per Widerspruch" +Title "Kontraposition" Introduction " -*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?" +Conclusion "" diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean index e2df673..396c31c 100644 --- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean +++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean @@ -14,14 +14,7 @@ Title "Kontraposition" Introduction " -*Oddeus* reicht euch das Papier. - -**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. +**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." diff --git a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean index 1e32524..5c51b37 100644 --- a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean +++ b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean @@ -14,23 +14,25 @@ Title "Contradiction" Introduction " -**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. + | | Taktik | Beispiel | |:------|:----------------|:-------------------------------------------------------| -| 177 | `have` | Zwischenresultat annehmen. | -| 18 | `suffices` | Zwischenresultat annehmen. | -| 19 | `by_contra` | Widerspruch. (startet einen Widerspruch) | -| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* | -| 20 | `contrapose` | Kontraposition. | -| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. | +| 177 | `have` | Zwischenresultat annehmen | +| 18 | `suffices` | Zwischenresultat annehmen | +| 19 | `by_contra` | Widerspruch *(startet einen Widerspruchsbeweis)* | +| *3* | `contradiction` | *(schliesst einen Widerspruchsbeweis)* | +| 20 | `contrapose` | Kontraposition | +| *9* | `revert` | nützlich, um danach `contrapose` anzuwenden | " diff --git a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean index fd7a5f2..8771d83 100644 --- a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean +++ b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean @@ -73,10 +73,17 @@ Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by --ring 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. | | Beschreibung | |:--------------|:----------------------------|