[ add ] Nat lemmas with _∸_, _⊔_ and _⊓_#2924
Conversation
MatthewDaggitt
left a comment
MatthewDaggitt
left a comment
There was a problem hiding this comment.
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?
| ------------------------------------------------------------------------ | ||
| -- Properties of _∸_ and _⊓_ and _⊔_ | ||
|
|
||
| m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n |
There was a problem hiding this comment.
This property doesn't feel natural to me, and the definition is short enough I don't really think it needs a name
There was a problem hiding this comment.
It looks kind of similar to the m⊔n≤m+n that is already here.
There was a problem hiding this comment.
I'm okay - lets one do proofs at a higher level with fewer steps.
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.
|
Monus |
| ∣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 |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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
There was a problem hiding this comment.
@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...
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
I'm fine with adding these. We can have later passes of simplification of proofs.
| ------------------------------------------------------------------------ | ||
| -- Properties of _∸_ and _⊓_ and _⊔_ | ||
|
|
||
| m∸n≤m⊔n : ∀ m n → m ∸ n ≤ m ⊔ n |
There was a problem hiding this comment.
I'm okay - lets one do proofs at a higher level with fewer steps.
5 participants
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.