[ add ] Nat lemmas with `_∸_`, `_⊔_` and `_⊓_` by jkopanski · Pull Request #2924 · agda/agda-stdlib

jkopanski · 2026-01-26T13:17:05Z

Some stuff that I've needed. I have no idea if those belong here in stdlib. I don't know if I've put those in the right place, or named them properly. Hence the draft and lack of changlog entry.

MatthewDaggitt

Thanks for the PR!

Naming and placement looks good to me.
We tend to avoid rewriting in favour of using equational reasoning as its a) less brittle and b) clearer to the user what is going on. Could you switch these to use equational reasoning?

Taneb · 2026-01-27T07:33:23Z

src/Data/Nat/Properties.agda

 ------------------------------------------------------------------------
 -- Properties of _∸_ and _⊓_ and _⊔_

+m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n


This property doesn't feel natural to me, and the definition is short enough I don't really think it needs a name

It looks kind of similar to the m⊔n≤m+n that is already here.

I'm okay - lets one do proofs at a higher level with fewer steps.

Can you provide an example of an "interesting" proof where this lemma is a useful step?

I don't know if that counts as interesting, but the only place where I used it is down below in the m⊔n∸[m∸n]≡n.

Just to be clear I'm fine with removing that. In this PR I've just included stuff that I've tried to lookup in the stdlib first and written down once I couldn't find it.

Having pondered this for a while, I'm leaning towards @Taneb 's position more than @JacquesCarette 's.

jamesmckinna · 2026-01-29T10:08:33Z

Monus m∸n is characterised #1949 by a pair of adjoint properties wrt the ordering _≤_, so it seems as though these properties also ought to be obtainable from those and the corresponding characterisations of _⊓_ and _⊔_ as glb (product) and lub (copoduct) in that category/preorder.

jamesmckinna · 2026-01-29T12:45:31Z

src/Data/Nat/Properties.agda

 ∣m-n∣≤m⊔n (suc m) zero    = ≤-refl
 ∣m-n∣≤m⊔n (suc m) (suc n) = m≤n⇒m≤1+n (∣m-n∣≤m⊔n m n)

+∣m-n∣≡m⊔n∸m⊓n : ∀ m n → ∣ m - n ∣ ≡ m ⊔ n ∸ m ⊓ n


The structure of this proof recalls that of ∣m-n∣≡[m∸n]∨[n∸m] (L1863).
Is there a refactoring which allows you to prove each result from some other, more general lemma?

Separately, you might like to consider refactoring this proof to not use with, but (more) simply via [ branch1 , branch2 ]′ $ ≤-total m n for suitable subproofs branch1, branch2, should you ever need to reason about this operation. cf. 'with (sometimes) considered harmful' #2123

The structure of this proof recalls that of ∣m-n∣≡[m∸n]∨[n∸m] (L1863).
Is there a refactoring which allows you to prove each result from some other, more general lemma?

Is this actual question or more like a teacher question where you know there is and you probing me to look for it? I'm asking as I can't really find it.
I could rewrite it where instead of ≤-total I would match on the result of ∣m-n∣≡m⊔n∸m⊓n but that would only handle lhs, for rhs I would still need to recover the m≤n and n≤m from the result using ∣m-n∣≡m∸n⇒n≤m and ∣m-n∣≡n∸m⇒m≤n*

*) seems this one is missing, let me add it here

@jkopanski Thanks!

While it possible that I do indeed ask questions in a 'teacher-like' style (as friends and colleagues often point out to me... you can't easily take the teacher out of me ;-)), here I must say that my question was one of curiosity!

I think that there is a general principle for stdlib that we try not to 'over-duplicate' or generate (too much) additional redundancy between lemmas. Here I could see that there is a 'similar' result, so I was hoping there might be a way to exploit the similarity. But if not, then not!

And if there is, then we can always refactor downstream... ;-)

UPDATED: happy to leave this for later, but perhaps this could be refactored using Relation.Binary.Consequences.wlog...

Something to think about for another day: to try to characterise what's going on here in terms of ∣ m - n ∣ as a symmetric difference operator, and any possible candidate IsBoolean(Semi)Ring structure on Nat...?

