From 2d9627920387619f1bccaff70d83d03f5bffe2be Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 6 Mar 2023 09:46:22 +0100 Subject: [PATCH] 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