Dependences of Nat/Core.v and DProp.v

[jdchristensen]

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 and dhor and results about them. dor and dhor 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 and dhor could be moved to a new file or put into another file, like Truncation/Core.v

• If 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.

[Alizter]

• 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.

The reason DPath is used for =n is that it literally is the path type rather than a bool. I think this is something nice that we would still like to keep, so I don't think we should remove it.

• 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.

That sounds like a sensible plan.

• Maybe the use of ReflectiveSubuniverse.v and Truncation/Core.v can be removed from DProp.v? They are only used for dor and dhor and results about them. dor and dhor 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.

That might be wroth using. It's a bit regrettable that hor is so heavy to use because of Truncations.Core, but I think simplifying dependencies here will be useful. What are the direct proofs of dor and dhor?

• If that's not easy, then the part of DProp.v dealing with dor and dhor could be moved to a new file or put into another file, like Truncation/Core.v

Wouldn't that mean Truncations now depends on DProp?

• If 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.

I wouldn't want to split up DProp as it can already be tricky to find scattered definitions in the library.

• 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.

Seems like a good idea.

• 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.

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.

[jdchristensen]

Here's a way to define dor without dependencies:

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 dhor. And then there are three lemmas about each of them. Not sure if there is a way to prove something more general here that would make this a one-liner again.

[jdchristensen]

The reason DPath is used for =n is that it literally is the path type rather than a bool. I think this is something nice that we would still like to keep, so I don't think we should remove it.

(You meant DHProp.)

DHProp is used in the current proof, but I imagine we could just give a direct proof of DecidablePaths nat, similar to the proof of DecideablePaths Pos in Pos/Core.v, without introducing =n.

Wouldn't that mean Truncations now depends on DProp?

Right, so that wouldn't work. So if we moved dor and dhor, we might need a new file, which would add clutter.

[jdchristensen]

#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.