JacquesCarette

I'm fine with adding these. We can have later passes of simplification of proofs.

JacquesCarette · 2026-02-04T15:39:40Z

src/Data/Nat/Properties.agda

 ------------------------------------------------------------------------
 -- Properties of _∸_ and _⊓_ and _⊔_

+m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n


I'm okay - lets one do proofs at a higher level with fewer steps.

jamesmckinna · 2026-02-09T09:56:41Z

@jkopanski Shall we take this out of draft and try to get it in shape to merge? Or do you still want time to work on it further?

Some stuff that I've needed. I have no idea if those belong here in stdlib. I don't know if I've put those in the right place, or named them properly. Hence the draft and lack of changlog entry.

jkopanski · 2026-02-09T11:42:24Z

@jkopanski Shall we take this out of draft and try to get it in shape to merge? Or do you still want time to work on it further?

yes, I would like to get it going. I've rebased it on recent changes and added changlog entry.

There's the case of m∸n≤m⊔n to be decided.

I've only now noticed your update regarding wlog. I don't think edits trigger notification here. Anyway that is something that I've never used so it may take me some time to figure out, if we were to push on it in this pr.

jamesmckinna · 2026-02-09T13:37:12Z

@jkopanski Shall we take this out of draft and try to get it in shape to merge? Or do you still want time to work on it further?

...
I've only now noticed your update regarding wlog. I don't think edits trigger notification here. Anyway that is something that I've never used so it may take me some time to figure out, if we were to push on it in this pr.

No, as @JacquesCarette observes, we can handle that as a downstream refactoring. And wlog itself could do with some fresh thought... since #523 #2577 #2626

jamesmckinna · 2026-02-09T14:06:13Z

src/Data/Nat/Properties.agda

+m∸n+o≡m∸[n∸o] : ∀ {m n o} → n ≤ m → o ≤ n → (m ∸ n) + o ≡ m ∸ (n ∸ o)
+m∸n+o≡m∸[n∸o] {m}     {zero}  {zero}  z≤n       _         = +-identityʳ m
+m∸n+o≡m∸[n∸o] {suc m} {suc n} {zero}  (s≤s n≤m) z≤n       = +-identityʳ (m ∸ n)
+m∸n+o≡m∸[n∸o] {suc m} {suc n} {suc o} (s≤s n≤m) (s≤s o≤n) = begin-equality
+  suc m ∸ suc n + suc o ≡⟨ +-suc (m ∸ n) o ⟩
+  suc (m ∸ n + o)       ≡⟨ cong suc (m∸n+o≡m∸[n∸o] n≤m o≤n) ⟩
+  suc (m ∸ (n ∸ o))     ≡⟨ ∸-suc (≤-trans (m∸n≤m n o) n≤m) ⟨
+  suc m ∸ (n ∸ o)       ∎


So... noting that it took me a long time to internalise this idiom, stdlib design tends to favour:

making at least m and n explicit (because not directly inferrable from _∸ _), as in the lemma immediately following this one, but probably also o as well, for the same reason

making arguments of (proof-irrelevant) propositions n ≤ m and o ≤ n definitionally irrelevant where possible
So, here:

Suggested change

m∸n+o≡m∸[n∸o] : ∀ {m n o} → n ≤ m → o ≤ n → (m ∸ n) + o ≡ m ∸ (n ∸ o)

m∸n+o≡m∸[n∸o] {m} {zero} {zero} z≤n _ = +-identityʳ m

m∸n+o≡m∸[n∸o] {suc m} {suc n} {zero} (s≤s n≤m) z≤n = +-identityʳ (m ∸ n)

m∸n+o≡m∸[n∸o] {suc m} {suc n} {suc o} (s≤s n≤m) (s≤s o≤n) = begin-equality

suc m ∸ suc n + suc o ≡⟨ +-suc (m ∸ n) o ⟩

suc (m ∸ n + o) ≡⟨ cong suc (m∸n+o≡m∸[n∸o] n≤m o≤n) ⟩

