update world 1
This commit is contained in:
Jon Eugster
@@ -21,26 +21,21 @@ Du siehst Robo hilflos an.
|
||||
Statement ""
|
||||
(A B C : Prop) :
|
||||
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
|
||||
Hint "Hello? {A}"
|
||||
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.
|
||||
|
||||
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
|
||||
|
||||
**Du** Ernsthaft?
|
||||
|
||||
**Robo** Ja. Schreib einfach `tauto`.
|
||||
|
||||
**Robo** Mach schon …"
|
||||
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?
|
||||
|
||||
**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
|
||||
|
||||
**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
|
||||
|
||||
**Du** Ernsthaft?
|
||||
|
||||
**Robo** Ja. Schreib einfach `tauto`.
|
||||
|
||||
**Robo** Mach schon …
|
||||
"
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Logisinde** (etwas konsterniert) Ja, das ist streng genommen richtig.
|
||||
|
||||
@@ -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 …
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -11,23 +11,20 @@ Introduction
|
||||
Der Schelm hat noch eine Schwester dabei.
|
||||
"
|
||||
|
||||
Statement "" :
|
||||
¬False := by
|
||||
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?
|
||||
|
||||
**Robo** Ja, richtig.
|
||||
|
||||
**Du** Ist das jetzt nicht doch wieder trivial?
|
||||
|
||||
**Robo** Probier mal!"
|
||||
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?
|
||||
|
||||
**Robo** Ja, richtig.
|
||||
|
||||
**Du** Ist das jetzt nicht doch wieder trivial?
|
||||
|
||||
**Robo** Probier mal!
|
||||
"
|
||||
|
||||
Conclusion
|
||||
"
|
||||
Die Schwester lacht und eilt ihrem Bruder hinterher.
|
||||
|
||||
@@ -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.
|
||||
|
||||
@@ -17,15 +17,11 @@ Auftritt zweiter Querulant.
|
||||
|
||||
Statement ""
|
||||
(n : ℕ) (h : n ≠ n) : n = 37 := by
|
||||
Hint "**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
|
||||
|
||||
**Robo** Probiers mal!"
|
||||
contradiction
|
||||
|
||||
Hint (n : ℕ) (h : n ≠ n) : n = 37 =>
|
||||
"
|
||||
**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
|
||||
|
||||
**Robo** Probiers mal!
|
||||
"
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Du** Ja, scheint funktioniert zu haben.
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
"
|
||||
|
||||
@@ -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…
|
||||
|
||||
@@ -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."
|
||||
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) =>
|
||||
"**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) ∧ (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 ∨ 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."
|
||||
|
||||
-- TODO: Hint nur Anhand der Annahmen?
|
||||
-- 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) : A ∨ B =>
|
||||
"**Robo** `left` oder `right`?"
|
||||
-- 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
|
||||
"
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user