[ add ] inequalities for 2 ^ log₂ n (#2925)

* [ add ] inequalities for `2 ^ log₂ n`

This adds the inequalities `2 ^ ⌊log₂ n ⌋ ≤ n` for non-zero `n` and
`n ≤ 2 ^ ⌈log₂ n ⌉` for all natural numbers `n`. Similar to the existing
properties of the logarithm, the main proofs
that keep track of the accumulators are added to
`Data.Nat.Logarithm.Core`. Both use a lemma that `2 * (ℕ.suc n) ≡ 2 + (n + n)`
which is added to `Data.Nat.Logarithm.Core` as well.

The respective simplified versions on `⌊log₂_⌋` and `⌈log₂_⌉` are added
directly to `Data.Nat.Logarithm`.

* move 2*suc[n]≡2+n+n to Data.Nat.Properties

* ℕ.suc -> suc

* Further ℕ.suc -> suc

* replace 1 + with suc

* Switch to equational reasoning

* Update Changelog

* RM unused 'trans'

* Use NonZero instance

* Update Changelog

* Update src/Data/Nat/Logarithm.agda

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

* Update CHANGELOG.md

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

---------

Co-authored-by: jamesmckinna <31931406+jamesmckinna@users.noreply.github.com>

Author: t-wissmann

CHANGELOG.md

@@ -236,6 +236,18 @@ Additions to existing modules
   map : P ⊆ Q → All P xs → All Q xs
   ```
 
+* In `Data.Nat.Logarithm`
+  ```agda
+  2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
+  n≤2^⌈log₂n⌉ : ∀ n → n ≤ 2 ^ ⌈log₂ n ⌉
+  ```
+
+* In `Data.Nat.Logarithm.Core`
+  ```agda
+  2^⌊log2n⌋≤n : ∀ n .{{_ : NonZero n}} → (acc : Acc _<_ n) → 2 ^ (⌊log2⌋ n acc) ≤ n
+  n≤2^⌈log2n⌉ : ∀ n → (acc : Acc _<_ n) → n ≤ 2 ^ (⌈log2⌉ n acc)
+  ```
+
 * In `Data.Nat.ListAction.Properties`
   ```agda
   *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)
@@ -248,6 +260,7 @@ Additions to existing modules
   ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
   ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
+  2*suc[n]≡2+n+n : ∀ n → 2 * (suc n) ≡ 2 + (n + n)
   ```
 
 * In `Data.Product.Properties`:

src/Data/Nat/Logarithm.agda

@@ -41,6 +41,9 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 ⌊log₂[2^n]⌋≡n : ∀ n → ⌊log₂ (2 ^ n) ⌋ ≡ n
 ⌊log₂[2^n]⌋≡n n = ⌊log2⌋2^n≡n n
 
+2^⌊log₂n⌋≤n : ∀ n .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
+2^⌊log₂n⌋≤n n = 2^⌊log2n⌋≤n n (<-wellFounded n)
+
 ------------------------------------------------------------------------
 -- Properties of ⌈log₂_⌉
 
@@ -55,3 +58,6 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 ⌈log₂2^n⌉≡n : ∀ n → ⌈log₂ (2 ^ n) ⌉ ≡ n
 ⌈log₂2^n⌉≡n n = ⌈log2⌉2^n≡n n
+
+n≤2^⌈log₂n⌉ : ∀ n → n ≤ 2 ^ ⌈log₂ n ⌉
+n≤2^⌈log₂n⌉ n = n≤2^⌈log2n⌉ n (<-wellFounded n)

src/Data/Nat/Logarithm/Core.agda

@@ -81,6 +81,18 @@ open import Relation.Binary.PropositionalEquality.Properties
   suc n                                 ∎
   where open ≡-Reasoning
 
+2^⌊log2n⌋≤n : ∀ n .{{_ : NonZero n}} → (acc : Acc _<_ n) → 2 ^ (⌊log2⌋ n acc) ≤ n
+2^⌊log2n⌋≤n (suc zero)     _       = ≤-refl
+2^⌊log2n⌋≤n (suc (suc n)) (acc rs) = begin
+  2 ^ (⌊log2⌋ (suc (suc n)) (acc rs)) ≡⟨⟩
+  2 * 2 ^ (⌊log2⌋ (suc ⌊ n /2⌋) _)    ≤⟨ *-monoʳ-≤ 2 (2^⌊log2n⌋≤n _ _) ⟩
+  2 * (suc ⌊ n /2⌋)                   ≡⟨ 2*suc[n]≡2+n+n _ ⟩
+  2 + (⌊ n /2⌋ + ⌊ n /2⌋)             ≤⟨ +-monoʳ-≤ (2 + ⌊ n /2⌋) (⌊n/2⌋≤⌈n/2⌉ _)  ⟩
+  2 + (⌊ n /2⌋ + ⌈ n /2⌉)             ≡⟨ cong (2 +_) (⌊n/2⌋+⌈n/2⌉≡n _) ⟩
+  2 + n
+  ∎
+  where open ≤-Reasoning
+
 ------------------------------------------------------------------------
 -- Properties of ⌈log2⌉
 
@@ -124,3 +136,17 @@ open import Relation.Binary.PropositionalEquality.Properties
   1 + ⌈log2⌉ (2 ^ n) (<-wellFounded _)  ≡⟨ cong suc (⌈log2⌉2^n≡n n) ⟩
   suc n                                 ∎
   where open ≡-Reasoning
+
+n≤2^⌈log2n⌉ : ∀ n → (acc : Acc _<_ n) → n ≤ 2 ^ (⌈log2⌉ n acc)
+n≤2^⌈log2n⌉ zero _ = z≤n
+n≤2^⌈log2n⌉ (suc zero) _ = s≤s z≤n
+n≤2^⌈log2n⌉ (suc (suc n)) (acc rs) =
+  begin
+  2 + n                                ≡⟨ cong (2 +_) (⌊n/2⌋+⌈n/2⌉≡n _) ⟨
+  2 + (⌊ n /2⌋ + ⌈ n /2⌉)              ≤⟨ +-monoʳ-≤ 2 (+-monoˡ-≤ _ (⌊n/2⌋≤⌈n/2⌉ n)) ⟩
+  2 + (⌈ n /2⌉ + ⌈ n /2⌉)              ≡⟨ 2*suc[n]≡2+n+n _ ⟨
+  2 * (suc ⌊ suc n /2⌋)                ≤⟨ *-monoʳ-≤ 2 (n≤2^⌈log2n⌉ (suc ⌊ suc n /2⌋) _) ⟩
+  2 * 2 ^ (⌈log2⌉ (suc ⌊ suc n /2⌋) _) ≡⟨⟩
+  2 ^ (⌈log2⌉ (2 + n) (acc rs))
+  ∎
+  where open ≤-Reasoning

src/Data/Nat/Properties.agda

@@ -774,6 +774,12 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
   suc (m + (n + m * n)) ≡⟨⟩
   suc m + suc m * n     ∎
 
+2*suc[n]≡2+n+n : ∀ n → 2 * (suc n) ≡ 2 + (n + n)
+2*suc[n]≡2+n+n n = begin-equality
+  2 * (suc n)    ≡⟨ cong (suc n +_) (+-identityʳ _) ⟩
+  suc n + suc n  ≡⟨ +-suc (suc n) n ⟩
+  2 + (n + n)    ∎
+
 ------------------------------------------------------------------------
 -- Algebraic properties of _*_