diff --git a/server/adam/Adam/LemmaDocs.lean b/server/adam/Adam/LemmaDocs.lean index 91fdc15..aa15b23 100644 --- a/server/adam/Adam/LemmaDocs.lean +++ b/server/adam/Adam/LemmaDocs.lean @@ -363,7 +363,7 @@ LemmaDoc add_pow_two as "add_pow_two" in "Nat" * Mathlib Doc: [#add_pow_two](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupPower/Ring.html#add_pow_two) " -LemmaDoc Finset.sum_comm as "Finset.sum_comm" in "Sum" +LemmaDoc Finset.sum_comm as "sum_comm" in "Sum" " ## Eigenschaften diff --git a/server/adam/Adam/Levels/Contradiction/L01_Have.lean b/server/adam/Adam/Levels/Contradiction/L01_Have.lean index 89e9d7c..39c85bc 100644 --- a/server/adam/Adam/Levels/Contradiction/L01_Have.lean +++ b/server/adam/Adam/Levels/Contradiction/L01_Have.lean @@ -7,6 +7,8 @@ import Mathlib.Tactic.Ring import Adam.ToBePorted +set_option tactic.hygienic false + Game "Adam" World "Contradiction" Level 1 @@ -49,10 +51,10 @@ Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by Hint (hidden := true) "**Robo**: `apply` sollte helfen" apply h assumption - · Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen? + Hint "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen? - **Robo**: `contradiction`." - contradiction + **Robo**: `contradiction`." + contradiction NewTactic «have» DisabledTactic «suffices» diff --git a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean index 0c75735..c16ae6c 100644 --- a/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean +++ b/server/adam/Adam/Levels/Contradiction/L04_ByContra.lean @@ -23,7 +23,7 @@ Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by Hint "**Du**: Ja, das habe ich tatsächlich schon einmal gesehen. **Robo**: Ja, klar hast du das schon einmal gesehen. Das benutzen Mathematiker doch ständig. Wenn ihnen zu $A ⇒ B$ nichts einfällt, zeigen sie stattdessen $¬B ⇒ ¬A$. Ich würde das ja statt *Kontraposition* oder `not_imp_not` eher *von_hinten_durch_die_Brust_ins_Auge* nennen. Aber gut, ich will mich nicht einmisschen. - " + " Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an." constructor intro h b @@ -44,5 +44,6 @@ Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by DisabledTactic rw DisabledLemma not_not +LemmaTab "Logic" Conclusion "" diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean index 638f18e..a040cec 100644 --- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean +++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean @@ -14,7 +14,7 @@ Title "Kontraposition" Introduction " -**Benedictus**: Gut, hier ist die angekündigte Frage. Versucht mal einen *direkten* Beweis, ohne `contrapose`. +**Benedictus**: Gut, hier ist die angekündigte Frage. Versucht mal einen *direkten* Beweis, ohne `by_contra`. " -- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma @@ -44,7 +44,7 @@ Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by **Robo**: Erinner dich an `revert`. Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Beweissziel schieben." revert h - Hint "**Du**: Und jetzt kann ich dieses Kontrapositionslemma anwenden? Wie hieß das noch einmal? + Hint "**Du**: Und jetzt kann ich dieses Kontrapositionslemma anwenden? Wie hieß das noch einmal? **Robo**: Tatsächlich kannst auch einfach `contrapose` schreiben. " @@ -52,10 +52,13 @@ Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by Hint (hidden := true) "**Robo**: Vielleicht hilft jetzt `even_iff_not_odd` weiter?" rw [← even_iff_not_odd] rw [← even_iff_not_odd] - Hint "**Du**: Das sieht schon ganz gut aus. Jetzt kann ich tatsächlich das alte Lemma anwenden!" + Hint "**Du**: Das sieht schon ganz gut aus. Jetzt kann ich tatsächlich das alte Lemma + `even_square` anwenden!" apply even_square +NewLemma even_square NewTactic contrapose DisabledTactic by_contra +LemmaTab "Nat" -Conclusion "**Benedictus**: Hervorragend! Ich glaube, damit seid Ihr jetzt ganz gut gewappnet." +Conclusion "**Benedictus**: Hervorragend! Ich glaube, damit seid Ihr jetzt ganz gut gewappnet." diff --git a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean index 5c51b37..c578ce3 100644 --- a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean +++ b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean @@ -31,11 +31,11 @@ open Nat Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by Hint "Sobald Ihr Euch sicher vom Gravitationsfeld des Asteroiden befreit habt, beugt Ihr Euch wieder über die Aufgabe. - + **Robo**: Ok, also diesmal fangen wir mit `by_contra g` an!" by_contra g Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen." - Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`." + Hint (hidden := true) "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`." suffices d : ¬ Odd (n ^ 2) contradiction rw [←even_iff_not_odd] at * @@ -49,7 +49,7 @@ Conclusion "**Robo**: Bravo! Hier ein Überblick, was uns Benediktus gezeigt hat | | Taktik | Beispiel | |:------|:----------------|:-------------------------------------------------------| -| 177 | `have` | Zwischenresultat annehmen | +| 17 | `have` | Zwischenresultat annehmen | | 18 | `suffices` | Zwischenresultat annehmen | | 19 | `by_contra` | Widerspruch *(startet einen Widerspruchsbeweis)* | | *3* | `contradiction` | *(schliesst einen Widerspruchsbeweis)* | diff --git a/server/adam/Adam/Levels/Implication/L06_Iff.lean b/server/adam/Adam/Levels/Implication/L06_Iff.lean index 73432b7..c63948b 100644 --- a/server/adam/Adam/Levels/Implication/L06_Iff.lean +++ b/server/adam/Adam/Levels/Implication/L06_Iff.lean @@ -27,7 +27,7 @@ Conclusion " **Operationsleiter**: Ok, das leuchtet mir ein. -**Robo** *(zu Dir)*: Übrigens, so wie bei `(h : A ∧ B)` die beiden Teile `h.left` und `h.right` heißen, +**Robo** *(zu dir)*: Übrigens, so wie bei `(h : A ∧ B)` die beiden Teile `h.left` und `h.right` heißen, heißen bei `(h : A ↔ B)` die beiden Teile `h.mp` und `h.mpr`. **Du**: Also `h.mp` ist `A → B`? Wieso `mp`? diff --git a/server/adam/Adam/Levels/Implication/L07_Rw.lean b/server/adam/Adam/Levels/Implication/L07_Rw.lean index c78334b..7551676 100644 --- a/server/adam/Adam/Levels/Implication/L07_Rw.lean +++ b/server/adam/Adam/Levels/Implication/L07_Rw.lean @@ -33,7 +33,7 @@ Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : sowas wie `A ↔ A` erhältst, kann `rfl` das beweisen. **Robo: Da fällt mir ein, `rw` wendet ohnehin auch versuchsweise `rfl` an. - Das heißt, Du musst `rfl` nicht einmal ausschreiben." + Das heißt, du musst `rfl` nicht einmal ausschreiben." rw [h₂] rw [←h₂] assumption diff --git a/server/adam/Adam/Levels/Inequality/L01_LE.lean b/server/adam/Adam/Levels/Inequality/L01_LE.lean index eaebe8b..b41f27b 100644 --- a/server/adam/Adam/Levels/Inequality/L01_LE.lean +++ b/server/adam/Adam/Levels/Inequality/L01_LE.lean @@ -8,7 +8,7 @@ Title "Kleinergleich" Introduction " -*(Gesrpäch)* +*(Gespräch)* **Robo** (*lallend*, oder war's fröhlich proklamierend?): …und deshalb sind `≥` und `>` eigentlich nur Notationen für `≤`, diff --git a/server/adam/Adam/Levels/Inequality/L02_Pos.lean b/server/adam/Adam/Levels/Inequality/L02_Pos.lean index a32b5ac..ea47042 100644 --- a/server/adam/Adam/Levels/Inequality/L02_Pos.lean +++ b/server/adam/Adam/Levels/Inequality/L02_Pos.lean @@ -4,6 +4,8 @@ import Mathlib.Tactic.LibrarySearch set_option tactic.hygienic false +open Nat + Game "Adam" World "Inequality" Level 2 @@ -12,12 +14,12 @@ Title "Kleinergleich" Introduction " -*weitere Person*: …ich sag dir, eine positive Zahl kann man sowohl mit `0 < n` +**weitere Person**: …ich sag dir, eine positive Zahl kann man sowohl mit `0 < n` als auch `n ≠ 0` darstellen. -*Robo*: Und da gibts leider keinen Standard dazu. +**Robo**: Und da gibts leider keinen Standard dazu. -**weitere Person*: Ja und, da kann man ja einfach mit `Nat.pos_iff_ne_zero` +**weitere Person**: Ja und, da kann man ja einfach mit `Nat.pos_iff_ne_zero` wechseln. Wart mal, wieso galt das nochmals… " @@ -35,7 +37,11 @@ Statement Nat.pos_iff_ne_zero (n : ℕ) : 0 < n ↔ n ≠ 0 := by **Robo** (*flüsternd*): Zweiter pompöser Auftritt: sag einfach `simp` und lass das alles automatisch geschehen." simp - Hint "**Du**: Und hier fang ich wohl am besten an wie ich das schon kenne." + Hint "**Du**: Ah und jetzt falls `n ≠ 0`." + Branch + simp + Hint "**Robo**: Warte! Den Rest geb ich dir als Lemma: `Nat.suc_pos`." + apply Nat.succ_pos constructor intro simp diff --git a/server/adam/Adam/Levels/Lean/L02_Universe.lean b/server/adam/Adam/Levels/Lean/L02_Universe.lean index c20c171..91ae55e 100644 --- a/server/adam/Adam/Levels/Lean/L02_Universe.lean +++ b/server/adam/Adam/Levels/Lean/L02_Universe.lean @@ -35,7 +35,12 @@ Statement (R : Type u) [CommRing R] (a b : R) : a + b = b + a := by Hint "**Robo**: Naja, Aufgaben zu Universen sind nicht so natürlich, aber vorige Aufgabe würde man eigentlich besser so schreiben, da - kannst du mindestens das Uniersum beobachten." + kannst du mindestens das Uniersum beobachten. + + **Du**: Ah ich sehe, `(R: Type u)` anstatt `(R : Type)`. Muss mich + das interessieren? + + **Robo**: Nicht wirklich…" ring Conclusion "**Du**: Na dann. Aber gut dass ich's mal gesehen hab." diff --git a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean index 19a8411..4a75f22 100644 --- a/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean +++ b/server/adam/Adam/Levels/Lean/L03_ImplicitArguments.lean @@ -9,6 +9,8 @@ Game "Adam" World "Lean" Level 3 +open Fin + Title "Implizite Argumente" Introduction @@ -20,8 +22,10 @@ haben als ich hinschreiben muss. ein Lemma von vorhin ``` -lemma Fin.sum_univ_castSucc {β : Type _} [AddCommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) : - ∑ i : Fin (n + 1), f i = ∑ i : Fin n, f (↑Fin.castSucc.toEmbedding i) + f (Fin.last n) := by +lemma Fin.sum_univ_castSucc {β : Type _} [AddCommMonoid β] + {n : ℕ} (f : Fin (n + 1) → β) : + ∑ i : Fin (n + 1), f i = + ∑ i : Fin n, f (↑Fin.castSucc.toEmbedding i) + f (Fin.last n) := by sorry ``` @@ -57,9 +61,11 @@ Statement (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Na nicht mehr geht, aber das war nicht der Punkt…" rfl rw [Fin.sum_univ_castSucc (n := m + 1)] + Hint "**Robo**: Gut der Rest ist easy." rfl -OnlyTactic rw rfl +OnlyTactic rw rfl simp trivial +LemmaTab "Sum" Conclusion "**Du**: Gibt es auch noch ander Methoden implizite Argumente anzugeben. diff --git a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean index dbb5425..9573286 100644 --- a/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean +++ b/server/adam/Adam/Levels/Lean/L04_InstanceArguments.lean @@ -35,12 +35,13 @@ open BigOperators Statement (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i := by - Hint "*Robo*: Schreibe `rw [@Fin.sum_univ_castSucc _ _ (m + 1)]` + Hint "**Robo**: Schreibe `rw [@Fin.sum_univ_castSucc _ _ (m + 1)]` anstatt `rw [Fin.sum_univ_castSucc (n := m + 1)]`!" rw [@Fin.sum_univ_castSucc _ _ (m + 1)] rfl -OnlyTactic rw rfl +OnlyTactic rw rfl simp trivial +LemmaTab "Sum" Conclusion " **Du**: Danke Robo! diff --git a/server/adam/Adam/Levels/Predicate.lean b/server/adam/Adam/Levels/Predicate.lean index e2f855b..4d7d0a1 100644 --- a/server/adam/Adam/Levels/Predicate.lean +++ b/server/adam/Adam/Levels/Predicate.lean @@ -12,7 +12,7 @@ Game "Adam" World "Predicate" Title "Quantus" -Introduction "Auf dem Schwestermond Quantus erwartet Euch bereits ein großer Ansammlung von Formalosopheninnen. Sie reden alle wild durcheinander und Ihr habt Probleme, Euch überhaupt Gehör zu verschaffen. Robo produziert schließlich ein lautes Gong-Geräusch, das sie kurzzeitig zur Ruhe bringt. +Introduction "Auf dem Schwestermond Quantus erwartet Euch bereits ein großer Ansammlung von Formalosopheninnen. Sie reden alle wild durcheinander und Ihr habt Probleme, Euch überhaupt Gehör zu verschaffen. Robo produziert schließlich ein lautes Gong-Geräusch, das sie kurzzeitig zur Ruhe bringt. **Du**: Wir haben einen Brief für Eure Königin. Könntet Ihr uns zu Eurer Königin führen? @@ -22,23 +22,23 @@ Introduction "Auf dem Schwestermond Quantus erwartet Euch bereits ein großer An Nun herrscht betretenes Schweigen. Alle zucken mit den Schultern. -**Du**: Habt Ihr überhaupt eine Königin? +**Du**: Habt Ihr überhaupt eine Königin? **Alle** *(im Chor)*: Ja, ja. Wir haben eine Königen, wir haben eine Königen. -**Robo** *(zu Dir)*: Ich fasse mal zusammen. Es existiert eine Königen, aber keiner weiß, wer sie ist … +**Robo** *(zu dir)*: Ich fasse mal zusammen. Es existiert eine Königen, aber keiner weiß, wer sie ist … -**Du**: Ist das nicht ein Widerspruch? +**Du**: Ist das nicht ein Widerspruch? **Robo**: Fragst du, du als Mathematiker? Nein, das ist kein Widerspruch. Das ist einfach eine „reine Existenzaussage“. Du bist dir nicht ganz sicher, wie ernst er das meint. -**Du**: Dann ich schlage vor, wir übergeben das Päckchen einfach an *alle* Bewohner. Dann haben wir es ja insbesondere der Königin übergeben. +**Du**: Dann ich schlage vor, wir übergeben das Päckchen einfach an *alle* Bewohner. Dann haben wir es ja insbesondere der Königin übergeben. **Du** *(in die Menge*): Wir haben Euch ein Päckchen von Implis gebracht. Hier, das ist für Euch. -Robo spuckt es aus, wirft es in die Menge, und die Formalosophinnen reißen es auf. Darin befinden sich ein paar loser Seiten, die sie sofort eingehend studieren. +Robo spuckt es aus, wirft es in die Menge, und die Formalosophinnen reißen es auf. Darin befinden sich ein paar loser Seiten, die sie sofort eingehend studieren. Zwei Minuten später liegen die Seiten wieder bei Euch. Es sind wieder mathematische Probleme. Und die Formalosophinnen wollen sehen, wie Ihr sie löst. " diff --git a/server/adam/Adam/Levels/Predicate/L01_Ring.lean b/server/adam/Adam/Levels/Predicate/L01_Ring.lean index f913b58..ba94755 100644 --- a/server/adam/Adam/Levels/Predicate/L01_Ring.lean +++ b/server/adam/Adam/Levels/Predicate/L01_Ring.lean @@ -10,7 +10,7 @@ Level 1 Title "Natürliche Zahlen" Introduction -"Du schaust Dir die erste Seite an." +"Du schaust dir die erste Seite an." Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by Hint "**Du**: Das ist doch Schulmathematik! Man rechnet das einfach aus, diff --git a/server/adam/Adam/Levels/Predicate/L06_Exists.lean b/server/adam/Adam/Levels/Predicate/L06_Exists.lean index b2f9fdc..340751f 100644 --- a/server/adam/Adam/Levels/Predicate/L06_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L06_Exists.lean @@ -39,7 +39,7 @@ Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by Dann siehst du besser, was los ist." Branch unfold Even - Hint "Robo**: Am besten machst Du auch noch `unfold Even at h`, damit Du verstehst, was los ist." + Hint "Robo**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst, was los ist." unfold Even at * Hint "**Du**: Also von `{h}` weiß ich jetzt, dass ein `r` existiert, so dass `r + r = n` … diff --git a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean index 0bcdde9..189290f 100644 --- a/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean +++ b/server/adam/Adam/Levels/Predicate/L09_PushNeg.lean @@ -77,7 +77,7 @@ NewTactic push_neg NewLemma Nat.even_iff_not_odd Nat.odd_iff_not_even not_exists not_forall Conclusion "Die Formalosophinnen sind ganz begeistert. -Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage. +Nachdem sich der Beifall gelegt hat, hast du auch einmal eine Frage. **Du**: Kann uns hier irgendjemand vielleicht ein bisschen Orientierung im Formaloversum geben? @@ -88,7 +88,7 @@ Nachdem sich der Beifall gelegt hat, hast Du auch einmal eine Frage. Die Frage war wieder zu konkret. Betretenes Schweigen. **Robo**: Lass nur. Ich schlage vor, wir machen als nächstes einen Ausflug auf den Asteroiden da -drüben. Und bevor Du fragst – hier ist wieder ein Überblick, was Du auf diesem Planeten +drüben. Und bevor du fragst – hier ist wieder ein Überblick, was du auf diesem Planeten gelernt hast. | | Beschreibung | diff --git a/server/adam/Adam/Levels/Proposition.lean b/server/adam/Adam/Levels/Proposition.lean index fbea081..79a7083 100644 --- a/server/adam/Adam/Levels/Proposition.lean +++ b/server/adam/Adam/Levels/Proposition.lean @@ -25,7 +25,7 @@ Richte dich besser darauf ein, hier bleiben und dich zurechtzufinden zu müssen. Wie es aussieht, gibt es hier viele nette kleine Planeten. Alle bewohnbar, und bis zu sieben Sonnenuntergänge täglich inklusive. Nur werden sie allesamt von Formalosophen bewohnt, seltsamen Wesen mit ausgefallenen mathematischen Obsessionen. Und dummerweise hat sich -herumgesprochen, dass du in deinem früheren Universum Mathematiker warst. Du wirst hier +herumgesprochen, dass du in deinem früheren Universum Mathematiker warst. du wirst hier keine Ruhe finden, solange du nicht lernst, ihren unablässigen Wissensdurst zu stillen. Es gibt nur zwei Schwierigkeiten: Erstens haben die Formalosophen allem Anschein nach diff --git a/server/adam/Adam/Levels/Proposition/L11_Or.lean b/server/adam/Adam/Levels/Proposition/L11_Or.lean index 68904cc..b18eb3d 100644 --- a/server/adam/Adam/Levels/Proposition/L11_Or.lean +++ b/server/adam/Adam/Levels/Proposition/L11_Or.lean @@ -20,7 +20,7 @@ Statement (A B : Prop) (hA : A) : A ∨ (¬ B) := by Hint "**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren? -**Robo** Nein, viel einfacher. Wenn du eine Oder-Aussage beweisen sollst, musst du Dich +**Robo** Nein, viel einfacher. Wenn du eine Oder-Aussage beweisen sollst, musst du dich einfach entscheiden, ob du die linke oder rechte Seite beweisen willst. **Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde? diff --git a/server/adam/Adam/Levels/Sum.lean b/server/adam/Adam/Levels/Sum.lean index 5f5172b..529b8fa 100644 --- a/server/adam/Adam/Levels/Sum.lean +++ b/server/adam/Adam/Levels/Sum.lean @@ -9,8 +9,7 @@ Game "Adam" World "Sum" Title "Endliche Summe" -Introduction "Mit dem Gefühl, dass sich *Evenine* und *Oddeus* in Zukunft wieder -besser verstehen werden, steigt ihr in eurer Raumschiff und setzt eure Reise fort. +Introduction "Ihr steigt in eurer Raumschiff und setzt eure Reise fort. Bald erreicht ihr einen neuen Planet. Die oberfläche scheint steinig zu sein, aber nicht etwa geröll oder Chaos. Stattdessen, scheinen unzählige Steinplatten zu bizzaren hohen Türme diff --git a/server/adam/Adam/Levels/Sum/L01_Simp.lean b/server/adam/Adam/Levels/Sum/L01_Simp.lean index a735024..66cfc86 100644 --- a/server/adam/Adam/Levels/Sum/L01_Simp.lean +++ b/server/adam/Adam/Levels/Sum/L01_Simp.lean @@ -43,24 +43,25 @@ In diesem Kapitel lernen wir endliche Summen und mehr Übungen zur Induktion. open BigOperators Statement (n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by - Hint "BUG" + Hint " + **Du**: Oh das ist ganz schön viel neues… Mal sehen, das sagt wohl + $( \\sum_i 0 + 0 ) = 0$. Dann ist das vielleicht doch nicht so komplex. - -- TODO (Bug): Invalid escape sequence: - -- "**Du**: Oh das ist ganz schön viel neues… Mal sehen, das sagt wohl - -- $( \\sum_i 0 + 0 ) = 0$. Dann ist das vielleicht doch nicht so komplex. + **Robo**: Genau! Man schreibt `\\sum`. Beachte den Index: + $( \\sum_\{i=0}^\{n-1} 0 + 0 ) = 0$, also `Fin n` ist ein Typ mit den Elementen + $(0, \\ldots, n-1)$. - -- **Robo**: Genau! Man schreibt `\\sum`. Beachte den Index: - -- $( \\sum_\{i=0}^\{n-1} 0 + 0 ) = 0$, also `Fin n` ist ein Typ mit den Elementen - -- $\\{0, \\ldots, n-1\\}$. + **Du**: Oke, also `Fin n` hat `n` Elemente. Und was mach ich jetzt? - -- **Du**: Oke, also `Fin n` hat `n` Elemente. Und was mach ich jetzt? + **Robo**: `simp` ist eine ganz starke Taktik, die viele Terme vereinfacht, wir + fangen besser an, diese zu benützen. - -- **Robo**: `simp` ist eine ganz starke Taktik, die viele Terme vereinfacht, wir - -- fangen besser an, diese zu benützen. - - -- Irgendwie hast du das Gefühl ein Déjà-vue zu haben…" + Irgendwie hast du das Gefühl ein Déjà-vue zu haben…" simp OnlyTactic simp +LemmaTab "Sum" Conclusion "**Unbekannte**: Sehr gut, folgt mir!" + +-- TODO: Cannot write $\\{0\\}$ inside a hint. diff --git a/server/adam/Adam/Levels/Sum/L02_Sum.lean b/server/adam/Adam/Levels/Sum/L02_Sum.lean index 65a3ad0..8c47b5e 100644 --- a/server/adam/Adam/Levels/Sum/L02_Sum.lean +++ b/server/adam/Adam/Levels/Sum/L02_Sum.lean @@ -4,6 +4,7 @@ import Adam.ToBePorted import Mathlib set_option tactic.hygienic false +open Finset Game "Adam" World "Sum" @@ -22,21 +23,21 @@ open BigOperators Statement "$\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$." (n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by - -- Hint "**Du**: Hmm, wieder `simp`? + Hint "**Du**: Hmm, wieder `simp`? - -- **Robo**: Nicht ganz. `simp` benützt nur Lemmas, die klar eine Vereinfachung darstellen, - -- und in deiner Bibliothek mit `@[simp]` markiert wird. Hier brauchen wir eine andere - -- Umformung: + **Robo**: Nicht ganz. `simp` benützt nur Lemmas, die klar eine Vereinfachung darstellen, + und in deiner Bibliothek mit `@[simp]` markiert wird. Hier brauchen wir eine andere + Umformung: - -- $$ - -- \\sum_\{i = 0}^n a_i + b_i = \\sum_\{i = 0}^n a_i + \\sum_\{j = 0}^n b_j - -- $$ + $$ + \\sum_\{i = 0}^n a_i + b_i = \\sum_\{i = 0}^n a_i + \\sum_\{j = 0}^n b_j + $$ - -- **Robo*: Da unklar ist, welche Seite \"einfacher\" ist, wird so ein Lemma nicht mit - -- `@[simp]` markiert. Das heisst du musst `Finset.sum_add_distrib` mit `rw` - -- explizit anwenden. - -- " - rw [Finset.sum_add_distrib] + **Robo**: Da unklar ist, welche Seite \"einfacher\" ist, wird so ein Lemma nicht mit + `@[simp]` markiert. Das heisst du musst `sum_add_distrib` mit `rw` + explizit anwenden. + " + rw [sum_add_distrib] Hint "**Robo**: Die zweite Summe `∑ x : Fin n, 1` kann jetzt aber mit `simp` zu `n` vereinfacht werden." simp @@ -49,6 +50,7 @@ Statement ring NewLemma Finset.sum_add_distrib add_comm +LemmaTab "Sum" Conclusion "Eure Begleitung scheint mit der Antwort zu frieden zu sein und zeigt freudig an dem Turm empor, den ihr soeben erreicht habt." diff --git a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean index c87d95e..ff80c3d 100644 --- a/server/adam/Adam/Levels/Sum/L03_ArithSum.lean +++ b/server/adam/Adam/Levels/Sum/L03_ArithSum.lean @@ -25,6 +25,8 @@ einmal Daten verarbeitet. Und die antwort auf deine Frage: Vermutlich ein Stein dem anderen. " +open Fin + open BigOperators Statement arithmetic_sum @@ -34,17 +36,18 @@ Statement arithmetic_sum wie zeige ich denn die arithmetische Summe, die hier gekritzelt steht? Ich würde gerne Induktion über $n$ anwenden. - **Robo**: Ja dann ist's einfach `induction n`, ist doch logisch!" - induction n + **Robo**: Ja dann ist's einfach `induction n with d hd`! Der `with d hd` teil ist + Optional und hilft dir die Induktionsvariable und -hypothese zu benennen." + induction n with d hd Hint "**Du**: Zuerst den Induktionsanfang… **Robo**: Diesen kannst du oft mit `simp` abkürzen!" simp Hint "**Robo**: Jetzt im Induktionsschritt: Bei Induktion über endlichen Summen willst du - immer mit `rw [Fin.sum_univ_castSucc]` anfangen" -- : + immer mit `rw [sum_univ_castSucc]` anfangen" -- : -- $$\\sum_\{i=0}^n a_i = \\sum_{i=0}^\{n-1} a_i + a_n$$" - rw [Fin.sum_univ_castSucc] + rw [sum_univ_castSucc] -- TODO: Bug. Dieser Hint wird nicht angezeigt. Hint "**Du**: Oh das sieht jetz aber kompliziert aus… @@ -63,27 +66,31 @@ Statement arithmetic_sum Hint "**Du**: Und wie wende ich jetzt die Induktionshypothese an? **Robo mit `rw` wie jede andere Annahme auch." - rw [n_ih] - Hint "**Robo**: Jetzt musst du noch kurz `rw [Nat.succ_eq_add_one]` anwenden. + rw [hd] + Hint "**Du**: Der Rest ist einfach Rechnerei. + + **Robo**: Dann wir `ring` wohl keine Probleme haben." + -- Hint "**Robo**: Jetzt musst du noch kurz `rw [Nat.succ_eq_add_one]` anwenden. - **Du**: Aber wieso? + -- **Du**: Aber wieso? - **Robo**: Naja, `ring` ist jetzt auch noch nicht so stark, und erkennt nicht dass `n.succ` - und `n + 1` das gleiche sind. + -- **Robo**: Naja, `ring` ist jetzt auch noch nicht so stark, und erkennt nicht dass `n.succ` + -- und `n + 1` das gleiche sind. - **Du**: Aber das könnte man doch ändern, oder? + -- **Du**: Aber das könnte man doch ändern, oder? - **Robo**: Vielleicht wenn wir einmal einem Techniker begegnen, der mir ein Update - einspielen kann…" - Branch - ring_nf - Hint "**Robo**: Wie gesagt, brauch doch `rw [Nat.succ_eq_add_one]` als Fix für meine - kleinen Maken." - rw [Nat.succ_eq_add_one] + -- **Robo**: Vielleicht wenn wir einmal einem Techniker begegnen, der mir ein Update + -- einspielen kann…" + -- Branch + -- ring_nf + -- Hint "**Robo**: Wie gesagt, brauch doch `rw [Nat.succ_eq_add_one]` als Fix für meine + -- kleinen Maken." + -- rw [Nat.succ_eq_add_one] ring NewTactic induction NewLemma Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul Nat.zero_eq +LemmaTab "Sum" Conclusion "Du schaust dich um und bewunderst das Tal in dem hunderte, wenn nicht tausende, Steintürme in allen Formen und Höhen stehen." diff --git a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean index d84dd40..b3a6427 100644 --- a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean +++ b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean @@ -18,6 +18,8 @@ Du gehst zu einem etwas kleineren Nachbarsturm. " set_option tactic.hygienic false +open Fin + open BigOperators Statement odd_arithmetic_sum @@ -26,8 +28,12 @@ Statement odd_arithmetic_sum Hint "**Robo**: Das funktioniert genau gleich wie zuvor, viel Glück." induction n simp - rw [Fin.sum_univ_castSucc] + Hint (hidden := true) "Den Induktionschritt mit Summen willst du + eigentlich immer mit `rw [sum_univ_castSucc]` beginnen." + rw [sum_univ_castSucc] simp rw [n_ih] - rw [Nat.succ_eq_add_one] + --rw [Nat.succ_eq_add_one] ring + +LemmaTab "Sum" diff --git a/server/adam/Adam/Levels/Sum/L05_SumComm.lean b/server/adam/Adam/Levels/Sum/L05_SumComm.lean index dd5cc37..bf73cf2 100644 --- a/server/adam/Adam/Levels/Sum/L05_SumComm.lean +++ b/server/adam/Adam/Levels/Sum/L05_SumComm.lean @@ -9,6 +9,7 @@ import Adam.Options.ArithSum set_option tactic.hygienic false open BigOperators +open Finset Game "Adam" World "Sum" @@ -35,10 +36,11 @@ Statement **Du**: Hast du nicht ein Lemma dafür? - **Robo**: Doch, probier mal `Finset.sum_comm`." + **Robo**: Doch, probier mal `sum_comm`." rw [Finset.sum_comm] NewLemma Finset.sum_comm +LemmaTab "Sum" Conclusion " Euer Begleiter ist ganz begeistert als er dir das Stück Papier aus den Händen nimmt, diff --git a/server/adam/Adam/Levels/Sum/L06_Summary.lean b/server/adam/Adam/Levels/Sum/L06_Summary.lean index 45f2a13..3e45e7b 100644 --- a/server/adam/Adam/Levels/Sum/L06_Summary.lean +++ b/server/adam/Adam/Levels/Sum/L06_Summary.lean @@ -38,6 +38,8 @@ Da löst sich aus der Steinlandschaft plötzlich ein grosser Steingolem. Er scha bedrohlich an und fragt in tiefer Stimme: " +open Fin + open BigOperators Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by @@ -45,7 +47,7 @@ Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), induction m Hint "**Du**: Also den Induktionsanfang kann man einfach zeigen…" simp - Hint "**Robo**: Und jetzt wieder `rw [Fin.sum_univ_castSucc]` und `simp` um vorwärts zu + Hint (hidden := true) "**Robo**: Und jetzt wieder `rw [sum_univ_castSucc]` und `simp` um vorwärts zu kommen!" rw [Fin.sum_univ_castSucc] simp @@ -56,9 +58,9 @@ Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), Der Golem schaut dich finster an. - **Robo**: Du willst `Fin.sum_univ_castSucc` auf der rechten Seite anwenden, aber es + **Robo**: Du willst `sum_univ_castSucc` auf der rechten Seite anwenden, aber es gibt mehrere Orte, wo das Lemma passen würde. - Deshalb musst du mit `rw [Fin.sum_univ_castSucc (n := {n} + 1)]` angeben, wo genau. + Deshalb musst du mit `rw [sum_univ_castSucc (n := {n} + 1)]` angeben, wo genau. **Du**: Was bedeutet das? @@ -83,9 +85,10 @@ Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), ring NewLemma arithmetic_sum add_pow_two +LemmaTab "Sum" Conclusion "Der Golem denkt ganz lange nach, und ihr bekommt das Gefühl, dass er gar nie -aggressive war, sondern nur eine sehr tiefe Stimme hat. +aggressiv war, sondern nur eine sehr tiefe Stimme hat. Mit einem kleinen Erdbeben setzt er sich hin und winkt euch dankend zu. diff --git a/server/adam/Adam/Metadata.lean b/server/adam/Adam/Metadata.lean index 35a7bab..3f8dba3 100644 --- a/server/adam/Adam/Metadata.lean +++ b/server/adam/Adam/Metadata.lean @@ -3,3 +3,4 @@ import Adam.TacticDocs import Adam.LemmaDocs import Adam.DefinitionDocs import Mathlib.Init.Data.Nat.Basic -- Imports the notation ℕ. +import Adam.Modification.Tactic diff --git a/server/adam/Adam/Modification/Tactic.lean b/server/adam/Adam/Modification/Tactic.lean new file mode 100644 index 0000000..941fca3 --- /dev/null +++ b/server/adam/Adam/Modification/Tactic.lean @@ -0,0 +1,83 @@ +import Mathlib.Lean.Expr.Basic +import Lean.Elab.Tactic.Basic +import Mathlib.Init.Data.Nat.Notation + +open Lean.Meta Lean.Elab.Tactic Lean.Parser.Tactic + +/-! +# Modified `induction` tactic + +Modify `induction` tactic to use the cases `0` and `n + 1` (isnstead of `zero` and `succ n`) +and support the lean3-style `with` keyword. + +This is mainly copied and modified from the mathlib-tactic `induction'`. +-/ + +/-- Custom induction principle that uses `0` and `n + 1` instead +of `Nat.zero` and `Nat.succ n`. -/ +def CustomTactic.rec' {P : ℕ → Prop} (zero : P 0) + (succ : (n : ℕ) → (n_ih : P n) → P (n + 1)) (t : ℕ) : P t := by + induction t with + | zero => assumption + | succ n => + apply succ + assumption + +namespace Lean.Parser.Tactic +open Meta Elab Elab.Tactic + +open private getAltNumFields in evalCases ElimApp.evalAlts.go in +def _root_.CustomTactic.ElimApp.evalNames (elimInfo : ElimInfo) (alts : Array ElimApp.Alt) (withArg : Syntax) + (numEqs := 0) (numGeneralized := 0) (toClear : Array FVarId := #[]) : + Lean.Elab.Term.TermElabM (Array MVarId) := do + let mut names : List Syntax := withArg[1].getArgs |>.toList + let mut subgoals := #[] + for { name := altName, mvarId := g, .. } in alts do + let numFields ← getAltNumFields elimInfo altName + let (altVarNames, names') := names.splitAtD numFields (Unhygienic.run `(_)) + names := names' + let (fvars, g) ← g.introN numFields <| altVarNames.map (getNameOfIdent' ·[0]) + let some (g, subst) ← Cases.unifyEqs? numEqs g {} | pure () + let (_, g) ← g.introNP numGeneralized + let g ← liftM $ toClear.foldlM (·.tryClear) g + for fvar in fvars, stx in altVarNames do + g.withContext <| (subst.apply <| .fvar fvar).addLocalVarInfoForBinderIdent ⟨stx⟩ + subgoals := subgoals.push g + pure subgoals + +open private getElimNameInfo generalizeTargets generalizeVars in evalInduction in + +/-- +Modified `induction` tactic for this game. + +Usage: `induction n with d hd`. + +For this game, `induction n` uses the cases `0` and `n + 1` instead of `Nat.zero` and +`Nat.succ n`. These are defEq, but it's currently annoying that `ring` does not like the +latter forms. + +*(The actual `induction` tactic has a more complex `with`-argument that works differently)* +-/ +elab (name := _root_.MyNat.induction) "induction " tgts:(casesTarget,+) + withArg:((" with " (colGt binderIdent)+)?) + : tactic => do + let targets ← elabCasesTargets tgts.1.getSepArgs + let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved + g.withContext do + let elimInfo ← getElimInfo `CustomTactic.rec' + let targets ← addImplicitTargets elimInfo targets + evalInduction.checkTargets targets + let targetFVarIds := targets.map (·.fvarId!) + g.withContext do + let forbidden ← mkGeneralizationForbiddenSet targets + let mut s ← getFVarSetToGeneralize targets forbidden + let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray) + let result ← withRef tgts <| ElimApp.mkElimApp elimInfo targets (← g.getTag) + let elimArgs := result.elimApp.getAppArgs + ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds + g.assign result.elimApp + let subgoals ← CustomTactic.ElimApp.evalNames elimInfo result.alts withArg + (numGeneralized := fvarIds.size) (toClear := targetFVarIds) + setGoals <| (subgoals ++ result.others).toList ++ gs + +end Lean.Parser.Tactic diff --git a/server/adam/Adam/TacticDocs.lean b/server/adam/Adam/TacticDocs.lean index 6a3b96d..63553e4 100644 --- a/server/adam/Adam/TacticDocs.lean +++ b/server/adam/Adam/TacticDocs.lean @@ -231,7 +231,16 @@ Diese Taktik erstellt zwei Goals: * Induktionsanfang, wo `n = 0` ersetzt wird. * Induktionsschritt, in dem man die Induktionshypothese `n_ih` zur Verfügung hat. -Der volle Syntax mit Option zum umbenennen der Induktionshypothes und -variable ist +## Modifikationen in diesem Spiel + +* `induction n with d hd` benennt Induktionsvariable und -hypothese. (das ist Lean3-Syntax) +und funktioniert ausserhalb vom Spiel nicht genau so. +* Ausserhalb des Spiels kriegst du `Nat.zero` und `Nat.succ n` anstatt `0` und `n + 1` +als Fälle. Diese +Terme sind DefEq, aber manchmal benötigt man die lemmas `zero_eq` und `Nat.succ_eq_add_one` +um zwischen den schreibweisen zu wechseln + +Der richtige Lean4-Syntax für `with` streckt sich über mehrere Zeilen und ist: ``` induction n with