Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
jamesmckinna merged 12 commits into from
Jan 29, 2026
Merged

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

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
7286a54
[ add ] inequalities for `2 ^ log₂ n`
t-wissmann Jan 28, 2026
f05723d
move 2*suc[n]≡2+n+n to Data.Nat.Properties
t-wissmann Jan 28, 2026
70b1148
ℕ.suc -> suc
t-wissmann Jan 28, 2026
76bd712
Further ℕ.suc -> suc
t-wissmann Jan 28, 2026
9ca32d6
replace 1 + with suc
t-wissmann Jan 28, 2026
79ac364
Switch to equational reasoning
t-wissmann Jan 28, 2026
5911038
Update Changelog
t-wissmann Jan 28, 2026
a2687d5
RM unused 'trans'
t-wissmann Jan 28, 2026
4e6b150
Use NonZero instance
t-wissmann Jan 28, 2026
cc1b10f
Update Changelog
t-wissmann Jan 28, 2026
209b2da
Update src/Data/Nat/Logarithm.agda
t-wissmann Jan 29, 2026
2cc2abf
Update CHANGELOG.md
t-wissmann Jan 29, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 6 additions & 0 deletions src/Data/Nat/Logarithm.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (ℕ.suc n) = 2^⌊log2n⌋≤n n (<-wellFounded (ℕ.suc n))
Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you implement the above changes, then this could/should now simply be:

Suggested change
2^⌊log₂n⌋≤n (ℕ.suc n) = 2^⌊log2n⌋≤n n (<-wellFounded (ℕ.suc n))
2^⌊log₂n⌋≤n n = 2^⌊log2n⌋≤n n (<-wellFounded n)


------------------------------------------------------------------------
-- Properties of ⌈log₂_⌉

Expand All @@ -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)
29 changes: 28 additions & 1 deletion src/Data/Nat/Logarithm/Core.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ open import Data.Nat.Properties
open import Data.Nat.Induction using (<-wellFounded)
open import Induction.WellFounded using (Acc; acc)
open import Relation.Binary.PropositionalEquality.Core
using (_≡_; refl; cong; sym)
using (_≡_; refl; cong; sym; trans)
open import Relation.Binary.PropositionalEquality.Properties
using (module ≡-Reasoning)

Expand Down Expand Up @@ -81,6 +81,19 @@ open import Relation.Binary.PropositionalEquality.Properties
suc n ∎
where open ≡-Reasoning

2^⌊log2n⌋≤n : ∀ n → (acc : Acc _<_ (1 + n)) → 2 ^ (⌊log2⌋ (1 + n) acc) ≤ 1 + n
2^⌊log2n⌋≤n ℕ.zero _ = s≤s z≤n
2^⌊log2n⌋≤n (ℕ.suc n) (acc rs) =
begin
Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is very nice, but I think that it would be 'better' (for a suitable definition of 'better' ;-) certainly 'more in line with the std-lib library style'...) to use the NonZero predicate as an (irrelevant) instance as part of the type, rather than relying on the knowledge that suc n/1 + n is automatically NonZero...

Accordingly:

Suggested change
2^⌊log2n⌋≤n : ∀ n → (acc : Acc _<_ (1 + n)) → 2 ^ (⌊log2⌋ (1 + n) acc) ≤ 1 + n
2^⌊log2n⌋≤n ℕ.zero _ = s≤s z≤n
2^⌊log2n⌋≤n (ℕ.suc n) (acc rs) =
begin
2^⌊log2n⌋≤n : ∀ n .{{_ : NonZero n}} → (acc : Acc _<_ n) → 2 ^ (⌊log2⌋ n acc) ≤ n
2^⌊log2n⌋≤n (ℕ.suc n) (acc rs) =
begin

I haven't checked that the rest of the proof goes through unchanged, but... it shouldn't require much more work to fix things?

Copy link
Contributor Author

@t-wissmann t-wissmann Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My proof needs the case

2^⌊log2n⌋≤n ℕ.zero _ = s≤s z≤n

at some point because the proof is by induction on n and I can't image how the induction should work without the base case. I tried it but I don't see how to update the proof such that it still compiles for your suggested type

2^⌊log2n⌋≤n : ∀ n .{{_ : NonZero n}} → (acc : Acc _<_ n) → 2 ^ (⌊log2⌋ n acc) ≤ n

Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, you're quite right. See below!

Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 28, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more. 

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

NB. style-guide mandates that begin should be on the same line as the LHS of the definition.

Copy link
Contributor Author

@t-wissmann t-wissmann Jan 28, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I've updated it (also in the Changelog). However, I find the definition in Logarithm.agda then more difficult to understand, because it is not visible that the property of n being NonZero is passed to the call:

2^⌊log₂n⌋≤n : ∀ n → .{{ _ : NonZero n }} → 2 ^ ⌊log₂ n ⌋ ≤ n
2^⌊log₂n⌋≤n n = 2^⌊log2n⌋≤n n (<-wellFounded n)

But it's fine for me. :-)

Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 29, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah!

There are two ways to think about this problem (there may be others... I offer only two here!?), of which the first is what I take to be your 'difficulty' above:

  • instance arguments are mysterious, because we neither see them explicitly bound on the LHS, nor see them explicitly passed as arguments on the RHS;
  • instance arguments are fantastically useful, especially as here, when used as irrelevant arguments, because we neither see them explicitly bound on the LHS, nor see them explicitly passed as arguments on the RHS.

Spelt out, the definition above amounts to (and I believe this is what the type checker is more or less doing):

2^⌊log₂n⌋≤n n {{nz}} = 2^⌊log2n⌋≤n n (<-wellFounded n) {{something}}
  where
  something = <a proof of NonZero n>

in such a way that:

  • something can be uniquely computed from the 'visible' arguments, and any other declared instances, in scope (this is the requirement for instance inference to succeed)
  • argument nz cannot actually be used in a relevant way, but that's OK, because here, the function 2^⌊log2n⌋≤n also expects its instance argument to be used in an irrelevant way
  • so... taking something = nz seems the only available choice, and moreover it satisfies the conditions above.

Ie.

2^⌊log₂n⌋≤n n {{nz}} = 2^⌊log2n⌋≤n n (<-wellFounded n) {{nz}}

or even, to emphasise that we are not allowed even to consider using nz in a relevant way

2^⌊log₂n⌋≤n n {{_}} = 2^⌊log2n⌋≤n n (<-wellFounded n) {{_}}

where the use of _ on the LHS means "I don't care", while on the RHS means "you figure it out", in the dialogue game between user ("I") and typechecker ("you").

Once we arrive at the version with underscores, well, then they really are just noise, so...

2 ^ (⌊log2⌋ (2 + 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⌉

Expand Down Expand Up @@ -124,3 +137,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 * (1 + ⌊ 1 + n /2⌋) ≤⟨ *-monoʳ-≤ 2 (n≤2^⌈log2n⌉ (1 + ⌊ 1 + n /2⌋) _) ⟩
2 * 2 ^ (⌈log2⌉ (1 + ⌊ 1 + n /2⌋) _) ≡⟨⟩
2 ^ (⌈log2⌉ (2 + n) (acc rs))
∎
where open ≤-Reasoning
3 changes: 3 additions & 0 deletions src/Data/Nat/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -774,6 +774,9 @@ 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 = trans (cong ((1 + n) +_) (+-identityʳ _)) (+-suc (1 + n) n)

------------------------------------------------------------------------
-- Algebraic properties of _*_

Expand Down