-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathproofs_by_induction.lean
119 lines (85 loc) · 3.64 KB
/
proofs_by_induction.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
import algebra.big_operators data.fintype
import tactic.ring
-- https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/
open nat
def odd : ℕ → ℕ := λ i, 2 * i + 1
def square : ℕ → ℕ := λ i, i ^ 2
theorem odd_square_inductive_step (d : ℕ) :
square d + odd d = square (succ d) :=
by dsimp [square, odd, pow]; rw [succ_eq_add_one]; ring
namespace def1
definition my_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ
| 0 := 0
| (succ n) := my_sum_to_n n + summand n
theorem my_zero_theorem (summand : ℕ → ℕ) :
my_sum_to_n summand 0 = 0 :=
rfl
theorem my_successor_theorem (summand : ℕ → ℕ) (n : ℕ) :
my_sum_to_n summand (succ n) = my_sum_to_n summand n + summand n :=
rfl
theorem my_odd_square_theorem : ∀ (n : ℕ), my_sum_to_n odd n = square n
| 0 := rfl
| (succ n) := by unfold my_sum_to_n; rw [my_odd_square_theorem n]; exact odd_square_inductive_step n
end def1
namespace def2
definition my_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ :=
λ n, ((list.range n).map summand).sum
theorem my_zero_theorem (summand : ℕ → ℕ) :
my_sum_to_n summand 0 = 0 :=
rfl
theorem my_successor_theorem (summand : ℕ → ℕ) (n : ℕ) :
my_sum_to_n summand (succ n) = my_sum_to_n summand n + summand n :=
by unfold my_sum_to_n; simp [list.range_concat]
theorem my_odd_square_theorem : ∀ (n : ℕ), my_sum_to_n odd n = square n
| 0 := rfl
| (succ n) := by rw [my_successor_theorem, my_odd_square_theorem n]; exact odd_square_inductive_step n
end def2
namespace def3
definition my_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ :=
λ n, (finset.range n).sum summand
theorem my_zero_theorem (summand : ℕ → ℕ) :
my_sum_to_n summand 0 = 0 :=
rfl
theorem my_successor_theorem (summand : ℕ → ℕ) (n : ℕ) :
my_sum_to_n summand (succ n) = my_sum_to_n summand n + summand n :=
by unfold my_sum_to_n; simp
theorem my_odd_square_theorem : ∀ (n : ℕ), my_sum_to_n odd n = square n
| 0 := rfl
| (succ n) := by rw [my_successor_theorem, my_odd_square_theorem n]; exact odd_square_inductive_step n
end def3
namespace def4
open finset nat
-- Credits to Chris Hughes
theorem chris (n : ℕ) (f : ℕ → ℕ) (g : fin n → ℕ) (h : ∀ i : fin n, f i.1 = g i) :
(range n).sum f = univ.sum g :=
sum_bij
(λ i h, ⟨i, mem_range.1 h⟩)
(λ i h, mem_univ _)
(λ a ha, h ⟨a, _⟩)
(λ _ _ _ _, fin.veq_of_eq)
(λ ⟨b, hb⟩ _, ⟨b, mem_range.2 hb, rfl⟩)
definition my_sum_to_n (summand : ℕ → ℕ) : ℕ → ℕ :=
λ n, (@finset.univ (fin n) _).sum (summand ∘ fin.val)
theorem my_zero_theorem (summand : ℕ → ℕ) :
my_sum_to_n summand 0 = 0 :=
rfl
-- Credits to Mario Carneiro
theorem my_successor_theorem (summand : ℕ → ℕ) (n : ℕ) :
my_sum_to_n summand (succ n) = my_sum_to_n summand n + summand n :=
by unfold my_sum_to_n;
rw [← chris _ _ _ (λ _, rfl), ← chris _ _ _ (λ _, rfl)]; simp
theorem my_odd_square_theorem : ∀ (n : ℕ), my_sum_to_n odd n = square n
| 0 := rfl
| (succ n) := by rw [my_successor_theorem, my_odd_square_theorem n]; exact odd_square_inductive_step n
end def4
namespace equality
theorem def12 : def1.my_sum_to_n = def2.my_sum_to_n :=
funext $ λ summand, funext $ λ n, nat.rec_on n rfl $
λ m ih, by rw [def1.my_successor_theorem, def2.my_successor_theorem, ih]
theorem def23 : def2.my_sum_to_n = def3.my_sum_to_n :=
funext $ λ summand, funext $ λ n, nat.rec_on n rfl $
λ m ih, by rw [def2.my_successor_theorem, def3.my_successor_theorem, ih]
theorem def34 : def3.my_sum_to_n = def4.my_sum_to_n :=
funext $ λ summand, funext $ λ n, nat.rec_on n rfl $
λ m ih, by rw [def3.my_successor_theorem, def4.my_successor_theorem, ih]
end equality