story contradiction

server/testgame/TestGame/Levels/Contradiction.lean

@@ -8,3 +8,9 @@ import TestGame.Levels.Contradiction.L06_Summary
 Game "TestGame"
 World "Contradiction"
 Title "Widerspruch"
+
+Introduction "
+Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
+eine Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
+gebeten.
+"

server/testgame/TestGame/Levels/Contradiction/L01_Have.lean

@@ -15,56 +15,46 @@ Title "Have"
 
 Introduction
 "
-Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
-Zwischenresultat beweisen, welches wir dann benützen können.
-
-Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
-dass man anschliessen beweisen muss.
-
-Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
-du mit
-```
-have g : ¬ B
-apply h
-assumption
-```
-eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
-bevor du dann mit dem Beweis forfährst.
+**Oddeus**: Willkommen Reisende! Ich muss eingestehen ich bin in Gedanken noch
+an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen?
 "
 
-Statement
-    "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
-    $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
-    (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
-  rcases k with ⟨h₁, h₂⟩
-  have h₃ : ¬ B
-  apply h
-  assumption
-  contradiction
+-- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
+-- Zwischenresultat beweisen, welches wir dann benützen können.
 
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
-" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
-"
+-- Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
+-- dass man anschliessen beweisen muss.
 
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
-"
-Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"
+-- Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
+-- du mit
+-- ```
+-- have g : ¬ B
+-- apply h
+-- assumption
+-- ```
+-- eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
+-- bevor du dann mit dem Beweis forfährst.
 
-In Lean :
+Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
+  Hint "**Du**: Also als erstes Teile ich wohl mal das Und (`∧`) auf."
+  rcases k with ⟨h₁, h₂⟩
+  Hint "**Du**: Aber jetzt…
 
-```
-have k : ¬ B
-[Beweis von k]
-```
-"
+  **Robo**: Du könntest dir ein passendes Zwischenresultat zurechtlegen, das dir hilft:
+  Mach mal `have g : ¬ B`!"
+  have g : ¬ B
+  · Hint "**Du**: Was und jetzt hab ich einfach angenommen das sei richtig?
 
--- example (n : ℕ) : n.succ + 2 = n + 3 := by
--- ring_nf
+    **Robo**: Ne, jetzt musst du das zuerst beweisen bevor du es dann benützen kannst."
+    Hint (hidden := true) "**Robo**: `apply` scheint passend zu sein."
+    apply h
+    assumption
+  · Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen?
 
-Conclusion ""
+    **Robo**: `contradiction`."
+    contradiction
 
 NewTactic «have»
 DisabledTactic «suffices»
 
-NewDefinition Even Odd
-NewLemma not_even not_odd
+Conclusion "*Oddeus*: Das stimmt wohl."

server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean

@@ -15,52 +15,49 @@ Title "Suffices"
 
 Introduction
 "
-Die Taktik `suffices` funktioniert genau gleich wie `have`,
-vertauscht aber die beiden Beweisblöcke:
+*Oddeus*' Partner meldet sich.
 
-```
-suffices h : [Aussage]
-[Beweis des Goals (mithilfe von h)]
-[Beweis der Aussage h]
-```
-Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
-\"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
+**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
+"
 
-Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
-dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
-`suffices` schöner gewesen:
+-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
+-- vertauscht aber die beiden Beweisblöcke:
 
-"
+-- ```
+-- suffices h : [Aussage]
+-- [Beweis des Goals (mithilfe von h)]
+-- [Beweis der Aussage h]
+-- ```
+-- Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
+-- \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
+
+-- Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
+-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
+-- `suffices` schöner gewesen:
 
 Statement
     "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
     $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
-    (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
-  rcases k with ⟨h₁, h₂⟩
-  suffices k : ¬ B
+    (A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
+  Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
+  brauchen. Das funktioniert genau gleich, aussert dass dann die beiden Goals vertauscht sind.
+
+  **Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
+  abschliesst bevor ich `g` beweise?
+
+  **Robo**: Genau! Verwendende `have` und `suffices` einfach nach gutdünken."
+  suffices g : ¬ B
+  Hint "**Robo**: Also hier beendest du den Beweis angenommen {g} sei wahr."
   contradiction
+  Hint "**Robo**: Und hier beweist du das Zwischenresultat."
   apply h
   assumption
 
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
-" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
-"
-
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
-" Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\"
+NewTactic «suffices»
+DisabledTactic «have»
 
-  In Lean :
+Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
 
-  ```
-  suffices k : ¬ B
-  contradiction
-  [...]
-  ```
-"
+**Oddeus**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
 
-Conclusion ""
-
-NewTactic «suffices»
-DisabledTactic «have»
-NewDefinition Even Odd
-NewLemma not_even not_odd
+Und er führt euch durch seinen Rosengarten."

server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean

@@ -15,41 +15,51 @@ Level 3
 Title "Per Widerspruch"
 
 Introduction
-"
-Eine sehr nützliche Beweismethode ist per Widerspruch.
-
-Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
-sucht, und damit jegliches beweisen kann.
+"**Oddeus**: Ich verstehe *Evenine* einfach nicht. Ich will euch auch gleich zeigen,
+was sie mir letzthin geschrieben hat, aber zuerst schaut einmal unseren
+wunderschönen Absurda-Tempel an!
 
-Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
-Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
+Damit kommt ihr vor einen sehr hohen Turm, der ausschliesslich aus Dornenranken gewachsen
+scheint.
 
-Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
-steht:
+**Oddeus**: Versteht ihr, was hier über dem Eingang steht?
 "
 
-Statement
-"Angenommen $B$ ist falsch und es gilt $A \\Rightarrow B$. Zeige, dass $A$ falsch sein
-muss."
-    (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
-  by_contra a
-  suffices b : B
-  contradiction
-  apply g
-  assumption
+--   Eine sehr nützliche Beweismethode ist per Widerspruch.
 
+-- Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
+-- sucht, und damit jegliches beweisen kann.
 
-HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) : ¬ A =>
-"`by_contra h` nimmt das Gegenteil des Goal als Annahme `(h : A)` und setzt das
-Goal auf `False`."
+-- Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
+-- Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
 
-Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
-"Jetzt kannst du mit `suffices` oder `have` Fortschritt machen."
+-- Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
+-- steht:
 
-HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
-"Zum Beispiel `suffices hb : B`."
+Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
+  Hint "**Robo**: Ein `¬` im Goal heisst häufig, dass du einen Widerspruchsbeweis führen
+  möchtest.
 
+  **Du**: Und wie mach ich das? Mit `contradiction`?
+
+  **Robo**: Mit `by_contra h` fängst du einen an. Mit `contradiction` schliesst du ihn dann
+  später ab."
+  by_contra h
+  Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : ¬ {A}`, und damit musst du einen
+  Widerspruch herbeileiten.
+
+  Ein Methode ist, dass du jetzt mit `suffices` sagts, zu was du denn gerne den Widerspruch
+  haben möchtest, zum Beispiel `suffices k : B`
+  "
+  suffices k : B
+  Hint "**Du**: Ah und jetzt kann ich einfach sagen dass sich die Anahmen `{B}` und `¬{B}`
+  widersprechen."
+  contradiction
+  Hint "**Robo**: Und jetzt kannst du noch das Ergebnis zeigen, das zu einem Widerspruch
+  geführt hat."
+  apply g
+  assumption
 
-Conclusion ""
+NewTactic by_contra
 
-NewTactic by_contra contradiction apply assumption
+Conclusion "**Oddeus**: Sehr gut, kommt mit hinein!"

server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean

@@ -16,34 +16,36 @@ Title "Per Widerspruch"
 
 Introduction
 "
-Als Übung zu `by_contra` und dem bisher gelernten, zeige folgendes Lemma welches
-wir für die Kontraposition brauchen werden:
+*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
+
+**Oddeus**: Ich hab's gleich. Hier ist eine Notiz meiner Gelehrter, die mir
+mit solchen kryptischen Nachrichten helfen wollten.
+
+Auf dem Pergament steht das ein Lemma mit dem Namen `not_imp_not`:
 "
 
-Statement not_imp_not
-"$A \\Rightarrow B$ ist äquivalent zu $\\neg B \\Rightarrow \\neg A$."
-    (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
+Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
+  Hint "**Du**: Ich glaube, dafür kenn ich das meiste schon."
+  Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
   constructor
   intro h b
   by_contra a
+  Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
+  herbeiführen."
   suffices b : B
   contradiction
   apply h
   assumption
   intro h a
+  Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruch anfangen."
   by_contra b
+  Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
   suffices g : ¬ A
   contradiction
   apply h
   assumption
 
--- TODO: Forbidden Tactics: apply, rw
--- TODO: forbidden Lemma: not_not
-
-HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
-""
-
-
-Conclusion ""
+DisabledTactic rw
+DisabledLemma not_not
 
-NewTactic contradiction constructor intro by_contra apply assumption
+Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"

server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean

@@ -14,53 +14,56 @@ Title "Kontraposition"
 
 Introduction
 "
-Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
+*Oddeus* reicht euch das Papier.
 
-```
-lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
-  [...]
-```
+**Du**: Da steht etwas über `contrapose` hier…
 
-Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
-entsprechend umdreht.
+**Oddeus**: Das ist doch klar eine Aggression uns gegenüber!
 
-Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
-im Goal erstellt.
+**Robo**: Wartet mal, vielleicht wollte euch eure Schwester einfach von ihren neuen
+Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
+"
 
-Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
-Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
-logisch equivalent sind.
+-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
 
-Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
-"
+-- ```
+-- lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
+--   [...]
+-- ```
 
-Statement
-    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
-    (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
-  revert h
-  contrapose
-  rw [not_odd]
-  rw [not_odd]
-  apply even_square
+-- Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
+-- entsprechend umdreht.
 
-HiddenHint (n : ℕ) (h : Odd (n ^ 2)) : Odd n =>
-"Um `contrapose` anzuwenden, brauchen wir eine Implikation `Odd (n ^ 2) → Odd n` im
-Goal. Benutze `revert h`!"
+-- Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
+-- im Goal erstellt.
 
-Hint (n : ℕ) : Odd (n ^ 2) → Odd n =>
-"Mit `contrapose` kann man die Implikation zu
-`¬ (Not n) → ¬ (Odd n^2)` umkehren."
+-- Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
+-- Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
+-- logisch equivalent sind.
 
-Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`."
+-- Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
 
-HiddenHint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden."
+Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
+  Hint "**Oddeus**: Wie soll das den gehen?
 
-Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
-"rw [not_odd] muss hier zweimal angewendet werden."
+  **Robo**: `contrapose` benutzt das Lemma eurer Gelehrter, `not_imp_not`. Also es wandelt
+  ein Goal `A → B` zu `¬B → ¬A ` um.
+
+  **Du**: Aber das Goal ist doch gar keine Implikation?
+
+  **Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
+  schieben."
+  revert h
+  Hint "*Oddeus*: Ob man jetzt wohl dieses `contrapose` benutzen kann?"
+  contrapose
+  Hint (hidden := true) "**Du**: Warte mal, jetzt kann man wohl `not_odd` verwenden…"
+  rw [not_odd]
+  rw [not_odd]
+  Hint "**Robo**: Und den Rest hast du bei *Evenine* als Lemma gezeigt!"
+  apply even_square
 
-Hint (n : ℕ) : Even n → Even (n ^ 2) =>
-"Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
+NewTactic contrapose
+DisabledTactic by_contra
 
-NewTactic contrapose rw apply
-NewDefinition Even Odd
-NewLemma not_even not_odd even_square
+Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
+Ich danke euch, darauf wäre ich nie gekommen."

server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean

@@ -14,63 +14,41 @@ Title "Contradiction"
 
 Introduction
 "
+**Du**: Sag mal Robo, das hätte ich aber auch als Widerspruch anstatt Kontraposition
+beweisen können?
+
+**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
+Probiers doch einfach!
 In diesem Kapitel hast du also folgende Taktiken kennengelernt:
 
-|       | Taktik          | Beispiel                                               |
-|:------|:----------------|:-------------------------------------------------------|
-| 16    | `have`          | Zwischenresultat annehmen.                             |
-| 17    | `suffices`      | Zwischenresultat annehmen.                             |
-| 18    | `by_contra`     | Widerspruch. (startet einen Widerspruch)               |
-| *3*   | `contradiction` | *(Schliesst einen Widerspruchsbeweis)*                 |
-| 19    | `contrapose`    | Contraposition.                                        |
-| *9*   | `revert`        | Nützlich um danach `contrapose` anzuwenden.            |
 
 Als Vergleich zwischen Beweisen \"per Widerspruch\"
 und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
 du mit `by_contra` einen Widerspruch suchst.
 "
 
-Statement
-    "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
-    (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
+Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
+  Hint "**Robo**: Fang diesmal mit `by_contra g` an!"
   by_contra g
+  Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
+  Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
   suffices d : ¬ Odd (n ^ 2)
   contradiction
   rw [not_odd] at *
   apply even_square
   assumption
 
-HiddenHint (n : ℕ) (h : Odd (n^2)) : Odd n =>
-"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten."
-
-Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False =>
-"
-Am sinnvollsten ist es, hier einen Widerspruch zu `Odd (n^2)` zu suchen.
-Dafür kannst du
-```
-suffices k : ¬ Odd (n ^ 2)
-contradiction
-```
-benützen.
-"
-
-HiddenHint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False =>
-"Hier brauchst du nur `contradiction`."
+DisabledTactic contrapose revert
 
-Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) =>
-"Das Zwischenresultat `¬Odd (n^2)` muss auch bewiesen werden.
-Hier ist wieder das Lemma `not_Odd` hilfreich."
+Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
+Mond gelernt haben:
 
-HiddenHint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) =>
-"Mit `rw [not_Odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben."
-
-Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
-"Diese Aussage hast du bereits als Lemma bewiesen."
-
-HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
-"Probiers mit `apply ...`"
-
-
-NewTactic contradiction by_contra rw apply assumption -- TODO: suffices, have
-NewDefinition Even Odd
-NewLemma not_odd not_even even_square
+|       | Taktik          | Beispiel                                               |
+|:------|:----------------|:-------------------------------------------------------|
+| 177   | `have`          | Zwischenresultat annehmen.                             |
+| 18    | `suffices`      | Zwischenresultat annehmen.                             |
+| 19    | `by_contra`     | Widerspruch. (startet einen Widerspruch)               |
+| *3*   | `contradiction` | *(Schliesst einen Widerspruchsbeweis)*                 |
+| 20    | `contrapose`    | Kontraposition.                                        |
+| *9*   | `revert`        | Nützlich um danach `contrapose` anzuwenden.            |
+"