Certified Programming with Dependent Types: src/Universes.v comparison

comparison src/Universes.v @ 437:8077352044b2

A pass over all formatting, after big pile of coqdoc changes

author	Adam Chlipala <adam@chlipala.net>
date	Fri, 27 Jul 2012 16:47:28 -0400
parents	5d5e44f905c7
children	0d66f1a710b8

comparison

equal deleted inserted replaced

-:5d5e44f905c7
+:8077352044b2
 The command outputs many more constraints, but we have collected only those that mention [Top] variables.  We see one constraint for each universe variable associated with a constructor argument from [exp]'s definition.  Universe variable [Top.19] is the type argument to [Eq].  The constraint for [Top.19] effectively says that [Top.19] must be less than [Top.8], the universe of [exp]'s indices; an intermediate variable [Top.9] appears as an artifact of the way the constraint was generated.
 The next constraint, for [Top.15], is more complicated.  This is the universe of the second argument to the [Pair] constructor.  Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38].  What is this new universe variable?  It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
 (* begin hide *)
+(* begin thide *)
 Inductive prod := pair.
 Reset prod.
+(* end thide *)
 (* end hide *)
 (** [[
 Print prod.
 ]]
 match x with
 | exist v _ => v
 end.
 (* begin hide *)
+(* begin thide *)
 Definition projE := O.
+(* end thide *)
 (* end hide *)
 (** We run into trouble with a version that has been changed to work with [ex].
 [[
 Definition projE A (P : A -> Prop) (x : ex P) : A :=
 | [ |- ?pf1 = ?pf2 ] => rewrite (UIP_refl pf1); rewrite (UIP_refl pf2); reflexivity
 end.
 Qed.
 (* begin hide *)
+(* begin thide *)
 Require Eqdep_dec.
+(* end thide *)
 (* end hide *)
 (** These corollaries are special cases of proof irrelevance.  In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
 Another facet of proof irrelevance is that, like excluded middle, it is often provable for specific propositions.  For instance, [UIP] is provable whenever the type [A] has a decidable equality operation.  The module [Eqdep_dec] of the standard library contains a proof.  A similar phenomenon applies to other notable cases, including less-than proofs.  Thus, it is often possible to use proof irrelevance without asserting axioms.
 ]]
 This axiom lets us convert a relational specification [R] into a function implementing that specification.  We need only prove that [R] is truly a function.  An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs.  We also simplify the statement of the theorem by considering only non-dependent function types. *)
 (* begin hide *)
+(* begin thide *)
 Require RelationalChoice.
+(* end thide *)
 (* end hide *)
 Require Import ClassicalChoice.
 Check choice.
 (** %\vspace{-.15in}% [[
 intros; dep_destruct f; eauto.
 Qed.
 (* begin hide *)
 Require Import JMeq.
+(* begin thide *)
 Definition jme := (JMeq, JMeq_eq).
+(* end thide *)
 (* end hide *)
 Print Assumptions fin_cases.
 (** %\vspace{-.15in}%[[
 Axioms:
 It looks like we are almost done.  Hypothesis [H1] gives [p = p0] by injectivity of constructors, and then [H] finishes the case. *)
 injection H1; intros.
 (* begin hide *)
+(* begin thide *)
 Definition existT' := existT.
+(* end thide *)
 (* end hide *)
 (** Unfortunately, the "equality" that we expected between [p] and [p0] comes in a strange form:
 [[

Mercurial > cpdt > repo

comparison src/Universes.v @ 437:8077352044b2