[ add ] inequalities for 2 ^ log₂ n

[t-wissmann]

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.

[gallais]

Nice!

[gallais]

The convention is to write 2*suc[n]≡2+n+n for this type of lemma.
It should probably be moved to Data.Nat.Properties.

[t-wissmann]

Thanks! I've renamed the lemma to 2*suc[n]≡2+n+n and have moved it to Data.Nat.Properties. Is the location in there OK? I put it right under *-suc

[jamesmckinna]

This looks great, but I think could be 'better' streamlined.

And... you'll need a CHANGELOG entry for the additional lemmas (once their statements have stabilised...).

[jamesmckinna]

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?

[t-wissmann]

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

[jamesmckinna]

Yes, you're quite right. See below!

[jamesmckinna]

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.

[t-wissmann]

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. :-)

[jamesmckinna]

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...

[jamesmckinna]

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)

[jamesmckinna]

I notice as well that your changes are on your master branch, rather than first cloning a fork of agda/master and then opening a new branch for the PR (as in the HACKING guide...).

This is (more or less) fine for a first PR, but generally not recommended as a future-proof strategy!

[t-wissmann]

Thanks for the pointer to HACKING! I will choose a different name next time.

[jamesmckinna]

Nearly there!

[jamesmckinna]

Yes, you're quite right. See below!

[jamesmckinna]

Again...

Suggested change

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

[jamesmckinna]

I fixed your proof.
Oh, for some reason, the suggestion didn't get recorded?

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 be on the same line as the LHS of the definition...

[jamesmckinna]

Modulo the noisy arrows, this is all fine.

Many thanks for a first contribution to std-lib

[t-wissmann]

Thank you for accepting! I also commited your suggestions regarding the removal of unnecessary →.
I'm not so familiar with the instances arguments, so I really appreciate your explanations on that! :-)