suc (m ∸ (n ∸ o)) ≡⟨ ∸-suc (≤-trans (m∸n≤m n o) n≤m) ⟨

suc m ∸ (n ∸ o) ∎

m∸n+o≡m∸[n∸o] : ∀ m n o → n ≤ m → .(o ≤ n) → (m ∸ n) + o ≡ m ∸ (n ∸ o)

m∸n+o≡m∸[n∸o] m zero zero _ _ = +-identityʳ m

m∸n+o≡m∸[n∸o] (suc m) (suc n) zero sn≤sm _ = +-identityʳ (m ∸ n)

m∸n+o≡m∸[n∸o] (suc m) (suc n) (suc o) sn≤sm so≤sn = begin-equality

suc m ∸ suc n + suc o ≡⟨ +-suc (m ∸ n) o ⟩

suc (m ∸ n + o) ≡⟨ cong suc (m∸n+o≡m∸[n∸o] m n o (s≤s⁻¹ sn≤sm) (s≤s⁻¹ so≤sn)) ⟩

suc (m ∸ (n ∸ o)) ≡⟨ ∸-suc (≤-trans (m∸n≤m n o) (s≤s⁻¹ sn≤sm)) ⟨

suc m ∸ (n ∸ o) ∎

And in fact, n ≤ m can also be made irrelevant, after refactoring lemma ∸-suc...

making at least m and n explicit (because not directly inferrable from _∸ _)

Oh I thought the m n o were inferred from the inequalities passed.

as in the lemma immediately following this one

indeed that seems to be the case in the m≤n+o⇒m∸n≤o, but the lemmas directly above: +-∸-assoc, ∸-+-assoc and +-∸-comm seems to follow the convention I mentioned: variables that are used in the inequalities are implicit, explicit ones are only the ones that aren't used in any arguments to the lemma.

Does making arguments proof irrelevant changes anything with that regard?

D'oh, yes, you're quite correct, each of m, n, and o, is inferrable from the hypotheses. Apologies!

But... see also #2790 : if you have an irrelevant (relation) argument, and the values on which it depends are implicit, sometimes Agda can't quite figure them out during inference when used, rather than defined. Puzzling...

jamesmckinna · 2026-02-13T11:14:29Z

@MatthewDaggitt are you happy that your review requests have been answered satisfactorily?
if so, I think we could move to merging this in?

MatthewDaggitt added this to the v2.4 milestone Jan 27, 2026

MatthewDaggitt added the addition label Jan 27, 2026

MatthewDaggitt requested changes Jan 27, 2026

View reviewed changes

Taneb reviewed Jan 27, 2026

View reviewed changes

jkopanski force-pushed the more-nats branch from f7ba325 to c4ff219 Compare January 28, 2026 11:01

jamesmckinna reviewed Jan 29, 2026

View reviewed changes

JacquesCarette approved these changes Feb 4, 2026

View reviewed changes

[ add ] Nat lemmas with _∸_, _⊔_ and _⊓_

e759a75

Some stuff that I've needed. I have no idea if those belong here in stdlib. I don't know if I've put those in the right place, or named them properly. Hence the draft and lack of changlog entry.

jkopanski force-pushed the more-nats branch from c4ff219 to e759a75 Compare February 9, 2026 11:39

jkopanski marked this pull request as ready for review February 9, 2026 11:42

jamesmckinna reviewed Feb 9, 2026

View reviewed changes

jamesmckinna mentioned this pull request Feb 9, 2026

[ refactor ] Data.Nat.Properties.∸-suc to make m≤n argument irrelevant #2939

Merged

Comments

Conversation

jkopanski commented Jan 26, 2026

Uh oh!

MatthewDaggitt left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Jan 29, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna Feb 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JacquesCarette left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Feb 9, 2026

Uh oh!

jkopanski commented Feb 9, 2026

Uh oh!

jamesmckinna commented Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

jamesmckinna commented Feb 13, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

jamesmckinna Feb 4, 2026 •

edited

Loading

jamesmckinna commented Feb 9, 2026 •

edited

Loading