[ 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.
There was a problem hiding this comment.
Can you provide an example of an "interesting" proof where this lemma is a useful step?
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
Having pondered this for a while, I'm leaning towards @Taneb 's position more than @JacquesCarette 's.
There was a problem hiding this comment.
Namely, ... TL;DR: Fairbairn threshhold, I think. It's used only once.
|
Monus |
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.
|
@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 I've only now noticed your update regarding |
No, as @JacquesCarette observes, we can handle that as a downstream refactoring. And |
|
@MatthewDaggitt are you happy that your review requests have been answered satisfactorily? |
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.
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.