-
Notifications
You must be signed in to change notification settings - Fork 350
/
Power2.lean
56 lines (46 loc) · 1.74 KB
/
Power2.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
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Data.Nat.Linear
namespace Nat
protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pos_pow_of_pos _ (by decide)
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power := by
have : power * 2 = power + power := by simp_arith
rw [this, Nat.sub_add_eq]
exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁
def nextPowerOfTwo (n : Nat) : Nat :=
go 1 (by decide)
where
go (power : Nat) (h : power > 0) : Nat :=
if power < n then
go (power * 2) (Nat.mul_pos h (by decide))
else
power
termination_by n - power
decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
theorem one_isPowerOfTwo : isPowerOfTwo 1 :=
⟨0, by decide⟩
theorem mul2_isPowerOfTwo_of_isPowerOfTwo (h : isPowerOfTwo n) : isPowerOfTwo (n * 2) :=
have ⟨k, h⟩ := h
⟨k+1, by simp [h, Nat.pow_succ]⟩
theorem pos_of_isPowerOfTwo (h : isPowerOfTwo n) : n > 0 := by
have ⟨k, h⟩ := h
rw [h]
apply Nat.pos_pow_of_pos
decide
theorem isPowerOfTwo_nextPowerOfTwo (n : Nat) : n.nextPowerOfTwo.isPowerOfTwo := by
apply isPowerOfTwo_go
apply one_isPowerOfTwo
where
isPowerOfTwo_go (power : Nat) (h₁ : power > 0) (h₂ : power.isPowerOfTwo) : (nextPowerOfTwo.go n power h₁).isPowerOfTwo := by
unfold nextPowerOfTwo.go
split
. exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
. assumption
termination_by n - power
decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
end Nat