Add ≤‴-irrelevant to Data.Nat.Properties

[tsung-ju]

No description provided.

[jamesmckinna]

Thanks for the proposed contribution.

Two quick comments in place ahead of a proper review:

• besides 'completeness', what's the rationale for the addition? (this relation is rarely used in the library, and never, AFAIK, in a context where its being Irrelevant is important) UPDATED: grep suggests that the relation is never used in stdlib! So better perhaps would be a PR to deprecate the relation and its properties entirely Refactor/deprecate Data.Nat.Base._≤‴_ and its properties #2504 ?
• the proofs do look very gnarly (esp. the use of subst; cf. the use of custom cast lemmas described here), so I wonder if they can be simplified.

If we do agree to add this, you will need a CHANGELOG entry as well.

[jamesmckinna]

Suggest adding the proof of Irreflexive _≡_ _≤‴_ in order to make use of it.

Needs CHANGELOG.

[tsung-ju]

Hi, thanks for the feedback!

My use case for m ≤‴ n is to represent numbers with a lower bound m, using ≤‴-refl and ≤‴-step to adjust the lower bound. I needed irrelevance to prove decidable equality for a data structure containing these proofs. The proof was tricky under without-K, so I thought it might be a helpful addition. That said, I’m not opposed to deprecating or revising _≤‴_, as it can be difficult to work with in its current form.

I’ve addressed the easier suggestions and will update the CHANGELOG soon. I’ll also explore possible simplifications using cast.

[jamesmckinna]

I’ve addressed the easier suggestions and will update the CHANGELOG soon. I’ll also explore possible simplifications using cast.

This last part is entirely optional, except to draw your attention to the subst (fully general)/cast (specific on a per-type/-per-predicate/per-relation basis) distinction as a basis for 'subst-like' reasoning where matching on refl is actually doing too much, or the wrong kind of, evaluation (in particular, work that isn't erasable at run-time in a backend).

[jamesmckinna]

My use case for m ≤‴ n is to represent numbers with a lower bound m, using ≤‴-refl and ≤‴-step to adjust the lower bound. I needed irrelevance to prove decidable equality for a data structure containing these proofs. The proof was tricky under without-K, so I thought it might be a helpful addition. That said, I’m not opposed to deprecating or revising _≤‴_, as it can be difficult to work with in its current form.

Yes, I agree it's not that easy to work with:

• few properties, and those mostly by delegation to the other relations
• whereas the refactoring characterisation I offer in Refactor/deprecate Data.Nat.Base._≤‴_ and its properties #2504 has much more direct proofs of equivalence with _≤_/_<_...
• as for Irrelevant _≤‴_ itself, it yields a more 'symmetric' proof structure

All this makes me speculate as to whether you might want to explore working directly with _≤_/_<_ together with the lemma Data.Nat.Properties.m<1+n⇒m<n∨m≡n (or an equivalent one based on inverting ≤‴-step as a statement about _<_? It's hard to guess exactly what you in fact 'need'...)

But all of these could be considered for downstream refactorings...