levels
This commit is contained in:
Jon Eugster
@@ -0,0 +1,9 @@
|
||||
import TestGame.Levels.Inequality.L01_Induction
|
||||
import TestGame.Levels.Inequality.L02_LE
|
||||
import TestGame.Levels.Inequality.L03_Pos
|
||||
import TestGame.Levels.Inequality.L04_Linarith
|
||||
import TestGame.Levels.Inequality.L05_Linarith
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Title "Ungleichung"
|
||||
@@ -0,0 +1,42 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Level 1
|
||||
|
||||
Title "Induktion"
|
||||
|
||||
set_option tactic.hygienic false
|
||||
|
||||
Introduction
|
||||
"
|
||||
Hier lernst du Induktion und Ungleichungen kennen. Beides essenziele Grundlagen, die du
|
||||
für spätere Aufgaben brauchst.
|
||||
|
||||
Die Leantaktik `induction n` führt einen Induktionsbeweis über `(n : ℕ)`. Hier zuerst
|
||||
ein abstraktes Beispiel.
|
||||
"
|
||||
|
||||
Statement
|
||||
"Sei $P(n)$ eine logische Aussage über die natürliche Zahl.
|
||||
Agenommen $P(0)$ ist wahr und $P(m) \\Rightarrow P(m+1)$ für alle $m$,
|
||||
dann gilt $P(n)$ für alle $n \\in \\mathbb{N}.$"
|
||||
(n : ℕ) (P : ℕ → Prop) (h_base : P 0) (h_step : ∀ m, P m → P m.succ) : P n := by
|
||||
induction n
|
||||
assumption
|
||||
apply h_step
|
||||
assumption
|
||||
|
||||
-- TODO: Why are these not shown.
|
||||
HiddenHint (n : ℕ) (P : ℕ → Prop) : P n =>
|
||||
"Benutze `induction n`."
|
||||
|
||||
Hint (P : ℕ → Prop) : P 0 =>
|
||||
"Das ist die Induktionsverankerung, hier musst du $P(0)$ zeigen."
|
||||
|
||||
Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
|
||||
"An der Stelle kommt der Beweis $P(m) \\Rightarrow P(m+1)$.
|
||||
|
||||
In diesem Beispiel kannst du `apply` benützen."
|
||||
|
||||
NewTactics induction
|
||||
@@ -0,0 +1,24 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Level 2
|
||||
|
||||
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 `<`.
|
||||
|
||||
Zudem sind `<` und `≤` auf `ℕ` so definiert, dass `0 < n` und `1 ≤ n` per Definition
|
||||
äquivalent sind. Die folgende Aussage ist also mit `rfl` beweisbar.
|
||||
"
|
||||
|
||||
Statement
|
||||
"$0 < n$ und $1 ≤ n$ sind äquivalente Aussagen."
|
||||
(n m : ℕ) : m < n ↔ m.succ ≤ n := by
|
||||
rfl
|
||||
@@ -0,0 +1,54 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Level 3
|
||||
|
||||
Title "Kleinergleich"
|
||||
|
||||
Introduction
|
||||
"
|
||||
Es gibt zwei intrinsische Möglichkeiten, zu sagen dass `(n : ℕ)` nicht Null ist:
|
||||
`n ≠ 0` oder `0 < n`.
|
||||
|
||||
Das folgende Lemma kannst du immer brauchen um zwischen den beiden zu wechseln.
|
||||
|
||||
Note: `0 < n` wird in Lemmanamen oft mit `_pos` beschrieben anstatt `zero_lt`, siehe z.B.
|
||||
`Nat.succ_pos`.
|
||||
"
|
||||
|
||||
Statement zero_lt_iff
|
||||
"$0 < n$ und $n \\ne 0$ sind äquivalente Aussagen."
|
||||
(n : ℕ) : 0 < n ↔ n ≠ 0 := by
|
||||
constructor
|
||||
intro h
|
||||
by_contra g
|
||||
rw [g] at h
|
||||
contradiction
|
||||
intro h
|
||||
induction n
|
||||
contradiction
|
||||
apply Nat.succ_pos
|
||||
|
||||
NewLemmas Nat.succ_pos
|
||||
|
||||
Hint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
|
||||
"An dieser Stelle fürst du am besten einen Beweis durch Widerspruch."
|
||||
|
||||
HiddenHint (n : ℕ) (h : 0 < n) : n ≠ 0 =>
|
||||
"Das macht man mit `by_contra`."
|
||||
|
||||
Hint (n : ℕ) (h : 0 < n) (g : n = 0) : False =>
|
||||
"Brauche `rw [_] at _` um eine Annahme `0 < 0` zu erzeugen."
|
||||
|
||||
HiddenHint (h : 0 < 0) : False =>
|
||||
"Mit `contradiction` schliesst du den Widerspruchsbeweis."
|
||||
|
||||
Hint (n : ℕ) (h : n ≠ 0) : 0 < n =>
|
||||
"Diese Richtung beweist du am besten per Induktion."
|
||||
|
||||
HiddenHint (n : ℕ) (h : n ≠ 0) : 0 < n =>
|
||||
"Starte mit `induction n`."
|
||||
|
||||
Hint (m : ℕ) : 0 < Nat.succ m =>
|
||||
"Hier kannst du das Lemma `Nat.succ_pos` anwenden."
|
||||
@@ -0,0 +1,23 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib.Tactic.Linarith
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Level 4
|
||||
|
||||
Title "Linarith"
|
||||
|
||||
Introduction
|
||||
"
|
||||
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
|
||||
|
||||
NewLemmas zero_lt_iff
|
||||
@@ -0,0 +1,28 @@
|
||||
import TestGame.Metadata
|
||||
import Mathlib.Tactic.Linarith
|
||||
|
||||
Game "TestGame"
|
||||
World "Inequality"
|
||||
Level 5
|
||||
|
||||
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
|
||||
@@ -0,0 +1,52 @@
|
||||
import TestGame.Metadata
|
||||
|
||||
import Mathlib.Tactic.Ring
|
||||
|
||||
Game "TestGame"
|
||||
World "Prime"
|
||||
Level 1
|
||||
|
||||
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
|
||||
|
||||
HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (h : m ∣ n) (g : m ∣ k) : m ∣ n + k =>
|
||||
"
|
||||
Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
|
||||
sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
|
||||
"
|
||||
|
||||
HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (h : n = m * x) (g : m ∣ k) : m ∣ n + k =>
|
||||
"
|
||||
Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
|
||||
sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
|
||||
"
|
||||
|
||||
HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (y : ℕ) (h : m ∣ n) (g : k = m * y) : m ∣ n + k =>
|
||||
"
|
||||
Wenn man explizit mit der Definition von Teilbarkeit arbeiten will,
|
||||
sollte man als erstes alle Annahmen der Form `x ∣ y` mit `rcases` aufteilen.
|
||||
"
|
||||
|
||||
HiddenHint (n : ℕ) (m : ℕ) (k : ℕ) (x : ℕ) (y : ℕ) (h : n = m * x) (g : k = m * y) : m ∣ n + k =>
|
||||
"
|
||||
Jetzt kannst du mit `use` eine Zahl angeben, so dass $m * X = n + k$.
|
||||
"
|
||||
Reference in New Issue
Block a user