Comments (4)
- 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
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.
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
anddhor
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.
from coq-hott.
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.
from coq-hott.
The reason
DPath
is used for=n
is that it literally is the path type rather than abool
. 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.
from coq-hott.
#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.
from coq-hott.
Related Issues (20)
- Use ViCaR to visualize terms in monoidal categories HOT 3
- dune frequently making full builds HOT 9
- Tensor products of modules
- Add break hints to =, ==, $==, $->
- Add `_ $== _ :> _` notation exposing the underlying type of homs
- Homological algebra lemmas HOT 3
- Spectral sequences HOT 5
- Experiment with redefining bifunctors as uncurried functors
- Work out why test/WildCat/Opposite.v is slow HOT 2
- Remove redundant fields from Ring
- Generalize lhs, lhs_V, rhs and rhs_V to all transitive relations HOT 2
- Define matrices as functions HOT 2
- Define matrices as a collection of columns rather than a collection of rows
- General Linear group HOT 1
- Finite fields (Galois fields)
- Prime numbers
- Idempotent ring elements
- grp_pow and related things
- Tensor product of cyclic groups
- use CongruenceQuotient to define coequalizer
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coq-hott.