Mercurial > cpdt > repo

comparison src/Equality.v @ 367:b809d3a8a5b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 *)