diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean index d4aadae..9679f58 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -19,7 +19,7 @@ Also z.B. `(h : A)` und `(g : ¬ A)`. Da `≠` als `¬(· = ·)` gelesen wird, gilt dasselbe für Annahmen `(h : a = b)` und `(g : a ≠ b)`. " -Statement absurd +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 diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean index 2b7570f..39461b8 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -19,7 +19,7 @@ welche Seite man beweisen möchte. " Statement - "Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$" + "Angenommen $A$ ist wahr, zeige $A \\lor (\\neg B))$." (A B : Prop) (hA : A) : A ∨ (¬ B) := by left assumption diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean index 2631266..a773a7e 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -11,93 +11,33 @@ Game "TestGame" World "Proposition" Level 12 -Title "Oder - Bonus" +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₂`. +**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. " -Statement distributivity - "Angenommen $ A \\lor (B \\land C)$ is wahr, zeige, dass $(A \\lor B) \\land (A \\lor C)$." - (A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by - rcases h with ha | h - constructor - left - assumption - left +Statement + "Angenommen \"$A$ oder ($A$ und $B$)\" wahr ist, zeige, dass $A$ wahr ist." + (A B : Prop) (h : A ∨ (A ∧ B)) : A := by + rcases h with h | h assumption rcases h with ⟨h₁, h₂⟩ - constructor - right - assumption - right assumption -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => -"Als erstes solltest du das OR in der Annahme `(h: A ∨ (B ∧ C))` aufteilen:" - -Hint (A : Prop) (B : Prop) (C : Prop) (h : A) : (A ∨ B) ∧ (A ∨ C) => -"Wie wär's mit zerlegen?" - -Hint (A : Prop) (B : Prop) : (A ∨ B) => -"`left` oder `right`?" - -Message (A : Prop) (B : Prop) (C : Prop) (h : (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) => -"Und jetzt der Fall, falls die rechte Seite $B \\land C$ wahr ist. Zerlege diese -Annahme doch als erstes." - -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) => -"Jetzt musst du die Annahme $A \\lor (B \\land C)$ trotzdem noch mit `rcases` zerlegen." - -Message (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) => -"So musst du die Annahme $A \\lor (B \\land C)$ nochmals mit `rcases` zerlegen... - -Wenn du am Anfang zuerst `rcases` und dann `constructor` aufrufst, -musst du das hier nur einmal machen..." - -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : A ∨ B => -"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen." - -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : A ∨ C => -"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen." - -Message (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : C => -"Die Annahme `B ∧ C` kannst du auch mit `rcases` zerlegen." - - --- Statement umsortieren --- "Angenommen $(A \\land B) \\lor (D \\lor C)$ is wahr, zeige, dass " --- (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by --- rcases h with x | (h | h) --- left --- assumption --- right --- right --- assumption --- right --- left --- assumption +Message (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." --- Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) => --- "Man kann hier entweder in mehren Schritten `rcases` anwenden: --- ``` --- rcases h with h₁ | h₂ --- rcases h₁ with ⟨hA, hB⟩ --- [...] --- rcases h₂ with h | h --- ``` --- oder man kann dies in einem Schritt verschachteln: --- ``` --- rcases h with ⟨ha, hb⟩ | (h | h) --- ``` --- " +Message (A : Prop) (B : Prop) (h : A ∧ B) : A => +"Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen." -Tactics left right assumption constructor rcases apply +Tactics assumption rcases diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Or.lean b/server/testgame/TestGame/Levels/Proposition/L13_Or.lean index ce1a007..bf1489d 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Or.lean @@ -23,7 +23,7 @@ umzugehen um folgende Aussage zu beweisen. -- Note: The other direction would need arguing by cases. -Statement or_and_left +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