-
Notifications
You must be signed in to change notification settings - Fork 193
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.
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
Dependences of Nat/Core.v and DProp.v #1882
Comments
The reason
That sounds like a sensible plan.
That might be wroth using. It's a bit regrettable that
Wouldn't that mean Truncations now depends on DProp?
I wouldn't want to split up DProp as it can already be tricky to find scattered definitions in the library.
Seems like a good idea.
Basics.Nat is a shadow of the Coq prelude rather than somewhere we wanted to put results about nat. But since we treat trunc_index in Basics in a fundamental way, it might be worth putting nat here too. |
Here's a way to define Definition dor (b1 b2 : DProp) : DProp.
Proof.
refine (Build_DProp (hor b1 b2) _ _).
unfold Decidable.
destruct (dec b1) as [d1 | nd1].
- exact (inl (tr (inl d1))).
- destruct (dec b2) as [d2 | nd2].
+ exact (inl (tr (inr d2))).
+ apply inr.
unfold not; apply Trunc_rec.
intros [d1|d2]; [exact (nd1 d1) | exact (nd2 d2)].
Defined. It's unfortunately a lot longer than the one-liner. We'd also need to define |
(You meant
Right, so that wouldn't work. So if we moved |
#1885 addresses the main point here, making Spaces.Nat.Core have reasonable dependencies. We could still think about whether there are ways to reduce the dependencies of DProp and/or move things around. The basic concept of a DProp could go in Basics/Decidable.v, for example. DHProp, on the other hand, needs Trunctype, so it could naturally go there, where other universes of truncated types are defined. |
We currently have some awkward, deep dependencies. For example, Nat/Core.v defines addition of natural numbers, and it depends on DProp.v, which needs Truncations/Core.v and Modalities/ReflectiveSubuniverse.v. ReflectiveSubuniverse.v needs Extensions.v, which needs Colimits/*.v. Truncations/Core.v needs Modalities/Modality.v, which needs some WildCat files and other things. All of that to add natural numbers.
Some options for dealing with this. Some of these are independent and could be combined.
Remove the use of DProp.v in Nat/Core.v. It's only used in one spot as part of the proof that nat is a set.
If that's not easy, then Nat/Core.v could be split into a part that uses DProp.v and a part that doesn't. The part that doesn't could be moved into Basics/Nat.v, so that the basic facts about nat are available there. The part that does could be renamed Nat/NatDec.v, or something like that. If this is done, then Nat/Arithmetic.v probably doesn't need to depend on Nat/NatDec.v, and so it also gets many fewer dependencies.
Maybe the use of ReflectiveSubuniverse.v and Truncation/Core.v can be removed from DProp.v? They are only used for
dor
anddhor
and results about them.dor
anddhor
are easy to prove directly (and I can share the code if needed). Not sure if there is a way to do this without duplicating much.If that's not easy, then the part of DProp.v dealing with
dor
anddhor
could be moved to a new file or put into another file, like Truncation/Core.vIf we move just the definitions of DHProp, DProp, True and False to TruncType.v, then Spaces/Nat/NatDec.v would only need TruncType.v, which has few dependencies. (True and False use things from TruncType.v, so it can't all be put into Basics/Decidable.v, which would be more natural...) However, this splits up a conceptually nice file.
If some of the above cleanup happens, some things that depend on Types could be made to depend on just a few parts. E.g. the current Nat/Core.v only needs Types/Sigma.v and Types/Prod.v, but since its dependencies depend on all of Types, that's not useful yet.
If material is moved to Basics/Nat.v, then some imports of Spaces.Nat or Spaces.Nat.Core could be removed or replaced with imports of Basics.Nat.
The text was updated successfully, but these errors were encountered: