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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
|
theorem Nat.power_of_two_go_eq_eq (n : Nat) (p : n >0) : Nat.nextPowerOfTwo.go n n p = n := by
unfold Nat.nextPowerOfTwo.go
simp_arith
theorem Nat.smaller_smaller_exp {n m o : Nat} (p : o ^ n < o ^ m) (q : o > 0) : n < m :=
if h₁ : m ≤ n then
by have h₂ := Nat.pow_le_pow_of_le_right (q) h₁
have h₃ := Nat.lt_of_le_of_lt h₂ p
simp_arith at h₃
else
by rewrite[Nat.not_ge_eq] at h₁
trivial
private theorem mul2_isPowerOfTwo_smaller_smaller_equal (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power < n) : power * 2 ≤ n := by
unfold Nat.isPowerOfTwo at h₁ h₂
have ⟨k, h₄⟩ := h₁
have ⟨l, h₅⟩ := h₂
rewrite [h₅]
rewrite[←Nat.pow_succ 2 l]
rewrite[h₄]
have h₆ : 2 > 0 := by decide
apply (Nat.pow_le_pow_of_le_right h₆)
rewrite [h₅] at h₃
rewrite [h₄] at h₃
have h₃ := Nat.smaller_smaller_exp h₃
simp_arith at h₃
assumption
private theorem power_of_two_go_one_eq (n : Nat) (power : Nat) (h₁ : n.isPowerOfTwo) (h₂ : power.isPowerOfTwo) (h₃ : power ≤ n) : Nat.nextPowerOfTwo.go n power (Nat.pos_of_isPowerOfTwo h₂) = n := by
unfold Nat.nextPowerOfTwo.go
split
case isTrue h₄ => exact power_of_two_go_one_eq n (power*2) (h₁) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂) (mul2_isPowerOfTwo_smaller_smaller_equal n power h₁ h₂ h₄)
case isFalse h₄ => rewrite[Nat.not_lt_eq power n] at h₄
exact Nat.le_antisymm h₃ h₄
termination_by n - power
decreasing_by
simp_wf
have := Nat.pos_of_isPowerOfTwo h₂
apply Nat.nextPowerOfTwo_dec <;> assumption
private theorem power_of_two_eq_power_of_two (n : Nat) : n.isPowerOfTwo → (n.nextPowerOfTwo = n) := by
intro h₁
unfold Nat.nextPowerOfTwo
apply power_of_two_go_one_eq
case h₁ => assumption
case h₂ => exact Nat.one_isPowerOfTwo
case h₃ => exact (Nat.pos_of_isPowerOfTwo h₁)
private theorem eq_power_of_two_power_of_two (n : Nat) : (n.nextPowerOfTwo = n) → n.isPowerOfTwo := by
have h₂ := Nat.isPowerOfTwo_nextPowerOfTwo n
intro h₁
revert h₂
rewrite[h₁]
intro
assumption
theorem Nat.power_of_two_iff_next_power_eq (n : Nat) : n.isPowerOfTwo ↔ (n.nextPowerOfTwo = n) :=
Iff.intro (power_of_two_eq_power_of_two n) (eq_power_of_two_power_of_two n)
theorem Nat.mul2_ispowerOfTwo_iff_isPowerOfTwo (n : Nat) : n.isPowerOfTwo ↔ (2*n).isPowerOfTwo :=
have h₁ : n.isPowerOfTwo → (2*n).isPowerOfTwo := by
simp[Nat.mul_comm]
apply Nat.mul2_isPowerOfTwo_of_isPowerOfTwo
have h₂ : (2*n).isPowerOfTwo → n.isPowerOfTwo :=
if h₂ : n.nextPowerOfTwo = n then by
simp[power_of_two_iff_next_power_eq,h₂]
else by
intro h₃
simp[←power_of_two_iff_next_power_eq] at h₂
have h₅ := h₃
unfold Nat.isPowerOfTwo at h₃
let ⟨k,h₄⟩ := h₃
cases n with
| zero => contradiction
| succ m => cases k with
| zero => simp_arith at h₄
| succ l => rewrite[Nat.pow_succ 2 l] at h₄
rewrite[Nat.mul_comm (2^l) 2] at h₄
have h₄ := Nat.eq_of_mul_eq_mul_left (by decide : 0<2) h₄
exists l
Iff.intro h₁ h₂
mutual
-- intentionally not decidable. This is a logical model, not meant for runtime!
def Nat.isEven : Nat → Prop
| .zero => True
| .succ n => Nat.isOdd n
-- intentionally not decidable. This is a logical model, not meant for runtime!
def Nat.isOdd : Nat → Prop
| .zero => False
| .succ n => Nat.isEven n
end
theorem Nat.mul_2_is_even {n m : Nat} (h₁ : n = 2 * m) : Nat.isEven n := by
cases m with
| zero => simp[Nat.isEven, h₁]
| succ o => simp_arith at h₁
simp[Nat.isEven, Nat.isOdd, h₁]
exact Nat.mul_2_is_even (rfl)
theorem Nat.isPowerOfTwo_even_or_one {n : Nat} (h₁ : n.isPowerOfTwo) : (n = 1 ∨ (Nat.isEven n)) := by
simp[Nat.isPowerOfTwo] at h₁
let ⟨k,h₂⟩ := h₁
cases k with
| zero => simp_arith[h₂]
| succ l => rewrite[Nat.pow_succ] at h₂
rewrite[Nat.mul_comm (2^l) 2] at h₂
exact Or.inr $ Nat.mul_2_is_even h₂
mutual
private theorem Nat.not_even_odd {n : Nat} (h₁ : ¬Nat.isEven n) : (Nat.isOdd n) := by
cases n with
| zero => unfold Nat.isEven at h₁; contradiction
| succ o => simp[Nat.isEven, Nat.isOdd] at *
exact (Nat.not_odd_even (by simp[h₁]))
private theorem Nat.not_odd_even {n : Nat} (h₁ : ¬Nat.isOdd n) : (Nat.isEven n) := by
cases n with
| zero => simp[isEven]
| succ o => simp[Nat.isEven, Nat.isOdd] at *
exact (Nat.not_even_odd (by simp[h₁]))
end
mutual
private theorem Nat.even_not_odd {n : Nat} (h₁ : Nat.isEven n) : ¬(Nat.isOdd n ):= by
cases n with
| zero => unfold Nat.isOdd; trivial
| succ o => simp[Nat.isEven, Nat.isOdd] at *
simp[Nat.odd_not_even h₁]
private theorem Nat.odd_not_even {n : Nat} (h₁ : Nat.isOdd n) : ¬(Nat.isEven n ):= by
cases n with
| zero => unfold isOdd at h₁; contradiction
| succ o => simp[Nat.isEven, Nat.isOdd] at *
simp[Nat.even_not_odd h₁]
end
theorem Nat.odd_not_even_odd {n : Nat} : Nat.isOdd n ↔ ¬Nat.isEven n :=
Iff.intro Nat.odd_not_even Nat.not_even_odd
theorem Nat.even_not_odd_even {n : Nat} : Nat.isEven n ↔ ¬Nat.isOdd n :=
Iff.intro Nat.even_not_odd Nat.not_odd_even
theorem Nat.pred_even_odd {n : Nat} (h₁ : Nat.isEven n) (h₂ : n > 0) : Nat.isOdd n.pred := by
cases n with
| zero => contradiction
| succ o => simp[Nat.isEven] at h₁
assumption
theorem Nat.sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) : a - b < c :=
have h₃ : a + 1 ≤ c + b := Nat.succ_le_of_lt h₁
have h₄ := Nat.sub_le_of_le_add h₃
have h₅ : 1 + a - b ≤ c := (Nat.add_comm a 1).subst (motive := λx ↦ x - b ≤ c) h₄
have h₆ := Nat.add_sub_assoc h₂ 1
have h₇ : 1 + (a-b) ≤ c := h₆.subst (motive := λx ↦ x ≤ c) h₅
have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
Nat.lt_of_succ_le h₈
theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by
apply Nat.sub_lt_of_lt_add
case h₂ => assumption
case h₁ =>
have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
rw[Nat.sub_add_cancel h₃]
assumption
theorem Nat.add_eq_zero {a b : Nat} : a + b = 0 ↔ a = 0 ∧ b = 0 := by
constructor <;> intro h₁
case mpr =>
simp[h₁]
case mp =>
cases a <;> simp_arith at *; assumption
|
