Coq-HoTT
Coq-HoTT copied to clipboard
HoTT
Natural number arithmetic
We add some theorems of natural number arithmetic involving pred, S, + , -, < and <=. We define a hint database for natural number arithmetic and add some lemmas to it. We define a "left-handed" <= as an inductive type in the other obvious way, namely: n <= n n + 1 <= m -> n <= m and prove it's equivalent to the other one. This is useful for cases where you want to loop from 0 to m, going from bottom to top; if you induct on the normal definition of <= then you will loop from top to bottom.
This looks pretty good to me. Aside from the points I mentioned specifically, I think a better name for the file would be something like
Spaces/Nat/Arithmetic.
Ok, done.
Did you force-push the right thing? Now it looks like the only change in this PR is adding ComplementaryProp.
I'm not really able to review the overall approach here. My comments are mainly minor stylistic issues. (Also, this appears to be WIP. Maybe mark it as "draft" until it is ready for full review?)
Ok, marked as draft for the time being. I would appreciate you continuing to make comments and suggestions anyway, please let me know when you think it is appropriate for it to be ready for full review. I would rather have small parts integrated if they are useful than try to submit a big monolithic chunk of code and discuss it for a long time.
I would rather have small parts integrated if they are useful than try to submit a big monolithic chunk of code and discuss it for a long time.
That's a good idea and would make it easier to review. But in that case, you should separate out the small parts into separate pull requests. For instance, it would probably be appropriate to have separate PRs for the boolean stuff and for the sprop stuff.
Regarding the proof terms of rewrite. Now that we have 8.16 we could start using the generalized rewriting feature of Coq (formerly setoid_rewrite). If we spent some time setting this up we could have nice proof terms when doing rewrites. It would be similar to an attempt at nice rewrite terms by @jdchristensen from a few years ago.
To be clear Coq had support for generalized rewriting for quite a while, what changed in 8.16 was compatibility with universe polymorphism.
@mikeshulman Ok, I got overly excited. SProp and BooleanReflection stuff deleted from the commit so we can just talk about natural number arithmetic stuff, I will open a second PR request soon for the boolean reflection stuff, SProp stuff seems like it might need further discussion.
@SkySkimmer Since we can give the rewrite instances directly, we can fill it with concatenations and aps depending on the form of the term.
@mikeshulman Your original "changes requested" applied to an early draft of this PR before I threw out a bunch of independent things like stuff related to boolean reflection or SPRop. Can you take another look at it and update the changes requested?
I know the stuff in here is minor but I want to get it approved so I can use it in other stuff I'm doing and plan to submit later.