Skip to content

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

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

Draft
jkopanski wants to merge 1 commit into
base: master
Choose a base branch
from
+39 −0
Draft

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

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
39 changes: 39 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 @@ -1634,6 +1634,15 @@ m≤n⇒n∸m≤n (s≤s m≤n) = m≤n⇒m≤1+n (m≤n⇒n∸m≤n m≤n)
suc ((m + n) ∸ o) ≡⟨ cong suc (+-∸-assoc m o≤n) ⟩
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} 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} → m ≤ n + o → m ∸ n ≤ o
m≤n+o⇒m∸n≤o m zero le = le
m≤n+o⇒m∸n≤o zero (suc n) _ = z≤n
Expand Down Expand Up @@ -1722,11 +1731,30 @@ even≢odd (suc m) (suc n) eq = even≢odd m n (suc-injective (begin-equality
------------------------------------------------------------------------
-- Properties of _∸_ and _⊓_ and _⊔_

m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n
Copy link
Member

@Taneb Taneb Jan 27, 2026

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

@jkopanski jkopanski Jan 27, 2026

Choose a reason for hiding this comment

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

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

Copy link
Collaborator

@JacquesCarette JacquesCarette Feb 4, 2026

Choose a reason for hiding this comment

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

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

m∸n≤m⊔n m n = ≤-trans (m∸n≤m m n) (m≤m⊔n m n)

m⊓n+n∸m≡n : ∀ m n → (m ⊓ n) + (n ∸ m) ≡ n
m⊓n+n∸m≡n zero n = refl
m⊓n+n∸m≡n (suc m) zero = refl
m⊓n+n∸m≡n (suc m) (suc n) = cong suc $ m⊓n+n∸m≡n m n

m⊔n∸[m∸n]≡n : ∀ m n → m ⊔ n ∸ (m ∸ n) ≡ n
m⊔n∸[m∸n]≡n zero n = cong (n ∸_) (0∸n≡0 n)
m⊔n∸[m∸n]≡n (suc m) zero = n∸n≡0 m
m⊔n∸[m∸n]≡n (suc m) (suc n) = begin-equality
suc (m ⊔ n) ∸ (m ∸ n) ≡⟨ ∸-suc (m∸n≤m⊔n m n) ⟩
suc ((m ⊔ n) ∸ (m ∸ n)) ≡⟨ cong suc (m⊔n∸[m∸n]≡n m n) ⟩
suc n ∎

m⊔n≡m∸n+n : ∀ m n → m ⊔ n ≡ m ∸ n + n
m⊔n≡m∸n+n zero n = sym (cong (_+ n) (0∸n≡0 n))
m⊔n≡m∸n+n (suc m) zero = sym (cong suc (+-identityʳ m))
m⊔n≡m∸n+n (suc m) (suc n) = begin-equality
suc (m ⊔ n) ≡⟨ cong suc (m⊔n≡m∸n+n m n) ⟩
suc (m ∸ n + n) ≡⟨ +-suc (m ∸ n) n ⟨
m ∸ n + suc n ∎

[m∸n]⊓[n∸m]≡0 : ∀ m n → (m ∸ n) ⊓ (n ∸ m) ≡ 0
[m∸n]⊓[n∸m]≡0 zero zero = refl
[m∸n]⊓[n∸m]≡0 zero (suc n) = refl
Expand Down Expand Up @@ -1844,6 +1872,17 @@ m∸n≤∣m-n∣ m n with ≤-total m n
∣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
Copy link
Collaborator

@jamesmckinna jamesmckinna Jan 29, 2026

Choose a reason for hiding this comment

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

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

Copy link
Contributor Author

@jkopanski jkopanski Feb 4, 2026

Choose a reason for hiding this comment

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

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

Copy link
Collaborator

@jamesmckinna jamesmckinna Feb 4, 2026 •
edited
Loading

Choose a reason for hiding this comment

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

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

∣m-n∣≡m⊔n∸m⊓n m n with ≤-total m n
... | inj₁ m≤n = begin-equality
∣ m - n ∣ ≡⟨ m≤n⇒∣m-n∣≡n∸m m≤n ⟩
n ∸ m ≡⟨ cong₂ _∸_ (m≤n⇒m⊔n≡n m≤n) (m≤n⇒m⊓n≡m m≤n) ⟨
m ⊔ n ∸ m ⊓ n ∎
... | inj₂ n≤m = begin-equality
∣ m - n ∣ ≡⟨ m≤n⇒∣n-m∣≡n∸m n≤m ⟩
m ∸ n ≡⟨ cong₂ _∸_ (m≥n⇒m⊔n≡m n≤m) (m≥n⇒m⊓n≡n n≤m) ⟨
m ⊔ n ∸ m ⊓ n ∎

∣-∣-identityˡ : LeftIdentity 0 ∣_-_∣
∣-∣-identityˡ x = refl

Expand Down