From 912ba39fe6aa2cf5efbe01a838f4b67a701ce74b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 3 Sep 2024 14:44:10 +0200 Subject: [PATCH] cleanup Quantus; introduce decide --- Game.lean | 14 ++++-- Game/Doc/Tactic.lean | 23 ++++++++- Game/Levels/FunctionBij/L03_Equivalence.lean | 2 +- Game/Levels/Luna.lean | 2 +- Game/Levels/Luna/L01_LE.lean | 2 +- Game/Levels/Luna/L02_Pos.lean | 2 +- Game/Levels/Luna/L03_Linarith.lean | 2 +- Game/Levels/Luna/L04_Linarith.lean | 2 +- Game/Levels/NewStuff/Prime.lean | 2 +- .../NewStuff/Prime/L04_ExistsUnique.lean | 7 ++- .../NewStuff/Prime/L07_InfinitudePrimes.lean | 4 +- Game/Levels/Quantus/L06_Exists.lean | 18 +++---- Game/Levels/Quantus/L09_PushNeg.lean | 30 ++++++------ Game/Levels/Quantus/L11_DrinkersParadox.lean | 49 ++++++++++--------- development-status.md | 8 +-- 15 files changed, 99 insertions(+), 68 deletions(-) diff --git a/Game.lean b/Game.lean index a0054dd..c15d239 100644 --- a/Game.lean +++ b/Game.lean @@ -13,6 +13,8 @@ import Game.Levels.Robotswana import Game.Levels.End +import Game.Levels.NewStuff.Prime + import Game.Levels.FunctionSurj import Game.Levels.FunctionInj import Game.Levels.FunctionBij @@ -95,10 +97,16 @@ CoverImage "images/Cover.png" Dependency Robotswana → End Dependency Cantor → End +-- Dependency Babylon → FunctionSurj + + +-- because of `∃!` +Dependency Prime → FunctionInj +-- Because of def `Injective` +Dependency FunctionInj → FunctionBij + --- Dependency Sum → FunctionSurj --- Dependency FunctionInj → FunctionBij -- Because of def `Injective` --- set_option lean4game.showDependencyReasons true +set_option lean4game.showDependencyReasons true /-! Build the game. Show's warnings if it found a problem with your game. diff --git a/Game/Doc/Tactic.lean b/Game/Doc/Tactic.lean index 55c2f6e..5a22043 100644 --- a/Game/Doc/Tactic.lean +++ b/Game/Doc/Tactic.lean @@ -780,7 +780,28 @@ Die Taktik `trans B` erstellt dann aus dem Goal zwei neue `A ↔ B` und `B ↔ C TacticDoc trans /-- -TODO +`decide` kann Aussagen beweisen, für die es einen einfachen Algorithmus +gibt, der die Wahr- oder Falschheit der Aussage bestimmt. + +Wichtige Beispiele sind: + +* `True` +* Aussagen zu konkreten Zahlen, wie `Even 4`, `2 ≤ 5`, `4 ≠ 6`, … + + +## Details + +Konkret sucht `decide` für eine Aussage `P` nach einer Instanz `Decidable P` +welche dann evaluiert entweder wahr oder falsch rausgibt. + +## Beispiel + +Folgendes kann mit `decide` gelöst werden: + +``` +Goal: + ¬ Odd 40 +``` -/ TacticDoc decide diff --git a/Game/Levels/FunctionBij/L03_Equivalence.lean b/Game/Levels/FunctionBij/L03_Equivalence.lean index 257afda..628f21a 100644 --- a/Game/Levels/FunctionBij/L03_Equivalence.lean +++ b/Game/Levels/FunctionBij/L03_Equivalence.lean @@ -37,5 +37,5 @@ Statement finThreeArrowEquiv {A : Type} : (Fin 3 → A) ≃ A × A × A := by · intro t simp -NewTactic fconstructor exact fin_cases +NewTactic fin_cases -- TODO: fin_cases should be in set-theory diff --git a/Game/Levels/Luna.lean b/Game/Levels/Luna.lean index 6799c1f..d561345 100644 --- a/Game/Levels/Luna.lean +++ b/Game/Levels/Luna.lean @@ -7,7 +7,7 @@ import Game.Levels.Luna.L04_Linarith The planet Luna is about inequalities `≤` and the tactic `linarith`. -/ -World "Inequality" +World "Luna" Title "Luna" Image "images/MoonLuna.png" diff --git a/Game/Levels/Luna/L01_LE.lean b/Game/Levels/Luna/L01_LE.lean index 005a513..b2d31c2 100644 --- a/Game/Levels/Luna/L01_LE.lean +++ b/Game/Levels/Luna/L01_LE.lean @@ -1,6 +1,6 @@ import Game.Metadata -World "Inequality" +World "Luna" Level 1 Title "Kleinergleich" diff --git a/Game/Levels/Luna/L02_Pos.lean b/Game/Levels/Luna/L02_Pos.lean index 4cbf057..ca7a02d 100644 --- a/Game/Levels/Luna/L02_Pos.lean +++ b/Game/Levels/Luna/L02_Pos.lean @@ -3,7 +3,7 @@ import Game.Metadata open Nat -World "Inequality" +World "Luna" Level 2 Title "Kleinergleich" diff --git a/Game/Levels/Luna/L03_Linarith.lean b/Game/Levels/Luna/L03_Linarith.lean index 303769b..082da44 100644 --- a/Game/Levels/Luna/L03_Linarith.lean +++ b/Game/Levels/Luna/L03_Linarith.lean @@ -1,7 +1,7 @@ import Game.Metadata -World "Inequality" +World "Luna" Level 3 Title "Linarith" diff --git a/Game/Levels/Luna/L04_Linarith.lean b/Game/Levels/Luna/L04_Linarith.lean index abb4280..410b079 100644 --- a/Game/Levels/Luna/L04_Linarith.lean +++ b/Game/Levels/Luna/L04_Linarith.lean @@ -1,6 +1,6 @@ import Game.Metadata -World "Inequality" +World "Luna" Level 4 Title "Linarith" diff --git a/Game/Levels/NewStuff/Prime.lean b/Game/Levels/NewStuff/Prime.lean index 43a8b75..0aec25c 100644 --- a/Game/Levels/NewStuff/Prime.lean +++ b/Game/Levels/NewStuff/Prime.lean @@ -12,7 +12,7 @@ The planet `Prime` is about prime numbers and divisibility. -/ World "Prime" -Title "[WIP] Primzahlen" +Title "Primzahlen" Introduction "Ihr schlendert durch die Befestigung ohne direktes Ziel. Und sprecht mit verschiedenen Einwohnern." diff --git a/Game/Levels/NewStuff/Prime/L04_ExistsUnique.lean b/Game/Levels/NewStuff/Prime/L04_ExistsUnique.lean index e6317c7..737fab1 100644 --- a/Game/Levels/NewStuff/Prime/L04_ExistsUnique.lean +++ b/Game/Levels/NewStuff/Prime/L04_ExistsUnique.lean @@ -20,8 +20,11 @@ Statement : ∃! p, Nat.Prime p ∧ Even p := by use 2 dsimp constructor - simp - exact Nat.prime_two + · decide + -- simp + -- exact Nat.prime_two rintro y ⟨hy, hy'⟩ rw [←Nat.Prime.even_iff hy] assumption + +NewDefinition ExistsUnique diff --git a/Game/Levels/NewStuff/Prime/L07_InfinitudePrimes.lean b/Game/Levels/NewStuff/Prime/L07_InfinitudePrimes.lean index ff32c03..150f996 100644 --- a/Game/Levels/NewStuff/Prime/L07_InfinitudePrimes.lean +++ b/Game/Levels/NewStuff/Prime/L07_InfinitudePrimes.lean @@ -19,9 +19,7 @@ open Nat Statement Nat.exists_infinite_primes (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by -- based on project by Maren Hint "**Du**: `minFac (n ! + 1)` ist der kleinste Primfaktor von $n! + 1$" - - let q := minFac (n ! + 1) - use q + use minFac (n ! + 1) constructor · apply le_minFac_factorial_succ n · apply minFac_factorial_succ_prime n diff --git a/Game/Levels/Quantus/L06_Exists.lean b/Game/Levels/Quantus/L06_Exists.lean index 51659ca..0c5c08f 100644 --- a/Game/Levels/Quantus/L06_Exists.lean +++ b/Game/Levels/Quantus/L06_Exists.lean @@ -60,30 +60,30 @@ Statement Nat.even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by was ausgerechnet `1 = 1 / 2 + 1 / 2 = 0 + 0` ist, du bist also auf dem Holzweg! " Hint " - **Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = {n}` … + **Du**: Also von `{h}` weiß ich jetzt, dass ein `s` existiert, so dass `s + s = {n}` … - **Robo**: Mit `obtain ⟨r, hr⟩ := {h}` kannst du dieses `r` tatsächlich einführen." - obtain ⟨r, hr⟩ := h + **Robo**: Mit `obtain ⟨s, hs⟩ := {h}` kannst du dieses `s` tatsächlich einführen." + obtain ⟨s, hs⟩ := h Hint " **Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = {n} ^ 2`? **Robo**: Genau. Und mit `use _` gibst du diese Zahl an." Hint (hidden := true) " - **Robo**: Also sowas ähnliches wie `use 4 * {r} ^ 3`, aber ich kann + **Robo**: Also sowas ähnliches wie `use 4 * {s} ^ 3`, aber ich kann dir leider nicht sagen, welche Zahl passt." Branch - rw [hr] + rw [hs] Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden." - use 2 * r ^ 2 + use 2 * s ^ 2 Hint (hidden := true) "**Du**: Ah, und jetzt `ring`!" ring - use 2 * r ^ 2 + use 2 * s ^ 2 Hint " **Du**: Ah, und jetzt `ring`! **Robo**: Aber zuerst musst du noch mit - `rw` `n` durch `{r} + {r}` ersetzen, da `ring` das sonst nicht weiß." - rw [hr] + `rw` `n` durch `{s} + {s}` ersetzen, da `ring` das sonst nicht weiß." + rw [hs] ring NewTactic unfold use diff --git a/Game/Levels/Quantus/L09_PushNeg.lean b/Game/Levels/Quantus/L09_PushNeg.lean index eb335d9..810844b 100644 --- a/Game/Levels/Quantus/L09_PushNeg.lean +++ b/Game/Levels/Quantus/L09_PushNeg.lean @@ -16,7 +16,7 @@ open Function Statement {X : Type} (P : X → Prop) : ¬ (∃ x : X, P x) ↔ ∀ x : X, ¬ P x := by Hint " - **Du**: Was ist denn jetzt dieses P? + **Du**: Was ist denn jetzt dieses `{P}`? **Robo**: `{P}` ist wieder irgendeine Aussage; eine Aussage über Objekte vom Typ `{X}`. Zum Beispiel könnte `{X}` wieder der Typ der natürlichen Zahlen sein. @@ -34,28 +34,28 @@ Statement {X : Type} (P : X → Prop) : **Robo**: Genau. Was du brauchst, ist `push_neg`." Branch + constructor + intro h + Hint (hidden := true) " + **Robo**: `push_neg` schiebt von links nach rechts. Du kannst es hier also nicht auf + das Beweisziel anwenden, wohl aber auf `{h}`." + push_neg at h + assumption + intro h push_neg - Hint (hidden := true) "**Robo**: Das ist jetzt eine Tautologie, oder?" - tauto - constructor - intro h - Hint (hidden := true) " - **Robo**: `push_neg` schiebt von links nach rechts. Du kannst es hier also nicht auf - das Beweisziel anwenden, wohl aber auf `{h}`." - push_neg at h - assumption - intro h + assumption push_neg - assumption + rfl NewTactic push_neg +DisabledTactic tauto Conclusion " -**Robo**: Gut gemacht. Intern benutzt `push_neg` übringens zwei Lemmas: +**Robo**: Gut gemacht. Intern benutzt `push_neg` übrigens zwei Lemmas: - - `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)` - - `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)` + - `not_exists (P : X → Prop) : ¬ (∃ x, P x) ↔ ∀ x, (¬ P x)` + - `not_forall (P : X → Prop) : ¬ (∀ x, P x) ↔ ∃ x, (¬ P x)` Das erste Lemma ist die Aussage, die du gerade gezeigt hast. diff --git a/Game/Levels/Quantus/L11_DrinkersParadox.lean b/Game/Levels/Quantus/L11_DrinkersParadox.lean index a32f172..e2ef693 100644 --- a/Game/Levels/Quantus/L11_DrinkersParadox.lean +++ b/Game/Levels/Quantus/L11_DrinkersParadox.lean @@ -7,7 +7,7 @@ Title "Drinker's Paradox" Introduction " -**Du**: Könnte ihr eigentlich immer nur im Chor oder durcheinander reden? +**Du**: Könnt ihr eigentlich immer nur im Chor oder durcheinander reden? Wieder herrscht längeres Schweigen. Dann auf einmal: @@ -33,40 +33,40 @@ open Function Statement {People : Type} [h_nonempty : Nonempty People] (isDrinking : People → Prop) : ∃ (x : People), isDrinking x → ∀ (y : People), isDrinking y := by Hint " - **Du**: Also, `isDrinking` ist wieder so ein Prädikat … - Wenn `p` eine Person ist, ist `isDrinking p` eine Aussage, + **Du**: Also, `{isDrinking}` ist wieder so ein Prädikat … + Wenn `p` eine Person ist, ist `{isDrinking} p` eine Aussage, die wahr oder falsch ist. Soweit so gut. - Und was bedeutet `Nonempty People`? + Und was bedeutet `Nonempty {People}`? **Robo**: Das ist Leansch für nicht-leer. Das heißt einfach, es gibt mindestens eine Person. - Mit `use Classical.arbitrary People` kannst du dir eine `pers : Person` aussuchen und verwenden, + Mit `use Classical.arbitrary {People}` kannst du dir eine `pers : {People}` aussuchen und verwenden, die es per Annahme gibt. **Du**: Und wie fang ich jetzt an? **Robo**: Ich sagte doch, schau am besten Mal in deine Handbibliothek. Wenn ich mich richtige erinnere, hilft eine Fallunterscheidung, ob die Aussage - `∀ (y : People), isDrinking y` wahr oder falsch ist." + `∀ (y : {People}), {isDrinking} y` wahr oder falsch ist." Hint (hidden := true) "**Robo**: Schau mal `by_cases` an." by_cases h : ∀ y, isDrinking y - Hint (hidden := true) " - **Du**: Und wen nehm ich jetzt? - - **Robo**: Wie gesagt, mit `use Classical.arbitrary People` kannst du eine beliebige - Person auswählen und verwenden." - use Classical.arbitrary People - intro - assumption - Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen." - push_neg at h - Hint (hidden := true) "**Du**: Also nach `{h}` existiert ja eine Person, die nicht trinkt. Könnte ich diese brauchen damit die Aussage trivialerweise wahr wird? - - **Robo**: Schau dir mal an wie man `obtain` auf die Annahme `{h}` anwenden könnte." - obtain ⟨p, hp⟩ := h - use p - intro hp' - Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?" - contradiction + · Hint (hidden := true) " + **Du**: Und wen nehm ich jetzt? + + **Robo**: Wie gesagt, mit `use Classical.arbitrary {People}` kannst du eine beliebige + Person auswählen und verwenden." + use Classical.arbitrary People + intro + assumption + · Hint (hidden := true) "**Robo**: Du könntest hier mit `push_neg at {h}` weitermachen." + push_neg at h + Hint (hidden := true) "**Du**: Also nach `{h}` existiert ja eine Person, die nicht trinkt. Könnte ich diese brauchen damit die Aussage trivialerweise wahr wird? + + **Robo**: Schau dir mal an wie man `obtain` auf die Annahme `{h}` anwenden könnte." + obtain ⟨p, hp⟩ := h + use p + intro hp' + Hint (hidden := true) "**Robo**: Was siehst du, wenn du `{hp}` und `{hp'}` anschaust?" + contradiction /-- TODO -/ TheoremDoc Classical.arbitrary as "Classical.arbitrary" in "Logic" @@ -93,6 +93,7 @@ Conclusion |:------|:--------------------------|:-------------------------------------------------------| | *13ᶜ* | `rw` | Umschreiben mit Gleichungen. | | 15 | `ring` | Löst Gleichungen mit `+, -, *, ^`. | +| *4ᵇ* | `decide` | Kann auch Aussagen zu konkreten Zahlen beantworten. | | 16 | `unfold` | Setzt visuell die Bedeutung einer Definition ein. | | 17 | `use` | Um ein `∃` im Goal anzugehen. | | *7ᵈ* | `obtain ⟨x, hx⟩ := h` | Um ein `∃` in den Annahmen zu zerlegen. | diff --git a/development-status.md b/development-status.md index 12994c0..f27d97f 100644 --- a/development-status.md +++ b/development-status.md @@ -1,9 +1,9 @@ | Planet | new name | levels | tried? | hints | story | summary | picture | desirable changes | |:-----------------------|:---------|:---------------|:-------|:-------|:-------|:--------|:--------|:------------------------------------------------------------------------------------------------------| -| Logos | == | +++ | +++ | +++ | +++ | + | +++ | JE: DONE TODO: TacticDoc `decide`. | +| Logos | == | +++ | +++ | +++ | +++ | + | +++ | JE: DONE | | Implis | == | +++ | +++ | +++ | ++ | + | +++ | JE: DONE | -| Quantus | == | +++ | +++ | +++ | +++ | + | +++ | (add ∃! ? -- see Prime planet); TODO: replace L05 by `decide` (eg: prove that 5 is odd or 8 is even) | +| Quantus | == | +++ | +++ | +++ | +++ | + | +++ | JE: DONE | | Spinoza | == | ++ | ++ | ++ | ++ | | +++ | TODO: add TFAE tactics (used in boss of FunctionSurj) | | Luna | == | + | +++ | +++ | +++ | | +++ | TODO: level explaining `obtain h_lt \| h_eq \| h_gt := lt_trichotomy a b` (needed in FunctionInj L04) | | Babylon | == | + | +++ | +++ | +++ | | +++ | TODO: add sum over zeroes, adding over singleton | @@ -17,7 +17,7 @@ | ~FiniteSetTheory | TODO | TODO | | | | | TODO | | | SymmSquare | TODO | o TODO: L08 | TODO | TODO | TODO | | TODO | | | Quotient | TODO | 7-? | TODO | | TODO | | TODO | | -| Prime | TODO | + | TODO | TODO | TODO | | TODO | TODO: introduce ∃! | +| Prime | TODO | + | TODO | TODO | TODO | | TODO | TODO: introduce ∃! | | ? RealUncountable | TODO | TODO . | | | | | | | | GoodByePlanet | | TODO (.) | | | | | +++ | JE: added empty `End` planet | | | | | | | | | | | @@ -64,7 +64,7 @@ Trick `obtain h_lt | h_eq | h_gt := lt_trichotomy a b` needs to be explained on #### L05: use the fact that StrictMono is injective Perhaps swap L04 and L05 (L05 is the easier level, and motivates L04) - + Both L04 and L05 could be move closer to levels about ‘existence of left inverse implies injectivity`. #### L06: succ has left inverse, using if … then … else