Mercurial > cpdt > repo
comparison src/Universes.v @ 479:40a9a36844d6
Batch of changes based on proofreader feedback
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 28 Nov 2012 19:33:21 -0500 |
| parents | 1fd4109f7b31 |
| children | 31258618ef73 |
comparison
equal
deleted
inserted
replaced
| 478:f02b698aadb1 | 479:40a9a36844d6 |
|---|---|
| 130 ]] | 130 ]] |
| 131 | 131 |
| 132 << | 132 << |
| 133 Error: Illegal application (Type Error): | 133 Error: Illegal application (Type Error): |
| 134 ... | 134 ... |
| 135 The 1st term has type "Type (* (Top.15)+1 *)" which should be coercible to "Set". | 135 The 1st term has type "Type (* (Top.15)+1 *)" |
| 136 which should be coercible to "Set". | |
| 136 >> | 137 >> |
| 137 | 138 |
| 138 The parameter [T] of [id] must be instantiated with a [Set]. The type [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *) | 139 The parameter [T] of [id] must be instantiated with a [Set]. The type [nat] is a [Set], but [Set] is not. We can try fixing the problem by generalizing our definition of [id]. *) |
| 139 | 140 |
| 140 Reset id. | 141 Reset id. |
| 167 | 168 |
| 168 << | 169 << |
| 169 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). | 170 Error: Universe inconsistency (cannot enforce Top.16 < Top.16). |
| 170 >> | 171 >> |
| 171 | 172 |
| 172 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is _predicative_, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, for any object of quantified type, none of those quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves" (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *) | 173 %\index{universe inconsistency}%This error message reminds us that the universe variable for [T] still exists, even though it is usually hidden. To apply [id] to itself, that variable would need to be less than itself in the type hierarchy. Universe inconsistency error messages announce cases like this one where a term could only type-check by violating an implied constraint over universe variables. Such errors demonstrate that [Type] is _predicative_, where this word has a CIC meaning closely related to its usual mathematical meaning. A predicative system enforces the constraint that, when an object is defined using some sort of quantifier, none of the quantifiers may ever be instantiated with the object itself. %\index{impredicativity}%Impredicativity is associated with popular paradoxes in set theory, involving inconsistent constructions like "the set of all sets that do not contain themselves" (%\index{Russell's paradox}%Russell's paradox). Similar paradoxes would result from uncontrolled impredicativity in Coq. *) |
| 173 | 174 |
| 174 | 175 |
| 175 (** ** Inductive Definitions *) | 176 (** ** Inductive Definitions *) |
| 176 | 177 |
| 177 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T]. | 178 (** Predicativity restrictions also apply to inductive definitions. As an example, let us consider a type of expression trees that allows injection of any native Coq value. The idea is that an [exp T] stands for a reflected expression of type [T]. |
| 1107 x = eq_rect p Q x p h | 1108 x = eq_rect p Q x p h |
| 1108 ]] | 1109 ]] |
| 1109 | 1110 |
| 1110 It turns out that this familiar axiom about equality (or some other axiom) is required to deduce [p = p0] from the hypothesis [H3] above. The soundness of that proof step is neither provable nor disprovable in Gallina. | 1111 It turns out that this familiar axiom about equality (or some other axiom) is required to deduce [p = p0] from the hypothesis [H3] above. The soundness of that proof step is neither provable nor disprovable in Gallina. |
| 1111 | 1112 |
| 1112 Hope is not lost, however. We can produce an even stranger looking lemma, which gives us the theorem without axioms. *) | 1113 Hope is not lost, however. We can produce an even stranger looking lemma, which gives us the theorem without axioms. As always when we want to do case analysis on a term with a tricky dependent type, the key is to refactor the theorem statement so that every term we [match] on has _variables_ as its type indices; so instead of talking about proofs of [And p q], we talk about proofs of an arbitrary [r], but we only conclude anything interesting when [r] is an [And]. *) |
| 1113 | 1114 |
| 1114 Lemma proj1_again'' : forall r, proof r | 1115 Lemma proj1_again'' : forall r, proof r |
| 1115 -> match r with | 1116 -> match r with |
| 1116 | And Ps p _ => match Ps return formula Ps -> Prop with | 1117 | And Ps p _ => match Ps return formula Ps -> Prop with |
| 1117 | nil => fun p => proof p | 1118 | nil => fun p => proof p |