@ -21,16 +21,18 @@ keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu
Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach
überhaupt kein tieferes mathematisches Verständnis, und zweitens kommunizieren Sie über Mathematik
ü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 Leansch [liːnʃ] nennen.
Zum Glück hat Robo mit Dir das Universum gewechselt.
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.
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 Leansch gelernt.
Und das ist Gold wert.
----
----
Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum Punkt:
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.
Und er kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung.
Dazwischen sollst Du offenbar einen Beweis eintragen.
Dazwischen sollst Du offenbar einen Beweis eintragen.
@ -44,7 +46,9 @@ Statement ""
Hint (A B C : Prop) :
Hint (A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
"**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?
"**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.
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
@ -59,7 +63,9 @@ Hint (A B C : Prop) :
Conclusion
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.
**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,7 +8,8 @@ Title "Aller Anfang ist... ein Einzeiler?"
Introduction
Introduction
"
"
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.
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.
**Untertan** Warum ist $42 = 42$?
**Untertan** Warum ist $42 = 42$?
@ -21,7 +22,8 @@ Statement "" :
rfl
rfl
Hint : 42 = 42 => "
Hint : 42 = 42 => "
**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`.
**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist.
Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
**Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl.
**Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl.
**Du** Warum schreibt er dann nicht `n ∈ ℕ`??
**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`.
**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`.
**Du** Aber das war doch gerade eine der Annahmen.
**Du** Aber das war doch gerade eine der Annahmen.
@ -35,7 +37,8 @@ Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
Conclusion
Conclusion
"
"
**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf zerbrochen habe!
**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf
Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
"
"
Statement
Statement ""
"Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`.
Zeige, dass daraus $A$ folgt."
(A : Prop) (h : False) : A := by
(A : Prop) (h : False) : A := by
contradiction
contradiction
Hint (A : Prop) (h : False) : A =>
Hint (A : Prop) (h : False) : A =>
"
"
**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?
**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`.
**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?
**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`.
**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`.
"
"
Conclusion
Conclusion
@ -39,7 +41,8 @@ Conclusion
**Du** War das jetzt ein Widerspruchsbeweis?
**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.
**Robo** Nein, nein, ein Widerspruchsbeweis sieht anders aus. Das Argument hier war:
wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
(n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by
(n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
contradiction
contradiction
Hint (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 =>
Hint (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 =>
"
"
**Du** Wieder ein Widerspruch in den Annahmen?
**Du** Wieder ein Widerspruch in den Annahmen?
**Robo** Ich sehe, du hast langsam den Dreh raus.
"
"
Conclusion
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.
**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`.
Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht. Er legt sie uns vor, setzt sich hin, und häkelt.
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
Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
constructor
constructor
@ -20,18 +21,27 @@ Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B =>
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?
**Du**: Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt. Auch. Und beweisen sollen wir
dass `{A} und {B}` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung.
Kann ich nicht wieder `trivial` sagen?
**Robo** Nee, diesmal wird das nicht funktionieren. Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
**Robo** Nee, diesmal wird das nicht funktionieren.
Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
**Du** Du meinst, `destructor`??
**Du** Du meinst, `destructor`??
**Robo** Nein, `constructor`. Ist verwirrend, ich weiß, aber so nennen die das hier.
**Robo** Nein, `constructor`. Ich weiß das ist verwirrend,
aber die nennen das hier so weil man die Aussage aus mehreren Teilen
konstruieren kann.
"
"
HiddenHint (A : Prop) (hA : A) : A =>
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*.
**Robo** Schau mal, das ist Zauberpapier.
Jetzt haben wir auf einmal zwei Beweisziele.
Hier ist dast Ziel `{A}`.
Ich glaube, Du weißt schon, wie man die jeweils erreicht.
Die Ziele stehen ja jeweils in den *Annahmen*.
"
"
Conclusion
Conclusion
@ -40,7 +50,8 @@ Conclusion
Ihm scheinen diese Fragen inzwischen Spaß zu machen.
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!
**Robo** Meinst Du, dieser Hebel, an dem \"Editor mode\" steht, ist echt?
"Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$."
""
(A B : Prop) (hA : A) : A ∨ (¬ B) := by
(A B : Prop) (hA : A) : A ∨ (¬ B) := by
left
left
assumption
assumption
@ -25,16 +25,18 @@ Hint (A B : Prop) (hA : A) : A ∨ (¬ B) =>
"
"
**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
**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.
**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?
**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?
"
"
Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
Hint (A B : Prop) (hA : A) : ¬ B =>
"
"
**Robo** Wusst gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
"Angenommen \"$A$ oder ($A$ und $B$)\" wahr ist, zeige, dass $A$ wahr ist."
(A B : Prop) (h : (A ∧ B) ∨ A) : A := by
(A B : Prop) (h : A ∨ (A ∧ B)) : A := by
rcases h with h | h
rcases h with h | h
assumption
rcases h with ⟨h₁, h₂⟩
rcases h with ⟨h₁, h₂⟩
assumption
assumption
assumption
Hint (A B : Prop) (h : A ∨(A ∧ B)) : A =>
Hint (A B : Prop) (h :(A ∧ B)∨ A) : A =>
"
"
**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** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
wie die Klammern gesetzt sind. Irre…
**Du** Ah ich sehe, also `({A} ∧ {B}) ∨ {A}`!
**Robo** Lass ihnen doch ihren Spaß. Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten weiterfliegen.
**Du** Ich glaube den ganzen Zircus hier langsam nicht mehr:
Zuerst ein \"Und\" im Ziel, dann \"Und\" in der Annahme, dann \"Oder\" im Ziel und jetzt
\"Oder\" in der Annahme, 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`.
**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`.
"
"
-- -- TODO: This also triggers later under the assumptions
-- -- `(A : Prop) (B : Prop) (h₁ : A) (h₂ : B) : A`
-- -- Could we do something about that?
-- Hint (A : Prop) (B : Prop) (h : A) : A =>
-- "
-- **Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
-- Einmal unter Annahme der linken Seite `{A}`,
-- und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
-- sei wahr.
-- "
Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
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`.
**Robo**
Jetzt musst Du Dein Ziel zweimal beweisen:
Einmal unter Annahme der linken Seite `{A} ∨ {B}`,
und einmal unter Annahme der rechten Seite `{A}`.
Hier haben nehmen wir an, die linke Seite
sei wahr.
"
"
HiddenHint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
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 `\\<>`.
**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
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?
"**Du** Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele…
Kannst Du mir vorher noch einmal kurz alles Leansch zusammenfassen,
das Du mir bis hierher beigebracht hast?
Robo straht überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
Robo strahlt überglücklich. Noch *nie* warst Du so auf ihn angewiesen.
Jon Eugster
3 years ago