From c35b66a0c674f7f2854211285379e4f9d4d78e66 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 6 Mar 2023 10:04:40 +0100 Subject: [PATCH] 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 => "