19e06acc65
I made a few choices so far that can probably be discussed: - got rid of `modn` on `UInt`, nobody seems to use it apart from the definition of `shift` which can use normal `mod` - removed the previous defeq optimized definition of `USize.size` in favor for a normal one. The motivation was to allow `OfNat` to work which doesn't seem to be necessary anymore afaict. - Minimized uses of `.val`, should we maybe mark it deprecated? - Mostly got rid of `.val` in basically all theorems as the proper next level of API would now be `.toBitVec`. We could probably re-prove them but it would be more annoying given the change of definition. - Did not yet redefine `log2` in terms of `BitVec` as this would require a `log2` in `BitVec` as well, do we want this? - I added a couple of theorems around the relation of `<` on `UInt` and `Nat`. These were previously not needed because defeq was used all over the place to save us. I did not yet generalize these to all types as I wasn't sure if they are the appropriate lemma that we want to have.
54 lines
1.7 KiB
Text
54 lines
1.7 KiB
Text
/-
|
|
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
|
|
|
|
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
|