wip
Jon Eugster
2 years ago
parent
5bf0cd9775
commit
63b9c6cbb6
@ -0,0 +1,43 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 7
|
||||
|
||||
Title "Implikation"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Angenommen man hat folgende Implikationen und weiss dass Aussage `A` wahr ist.
|
||||
```
|
||||
A → B ← C
|
||||
↓ ↓
|
||||
D → E → F
|
||||
```
|
||||
Beweise Aussage `F`.
|
||||
"
|
||||
|
||||
Statement
|
||||
"
|
||||
Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
|
||||
Zeige, dass `B` wahr ist.
|
||||
"
|
||||
(A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E)
|
||||
(i : D → E) (k : E → F) (m : C → F) : F := by
|
||||
apply k
|
||||
apply h
|
||||
apply f
|
||||
assumption
|
||||
|
||||
Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
|
||||
(hA : A) (f : A → B) (g : C → B) (h : B → E)
|
||||
(i : D → E) (k : E → F) (m : C → F) : C =>
|
||||
"Sackgasse. Probier doch einen anderen Weg."
|
||||
|
||||
Message (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
|
||||
(hA : A) (f : A → B) (g : C → B) (h : B → E)
|
||||
(i : D → E) (k : E → F) (m : C → F) : D =>
|
||||
"Sackgasse. Probier doch einen anderen Weg."
|
||||
|
||||
Tactics apply
|
||||
Tactics assumption
|
||||
@ -0,0 +1,24 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 8
|
||||
|
||||
Title "Implikation"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Wenn das Goal von der Form `A → B` ist, kann man mit `intro` annehmen, dass `A` wahr ist
|
||||
und das Goal wird zu `B`.
|
||||
"
|
||||
|
||||
Statement
|
||||
(A B C: Prop) (f : A → B) (g : B → C) : A → C := by
|
||||
intro hA
|
||||
apply g
|
||||
apply f
|
||||
assumption
|
||||
|
||||
Tactics intro
|
||||
Tactics apply
|
||||
Tactics assumption
|
||||
@ -0,0 +1,30 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 9
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Genau-dann-wenn `A ↔ B` (`\\iff`) besteht aus zwei Implikationen `A → B` und `B → A`.
|
||||
|
||||
Als erstes kann man mit `rw` Annahmen der Form `(h : A ↔ B)` genau gleich wie Gleichungen
|
||||
`(h : a = b)` benützen, um das Goal umzuschreiben.
|
||||
|
||||
Hier also nochmals die Gleiche Aufgabe, aber diesmal mit Iff-Statements von Aussagen anstatt
|
||||
Gleichungen von natürlichen Zahlen.
|
||||
"
|
||||
|
||||
Statement
|
||||
"
|
||||
Zeige dass `B ↔ C`.
|
||||
"
|
||||
(A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
|
||||
rw [h₁]
|
||||
rw [←h₂]
|
||||
assumption
|
||||
|
||||
Tactics rw
|
||||
Tactics assumption
|
||||
@ -0,0 +1,39 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 10
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Als nächstes will man oft ein Iff-Statement `A ↔ B` wie zwei einzelne Implikationen
|
||||
`A → B` und `B → A` behandeln.
|
||||
|
||||
Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in die Einzelteile
|
||||
`A → B` und `B → A` zerlegen.
|
||||
|
||||
"
|
||||
|
||||
Statement
|
||||
"
|
||||
Zeige dass `B ↔ C`.
|
||||
"
|
||||
(A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
|
||||
constructor
|
||||
assumption
|
||||
assumption
|
||||
|
||||
|
||||
Conclusion
|
||||
"
|
||||
Die Taktik `constructor` heisst so, weil `↔` als \"Struktur\" definiert ist, die
|
||||
aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, es soll versuchen,
|
||||
ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
|
||||
"
|
||||
|
||||
Tactics constructor
|
||||
Tactics assumption
|
||||
|
||||
-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
|
||||
@ -0,0 +1,42 @@
|
||||
import TestGame.Metadata
|
||||
import Std.Tactic.RCases
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 11
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Umgekehrt, wenn man eine Annahme `(h : A ↔ B)` hat, kann man auf verschiedene
|
||||
Arten die Einzelteile `A → B` und `B → A` extrahieren.
|
||||
|
||||
- mit `rcases h` oder `rcases h with ⟨h₁, h₂⟩` teilt man die Annahme `h` auf. (Im zweiten Fall gibt
|
||||
man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<` und `\\>`).
|
||||
|
||||
"
|
||||
Statement
|
||||
(A B : Prop) : (A ↔ B) → (A → B) := by
|
||||
intro h
|
||||
cases h
|
||||
case intro x y =>
|
||||
assumption
|
||||
|
||||
Message (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
|
||||
"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
|
||||
|
||||
Conclusion
|
||||
"
|
||||
Anstatt
|
||||
```
|
||||
intro h
|
||||
rcases h with ⟨h₁, h₂⟩
|
||||
```
|
||||
kann man direkt `intro ⟨h₁, h₂⟩` schreiben.
|
||||
Wie du schon gesehen hast, sind diese Klammern `⟨⟩` Lean's Syntax für eine Struktur aus
|
||||
mehreren Teilen.
|
||||
|
||||
"
|
||||
|
||||
Tactics intro apply rcases assumption
|
||||
@ -0,0 +1,33 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 12
|
||||
|
||||
Title "Genau dann wenn"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Man kann auch die einzelnen Richtungen benützen, ohne `h` selber zu verändern:
|
||||
|
||||
- `h.1` und `h.2` sind direkt die einzelnen Richtungen. Man kann also z.B. mit `apply h.1` die
|
||||
Implikation `A → B` auf ein Goal `B` anwenden.
|
||||
- `h.mp` und `h.mpr` sind die bevorzugten Namen anstatt `.1` und `.2`. \"mp\" kommt von
|
||||
\"Modus Ponens\", aber das ist hier irrelevant.
|
||||
"
|
||||
|
||||
Statement
|
||||
"
|
||||
Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen.
|
||||
"
|
||||
(A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
|
||||
intro hA
|
||||
apply g
|
||||
apply h.mp
|
||||
assumption
|
||||
|
||||
Message (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
|
||||
"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
|
||||
|
||||
Tactics apply
|
||||
Tactics assumption
|
||||
@ -0,0 +1,69 @@
|
||||
import TestGame.Metadata
|
||||
import Std.Tactic.RCases
|
||||
|
||||
Game "TestGame"
|
||||
World "TestWorld"
|
||||
Level 13
|
||||
|
||||
Title "Und"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Das logische UND `A ∧ B` (`\\and`) funktioniert sehr ähnlich zum Iff (`↔`).
|
||||
Grund dafür ist, dass `A ∧ B` auch eine Struktur aus zwei Teilen `⟨A, B⟩` ist.
|
||||
|
||||
Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man
|
||||
`.1` und `.2` für die Einzelteile brauchen, diese heissen lediglich
|
||||
`h.left` und `h.right` anstatt `.mp` und `.mpr`.
|
||||
"
|
||||
|
||||
Statement
|
||||
(A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by
|
||||
constructor
|
||||
intro h
|
||||
rcases h with ⟨h₁, h₂⟩
|
||||
constructor
|
||||
assumption
|
||||
apply h₂
|
||||
assumption
|
||||
intro h
|
||||
rcases h with ⟨h₁, h₂⟩
|
||||
constructor
|
||||
assumption
|
||||
intro
|
||||
assumption
|
||||
|
||||
Message (A : Prop) (B : Prop) : A ∧ (A → B) ↔ A ∧ B =>
|
||||
"`↔` oder `∧` im Goal kann man mit `constructor` aufteilen."
|
||||
|
||||
-- if they don't use `intro ⟨_, _⟩`.
|
||||
Message (A : Prop) (B : Prop) (h : A ∧ (A → B)) : A ∧ B =>
|
||||
"Jetzt erst mal noch schnell die Annahme `A ∧ (A → B)` mit `rcases` aufteilen."
|
||||
|
||||
-- if they don't use `intro ⟨_, _⟩`.
|
||||
Message (A : Prop) (B : Prop) (h : A ∧ B) : A ∧ (A → B) =>
|
||||
"Jetzt erst mal noch schnell die Annahme `A ∧ B` mit `rcases` aufteilen."
|
||||
|
||||
Message (A : Prop) (B : Prop) (hA : A) (h : A → B) : A ∧ B =>
|
||||
"Wieder in Einzelteile aufteilen..."
|
||||
|
||||
Message (A : Prop) (B : Prop) : A ∧ (A → B) =>
|
||||
"Immer das gleiche ... noch mehr aufteilen."
|
||||
|
||||
Message (A : Prop) (B : Prop) (h₁: A) (h₂: B) : A → B =>
|
||||
"Das ist jetzt vielleicht etwas verwirrend: Wir wollen die Implikation `A → B` zeigen,
|
||||
wissen aber, dass `B` immer wahr ist (habe eine Annahme der Form `(hB : B)`).
|
||||
|
||||
Mit intro können wir einfach nochmal annehmen, dass `A` wahr ist. Es stört uns nicht,
|
||||
dass wir das schon wissen und auch gar nicht brauchen. Damit müssen wir nur noch zeigen,
|
||||
dass `B` wahr ist."
|
||||
|
||||
Hint (A : Prop) (B : Prop) (hA : A) (h : A → B) : B =>
|
||||
"Sieht nach einem Fall für `apply` aus."
|
||||
|
||||
|
||||
-- TODO
|
||||
|
||||
|
||||
Tactics apply rcases
|
||||
Tactics assumption
|
||||
Loading…
Reference in New Issue