levels
This commit is contained in:
Jon Eugster
@@ -23,6 +23,33 @@ Game "Adam"
|
||||
Title "Lean 4 game"
|
||||
Introduction
|
||||
"
|
||||
|
||||
# Game Over oder QED?
|
||||
|
||||
Willkommen zu unserem Prototyp eines Lean4-Lernspiels. Hier lernst du Computer-gestütztes
|
||||
Beweisen. Das Interface ist anfangs etwas vereinfacht, der \"Editor Mode\" funktioniert aber
|
||||
ziemlich gleich wie wenn du später Lean im VSCode benützt.
|
||||
|
||||
Rechts siehst du eine Übersicht der Welt dieses Spiels. Jeder Planet hat mehrere Levels,
|
||||
die in Form von grauen Punkten dargestellt sind. Gelöste Levels werden dann grün.
|
||||
|
||||
Klicke auf die erste Welt \"Aussagenlogik 1\" um deine Reise zu starten.
|
||||
|
||||
### Spielstand
|
||||
|
||||
Dein Spielstand wird lokal in deinem Browser als \"site data\" gespeichert.
|
||||
Solltest du diese löschen, verlierst du deinen Spielstand! Du kannst aber jederzeit jeden
|
||||
Level spielen, auch wenn frühere Levels nicht grün sind.
|
||||
|
||||
(oft werden *Site data & Cookies* zusammen gelöscht).
|
||||
|
||||
### Kontakt
|
||||
|
||||
Wenn du Bugs findest, schreib doch ein Email oder erstelle einen
|
||||
[Issue auf Github](https://github.com/leanprover-community/lean4game/issues).
|
||||
|
||||
Jon Eugster, jon.eugster@hhu.de
|
||||
|
||||
"
|
||||
|
||||
Conclusion
|
||||
|
||||
@@ -0,0 +1,87 @@
|
||||
import GameServer.Commands
|
||||
|
||||
/-! ## Definitions -/
|
||||
|
||||
DefinitionDoc Even as "Even"
|
||||
"
|
||||
`even n` ist definiert als `∃ r, a = 2 * r`.
|
||||
Die Definition kann man mit `unfold even at *` einsetzen.
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#Even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Even)"
|
||||
|
||||
DefinitionDoc Odd as "Odd"
|
||||
"
|
||||
`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
|
||||
Die Definition kann man mit `unfold odd at *` einsetzen.
|
||||
|
||||
* Mathlib Doc: [Odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd)"
|
||||
|
||||
DefinitionDoc Injective as "Injective"
|
||||
"
|
||||
`Injective f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a b, f a = f b → a = b
|
||||
```
|
||||
definiert.
|
||||
|
||||
* Mathlib Doc: [Injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Injective)"
|
||||
|
||||
DefinitionDoc Surjective as "Surjective"
|
||||
"
|
||||
`Surjective f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a, (∃ b, f a = b)
|
||||
```
|
||||
|
||||
* Mathlib Doc: [Surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Surjective)"
|
||||
|
||||
DefinitionDoc Bijective as "Bijective"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#Bijective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Bijective)
|
||||
"
|
||||
|
||||
DefinitionDoc LeftInverse as "LeftInverse"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#LeftInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.LeftInverse)
|
||||
"
|
||||
|
||||
DefinitionDoc RightInverse as "RightInverse"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#RightInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Logic.html#RightInverse)
|
||||
"
|
||||
|
||||
DefinitionDoc StrictMono as "StrictMono"
|
||||
"
|
||||
`StrictMono f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a b, a < b → f a < f b
|
||||
```
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#StrictMono](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono)
|
||||
|
||||
"
|
||||
|
||||
DefinitionDoc Symbol.Subset as "⊆" "
|
||||
|
||||
Auf Mengen (`Set`) ist `A ⊆ B` als `∀x, x ∈ A → x ∈ B` implementiert.
|
||||
"
|
||||
|
||||
DefinitionDoc Set.Nonempty as "Nonempty" "
|
||||
|
||||
`A.Nonemty` ist als `∃ x, x ∈ A` definiert.
|
||||
"
|
||||
@@ -165,7 +165,7 @@ Jedes Element ist in `univ`, der Menge aller Elemente eines Typs `α`.
|
||||
* Mathlib Doc: [#mem_univ](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.mem_univ)
|
||||
"
|
||||
|
||||
LemmaDoc not_mem_empty as "not_mem_empty" in "Set"
|
||||
LemmaDoc Set.not_mem_empty as "not_mem_empty" in "Set"
|
||||
"
|
||||
`Set.not_mem_empty {α : Type _} (x : α) : x ∉ ∅`
|
||||
|
||||
@@ -175,11 +175,21 @@ Kein Element ist in der leeren Menge.
|
||||
|
||||
* `simp`-Lemma: Nein
|
||||
* Namespace: `Set`
|
||||
* Minimal Import: `Mathlib.Data.Set.Basic`
|
||||
* Mathlib Doc: [#not_mem_empty](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.not_mem_empty)
|
||||
"
|
||||
|
||||
LemmaDoc empty_subset as "empty_subset" in "Set"
|
||||
LemmaDoc Set.subset_empty_iff as "subset_empty_iff" in "Set"
|
||||
"
|
||||
`Set.subset_empty_iff.{u} {α : Type u} {s : Set α} : s ⊆ ∅ ↔ s = ∅`
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* `simp`-Lemma: Nein
|
||||
* Namespace: `Set`
|
||||
* Mathlib Doc: [#empty_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.subset_empty_iff)
|
||||
"
|
||||
|
||||
LemmaDoc Set.empty_subset as "empty_subset" in "Set"
|
||||
"
|
||||
`Set.empty_subset {α : Type u} (s : Set α) : ∅ ⊆ s`
|
||||
|
||||
@@ -187,11 +197,10 @@ LemmaDoc empty_subset as "empty_subset" in "Set"
|
||||
|
||||
* `simp`-Lemma: Ja
|
||||
* Namespace: `Set`
|
||||
* Minimal Import: `Mathlib.Data.Set.Basic`
|
||||
* Mathlib Doc: [#empty_subset](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.empty_subset)
|
||||
"
|
||||
|
||||
LemmaDoc Subset.antisymm as "Subset.antisymm" in "Set"
|
||||
LemmaDoc Set.Subset.antisymm as "Subset.antisymm" in "Set"
|
||||
"
|
||||
`Set.Subset.antisymm {α : Type u} {a : Set α} {b : Set α} (h₁ : a ⊆ b) (h₂ : b ⊆ a) : a = b`
|
||||
|
||||
@@ -212,7 +221,7 @@ für die Iff-Version.
|
||||
* Mathlib Doc: [#Subset.antisymm](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm)
|
||||
"
|
||||
|
||||
LemmaDoc Subset.antisymm_iff as "Subset.antisymm_iff" in "Set"
|
||||
LemmaDoc Set.Subset.antisymm_iff as "Subset.antisymm_iff" in "Set"
|
||||
"
|
||||
`Set.Subset.antisymm_iff {α : Type u} {a : Set α} {b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a`
|
||||
|
||||
@@ -234,6 +243,17 @@ für eine verwandte Version.
|
||||
* Mathlib Doc: [#Subset.antisymm_iff](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.Subset.antisymm_iff)
|
||||
"
|
||||
|
||||
LemmaDoc Set.diff_inter as "union_assoc" in "Set"
|
||||
""
|
||||
|
||||
LemmaDoc Set.union_assoc as "union_assoc" in "Set"
|
||||
""
|
||||
|
||||
LemmaDoc Set.union_diff_distrib as "union_diff_distrib" in "Set"
|
||||
""
|
||||
|
||||
LemmaDoc Set.univ_union as "univ_union" in "Set"
|
||||
""
|
||||
|
||||
LemmaDoc Nat.prime_def_lt'' as "prime_def_lt''" in "Nat"
|
||||
"
|
||||
@@ -249,7 +269,6 @@ Die bekannte Definition einer Primmzahl in `ℕ`: Eine Zahl (`p ≥ 2`) mit gena
|
||||
* Mathlib Doc: [#Nat.prime_def_lt''](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html#Nat.prime_def_lt'')
|
||||
"
|
||||
|
||||
|
||||
LemmaDoc Finset.sum_add_distrib as "sum_add_distrib" in "Sum"
|
||||
"
|
||||
|
||||
@@ -280,6 +299,22 @@ LemmaDoc Nat.succ_eq_add_one as "succ_eq_add_one" in "Sum"
|
||||
* Mathlib Doc: [#succ_eq_add_one](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Basic.html#Nat.succ_eq_add_one)
|
||||
"
|
||||
|
||||
LemmaDoc ne_eq as "ne_eq" in "Logic"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#ne_eq](https://leanprover-community.github.io/mathlib4_docs/Init/SimpLemmas.html#ne_eq)
|
||||
"
|
||||
|
||||
LemmaDoc Set.eq_empty_iff_forall_not_mem as "eq_empty_iff_forall_not_mem" in "Sum"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#eq_empty_iff_forall_not_mem](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.eq_empty_iff_forall_not_mem)
|
||||
"
|
||||
|
||||
LemmaDoc Nat.zero_eq as "zero_eq" in "Sum"
|
||||
"
|
||||
|
||||
@@ -429,86 +464,3 @@ LemmaDoc Iff.symm as "Iff.symm" in "Logic"
|
||||
|
||||
* Mathlib Doc: [#Iff.symm](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff.symm)
|
||||
"
|
||||
|
||||
|
||||
|
||||
/-! ## Definitions -/
|
||||
|
||||
DefinitionDoc Even as "Even"
|
||||
"
|
||||
`even n` ist definiert als `∃ r, a = 2 * r`.
|
||||
Die Definition kann man mit `unfold even at *` einsetzen.
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#Even](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Even)"
|
||||
|
||||
DefinitionDoc Odd as "Odd"
|
||||
"
|
||||
`odd n` ist definiert als `∃ r, a = 2 * r + 1`.
|
||||
Die Definition kann man mit `unfold odd at *` einsetzen.
|
||||
|
||||
* Mathlib Doc: [Odd](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Parity.html#Odd)"
|
||||
|
||||
DefinitionDoc Injective as "Injective"
|
||||
"
|
||||
`Injective f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a b, f a = f b → a = b
|
||||
```
|
||||
definiert.
|
||||
|
||||
* Mathlib Doc: [Injective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Injective)"
|
||||
|
||||
DefinitionDoc Surjective as "Surjective"
|
||||
"
|
||||
`Surjective f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a, (∃ b, f a = b)
|
||||
```
|
||||
|
||||
* Mathlib Doc: [Surjective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Surjective)"
|
||||
|
||||
DefinitionDoc Bijective as "Bijective"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#Bijective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.Bijective)
|
||||
"
|
||||
|
||||
DefinitionDoc LeftInverse as "LeftInverse"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#LeftInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Function.html#Function.LeftInverse)
|
||||
"
|
||||
|
||||
DefinitionDoc RightInverse as "RightInverse"
|
||||
"
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#RightInverse](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Logic.html#RightInverse)
|
||||
"
|
||||
|
||||
DefinitionDoc StrictMono as "StrictMono"
|
||||
"
|
||||
`StrictMono f` ist definiert als
|
||||
|
||||
```
|
||||
∀ a b, a < b → f a < f b
|
||||
```
|
||||
|
||||
## Eigenschaften
|
||||
|
||||
* Mathlib Doc: [#StrictMono](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Monotone/Basic.html#StrictMono)
|
||||
|
||||
"
|
||||
|
||||
DefinitionDoc Symbol.Subset as "⊆" "
|
||||
|
||||
Auf Mengen (`Set`) ist `A ⊆ B` als `∀x, x ∈ A → x ∈ B` implementiert.
|
||||
"
|
||||
|
||||
@@ -29,8 +29,8 @@ Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
|
||||
|
||||
Conclusion
|
||||
"
|
||||
**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen,
|
||||
hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
|
||||
**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheißen,
|
||||
hier bei `(h : A ↔ B)` heißen sie `h.mp` und `h.mpr`.
|
||||
|
||||
**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
|
||||
|
||||
|
||||
@@ -29,21 +29,8 @@ Fast immer wenn man Gleichheiten von Mengen zeigen muss, will man diese in zwei
|
||||
aufteilen.
|
||||
"
|
||||
|
||||
namespace MySet
|
||||
|
||||
open Set Subset
|
||||
|
||||
-- Copied some lemmas from `Matlib.Data.Set.Basic` in order to not import the entire file.
|
||||
theorem tmp {α : Type _} {s t : Set α} : s = t → s ⊆ t :=
|
||||
fun h₁ _ h₂ => by rw [← h₁] ; exact h₂
|
||||
|
||||
theorem Subset.antisymm_iff {α : Type _} {a b : Set α} : a = b ↔ a ⊆ b ∧ b ⊆ a :=
|
||||
⟨fun e => ⟨tmp e, tmp e.symm⟩, fun ⟨h₁, h₂⟩ => Set.ext fun _ => ⟨@h₁ _, @h₂ _⟩⟩
|
||||
|
||||
@[simp]
|
||||
theorem empty_subset {α : Type _} (s : Set α) : ∅ ⊆ s :=
|
||||
fun.
|
||||
|
||||
Statement subset_empty_iff {A : Type _} (s : Set A) :
|
||||
s ⊆ ∅ ↔ s = ∅ := by
|
||||
Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge.
|
||||
@@ -53,16 +40,16 @@ Statement subset_empty_iff {A : Type _} (s : Set A) :
|
||||
Hint (hidden := true) "**Robo**: Fang doch einmal mit `constructor` an."
|
||||
constructor
|
||||
intro h
|
||||
Hint "**Robo**: "
|
||||
Hint "**Robo**: Gleichheit zwischen Mengen kann man zum Beispiel zeigen,
|
||||
indem man `A ⊆ B` und `B ⊆ A` zeigt.
|
||||
|
||||
Dieser Schritt ist `apply Subset.antisymm`"
|
||||
apply Subset.antisymm
|
||||
assumption
|
||||
simp only [empty_subset]
|
||||
intro a
|
||||
rw [Subset.antisymm_iff] at a
|
||||
rcases a with ⟨h₁, h₂⟩
|
||||
assumption
|
||||
Hint "**Robo**: Hier ist das Lemma `empty_subset` hilfreich."
|
||||
apply empty_subset
|
||||
intro h
|
||||
rw [h]
|
||||
|
||||
DisabledTactic tauto
|
||||
NewLemma Subset.antisymm Subset.antisymm_iff empty_subset
|
||||
|
||||
end MySet
|
||||
NewLemma Set.Subset.antisymm Set.Subset.antisymm_iff Set.empty_subset
|
||||
|
||||
@@ -12,39 +12,23 @@ Game "Adam"
|
||||
World "SetTheory"
|
||||
Level 5
|
||||
|
||||
Title "Nonempty"
|
||||
Title "Empty"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Das Gegenteil von `A = ∅` ist `A ≠ ∅`, aber in Lean wird der Ausdruck `A.Nonempty` bevorzugt.
|
||||
Dieser ist dadurch existiert, dass in `A` ein Element existiert: `∃x, x ∈ A`.
|
||||
|
||||
Zeige dass die beiden Ausdrücke äquivalent sind:
|
||||
Zeige folgendes Lemma, welches wir gleich brauchen werden:
|
||||
"
|
||||
|
||||
namespace MySet
|
||||
|
||||
open Set
|
||||
|
||||
theorem subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by
|
||||
constructor
|
||||
intro h
|
||||
rw [Subset.antisymm_iff]
|
||||
constructor
|
||||
assumption
|
||||
simp only [empty_subset]
|
||||
intro a
|
||||
rw [Subset.antisymm_iff] at a
|
||||
rcases a with ⟨h₁, h₂⟩
|
||||
assumption
|
||||
|
||||
Statement eq_empty_iff_forall_not_mem
|
||||
""
|
||||
{A : Type _} (s : Set A) :
|
||||
s = ∅ ↔ ∀ x, x ∉ s := by
|
||||
Hint "Das Lemma `subset_empty_iff` von letzter Aufgabe könnte hilfreich sein."
|
||||
rw [←subset_empty_iff]
|
||||
rfl -- This is quite a miracle :)
|
||||
|
||||
NewTactic constructor intro rw assumption rcases simp tauto trivial
|
||||
|
||||
end MySet
|
||||
NewLemma Set.subset_empty_iff
|
||||
|
||||
@@ -25,9 +25,13 @@ Statement nonempty_iff_ne_empty
|
||||
""
|
||||
{A : Type _} (s : Set A) :
|
||||
s.Nonempty ↔ s ≠ ∅ := by
|
||||
rw [Set.Nonempty]
|
||||
Hint "Am besten fängst du mit `unfold Set.Nonempty` an."
|
||||
unfold Set.Nonempty
|
||||
Hint "Mit `ne_eq` und `eq_empty_iff_forall_not_mem` kannst du hier weiterkommen."
|
||||
rw [ne_eq, eq_empty_iff_forall_not_mem]
|
||||
Hint (hidden := true) "`push_neg` kann hier helfen."
|
||||
push_neg
|
||||
rfl
|
||||
|
||||
NewTactic constructor intro rw assumption rcases simp tauto trivial
|
||||
NewLemma ne_eq Set.eq_empty_iff_forall_not_mem
|
||||
NewDefinition Set.Nonempty
|
||||
|
||||
@@ -31,3 +31,4 @@ Statement
|
||||
rw [univ_union]
|
||||
|
||||
NewTactic constructor intro rw assumption rcases simp tauto trivial
|
||||
NewLemma Set.diff_inter Set.union_assoc Set.union_diff_distrib Set.univ_union
|
||||
|
||||
@@ -1,4 +1,5 @@
|
||||
import GameServer.Commands
|
||||
import Adam.TacticDocs
|
||||
import Adam.LemmaDocs
|
||||
import Adam.DefinitionDocs
|
||||
import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ.
|
||||
|
||||
Reference in New Issue
Block a user