Mercurial > cpdt > repo
comparison src/Equality.v @ 367:b809d3a8a5b1
Pass over old Large material; index fixes
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 08 Nov 2011 11:54:09 -0500 |
parents | 990151eac6af |
children | 549d604c3d16 |
comparison
equal
deleted
inserted
replaced
366:03e200599633 | 367:b809d3a8a5b1 |
---|---|
393 (** %\vspace{-.15in}% [[ | 393 (** %\vspace{-.15in}% [[ |
394 UIP_refl | 394 UIP_refl |
395 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x | 395 : forall (U : Type) (x : U) (p : x = x), p = refl_equal x |
396 ]] | 396 ]] |
397 | 397 |
398 The theorem %\index{Gallina terms!UIF\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an %\textit{%#<i>#axiom#</i>#%}%. *) | 398 The theorem %\index{Gallina terms!UIP\_refl}%[UIP_refl] comes from the [Eqdep] module of the standard library. Do the Coq authors know of some clever trick for building such proofs that we have not seen yet? If they do, they did not use it for this proof. Rather, the proof is based on an %\textit{%#<i>#axiom#</i>#%}%. *) |
399 | 399 |
400 Print eq_rect_eq. | 400 Print eq_rect_eq. |
401 (** %\vspace{-.15in}% [[ | 401 (** %\vspace{-.15in}% [[ |
402 eq_rect_eq = | 402 eq_rect_eq = |
403 fun U : Type => Eq_rect_eq.eq_rect_eq U | 403 fun U : Type => Eq_rect_eq.eq_rect_eq U |
414 x = match h in (_ = y) return (Q y) with | 414 x = match h in (_ = y) return (Q y) with |
415 | eq_refl => x | 415 | eq_refl => x |
416 end | 416 end |
417 ]] | 417 ]] |
418 | 418 |
419 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axiom}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via %``%#"#informal#"#%''% metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC. | 419 Perhaps surprisingly, we cannot prove [eq_rect_eq] from within Coq. This proposition is introduced as an %\index{axioms}%axiom; that is, a proposition asserted as true without proof. We cannot assert just any statement without proof. Adding [False] as an axiom would allow us to prove any proposition, for instance, defeating the point of using a proof assistant. In general, we need to be sure that we never assert %\textit{%#<i>#inconsistent#</i>#%}% sets of axioms. A set of axioms is inconsistent if its conjunction implies [False]. For the case of [eq_rect_eq], consistency has been verified outside of Coq via %``%#"#informal#"#%''% metatheory%~\cite{AxiomK}%, in a study that also established unprovability of the axiom in CIC. |
420 | 420 |
421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) | 421 This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *) |
422 | 422 |
423 Print Streicher_K. | 423 Print Streicher_K. |
424 (* end thide *) | 424 (* end thide *) |