Nat: direct proof of Dec Paths; move equiv_path_nat to Nat/Paths.v

[jdchristensen]

It turns out to be very easy to prove that nat has decidable equality without using DProp.v, and that is done in this PR. I moved the characterization of the path types as DHProps to Nat/Paths.v, but I'm not sure if we should keep this. It is a result from the HoTT book, which is mentioned in HoTTBook.v, so for now I have left it here.

This addresses the main point of #1882.

Nat/Core.v and Nat/Arithmetic.v use almost all of the files in Basics, as well as Types.Sigma for one use of path_sigma_hprop. So this prevents us from moving the whole thing into Basics. We could:

• Leave it all in Spaces/Nat/
• Move Nat/Core.v to Types/Nat.v, since it plays a similar role to other files there. The other two files could move or stay.
• Move Nat/Core.v, except for the leq material that uses Types.Sigma, to Basics/Nat.v, and move the leq material into Spaces/Nat/Arithmetic.v

Thoughts?

[jdchristensen]

I also removed the use of DProp in Fin.v. All that was used was the definition of the record, which could be in Basics/Decidable.v, for example.

[Alizter]

I'm in favour of moving most of the Nat stuff to Basics. I think the non-trivial stuff in Arithmetic will eventually consist of things about primes etc. rather than lemmas just about leq.

[Alizter]

I'm also in favour of keeping the DProp version of paths as it is in the book. We could put it in Meta or elsewhere.

[jdchristensen]

@Alizter Do you mean that you like the third choice I mentioned:

Move Nat/Core.v, except for the leq material that uses Types.Sigma, to Basics/Nat.v, and move the leq material into Spaces/Nat/Arithmetic.v

This would leave the Arithmetic.v file in Spaces/Nat/, which seems like a slightly odd place for work on arithmetic, but I can't think of a better place. This plan also means that there is a somewhat arbitrary split between the material on nat across two different folders.

Another idea is that if we can get rid of the use of path_sigma_hprop, then both Nat/Core.v and Nat/Arithmetic.v could go into Basics. Not sure how feasible that is.

Yet another idea is to have a folder Types/Nat/ and put Core.v and Arithmetic.v in there.

[Alizter]

FTR I don't like the idea of introducing more stuff into Types. But I need to think further about how we can best organize stuff about nat.

[jdchristensen]

I definitely think the material about leq should move from Nat/Core.v to Nat/Arithmetic.v. There are already lots of results about leq, geq, etc, in Arithmetic.v. And this would mean that many things about nat, including addition, multiplication, that it has decidable equality, nat_iter, etc would all only depend on a few files in Basics. So I'll go ahead and move this material, unless there is an objection.

As to where the files should go, I'm still not sure. Maybe leaving it all in Spaces/Nat is fine, where Spaces/Pos and Spaces/Int are also located. Or moving Nat/Core.v into Basics/Nat.v, still leaving the rest in Spaces/Nat.

There's another point, that the material currently in Basics/Nat.v is technical. Is it really needed? I'm guessing the material on decimal conversion is needed for parsing and printing, but what about hexadecimal conversion?

[Alizter]

@jdchristensen That sounds good to me. Spaces/Nat for now seems like the best place, we can defer a major relocation to the future if we feel like it.

The stuff about datatypes in Basics, basically any file with a Coq header, is all from the Coq prelude extracted out. Coq expects certain datatypes to be present in order to do printing and parsing. We don't use hexidecimal notations in the library, so it is more of a programming language artefact. I think they are harmless to have around.

I think we should clearly demarcate the technical parts of those files and say they are about datastructures that Coq expects for printing and parsing and users shouldn't look into it much. That way you can add in the stuff about Nat later.

[jdchristensen]

I decided to just move equiv_leq_add from Core.v to Arithmetic.v, since some files that import only Core.v use some of the other results there. (equiv_leq_add is never used, but does seem worth having.) Then, in the second new commit, I use some of the results in Arithmetic.v to simplify the proof of equiv_leq_add, and also avoid the use of Types.Sigma. So now, both Core.v and Arithmetic.v only depend on Basics, while Nat/Paths.v is the outlier that depends on a ton of stuff. In the third new commit, I add a comment about dependencies.

[jdchristensen]

The one build fail was a network fail, so I think this is good to merge when the doc jobs finish.