Agda-stdlib: `_≤ᵇ_` for Natural numbers

[HuStmpHrrr]

I realized that now in stdlib, _<ᵇ_ is defined and _≤?_ depends on it. Does that make sense to define _≤ᵇ_ in terms of _<ᵇ_ and have _≤?_ derive proofs from _≤ᵇ_? Namely, two additional lemmas, ≤ᵇ⇒≤ and ≤⇒≤ᵇ. I am asking this, because for me _≤_ is a more frequent relation than _<_.

[MatthewDaggitt]

Hmm, well the idea is that _<ᵇ_ should only be used very rarely. We've only added it in order to give _≤?_ a performance boost behind the scenes.

I'm struggling to think of a use case for where using m ≤ᵇ n wouldn't be able to be replaced by ⌊ m ≤? n ⌋. Maybe there's a small constant factor in difference in performance, but that's probably eliminated by the necessity of having to define m ≤ᵇ n as m <ᵇ n ∨ m =ᵇ n.

Basically if we can come up with a use for it then yes. Otherwise I think best to try and keep the boolean versions as unobtrusive as possible and encourage everyone to use the proper dependent types. I know as an Agda beginner I would have gone straight for the boolean versions if they were prominently available.

[HuStmpHrrr]

one trouble I have with the current definition of _≤?_ is that it builds the proof by depending on _<_ relation. my use case is the following two lemmas.

≤?-yes : ∀ {m n} (m≤n : m ≤ n) → (m ≤? n) ≡ yes m≤n

≤?-no : ∀ {m n} (m>n : ¬ m ≤ n) → ∃ λ ¬p → (m ≤? n) ≡ no ¬p

the idea is that if _≤ᵇ_ exists, then probably _≤?_ can depend on it and make use of T and derive this conclusion. that's where these two lemmas are coming from: ≤ᵇ⇒≤ and ≤⇒≤ᵇ.

[gallais]

We should probably provide a pair of general lemmas:

(p? : Decidable P) -> Irrelevant P -> (p : P) -> p? ≡ yes p
(p? : Decidable P) -> ¬ P ->  ∃ λ ¬p → p? ≡ no ¬p

Which could then be used to reimplement ≡-≟-identity and ≢-≟-identity in
Relation.Binary.PropositionalEquality as well as the result you
are interested in.

[HuStmpHrrr]

yes that's true. probably the first lemma can have a relevant variant.

[jespercockx]

Why does ≤?-no need the extra ∃ λ ¬p → ...? Any two proofs of a negative proposition are equal, so we should be able to strengthen it to ≤?-no : ∀ {m n} (m>n : ¬ m ≤ n) → (m ≤? n) ≡ no m>n (which also makes it more symmetric to ≤?-yes).

[HuStmpHrrr]

sorry I might not react fast enough today. could you please explain why that's true?

for example,

module _ {m n : ℕ}
         (m>n : ¬ m ≤ n) where

  m>n′ : ¬ m ≤ n
  m>n′ z≤n       = m>n z≤n
  m>n′ (s≤s m≤n) = m>n (s≤s m≤n)

  irrelevant : m>n ≡ m>n′
  irrelevant = {!!}

how can this be proved?

[jespercockx]

Hm, I was a bit too fast: you can prove that they are pointwise equal (because any two elements of the empty type are equal) but to prove that m>n and m>n′ are equal you need functional extensionality. Maybe it's not worth making that extra assumption (though it's quite common).

[WolframKahl]

On Sun, May 19, 2019 at 10:57:12AM -0700, Jesper Cockx wrote:

Any two proofs of a negative proposition are equal

Are they? You seemed to argue differently in and around https://github.com/agda/agda/issues/2516#issuecomment-290532034 ...

[jespercockx]

They are propositionally equal, not definitionally equal (if you want them to be, you can use irrelevance or Prop).

[gallais]

Yep. That's why I opened #645 but then we decided that the change would be too
invasive, effectively forcing all the users of the standard library to accept
working in Agda with --prop enabled.

[jespercockx]

I always argued in favour of making --prop enabled by default, you can blame @andreasabel for that :P

[MatthewDaggitt]

We should probably provide a pair of general lemmas:

(p? : Decidable P) -> Irrelevant P -> (p : P) -> p? ≡ yes p
(p? : Decidable P) -> ¬ P ->  ∃ λ ¬p → p? ≡ no ¬p

Which could then be used to reimplement ≡-≟-identity and ≢-≟-identity in
Relation.Binary.PropositionalEquality as well as the result you
are interested in.

Yup, we'd need to add the definition Irrelevant to Relation.Nullary as well.

[HuStmpHrrr]

It's OK to always have --prop open, isn't it? what can it hurt?

[jespercockx]

Without --prop, you can write the following:

data D A : Set where
  c : A -> D A

and Agda will figure out that A : Set. With --prop it could be either A : Set or A : Prop, so Agda refuses the type.

[MatthewDaggitt]

The original problem has been solved so I'm closing this.