levels

2023-02-27 10:40:46 +01:00
parent c065dcc5e3
commit cbd1867148
12 changed files with 46 additions and 106 deletions
@@ -8,6 +8,7 @@ import TestGame.Levels.Prime
 import TestGame.Levels.Induction

 import TestGame.Levels.Numbers
+import TestGame.Levels.Inequality

 import TestGame.Levels.LeanStuff
 import TestGame.Levels.SetTheory
@@ -43,9 +44,10 @@ Conclusion

 Path Proposition → Implication → Predicate → Prime
 Path Predicate → Contradiction → LeanStuff → SetTheory → SetTheory2 → SetFunction
-Path Predicate → Induction → LeanStuff → Function → SetFunction
 Path SetTheory2 → Numbers

 Path Module → Basis → Module2

+Path Contradiction → Inequality → Induction → LeanStuff → Function → SetFunction
+
 MakeGame
@@ -37,6 +37,15 @@ LemmaDoc imp_iff_not_or as imp_iff_not_or in "Logic"
 `(A B : Prop)`
 "

+
+LemmaDoc Nat.succ_pos as Nat.succ_pos in "Nat"
+"
+"
+
+LemmaDoc zero_lt_iff as zero_lt_iff in "Nat"
+"
+"
+
 LemmaDoc zero_add as zero_add in "Addition"
 "This lemma says `∀ a : ℕ, 0 + a = a`."

@@ -17,4 +17,4 @@ TODO
 Statement
 "TODO: Find an exercise."
    (U S T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x)  := by
-  trivial
+  simp only [Function.comp_apply]
@@ -32,8 +32,6 @@ Zum Beispiel kennt es ein Lemma das ungefähr so aussieht:
 lemma sum_const_add (n : ℕ) : (∑ i in Fin n, 0) = 0 := by
  sorry
 ```
-
-Mit `simp?` anstatt `simp` kannst du zudem schauen, welche Lemmas von `simp` benutzt wurde.
 "

 open BigOperators
@@ -1,10 +1,8 @@
-import TestGame.Levels.Prime.L01_Linarith
-import TestGame.Levels.Prime.L02_Linarith
-import TestGame.Levels.Prime.L03_Dvd
+import TestGame.Levels.Prime.L01_Dvd
 import TestGame.Levels.Prime.L04_Prime
 import TestGame.Levels.Prime.L05_Prime
 import TestGame.Levels.Prime.L06_ExistsUnique

 Game "TestGame"
 World "Prime"
-Title "mehr Nat"
+Title "Teilbarkeit"
@@ -1,29 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Linarith
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Prime"
-Level 1
-
-Title "Kleinergleich"
-
-Introduction
-"
-Ungleichheiten werden in Lean generell immer als Kleinergleich `≤` (`\\le`) oder `<`
-geschrieben.
-
-Die Symbole `≥` und `>` gibt es zwar auch, sind aber nur Notation für die gleiche
-Aussage mit `≤` und `<`.
-
-Die Taktik `linarith` kann alle Systeme von linearen (Un-)gleichungen über `ℤ`, `ℚ`, etc. lösen.
-Über `ℕ` ist sie etwas schwächer, aber einfache Aussagen kann sie trotzdem beweisen.
-"
-
-Statement
-"Wenn $n \\ge 2$, zeige, dass $n$ nich Null sein kann."
-    (n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
-  linarith
-
-NewTactics linarith
@@ -1,31 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.Linarith
-
-Game "TestGame"
-World "Prime"
-Level 2
-
-Title "Linarith"
-
-Introduction
-"
-Sobald man mit einem Ring arbeitet, der eine lineare Order hat (also z.B. `ℤ` oder `ℚ`),
-ist `linarith` stärker und kann Systeme von Gleichungen und Ungleichungen angehen.
-
-`linarith` kann aber nur mit linearen Ungleichungen umgehen, mit Termen der Form `x ^ 2`
-kann es nicht umgehen.
-"
-
-Statement
-"Angenommen man hat für zwei Ganzzahlen $x, y$ folgende Ungleichungen.
-$$
-\\begin{aligned} 5 * y &\\le 35 - 2 * x \\\\ 2 * y &\\le x + 3 \\end{aligned}
-$$
-Zeige, dass $y \\le 5$.
-
-"
-    (x y : ℤ)
-    (h₂ : 5 * y ≤ 35 - 2 * x)
-    (h₃ : 2 * y ≤ x + 3)
-    : y ≤ 5 := by
-  linarith
@@ -1,29 +0,0 @@
-import TestGame.Metadata
-
-import Mathlib.Tactic.Ring
-
-Game "TestGame"
-World "Prime"
-Level 3
-
-Title "Teilbarkeit"
-
-Introduction
-"
-Die Aussage \"$m$ teilt $n$.\" wird in Lean als `m | n` (`\\|`) geschrieben.
-
-**Wichtig:** `∣` (Teilbarkeit) ist ein spezielles Unicode Symbol, das nicht dem
-senkrechten Strich auf der Tastatur (`|`) entspricht. Man erhält es mit `\\|`.
-
-`m ∣ n` bedeutet `∃ c, n = m * c`, das heisst, man kann damit genau gleich umgehen
-wie mit einem `∃`-Quantifier.
-"
-
-Statement dvd_add
-  "Wenn $m$ ein Teiler von $n$ und $k$ ist, dann teilt es die Summe."
-  (n m k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k := by
-  rcases h with ⟨x, h⟩
-  rcases g with ⟨y, g⟩
-  use x + y
-  rw [h, g]
-  ring
@@ -11,20 +11,21 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Prime"
-Level 4
+Level 2

 Title "Primzahlen"

 Introduction
 "
-Um zu sagen, dass eine natürliche Zahl $n$ eine Primzahl ist, braucht man
-eine Aussage `Nat.Prime n`, ähnlich wie `Even n`.
+Eine Primzahl wird mit `(n : ℕ) (h : Nat.Prime n)` dargestellt.

-Primzahlen sind ein Objekt in Lean, das genug abstrakt definiert ist, dass es sich
-aus mathematischer Sicht nicht lohnt mit der Definition zu arbeiten.
+Wichtige Lemmas über Primzhalen werden mit

-Alle wichtigen Lemmas um mit Primzahlen zu arbeiten sind in
-[`import Data.Nat.Prime`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html)
+```
+import Data.Nat.Prime
+```
+importiert (siehe
+[Docs](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Nat/Prime.html))

 Insbesondere `Nat.prime_def_lt''` welches die aus der Schule bekannte Definition einer
 Primzahl `Prime p ↔ 2 ≤ p ∧ (∀ m, m ∣ p → m = 1 ∨ m = p)` gibt.
@@ -11,7 +11,7 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Prime"
-Level 5
+Level 3

 Title "Primzahlen"

@@ -11,7 +11,7 @@ import TestGame.ToBePorted

 Game "TestGame"
 World "Prime"
-Level 6
+Level 4

 Title "Existiert eindeutig"

@@ -61,12 +61,33 @@ TacticDoc rewrite
 Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
 "

+TacticDoc induction
+"
+## Beschreibung
+
+Wie `rw` aber ruft `rfl` am Schluss nicht automatisch auf.
+"
+
+
 TacticDoc linarith
 "
 ## Beschreibung

 "

+TacticDoc fin_cases
+"
+## Beschreibung
+
+"
+
+TacticDoc funext
+"
+## Beschreibung
+
+"
+
+
 TacticDoc rw
 "
 ## Beschreibung