From 7c2b1b048215483a81029aea04546f1bf86cd1df Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 10 Mar 2023 15:14:07 +0100 Subject: [PATCH] update world 1 --- .../Levels/Proposition/L00_Tauto.lean | 23 ++-- .../TestGame/Levels/Proposition/L01_Rfl.lean | 7 +- .../Levels/Proposition/L02_Assumption.lean | 8 +- .../Levels/Proposition/L03_Assumption.lean | 10 +- .../TestGame/Levels/Proposition/L04_True.lean | 8 +- .../TestGame/Levels/Proposition/L05_Not.lean | 21 ++- .../Levels/Proposition/L06_False.lean | 12 +- .../Levels/Proposition/L07_ContraNotEq.lean | 10 +- .../Levels/Proposition/L08_Contra.lean | 8 +- .../TestGame/Levels/Proposition/L09_And.lean | 34 +++-- .../TestGame/Levels/Proposition/L10_And.lean | 21 +-- .../TestGame/Levels/Proposition/L11_Or.lean | 20 +-- .../TestGame/Levels/Proposition/L12_Or.lean | 47 +++---- .../Levels/Proposition/L13_Summary.lean | 121 ++++++++++++------ .../TestGame/Levels/SetTheory/L03_Subset.lean | 10 +- 15 files changed, 177 insertions(+), 183 deletions(-) diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean index 25919a7..99204e4 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -21,25 +21,20 @@ Du siehst Robo hilflos an. Statement "" (A B C : Prop) : ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by - Hint "Hello? {A}" - 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 sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder? + Hint "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint er: + `{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. + **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** Ja. Schreib einfach `tauto`. -**Robo** Mach schon … -" + **Robo** Mach schon …" + tauto Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean index 74749db..3c56590 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -19,13 +19,10 @@ Er schreibt es Dir wieder auf. Statement "" : 42 = 42 := by + Hint " **Robo** Ist doch klar. Du musst ihn einfach daran erinnern, + dass Gleichheit *reflexiv* ist. Probier mal `rfl`." 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 4a6f09f..e75e141 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -13,9 +13,7 @@ Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste 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 => " + Hint " **Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl. **Du** Warum schreibt er dann nicht `{n} ∈ ℕ`?? @@ -32,8 +30,8 @@ für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`. **Du** ??? -**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`. -" +**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`." + assumption Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean index 9579d2a..7a177eb 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -14,9 +14,7 @@ Ein dritter Untertan kommt mit folgendem Problem. Statement "" (A : Prop) (hA : A) : A := by - assumption - -Hint (A : Prop) (hA : A) : A => " + 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. @@ -24,10 +22,10 @@ Hint (A : Prop) (hA : A) : A => " **Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder? " - -HiddenHint (A : Prop) (hA : A) : A => -"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. + Hint (hidden := true) "Ist doch genau wie eben: +die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen. Also wird `asumption` auch wieder funktionieren." + assumption Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean index 88e26aa..0549e7c 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -11,11 +11,8 @@ Introduction Der nächste Untertan in der Reihe ist ein Schelm. " -Statement "" : -True := by - trivial - -Hint : True => " +Statement "" : True := by + Hint " **Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und bedingungslos wahr ist. @@ -23,6 +20,7 @@ bedingungslos wahr ist. **Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben. " + trivial Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean index 6f2ea13..dc1d413 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -11,22 +11,19 @@ Introduction Der Schelm hat noch eine Schwester dabei. " -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. +Statement "" : ¬False := by + 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? +**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? +**Du** Ist das jetzt nicht doch wieder trivial? - **Robo** Probier mal! -" +**Robo** Probier mal!" + trivial Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean index 5bcb6e2..f60ad4f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -15,12 +15,8 @@ Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem: 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 … + 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. @@ -33,8 +29,8 @@ 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`. -" +Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`." + contradiction Conclusion "Der erste Querulant ist offenbar zufrieden. diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean index 2d27c5b..88900b5 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -17,14 +17,10 @@ Auftritt zweiter Querulant. Statement "" (n : ℕ) (h : n ≠ n) : n = 37 := by - contradiction - -Hint (n : ℕ) (h : n ≠ n) : n = 37 => -" -**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch? + Hint "**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch? -**Robo** Probiers mal! -" +**Robo** Probiers mal!" + contradiction Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index 3a0043b..6f9a195 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -17,14 +17,12 @@ Auftritt dritter Querulant. Statement "" (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by + Hint "**Du** Wieder ein Widerspruch in den Annahmen? + +**Robo** Ich sehe, du hast langsam den Dreh raus." contradiction -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 " diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean index 6456d35..773259e 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -15,34 +15,46 @@ 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 - -Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B => + Hint " **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. +**Robo**: Nee, diesmal wird das nicht funktionieren. Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`. -**Du** Du meinst, `destructor`?? +**Du**: Du meinst, `destructor`?? -**Robo** Nein, `constructor`. Ich weiß das ist verwirrend, +**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 => + constructor + -- TODO: (BUG) Hier werden beide der folgenden Hints angezeigt. + -- Das logiste Verhalten wäre, wenn jeder nur am richtigen Ort + -- angezeigt würde. + -- Ein cooles Feature wäre, wenn man nur diesen ersten Hint schreiben könnte + -- und dieser dann automatisch auch beim zweiten Goal angezeigt wird, aber dann mit `B` statt `A`. + Hint (hidden := true) " -**Robo** Schau mal, das ist Zauberpapier. +**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*. " + assumption + Hint (hidden := true) +" +**Robo**: Schau mal, das ist Zauberpapier. +Jetzt haben wir auf einmal zwei Beweisziele. +Hier ist dast Ziel `{B}`. +Ich glaube, Du weißt schon, wie man die jeweils erreicht. +Die Ziele stehen ja jeweils in den *Annahmen*. +" + assumption + Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean index c2000c0..44aad21 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -16,10 +16,7 @@ Langsam wird die Schlange kürzer. Die nächste Formalosophin hat folgendes Anli 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 => " + Hint " **Du** Jetzt müssen wir wohl die Annahme de-konstruieren. **Robo** Ja, genau. Das geht am einfachsten mit `rcases {h} with ⟨h₁, h₂⟩`. @@ -30,16 +27,12 @@ Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => " 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! -" - -HiddenHint (A : Prop) (hA : A) : A => -" -**Robo** Du hast einen Beweis dafür in den *Annahmen*. -" + Branch + rcases h with ⟨h₁, h₂⟩ + Hint "**Robo** Das sieht doch schon besser aus! Gleich nochmal!" + rcases h with ⟨_, ⟨g , _⟩⟩ + Hint (hidden := true) "**Robo** Du hast einen Beweis dafür in den *Annahmen*." + assumption Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index 712ad00..0c5878b 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -18,12 +18,7 @@ Der nächste bitte … Statement "" (A B : Prop) (hA : A) : A ∨ (¬ B) := by - left - assumption - -Hint (A B : Prop) (hA : A) : A ∨ (¬ B) => -" -**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren? + 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. @@ -31,13 +26,12 @@ 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 B : Prop) (hA : A) : ¬ B => -" -**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal. -" +**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?" + Branch + right + Hint "**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal." + left + assumption Conclusion " diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index 9b90569..90aa1b1 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -20,14 +20,7 @@ Der nächste bitte … Statement "" (A B : Prop) (h : (A ∧ B) ∨ A) : A := by - rcases h with h | h - rcases h with ⟨h₁, h₂⟩ - assumption - assumption - -Hint (A B : Prop) (h :(A ∧ B) ∨ A) : A => -" -**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir, + Hint "**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}`! @@ -41,34 +34,24 @@ Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten we **Du** Also, wieder `rcases …`? -**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** +**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`." + rcases h with h | h + Hint "**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 `\\<>`. -" +sei wahr." + Hint (hidden := true) " **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 `\\<>`." + rcases h with ⟨h₁, h₂⟩ + Hint "**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." + assumption + assumption Conclusion "**Du** Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele… diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean index 3be2eba..6db6c77 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -14,7 +14,9 @@ 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. +**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 (`∨`) | |-------------|:-------------------------|:------------------------| @@ -26,46 +28,83 @@ Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vor Statement "" (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by - constructor - rcases h with h | h - left - assumption - rcases h with ⟨h₁, h₂⟩ - right - assumption - rcases h with h | h - left - assumption - rcases h with ⟨h₁, h₂⟩ - right - assumption - -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." - -HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => -"**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen." - -HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => -"**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) => -"**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) => -"**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) => -"**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) => -"**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 => -"**Robo** `left` oder `right`?" + Hint (hidden := true) + "**Robo**: Ich würd zuerst die Annahme {h} mit `rcases {h}` aufteilen." + Branch + constructor + · rcases h with h' | h' + · left + assumption + · rcases h' with ⟨h₁, h₂⟩ + right + assumption + · rcases h with h' | h' + · left + assumption + · rcases h' with ⟨h₁, h₂⟩ + right + assumption + rcases h + Hint (hidden := true) "**Robo**: Jetzt kannst Du das `∧` im Goal mit `constructor` angehen." + · constructor + · left + assumption + · left + assumption + · Hint (hidden := true) + "**Robo**: Hier würde ich die Annahme {h} nochmals mit `rcases` aufteilen." + Branch + constructor + · Hint "**Robo**: Der Nachteil an der Reihenfolge ist, dass du jetzt in jedem Untergoal +`rcases h` aufrufen musst." + Branch + right + rcases h with ⟨h₁, h₂⟩ + assumption + rcases h with ⟨h₁, h₂⟩ + right + assumption + · Branch + right + rcases h with ⟨h₁, h₂⟩ + assumption + rcases h with ⟨h₁, h₂⟩ + right + assumption + rcases h with ⟨h₁, h₂⟩ + constructor + · right + assumption + · right + assumption + + +-- 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." + +-- HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) => +-- "**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen." + +-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => +-- "**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) => +-- "**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) => +-- "**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) => +-- "**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) => +-- "**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 => +-- "**Robo** `left` oder `right`?" Conclusion " diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean index 801ad43..a876537 100644 --- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean +++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean @@ -28,16 +28,16 @@ namespace MySet open Set -theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by - trivial +-- theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by +-- trivial -theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by - tauto +-- theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by +-- tauto Statement subset_empty_iff "." (A : Set ℕ) : A ⊆ univ := by intro h hA - apply mem_univ -- or `trivial`. + trivial --apply mem_univ -- or `trivial`. NewTactic intro trivial apply -- blocked: tauto simp