From 07b140acf75c1fdf3ca610c476bde342d394297a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 8 Feb 2023 10:33:45 +0100 Subject: [PATCH] levels --- .../Levels/Induction/L03_Induction.lean | 17 ++++++------ .../TestGame/Levels/Induction/L04_SumOdd.lean | 11 +++----- .../TestGame/Levels/Induction/T00_Sum.lean | 27 ++++++++++++++++--- .../Levels/Induction/T01_Induction.lean | 10 ++++++- .../Levels/Induction/T02_Induction.lean | 10 ++++++- .../TestGame/Levels/Prime/L01_Prime.lean | 6 +++-- .../Levels/SetTheory/PowersetPlayground.lean | 2 +- server/testgame/TestGame/ToBePorted.lean | 2 -- 8 files changed, 59 insertions(+), 26 deletions(-) diff --git a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean index 108c0a8..3d37c74 100644 --- a/server/testgame/TestGame/Levels/Induction/L03_Induction.lean +++ b/server/testgame/TestGame/Levels/Induction/L03_Induction.lean @@ -2,7 +2,6 @@ import TestGame.Metadata import Mathlib.Tactic.Ring import Mathlib -import TestGame.ToBePorted Game "TestGame" World "Induction" @@ -31,16 +30,16 @@ Für den Induktionsschritt braucht man fast immer zwei technische Lemmas: open BigOperators -Statement +Statement arithmetic_sum "Zeige $\\sum_{i = 0}^n i = \\frac{n \\cdot (n + 1)}{2}$." (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by - induction n + induction' n with n hn simp - - sorry - -- rw [Fin.sum_univ_castSucc] - -- simp [nat_succ] - -- rw [mul_add, hn] - -- ring + rw [Fin.sum_univ_castSucc] + rw [mul_add] + simp + rw [mul_add, hn] + simp_rw [Nat.succ_eq_one_add] + ring Tactics ring diff --git a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean index e796abd..2741bdf 100644 --- a/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean +++ b/server/testgame/TestGame/Levels/Induction/L04_SumOdd.lean @@ -2,8 +2,6 @@ import TestGame.Metadata import Mathlib.Tactic.Ring import Mathlib -import TestGame.ToBePorted - Game "TestGame" World "Induction" Level 4 @@ -24,10 +22,9 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$." (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by induction' n with n hn simp - rw [nat_succ] - sorry -- waiting on Algebra.BigOperators.Fin - --simp [Fin.sum_univ_cast_succ] - --rw [hn] - --ring + rw [Fin.sum_univ_castSucc] + simp + rw [hn, Nat.succ_eq_add_one] + ring Tactics ring diff --git a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean index be78477..c57f5f3 100644 --- a/server/testgame/TestGame/Levels/Induction/T00_Sum.lean +++ b/server/testgame/TestGame/Levels/Induction/T00_Sum.lean @@ -16,11 +16,32 @@ Introduction open BigOperators +lemma arithmetic_sum (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by + induction' n with n hn + simp + rw [Fin.sum_univ_castSucc] + rw [mul_add] + simp + rw [mul_add, hn] + simp_rw [Nat.succ_eq_one_add] + ring + + Statement -"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i^3)^2$." +"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i)^2$." (n : ℕ) : (∑ i : Fin (n + 1), (i : ℕ)^3) = (∑ i : Fin (n + 1), (i : ℕ))^2 := by - induction n + induction' n with n hn simp - sorry + conv_rhs => + rw [Fin.sum_univ_castSucc] + simp + rw [add_pow_two] + rw [arithmetic_sum] + rw [mul_assoc, add_assoc, ←pow_two, ←Nat.succ_mul n, Nat.succ_eq_add_one, ←pow_succ] + conv_lhs => + rw [Fin.sum_univ_castSucc] + simp + rw [hn] + Tactics ring diff --git a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean index 2197ebe..8dd5c1e 100644 --- a/server/testgame/TestGame/Levels/Induction/T01_Induction.lean +++ b/server/testgame/TestGame/Levels/Induction/T01_Induction.lean @@ -18,7 +18,15 @@ Introduction Statement "2^n > n^2 für n ≥ 5" - (n : ℕ) : True := by + (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n := by + induction n with + | 0 | 1 | 2 | 3 | 4 => by contradiction + | n.succ => by sorry + + +example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n +| 0 | 1 | 2 | 3 | 4 => by sorry +| n + 5 => by sorry Tactics rw simp ring diff --git a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean index cc0d2dd..8b53ad1 100644 --- a/server/testgame/TestGame/Levels/Induction/T02_Induction.lean +++ b/server/testgame/TestGame/Levels/Induction/T02_Induction.lean @@ -18,7 +18,15 @@ n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n Statement "n^3 + 2n ist durch 3 teilbar für alle ganzen Zahlen n" - (n : ℤ) : True := by + (n : ℤ) : 3 ∣ n^3 + 2*n := by + induction n + sorry sorry Tactics rw simp ring + +-- example (n : ℕ) : (n - 1) * (n + 1) = (n ^ 2 - 1) := by +-- induction' n with n hn +-- ring +-- rw [Nat.succ_eq_one_add] +-- rw [] diff --git a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean index b6ae747..b6a177b 100644 --- a/server/testgame/TestGame/Levels/Prime/L01_Prime.lean +++ b/server/testgame/TestGame/Levels/Prime/L01_Prime.lean @@ -24,14 +24,16 @@ Statement (n : ℕ) : ∃! (n : ℕ), Nat.Prime n ∧ Even n := by use (2 : ℕ) constructor - simp only [true_and] - use 1 + simp only [] intro y rintro ⟨h₁, h₂⟩ rw [← Nat.Prime.even_iff] assumption assumption +example : True := by + by_cases h : 1 = 0 + Conclusion "" Tactics diff --git a/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean b/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean index 44fd72b..01f9e22 100644 --- a/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean +++ b/server/testgame/TestGame/Levels/SetTheory/PowersetPlayground.lean @@ -57,7 +57,7 @@ lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) : lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) : S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by - rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff] + simp_rw [mem_powerset_iff, diff_singleton_subset_iff] lemma powerset_insert {U : Type _} (A : Set U) (x : U) : 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean index 807087f..564a4a3 100644 --- a/server/testgame/TestGame/ToBePorted.lean +++ b/server/testgame/TestGame/ToBePorted.lean @@ -13,8 +13,6 @@ lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by rw [hx] ring -theorem nat_succ (n : ℕ) : Nat.succ n = n + 1 := rfl - section powerset open Set