blob: 71420edb2116054e698d918b3cafbcb325610935 (
plain) (
blame)
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
|
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 inl 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 inr h₄ => rewrite[Nat.not_lt_eq power n] at h₄
exact Nat.le_antisymm h₃ h₄
termination_by power_of_two_go_one_eq _ p _ _ _ => n - p
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₄
have h₆ (m : Nat) : 2*m+2 > 2^0 := by
induction m with
| zero => decide
| succ o o_ih => simp_arith at *
have h₆ := Nat.le_step $ Nat.le_step o_ih
simp_arith at h₆
assumption
have h₆ := Nat.ne_of_lt (h₆ m)
simp_arith at h₆
rewrite[h₄] at h₆ --why is this needed?!?
contradiction
| 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₂
|
