@ -21,7 +21,7 @@ keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu
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.
exklusiv in einem Dir fremden Dialekt, den sie Leanish [liːnɪʃ] nennen.
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.
@ -30,32 +30,28 @@ Robo, das ist Dein kleiner SmartElf. Robo ist war auch nicht die mathematische L
Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum Punkt:
**Logisinde** Werte Wesen aus fremden Welten, gestatten Sie eine Frage. Warum gilt …
**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.
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
(A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
tauto
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?
Statement "**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.
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
**Du** Ernsthaft?
**Du** Ernsthaft?
**Robo** Ja. Schreib einfach `tauto`.
**Robo** Mach schon …
"
(A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste nach vorne. Es ist schüchtern und schreibt bloß.
Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste nach vorne. Es ist schüchtern und schreibt bloß.
"
Statement
(n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
assumption
Hint
"
Statement "
**Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl.
**Du** Warum schreibt er dann nicht `n ∈ ℕ`??
**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.
**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.
**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`.
@ -33,9 +28,10 @@ Hint
**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`.
"
(n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
assumption
Conclusion
Conclusion
"
**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf zerbrochen habe!
**Du** Wenn ich das jetzt richtig lese, ist `A` eine Aussage, und wir haben außerdem eine Annahme names `h`, die besagt …
**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.
**Robo** … die besagt, dass `False` gilt.
**Du** Ich dachte, `False` gilt nie?
@ -34,7 +34,7 @@ Hint
**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`.
@ -18,7 +18,7 @@ Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
assumption
assumption
Hint
Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B =>
"
**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?
@ -34,7 +34,7 @@ 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*.
**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
Hint (A B : Prop) (hA : A) : A ∨ (¬ B) =>
"
**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!
**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?
**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 …`?
**Du** Also, wieder `rcases …`?
**Robo** Ja, aber diesmal nicht `rcases h with ⟨h₁, h₂⟩`, sondern `rcases h with h | h`.
"
@ -42,14 +42,14 @@ Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
**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.
Robo straht überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
@ -17,7 +17,7 @@ Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vor
-- Note: The other direction would need arguing by cases.
Statement
Statement ""
(A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
constructor
rcases h with h | h
@ -33,7 +33,7 @@ Statement
right
assumption
Hint
Hint (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
"
**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.
@ -72,9 +72,9 @@ HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
Conclusion
"
**Robo** Bravo! Jetzt aber nichts wie weg hier, bevor sich eine neue Schlange bildet!
**Robo** Bravo! Jetzt aber nichts wie weg hier, bevor sich eine neue Schlange bildet!
Logisinde ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
Logisinde ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
"
NewTactics left right assumption constructor rcases rfl contradiction trivial
Alexander Bentkamp
3 years ago