Durch eine unvorhergesehene und nicht-kanonische Singularität in der Raumzeit
bist Du ausversehen in ein Paralleluniversum gestolpert. Wie es aussieht, gibt es kein zurück.
Richte Dich besser darauf ein, hier bleiben und Dich zurechtzufinden zu müssen.
Gerade seid Ihr auf Königin *Logisindes* Planeten. Sie kommt ohne Umschweife zum Punkt:
Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu
sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt,
seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich
herumgesprochen, dass Du in Deinem früheren Universum Mathematiker warst. Du wirst hier
keine Ruhe finden, solange Du nicht lernst, ihren unablässigen Wissensdurst zu stillen.
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.
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.
----
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 sie kritzelt etwas auf ein Stück Papier: oben ein paar Annahmen, unten eine Schlussfolgerung.
Dazwischen sollst Du offenbar einen Beweis eintragen.
@ -44,7 +25,9 @@ Statement ""
Hint (A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
"**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint sie: `A`, `B` und `C` sind irgendwelche Aussagen (*propositions*). Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
"**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
`{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
@ -59,7 +42,9 @@ Hint (A B C : Prop) :
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
"
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$?
@ -21,7 +22,8 @@ Statement "" :
rfl
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 => "
**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.
@ -35,7 +37,8 @@ Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
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:
"
Statement
"Sei $A$ eine Aussage und angenommen man hat einen Beweis für `False`.
Zeige, dass daraus $A$ folgt."
Statement ""
(A : Prop) (h : False) : A := by
contradiction
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.
**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?
**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
@ -39,7 +41,8 @@ Conclusion
**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
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?
**Robo** Ich sehe, du hast langsam den Dreh raus.
"
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
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 =>
"
**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`??
**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 =>
"
**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
@ -40,7 +50,8 @@ Conclusion
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
left
assumption
@ -25,16 +25,18 @@ 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.
**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 ∨ (A ∧ B)) : A := by
Statement ""
(A B : Prop) (h : (A ∧ B) ∨ A) : A := by
rcases h with h | h
assumption
rcases h with ⟨h₁, h₂⟩
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 …`?
**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 =>
"
**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 =>
"
**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
"**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.
Marcus Zibrowius
3 years ago