From b33febfaddb62153b65479c56521ab0591027536 Mon Sep 17 00:00:00 2001 From: Marcus Zibrowius Date: Sun, 5 Mar 2023 18:43:59 +0100 Subject: [PATCH 1/4] story line for planet 1 --- .../Levels/Proposition/L00_Tauto.lean | 63 +++++++---- .../TestGame/Levels/Proposition/L01_Rfl.lean | 25 ++-- .../Levels/Proposition/L02_Assumption.lean | 45 ++++---- .../Levels/Proposition/L03_Assumption.lean | 28 +++-- .../TestGame/Levels/Proposition/L04_True.lean | 32 +++--- .../TestGame/Levels/Proposition/L05_Not.lean | 26 +++-- .../Levels/Proposition/L06_False.lean | 31 +++-- .../Levels/Proposition/L07_ContraNotEq.lean | 21 +++- .../Levels/Proposition/L08_Contra.lean | 16 +-- .../TestGame/Levels/Proposition/L09_And.lean | 98 ++++------------ .../TestGame/Levels/Proposition/L10_And.lean | 107 +++++------------- .../TestGame/Levels/Proposition/L11_Or.lean | 26 +++-- .../TestGame/Levels/Proposition/L12_Or.lean | 87 +++++++++++--- .../Levels/Proposition/L13_Summary.lean | 99 +++++----------- 14 files changed, 336 insertions(+), 368 deletions(-) diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 3c1fe38..10ff90a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -5,46 +5,61 @@ Game "TestGame" World "Proposition" Level 1 -Title "Atomatisierung" +Title "Automatisierung" Introduction " -Willkommen zum Lean-Crashkurs wo du lernst wie man mathematische Beweise vom Computer -unterstützt und verifiziert schreiben kann. +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. -In der *mittleren Spalte* siehst den Status des Beweis. Unter **Main Goal** steht, was du im Moment -beweisen musst. Falls es mehrere Dinge zu beweisen gibt, werden alle weiteren darunter unter **Further Goals** -aufgelistet, diese musst du dann später auch noch zeigen. +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. -Ein Beweis besteht aus mehreren **Taktiken**. Das sind einzelne Beweisschritte, ähnlich wie -man auf Papier argumentieren würde. Manche Taktiken können ganz konkret etwas kleines machen, -andere sind stark und lösen ganze Probleme automatisiert. Du findest die Taktiken in der *rechten Spalte*. +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. -Wenn der Beweis komplett ist, erscheint \"Level completed! 🎉\". +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. -Als erste kleine Vorschau, dass Lean auch vieles automatisch kann, gibt es eine -Taktik `tauto`, die alle wahren Aussagen der Prädikaten-Logik beweisen kann. +---- -Dieses Beispiel würde von Hand etwas Zeit in Anspruch nehmen. Lean ist da viel schneller. +Gerade seid Ihr auf Königin Logisindes Planeten. Sie kommt ohne Umschweife zum Punkt: -Gib also `tauto` gefolgt von Enter ⏎ ein um deinen ersten automatisierten Beweis zu führen! +**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. " Statement -"Zeige dass folgende Aussage wahr ist: - -$$ - \\neg ((\\neg B\\textrm{ oder }\\neg C) \\textrm{ oder } (A \\Rightarrow B)) \\Rightarrow - (\\neg A \\textrm{ oder } B) \\textrm{ und } \\neg (B \\textrm{ und } C) -$$ -" (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by tauto -Hint (A B C : Prop): ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) => -"Gib `tauto` ein und drücke Enter ⏎." -Conclusion "" +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? + +**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen. + +**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie. + +**Du** Ernsthaft? + +**Robo** Ja. Schreib einfach `tauto`. + +**Robo** Mach schon … +" + +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. +" NewTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 34d8ce0..a4eda42 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -8,24 +8,27 @@ Title "Aller Anfang ist... ein Einzeiler?" Introduction " -Jetzt gehen wir aber einen Schritt zurück und lernen, wie man konkret mit Lean arbeitet, -damit du verstehst, was `tauto` hinter der Kulisse macht. +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. -Eine der grundlegendsten Taktiken ist `rfl` (für \"reflexivity\"), welche dazu da ist, -ein Goal der Form $X = X$ zu schließen. +**Untertan** Warum ist $42 = 42$? + +Du schaust ihn fassungslos an. +Er schreibt es Dir wieder auf. " Statement -"Zeige $ 42 = 42 $." : 42 = 42 := by + 42 = 42 := by rfl --- Hint : 42 = 42 => --- "Die Taktik `rfl` beweist ein Goal der Form `X = X`." - -HiddenHint : 42 = 42 => -"Die beiden Seiten dieser Gleichung sind identisch, also gib `rfl` ein und drücke Enter ⏎" +Hint +" +**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`. +" -Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"." +Conclusion +" +**Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl … +" NewTactics rfl DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index d09bd9a..856ea83 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -8,42 +8,37 @@ Title "Annahmen" Introduction " -Um spannendere Aussagen zu formulieren brauchen wir Objekte und Annahmen über diese -Objekte. +Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste nach vorne. Es ist schüchtern und schreibt bloß. +" -Hier zum Beispiel haben wir eine natürliche Zahl $n$ und eine Annahme $1 < n$, die -wir $h$ nennen. +Statement + (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by + assumption -Wenn das Goal genau einer Annahme entspricht, kann man diese mit `assumption` beweisen. +Hint +" +**Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl. +**Du** Warum schreibt er dann nicht `n ∈ ℕ`?? -**Note:** -Wenn du den \"Editor mode\" umstellst, kannst du sehen, wie die Aufgabe in vollständigem -Lean-Code geschrieben wird. Hier sieht das wie folgt aus: +**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. -``` -example (n : ℕ) (h : 1 < n) : 1 < n := by - sorry -``` +**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`. -Also +**Du** Aber das war doch gerade eine der Annahmen. -``` -example [Objekte/Annahmen] : [Aussage] := by - [Beweis] -``` -" +**Robo** Ja, stimmt. -Statement -"Angenommen $1 < n$. Dann ist $1 < n$." - (n : ℕ) (h : 1 < n) : 1 < n := by - assumption +**Du** ??? -HiddenHint (n : ℕ) (h : 1 < n) : 1 < n => - "`assumption` sucht nach einer Annahme, die dem Goal entspricht." +**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`. +" -Conclusion "" +Conclusion +" +**Untertan** Ja richtig! Wenn Ihr nur wüsstet, was ich mir an dieser Frage schon den Kopf zerbrochen habe! +" NewTactics assumption DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index c7ba685..583783c 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -9,23 +9,31 @@ Title "Logische Aussagen" Introduction " -Eine allgemeine logische Aussage definiert man mit `(A : Prop)`. - -Damit sagt man noch nicht, ob die Aussage $A$ wahr oder falsch ist. -Mit einer Annahme `(hA : A)` nimmt man an, dass $A$ wahr ist: -`hA` ist sozusagen ein Beweis von $A$. +Ein dritter Untertan kommt mit folgendem Problem. " Statement -"Sei $A$ eine logische Aussage und sei `hA` ein Beweis für $A$. -Zeige, dass $A$ wahr ist." - (A : Prop) (hA : A) : A := by + (A : Prop) (hA : A) : A := by assumption + +Hint +" +**Robo** Hier bedeutet `A : Prop` wieder, dass `A` irgendeine Aussage ist. + Und `hA` ist eine Name für die Annahme, dass `A` wahr ist. + +**Du** Und unter dieser Annahme sollen wir jetzt `A` beweisen? + +**Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder? +" + HiddenHint (A : Prop) (hA : A) : A => -"Auch hier kann `assumption` den Beweis von `{A}` finden." +"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. Also wird `asumption` auch wieder funktionieren." -Conclusion "" +Conclusion +" +**Untertan** Das ging ja schnell. Super! Vielen Dank. +" NewTactics assumption DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index 352ce3e..32959b8 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -8,30 +8,30 @@ Title "True/False" Introduction " -Unter den logischen Aussagen gibt es zwei spezielle Aussagen: +Der nächste Untertan in der Reihe ist ein Schelm. +" -- `True` ist eine Aussage, die immer und bedingungslos wahr ist. -- `False` ist eine Aussage, die nie wahr ist. +Statement +True := by + trivial -Die Aussage `True` werden wir kaum brauchen, die Aussage `False` ist jedoch wichtig, sie -repräsentiert einen Widerspruch. Mehr dazu in den nächsten Levels. +Hint +" +**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist. -**Beachte**, dass beide gross geschrieben werden. In Lean gibt es auf das klein geschriebene -`true` und `false`, diese sind aber etwas anderes (Typ `Bool` und nicht `Prop`) -und werden erst mal nicht gebraucht. +**Du** Und was genau ist dann zu beweisen? -Wir können `True` aus dem nichts mit der Taktik `trivial` beweisen. +**Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben. +" -*Bemerkung: Was die Taktik `trivial` kann und nicht kann bleibt in diesem Spiel ein bisschen eine Blackbox, -aber manchmal ist sie nützlich.* +Conclusion " +**Schelm** Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid … -Statement -"Zeige, dass die logische Aussage `True` immer wahr ist." : -True := by - trivial +**Du** (zu Robo)** Können wir nicht einfach immer dieses `trivial` verwenden? Wie in einer Mathe-Vorlesung? -Conclusion "" +**Robo** Nein, das `trivial` hier hat eine ziemlich spezielle Bedeutung. Das funktioniert nur in einer Handvoll Situationen. +" NewTactics trivial DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index 1030b90..db89e0b 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -8,18 +8,30 @@ Title "Not" Introduction " -Wenn eine Aussage `(A : Prop)` wahr oder falsch ist, dann ist die Umkehrung \"nicht $A$\", -geschrieben `¬A` (`\\not`), gegenteilig falsch oder wahr. - -Da die Aussage `False` nie wahr ist, ist die Aussage `¬False` immer wahr, genau wie `True`. +Der Schelm hat noch eine Schwester dabei. " Statement -"Zeige dass die Aussage `¬False` immer wahr ist." : - ¬False := by + ¬False := by trivial -Conclusion "" +Hint +" + **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist `¬A` falsch, und umgekehrt. + + **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist? + + **Robo** Ja, richtig. + + **Du** Ist das jetzt nicht doch wieder trivial? + + **Robo** Probier mal! +" + +Conclusion +" +Die Schwester lacht und eilt ihrem Bruder hinterher. +" NewTactics trivial DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index b81feb4..3a181ac 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -10,11 +10,7 @@ Title "Widerspruch beweist alles." Introduction " -Die Aussage `False` ist für uns wichtiger als `True`, da ein Beweis der falschen Aussage -`False` einen Widerspruch repräsentiert. -Hat man einen Widerspruch, kann man daraus mit der Taktik `contradiction` alles beweisen. - -Der erste Widerspruch, den `contradiction` erkennt, ist ein Beweis von `False`. +Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem: " Statement @@ -23,9 +19,28 @@ Zeige, dass daraus $A$ folgt." (A : Prop) (h : False) : A := by contradiction -HiddenHint (A : Prop) (h : False) : A => -"Wenn man einen Beweis von `False` hat, kann man mit `contradiction` das Goal beweisen, -unabhängig davon, was das Goal ist." +Hint +" +**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`. + +**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`. +" + +Conlusion +"Der erste Querulant ist offenbar zufrieden. + +**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. +" NewTactics contradiction DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index d2d6309..03f3c07 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -12,18 +12,29 @@ Title "Widerspruch" Introduction " -Zweitens kann `contradiction` auch aus Annahmen der Form `a ≠ a` einen Widerspruch finden. - -*Bemerkung:* Das Ungleichzeichen `≠` (`\\ne`) sollte immer als `¬(· = ·)` gelesen werden. +Auftritt zweiter Querulant. " Statement -"Sei $n$ eine natürliche Zahl die ungleich sich selbst ist. Dann ist $n = 37$." - (n : ℕ) (h : n ≠ n) : n = 37 := by + (n : ℕ) (h : n ≠ n) : n = 37 := by contradiction +Hint +" +**Du** Ist `n ≠ n` nicht auch ein Widerspruch? + +**Robo** Probiers mal! +" + Conclusion " +**Du** Ja, scheint funktioniert zu haben. + +**Du** Aber irgendwie kommt mir das immer noch ein wenig suspekt vor. Jetzt habe ich bewiesen, dass eine beliebige natürliche Zahl gleich 37 ist? + +**Robo** Nein, nicht doch. Nur eine beliebige Zahl, die ungleich sich selbst ist, ist gleich 37. Und gleich 38, und gleich 39, … + +**Du** Ok, ok, verstehe. " NewTactics contradiction diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index dca804b..65602af 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -12,21 +12,21 @@ Title "Widerspruch" Introduction " -Drittens kann die Taktik `contradiction` auch einen Widerspruch finden, -wenn zwei Annahmen genaue Gegenteile voneinander sind. -Also z.B. `(h : A)` und `(g : ¬ A)`. - -Da `≠` als `¬(· = ·)` gelesen wird, gilt dasselbe für Annahmen `(h : a = b)` und `(g : a ≠ b)`. +Auftritt dritter Querulant. " Statement -"Sei $n$ eine natürliche Zahl die sowohl gleich als auch ungleich `10` ist. -Zeige, dass daraus $n = 42$ folgt. (oder, tatsächlich $n = x$ für jedes beliebige $x$)" - (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by + (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by contradiction +Hint +" +**Du** Wieder ein Widerspruch in den Annahmen? +" + 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. " NewTactics contradiction diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 638227d..63564bd 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -11,95 +11,37 @@ Title "Und" Introduction " -Zusätzlich zur Verneinung (`¬`) können wir logische Aussagen auch mit UND (`∧`) und ODER (`∨`) kombinieren. - -In einer Mathevorlesung würde man vielleicht `A ∧ B` als Tupel `⟨A, B⟩` definieren. In Lean -sind dies *Strukturen*. Eine Struktur hat mehrere Felder, in diesem Fall zwei, -nämlich die linke und die rechte Seite. - -Will man eine Aussage `A ∧ B` beweisen (im Goal), dann kann man diese mit der Taktik -`constructor` in die einzelnen Felder aufteilen. +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 assumption assumption -HiddenHint (A : Prop) (B : Prop) (hA : A) (hB : B) : A ∧ B => - "`constructor` zerlegt die Struktur in Einzelteile." - -HiddenHint (A : Prop) (hA : A) : A => - "Du hast einen Beweis dafür in den *Annahmen*." - -NewTactics constructor -DisabledTactics tauto - --- Statement --- "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$." --- (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by --- constructor --- intro h --- rcases h with ⟨h₁, h₂⟩ --- constructor --- assumption --- apply h₂ --- assumption --- intro h --- rcases h with ⟨h₁, h₂⟩ --- constructor --- assumption --- intro --- assumption - --- Hint (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => --- "`↔` oder `∧` im Goal kann man mit `constructor` zerlegen." - --- Hint (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => --- "Hier würdest du mit `intro` die Implikation angehen. - --- (Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf --- das UND in der Implikationsannahme)" - --- -- if they don't use `intro ⟨_, _⟩`. --- Hint (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => --- "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen." - --- HiddenHint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => --- "Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?" - --- -- Rückrichtung --- Hint (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => --- "Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$ --- Da hilft `intro`. - --- (auch hier kann man wieder mit `intro ⟨ha, hb⟩` gleich noch die Premisse zerlegen.)" - - - - --- -- if they don't use `intro ⟨_, _⟩`. --- Hint (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => --- "Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen." - --- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => --- "Wieder in Einzelteile zerlegen..." +Hint +" +**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? --- Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => --- "Immer das gleiche ... noch mehr zerlegen." +**Robo** Nee, diesmal wird das nicht funktionieren. Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`. --- -- Hint (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => --- -- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen, --- -- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`). +**Du** Du meinst, `destructor`?? --- -- Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht, --- -- dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen, --- -- dass `B` wahr ist." +**Robo** Nein, `constructor`. Ist verwirrend, ich weiß, aber so nennen die das hier. +" +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*. +" +Conclusion +" +**Robo** Super! --- -- TODO +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! +" --- Tactics apply rcases --- Tactics assumption +NewTactics constructor +DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 3237428..97a2944 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -11,96 +11,41 @@ Title "Und" Introduction " -Hat man ein UND `(h : A ∧ B)` in den Annahmen, möchte man normalerweise die einzelnen Felder -(linke/rechte Seite) einzeln verwenden. Dazu hat man zwei Möglichkeiten: - -1. Mit `h.left` und `h.right` (oder `h.1` und `h.2`) kann man die Felder direkt auswählen. -2. Mit `rcases h with ⟨h₁, h₂⟩` kann man die Struktur `h` zerlegen und man erhält zwei - separate Annahmen `(h₁ : A)` und `(h₂ : B)` - -Die Klammern `⟨·,·⟩` sind `\\<` und `\\>` oder `\\<>` als Paar. +Langsam wird die Schlange kürzer. Die nächste Formalosophin hat folgendes Anliegen: " -Statement "Benutze `rcases` um das UND in `(h : A ∧ (B ∧ C))` zu zerlegen und beweise, dass $B$ wahr ist." - (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by +Statement + (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by rcases h with ⟨_, ⟨g , _⟩⟩ assumption -HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B => -"Du kannst mit `rcases` auch verschachtelt mehrere Strukturen in einem Schritt zerlegen: -`rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`." - -HiddenHint (A : Prop) (hA : A) : A => - "Du hast einen Beweis dafür in den *Annahmen*." - -NewTactics rcases -DisabledTactics tauto - --- Statement --- "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$." --- (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by --- constructor --- intro h --- rcases h with ⟨h₁, h₂⟩ --- constructor --- assumption --- apply h₂ --- assumption --- intro h --- rcases h with ⟨h₁, h₂⟩ --- constructor --- assumption --- intro --- assumption - --- Hint (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B => --- "`↔` oder `∧` im Goal kann man mit `constructor` zerlegen." - --- Hint (A : Prop) (B : Prop) : A ∧ (A → B) → A ∧ B => --- "Hier würdest du mit `intro` die Implikation angehen. - --- (Experten können mit `intro ⟨h₁, h₂⟩` im gleichen Schritt noch ein `rcases` auf --- das UND in der Implikationsannahme)" - --- -- if they don't use `intro ⟨_, _⟩`. --- Hint (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B => --- "Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen." - --- HiddenHint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B => --- "Wie wär's mit `apply`? Hast du ne Implikation, die anwendbar ist?" - --- -- Rückrichtung --- Hint (A : Prop) (B : Prop) : A ∧ B → A ∧ (A → B) => --- "Das Goal ist ne Implikation $\\ldots \\Rightarrow \\ldots$ --- Da hilft `intro`. - --- (auch hier kann man wieder mit `intro ⟨ha, hb⟩` gleich noch die Premisse zerlegen.)" - - - - --- -- if they don't use `intro ⟨_, _⟩`. --- Hint (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) => --- "Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` zerlegen." - --- Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B => --- "Wieder in Einzelteile zerlegen..." - --- Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : A ∧ (A → B) => --- "Immer das gleiche ... noch mehr zerlegen." +Hint +" +**Du** Jetzt müssen wir wohl die Annahme de-konstruieren. --- -- Hint (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B => --- -- "Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen, --- -- wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`). +**Robo** Ja, genau. Das geht am einfachsten mit `rcases h with ⟨h₁, h₂⟩`. --- -- Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht, --- -- dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen, --- -- dass `B` wahr ist." +**Du** Moment, wie schreib ich *das* denn hier auf? +**Robo** Die bleiden Klammern schreibst Du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`. + Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen für `h₁` und `h₂`, zum Beispiel `rcases h with ⟨hA, hBC⟩` +" +Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B => +" +**Robo** Das sieht doch schon besser aus! Gleich nochmal! +" --- -- TODO +HiddenHint (A : Prop) (hA : A) : A => +" +**Robo** Du hast einen Beweis dafür in den *Annahmen*. +" +Conclusion +" +**Robo** Du hättest übrigens auch direkt schreiben können `rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`. +" --- Tactics apply rcases --- Tactics assumption +NewTactics rcases +DisabledTactics tauto + diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index deeb72e..48ac21a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -12,10 +12,7 @@ Title "Oder" Introduction " -Das logische ODER `A ∨ B` (`\\or`) funktioniert ein wenig anders als das UND. - -Wenn das Goal ein `∨` ist kann man mit den Taktiken `left` oder `right` entscheiden, -welche Seite man beweisen möchte. +Der nächste bitte … " Statement @@ -24,11 +21,26 @@ Statement left assumption -HiddenHint (A : Prop) (B : Prop) (hA : A) : A ∨ (¬ B) => -"Entscheide dich, `right` oder `left`?" +Hint +" +**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! + +**Robo** Mit `left` bzw. `right'. Ist doch logisch, oder? +" Hint (A : Prop) (B : Prop) (hA : A) : ¬ B => -"Sackgasse. Probier's nochmals." +" +**Robo** Wusst gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal. +" + +Conclusion +" +Auch dieser Formalosoph zieht zufrieden von dannen. +" NewTactics left right assumption DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index 272dc84..a7785df 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -15,19 +15,7 @@ Title "Oder" Introduction " -Wenn man hingegen ein ODER `(h : A ∨ B)` in den Annahmen hat, kann man dieses -ähnlich wie beim UND mit `rcases h` aufteilen. - -**Wichtig:** der Syntax dafür ist `rcases h with h | h`. Das \"`h | h`\" bedeutet, dass -wir in beiden Fälle (linke oder rechte Seite wahr) diese Seite wieder `h` nennen wollen. - -Der Unterschied ist, dass man beim UND eine Annahme in zwei Einzelteile zerlegt (mit `⟨h₁, h₂⟩`). -Beim ODER hingegen, kriegt man stattdessen zwei *Goals*, nämlich eines wo man annimmt, -die linke Seite sei wahr und eines wo man annimmt, rechts sei wahr. - -*Notiz:* UND hat stärkere Bindung als ODER, und beide binden rechts, d.h. -`A ∨ B ∧ C` wird als `A ∨ (B ∧ C)` gelesen. Zudem binden beide nach rechts, -also `A ∨ B ∨ C` ist `A ∨ (B ∨ C)`. +Der nächste bitte … " Statement @@ -38,11 +26,78 @@ Statement rcases h with ⟨h₁, h₂⟩ assumption -HiddenHint (A : Prop) (B : Prop) (h : A ∨ (A ∧ B)) : A => -"Als erstes kannst du das ODER in den Annahmen mit `rcases h with h | h` zerlegen." +Hint +" +**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 …`? + +**Robo** Ja, aber diesmal nicht `rcases h with ⟨h₁, h₂⟩`, sondern `rcases h with h | h`. +" Hint (A : Prop) (B : Prop) (h : A ∧ B) : A => -"Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen." +" +**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** Na klar, schau her! + +## Notationen / Begriffe + +| | Beschreibung | +|:--------------|:-------------------------------------------------------------------------| +| *Goal* | Was aktuell zu beweisen ist. | +| *Annahme* | Objekte & Resultate, die man zur Verfügung hat. | +| *Taktik* | Befehl im Beweis. Entspricht einem Beweisschritt. | +| `ℕ` | Typ aller natürlichen Zahlen. | +| `0, 1, 2, …` | Explizite natürliche Zahlen. | +| `=` | Gleichheit. | +| `≠` | Ungleichheit. Abkürzung für `¬(·=·)`. | +| `Prop` | Typ aller logischen Aussagen. | +| `True` | Die logische Aussage `(True : Prop)` ist bedingungslos wahr. | +| `False` | Die logische Aussage `(False : Prop)` ist bedingungslos falsch. | +| `¬` | Logische Negierung. | +| `∧` | Logisch UND. | +| `∨` | Logisch ODER. | +| `(n : ℕ)` | Eine natürliche Zahl. | +| `(A : Prop)` | Eine logische Aussage. | +| `(ha : A)` | Ein Beweis, dass die logische Aussage `(A : Prop)` wahr ist. | +| `(h : A ∧ B)` | Eine Annahme, die den Namen `h` bekommen hat. | +| `⟨·,·⟩` | Schreibweise für Struktur mit mehreren Feldern (kommt später im Detail). | +| `h.1, h.2, …` | Die einzelnen Felder der Stuktur. Auch `h.[Name des Feldes]` | + + +## Taktiken + +Die Worte, die Du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`. Hier sind alle Taktiken, die wir auf diesem Planeten gebraucht haben: + +| | Taktik | Beispiel | +|:---|:--------------------------|:--------------------------------------------------| +| 1 | `rfl` | Beweist `A = A`. | +| 2 | `assumption` | Sucht das Goal in den Annahmen. | +| 3 | `contradiction` | Sucht einen Widerspruch. | +| 4 | `trivial` | Kombiniert die obigen drei Taktiken (und mehr). | +| 5 | `constructor` | Teilt ein UND im Goal auf. | +| 6 | `left`/`right` | Beweist eine Seite eines ODER im Goal. | +| 7ᵃ | `rcases h with ⟨h₁, h₂⟩` | Teilt ein UND in den Annahmen auf. | +| 7ᵇ | `rcases h with h \\| h` | Teilt ein ODER in den Annahmen in zwei Fälle auf. | + +**Du** Woher weißt Du das eigentlich alles? + +**Robo** Keine Ahnung. War, glaube ich, vorinstalliert. +" + NewTactics assumption rcases DisabledTactics tauto diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index 00f1f86..19f5dfc 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -12,75 +12,13 @@ Title "Zusammenfassung" Introduction " -Damit bist du am Ende der ersten Lektion angekommen. Hier ein Überblick über alle Begriffe, -Notationen, und Taktiken, die in diesem Kapitel -eingeführt wurden. Danach folgt eine Abschlussaufgabe. - -## Notationen / Begriffe - -| | Beschreibung | -|:--------------|:-------------------------------------------------------------------------| -| *Goal* | Was aktuell zu beweisen ist. | -| *Annahme* | Objekte & Resultate, die man zur Verfügung hat. | -| *Taktik* | Befehl im Beweis. Entspricht einem Beweisschritt. | -| `ℕ` | Typ aller natürlichen Zahlen. | -| `0, 1, 2, …` | Explizite natürliche Zahlen. | -| `=` | Gleichheit. | -| `≠` | Ungleichheit. Abkürzung für `¬(·=·)`. | -| `Prop` | Typ aller logischen Aussagen. | -| `True` | Die logische Aussage `(True : Prop)` ist bedingungslos wahr. | -| `False` | Die logische Aussage `(False : Prop)` ist bedingungslos falsch. | -| `¬` | Logische Negierung. | -| `∧` | Logisch UND. | -| `∨` | Logisch ODER. | -| `(n : ℕ)` | Eine natürliche Zahl. | -| `(A : Prop)` | Eine logische Aussage. | -| `(ha : A)` | Ein Beweis, dass die logische Aussage `(A : Prop)` wahr ist. | -| `(h : A ∧ B)` | Eine Annahme, die den Namen `h` bekommen hat. | -| `⟨·,·⟩` | Schreibweise für Struktur mit mehreren Feldern (kommt später im Detail). | -| `h.1, h.2, …` | Die einzelnen Felder der Stuktur. Auch `h.[Name des Feldes]` | - - -Im weiteren haben wir gesehen, wie wir in Lean Aufgaben formulieren : - -``` -example [Annahmen] : [Aussage] := by - [Beweis] -``` - -## Taktiken - -Für die Beweise haben wir verschiedene Taktiken kennengelernt. - -| | Taktik | Beispiel | -|:---|:--------------------------|:--------------------------------------------------| -| 1 | `rfl` | Beweist `A = A`. | -| 2 | `assumption` | Sucht das Goal in den Annahmen. | -| 3 | `contradiction` | Sucht einen Widerspruch. | -| 4 | `trivial` | Kombiniert die obigen drei Taktiken (und mehr). | -| 5 | `constructor` | Teilt ein UND im Goal auf. | -| 6 | `left`/`right` | Beweist eine Seite eines ODER im Goal. | -| 7ᵃ | `rcases h with ⟨h₁, h₂⟩` | Teilt ein UND in den Annahmen auf. | -| 7ᵇ | `rcases h with h \\| h` | Teilt ein ODER in den Annahmen in zwei Fälle auf. | - - -Zum Schluss gibt es noch eine kleine Übungsaufgabe: - -Benutze alle vier Methoden mit UND und ODER -umzugehen um folgende Aussage zu beweisen. - -| (Übersicht) | Und (`∧`) | Oder (`∨`) | -|-------------|:-------------------------|:------------------------| -| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` | -| Goal | `constructor` | `left`/`right` | +Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vorherigen. " -- Note: The other direction would need arguing by cases. Statement -"Angenommen $A \\lor (B \\land C)$ ist wahr, zeige dass -$(A \\lor B) \\land (A \\lor C)$ wahr ist." - (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by + (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by constructor rcases h with h | h left @@ -95,32 +33,49 @@ $(A \\lor B) \\land (A \\lor C)$ wahr ist." right assumption +Hint +" +**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. + +| (Übersicht) | Und (`∧`) | Oder (`∨`) | +|-------------|:-------------------------|:------------------------| +| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` | +| Goal | `constructor` | `left`/`right` | +" + HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => -"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." +"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => -"Das `∧` im Goal kann mit `constructor` zerlegt werden." +"**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => -"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." +"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => -"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." +"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => -"Das `∨` in der Annahme kann mit `rcases h with h | h` zerlegt werden." +"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) => -"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." +"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen." HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) => -"Das `∧` in der Annahme kann mit `rcases h with ⟨h₁, h₂⟩` zerlegt werden." +"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen." -- TODO: Hint nur Anhand der Annahmen? HiddenHint (A : Prop) (B : Prop) : A ∨ B => -"`left` oder `right`?" +"**Robo** `left` oder `right`?" + +Conclusion +" +**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. +" NewTactics left right assumption constructor rcases rfl contradiction trivial DisabledTactics tauto From 2d9627920387619f1bccaff70d83d03f5bffe2be Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 6 Mar 2023 09:46:22 +0100 Subject: [PATCH 2/4] make it compile --- .../Levels/Proposition/L00_Tauto.lean | 26 ++++++++----------- .../TestGame/Levels/Proposition/L01_Rfl.lean | 11 +++----- .../Levels/Proposition/L02_Assumption.lean | 16 +++++------- .../Levels/Proposition/L03_Assumption.lean | 17 +++++------- .../TestGame/Levels/Proposition/L04_True.lean | 17 +++++------- .../TestGame/Levels/Proposition/L05_Not.lean | 18 ++++++------- .../Levels/Proposition/L06_False.lean | 8 +++--- .../Levels/Proposition/L07_ContraNotEq.lean | 6 ++--- .../Levels/Proposition/L08_Contra.lean | 4 +-- .../TestGame/Levels/Proposition/L09_And.lean | 4 +-- .../TestGame/Levels/Proposition/L10_And.lean | 12 +++------ .../TestGame/Levels/Proposition/L11_Or.lean | 8 +++--- .../TestGame/Levels/Proposition/L12_Or.lean | 10 +++---- .../Levels/Proposition/L13_Summary.lean | 8 +++--- 14 files changed, 71 insertions(+), 94 deletions(-) diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 10ff90a..9ce1753 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -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 + tauto Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index a4eda42..2a19661 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -16,16 +16,13 @@ Du schaust ihn fassungslos an. Er schreibt es Dir wieder auf. " -Statement +Statement " +**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`. +" : 42 = 42 := by rfl -Hint -" -**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`. -" - -Conclusion +Conclusion " **Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl … " diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index 856ea83..97c797d 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -8,20 +8,15 @@ Title "Annahmen" Introduction " -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! " diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index 583783c..fe6ef22 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -12,27 +12,24 @@ Introduction Ein dritter Untertan kommt mit folgendem Problem. " -Statement - (A : Prop) (hA : A) : A := by - assumption - - -Hint -" +Statement " **Robo** Hier bedeutet `A : Prop` wieder, dass `A` irgendeine Aussage ist. Und `hA` ist eine Name für die Annahme, dass `A` wahr ist. -**Du** Und unter dieser Annahme sollen wir jetzt `A` beweisen? +**Du** Und unter dieser Annahme sollen wir jetzt `A` beweisen? **Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder? " + (A : Prop) (hA : A) : A := by + assumption + HiddenHint (A : Prop) (hA : A) : A => "Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. Also wird `asumption` auch wieder funktionieren." -Conclusion +Conclusion " -**Untertan** Das ging ja schnell. Super! Vielen Dank. +**Untertan** Das ging ja schnell. Super! Vielen Dank. " NewTactics assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index 32959b8..ff6d696 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -8,23 +8,20 @@ Title "True/False" Introduction " -Der nächste Untertan in der Reihe ist ein Schelm. +Der nächste Untertan in der Reihe ist ein Schelm. " -Statement -True := by - trivial - -Hint -" -**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist. +Statement " +**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist. **Du** Und was genau ist dann zu beweisen? **Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben. -" +" : +True := by + trivial -Conclusion +Conclusion " **Schelm** Wollte nur mal sehen, dass Ihr nicht auf den Kopf gefallen seid … diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index db89e0b..b3c56f7 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -11,24 +11,22 @@ Introduction Der Schelm hat noch eine Schwester dabei. " -Statement - ¬False := by - trivial - -Hint -" +Statement " **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist `¬A` falsch, und umgekehrt. - **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist? + **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist? - **Robo** Ja, richtig. + **Robo** Ja, richtig. **Du** Ist das jetzt nicht doch wieder trivial? **Robo** Probier mal! -" +" : + ¬False := by + trivial + -Conclusion +Conclusion " Die Schwester lacht und eilt ihrem Bruder hinterher. " diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 3a181ac..51855ae 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -19,11 +19,11 @@ Zeige, dass daraus $A$ folgt." (A : Prop) (h : False) : A := by contradiction -Hint +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? @@ -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`. " -Conlusion +Conclusion "Der erste Querulant ist offenbar zufrieden. **Du** War das jetzt ein Widerspruchsbeweis? diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index 03f3c07..81d3627 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -15,13 +15,13 @@ Introduction Auftritt zweiter Querulant. " -Statement +Statement "" (n : ℕ) (h : n ≠ n) : n = 37 := by contradiction -Hint +Hint (n : ℕ) (h : n ≠ n) : n = 37 => " -**Du** Ist `n ≠ n` nicht auch ein Widerspruch? +**Du** Ist `n ≠ n` nicht auch ein Widerspruch? **Robo** Probiers mal! " diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index 65602af..40190cf 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -15,11 +15,11 @@ Introduction Auftritt dritter Querulant. " -Statement +Statement "" (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 := by contradiction -Hint +Hint (n : ℕ) (h : n = 10) (g : (n ≠ 10)) : n = 42 => " **Du** Wieder ein Widerspruch in den Annahmen? " diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 63564bd..cd12ca7 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -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*. " -Conclusion +Conclusion " **Robo** Super! diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 97a2944..2d3bc4c 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -14,13 +14,7 @@ Introduction Langsam wird die Schlange kürzer. Die nächste Formalosophin hat folgendes Anliegen: " -Statement - (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by - rcases h with ⟨_, ⟨g , _⟩⟩ - assumption - -Hint -" +Statement " **Du** Jetzt müssen wir wohl die Annahme de-konstruieren. **Robo** Ja, genau. Das geht am einfachsten mit `rcases h with ⟨h₁, h₂⟩`. @@ -30,6 +24,9 @@ Hint **Robo** Die bleiden Klammern schreibst Du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`. Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen für `h₁` und `h₂`, zum Beispiel `rcases h with ⟨hA, hBC⟩` " + (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by + rcases h with ⟨_, ⟨g , _⟩⟩ + assumption Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B => " @@ -48,4 +45,3 @@ Conclusion NewTactics rcases DisabledTactics tauto - diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index 48ac21a..7d6ced3 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -21,13 +21,13 @@ Statement left assumption -Hint -" -**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? " diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index a7785df..919f127 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -15,7 +15,7 @@ Title "Oder" Introduction " -Der nächste bitte … +Der nächste bitte … " Statement @@ -26,13 +26,13 @@ Statement rcases h with ⟨h₁, h₂⟩ assumption -Hint +Hint (A B : Prop) (h : A ∨ (A ∧ B)) : 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** 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. **Robo** Na klar, schau her! diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index 19f5dfc..32879ce 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -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 From c35b66a0c674f7f2854211285379e4f9d4d78e66 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 6 Mar 2023 10:04:40 +0100 Subject: [PATCH 3/4] use hints for initial texts --- .../TestGame/Levels/Proposition/L00_Tauto.lean | 12 ++++++++---- .../TestGame/Levels/Proposition/L01_Rfl.lean | 8 +++++--- .../TestGame/Levels/Proposition/L02_Assumption.lean | 8 +++++--- .../TestGame/Levels/Proposition/L03_Assumption.lean | 9 +++++---- .../TestGame/Levels/Proposition/L04_True.lean | 10 ++++++---- .../TestGame/Levels/Proposition/L05_Not.lean | 11 ++++++----- .../TestGame/Levels/Proposition/L10_And.lean | 10 ++++++---- 7 files changed, 41 insertions(+), 27 deletions(-) diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 9ce1753..0f18dc5 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -37,7 +37,14 @@ Dazwischen sollst Du offenbar einen Beweis eintragen. Du siehst Robo hilflos an. " -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? +Statement "" + (A B C : Prop) : + ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by + tauto + +Hint (A B C : Prop) : + ¬((¬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? **Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen. @@ -49,9 +56,6 @@ Statement "**Robo** Das ist ganz einfach. Mit `A B C : Prop` meint er: `A`, ` **Robo** Mach schon … " - (A B C : Prop) : - ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by - tauto Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 2a19661..a519591 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -16,12 +16,14 @@ Du schaust ihn fassungslos an. Er schreibt es Dir wieder auf. " -Statement " -**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`. -" : +Statement "" : 42 = 42 := by rfl +Hint : 42 = 42 => " +**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist. Probier mal `rfl`. +" + Conclusion " **Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl … diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean index 97c797d..169583c 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -11,7 +11,11 @@ Introduction 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 " +Statement "" + (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by + assumption + +Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => " **Robo** `n : ℕ` bedeutet, `n` ist eine natürliche Zahl. **Du** Warum schreibt er dann nicht `n ∈ ℕ`?? @@ -28,8 +32,6 @@ Statement " **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 " diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index fe6ef22..1db00a7 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -12,7 +12,11 @@ Introduction Ein dritter Untertan kommt mit folgendem Problem. " -Statement " +Statement "" + (A : Prop) (hA : A) : A := by + assumption + +Hint (A : Prop) (hA : A) : A => " **Robo** Hier bedeutet `A : Prop` wieder, dass `A` irgendeine Aussage ist. Und `hA` ist eine Name für die Annahme, dass `A` wahr ist. @@ -20,9 +24,6 @@ Statement " **Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder? " - (A : Prop) (hA : A) : A := by - assumption - HiddenHint (A : Prop) (hA : A) : A => "Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. Also wird `asumption` auch wieder funktionieren." diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index ff6d696..09e2ddf 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -11,15 +11,17 @@ Introduction Der nächste Untertan in der Reihe ist ein Schelm. " -Statement " +Statement "" : +True := by + trivial + +Hint : True => " **Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist. **Du** Und was genau ist dann zu beweisen? **Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben. -" : -True := by - trivial +" Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index b3c56f7..3c5c77f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -11,7 +11,11 @@ Introduction Der Schelm hat noch eine Schwester dabei. " -Statement " +Statement "" : + ¬False := by + trivial + +Hint : ¬False => " **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)` wahr ist, dann ist `¬A` falsch, und umgekehrt. **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist? @@ -21,10 +25,7 @@ Statement " **Du** Ist das jetzt nicht doch wieder trivial? **Robo** Probier mal! -" : - ¬False := by - trivial - +" Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index 2d3bc4c..68bfe13 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -14,7 +14,12 @@ Introduction Langsam wird die Schlange kürzer. Die nächste Formalosophin hat folgendes Anliegen: " -Statement " +Statement "" + (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by + rcases h with ⟨_, ⟨g , _⟩⟩ + assumption + +Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => " **Du** Jetzt müssen wir wohl die Annahme de-konstruieren. **Robo** Ja, genau. Das geht am einfachsten mit `rcases h with ⟨h₁, h₂⟩`. @@ -24,9 +29,6 @@ Statement " **Robo** Die bleiden Klammern schreibst Du als `\\<` und `\\>`, oder gleichzeitig als `\\<>`. Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen für `h₁` und `h₂`, zum Beispiel `rcases h with ⟨hA, hBC⟩` " - (A B C : Prop) (h : A ∧ (B ∧ C)) : B := by - rcases h with ⟨_, ⟨g , _⟩⟩ - assumption Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B => " From 874999ed34482fd2e43caa6916b80ca225b3efe3 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 6 Mar 2023 10:19:45 +0100 Subject: [PATCH 4/4] show summary permanently --- .../Levels/Proposition/L13_Summary.lean | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index 32879ce..d5d7826 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -13,6 +13,13 @@ Title "Zusammenfassung" Introduction " Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vorherigen. + +**Robo** Wirf einfach alles drauf, was Du gelernt hast. Hier, ich bin sogar so nett und zeig Dir noch einmal die vier wichtigsten Taktiken für diese Situation an. + +| (Übersicht) | Und (`∧`) | Oder (`∨`) | +|-------------|:-------------------------|:------------------------| +| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` | +| Goal | `constructor` | `left`/`right` | " -- Note: The other direction would need arguing by cases. @@ -33,16 +40,6 @@ Statement "" right assumption -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. - -| (Übersicht) | Und (`∧`) | Oder (`∨`) | -|-------------|:-------------------------|:------------------------| -| Annahme | `rcases h with ⟨h₁, h₂⟩` | `rcases h with h \\| h` | -| Goal | `constructor` | `left`/`right` | -" - HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) => "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."