levels

2023-02-08 10:33:45 +01:00
parent ad50fb986d
commit 07b140acf7
8 changed files with 61 additions and 28 deletions
@@ -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
@@ -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
@@ -16,11 +16,32 @@ Introduction

 open BigOperators

-Statement
-"Zeige $\\sum_{i = 0}^n i^3 = (\\sum_{i = 0}^n i^3)^2$."
-  (n : ℕ) : (∑ i : Fin (n + 1), (i : ℕ)^3) = (∑ i : Fin (n + 1), (i : ℕ))^2 := by
-  induction n
+lemma arithmetic_sum (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
+  induction' n with n hn
  simp
-  sorry
+  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)^2$."
+  (n : ℕ) : (∑ i : Fin (n + 1), (i : ℕ)^3) = (∑ i : Fin (n + 1), (i : ℕ))^2 := by
+  induction' n with n hn
+  simp
+  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
@@ -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
@@ -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 []
@@ -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
@@ -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
@@ -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