From 99080aa5ff4875df026f4e33c3fcde0e41baff82 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 3 Mar 2023 11:54:37 +0100 Subject: [PATCH] levels up to 'Lean' --- .../TestGame/Levels/Sum/L03_ArithSum.lean | 7 ++-- .../TestGame/Levels/Sum/L04_SumOdd.lean | 4 +-- .../TestGame/Levels/Sum/L06_Summary.lean | 35 +++++++++++++------ 3 files changed, 32 insertions(+), 14 deletions(-) diff --git a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean index 320fe9a..0132d52 100644 --- a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean +++ b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean @@ -3,6 +3,8 @@ import TestGame.Metadata import Mathlib.Algebra.BigOperators.Fin import Mathlib.Tactic.Ring +import TestGame.Options.BigOperators + set_option tactic.hygienic false Game "TestGame" @@ -56,7 +58,7 @@ NewLemmas Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul Hint (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) => "Als Erinnerung, einen Induktionsbeweis startet man mit `induction n`." -Hint (n : ℕ) : 2 * ∑ i : Fin (0 + 1), ↑i = 0 * (0 + 1) => +Hint : 2 * ∑ i : Fin (Nat.zero + 1), ↑i = Nat.zero * (Nat.zero + 1) => "Den Induktionsanker $n = 0$ kann `simp` oft beweisen." Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) : @@ -77,7 +79,8 @@ umschreiben. Dazu kannst du `mul_add` benützen. Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) : 2 * ∑ x : Fin (n + 1), ↑x + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) => -"Jetzt kann die Induktionshypothese mit `rw` angewendet werden." +"`simp` vereinfacht `↑(↑Fin.castSucc.toEmbedding i)` zu `↑i`. +Danach kann die Induktionshypothese mit `rw` angewendet werden." Hint (n : ℕ) (hn : 2 * ∑ i : Fin (n + 1), ↑i = n * (n + 1)) : n * (n + 1) + 2 * (n + 1) = Nat.succ n * (Nat.succ n + 1) => diff --git a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean index a772383..76ab5f6 100644 --- a/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean +++ b/server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean @@ -36,7 +36,7 @@ HiddenHint (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 => Fange wieder mit `induction n` an. " -HiddenHint (n : ℕ) : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 => +HiddenHint : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 => " Den Induktionsanfang kannst du wieder mit `simp` beweisen. " @@ -54,5 +54,5 @@ Hier kommt die Induktionshypothese ins Spiel. HiddenHint (n : ℕ) : n ^ 2 + (2 * n + 1) = Nat.succ n ^ 2 => " -Mit `rw [Fin.sum_univ_castSucc]` und `ring` kannst du hier abschliessen. +Mit `rw [Nat.succ_eq_add_one]` und `ring` kannst du hier abschliessen. " diff --git a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean index 19da7b8..bc6f4e3 100644 --- a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean +++ b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean @@ -44,7 +44,7 @@ $$ open BigOperators Statement -"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i)^2$." +"Zeige $\\sum_{i = 0}^m i^3 = (\\sum_{i = 0}^m i)^2$." (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1), (i : ℕ))^2 := by induction' m with m hm simp @@ -59,26 +59,35 @@ Statement NewLemmas arithmetic_sum add_pow_two -HiddenHint (m : ℕ) : ∑ i : Fin (Nat.zero + 1), ↑i ^ 3 = (∑ i : Fin (Nat.zero + 1), ↑i) ^ 2 => +HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (m + 1), ↑i) ^ 2 => +"Führe auch hier einen Induktionsbeweis." + +HiddenHint : ∑ i : Fin (Nat.zero + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.zero + 1), ↑i) ^ 2 => "`simp` kann den Induktionsanfang beweisen." -Hint (m : ℕ) : ∑ i : Fin (Nat.succ m + 1), ↑i ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => -"Im Induktionsschritt musst du versuchen, das Goal so umzuformen, dass du -`∑ i : Fin (m + 1), ↑i ^ 3` (Induktionshypothese) oder -`2 * (∑ i : Fin (m + 1), ↑i)` (arithmetische Summe) erhälst. +Hint (m : ℕ) : ∑ i : Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => +"Im Induktionsschritt willst du das Goal so umformen, dass du folgende Therme +ersetzen kannst: + +* `∑ i : Fin (m + 1), ↑i ^ 3` (Induktionshypothese) +* `2 * (∑ i : Fin (m + 1), ↑i)` (arithmetische Summe) +" +HiddenHint (m : ℕ) : ∑ i : + Fin (Nat.succ m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => +" Als erstes kannst du mal mit dem bekannten `rw [Fin.sum_univ_castSucc]` anfangen. " -HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), ↑(Fin.castSucc.toEmbedding i) ^ 3 + +HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (Fin.castSucc.toEmbedding i : ℕ) ^ 3 + ↑(Fin.last (m + 1)) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => "Mit `simp` kriegst du das `↑(Fin.castSucc.toEmbedding i)` weg" Hint (m : ℕ) : ∑ x : Fin (m + 1), (x : ℕ) ^ 3 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => -"Jetzt kannst du die Induktionshypothese mit `rw` einsetzen." +"Jetzt kannst du die Induktionshypothese benützen." -Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => +Hint (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (Nat.succ m + 1), ↑i) ^ 2 => "Die linke Seite ist jetzt erst mal gut. Um auf der rechten Seite `Fin.sum_univ_castSucc` anzuwenden, haben wir ein Problem: Lean schreibt immer die erste Instanz um, also würde gerne auf der linken Seite `(∑ i : Fin (m + 1), ↑i) ^ 2` umschreiben. @@ -94,12 +103,18 @@ rw [Fin.sum_univ_castSucc (n := m + 1)] HiddenHint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (m + 1), ↑(Fin.castSucc.toEmbedding i) + ↑(Fin.last (m + 1))) ^ 2 => -"wieder `simp`" +"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal +`simp` aufrufen." Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (m + 1), ↑i + (m + 1)) ^ 2 => "Die rechte Seite hat die Form $(a + b)^2$ welche mit `add_pow_two` zu $a^2 + 2ab + b^2$ umgeschrieben werden kann." +HiddenHint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = + (∑ i : Fin (m + 1), ↑i) ^ 2 + (2 * ∑ i : Fin (m + 1), ↑i) * (m + 1) + (m + 1) ^ 2 => +"Wenn du noch einen AUsdruck `↑(Fin.castSucc.toEmbedding i)` hast, solltest du mal +`simp` aufrufen." + Hint (m : ℕ) : (∑ i : Fin (m + 1), ↑i) ^ 2 + (m + 1) ^ 3 = (∑ i : Fin (m + 1), ↑i) ^ 2 + (2 * ∑ i : Fin (m + 1), ↑i) * (m + 1) + (m + 1) ^ 2 => "Jetzt hast du in der Mitte `2 * ∑ i : Fin (m + 1), ↑i)`, welches du mit der