Mercurial > cpdt > repo

comparison src/Equality.v @ 272:19fbda8a8117

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fix in Equality, found proof-reading tutorial
author Adam Chlipala <adamc@hcoop.net>
date Wed, 28 Apr 2010 11:40:03 -0400
parents aa3c054afce0
children bd7f8720a691
comparison
equal deleted inserted replaced
271:aa3c054afce0 272:19fbda8a8117
667 (** * Equivalence of Equality Axioms *) 667 (** * Equivalence of Equality Axioms *)
668 668
669 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *) 669 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)
670 670
671 (* begin thide *) 671 (* begin thide *)
672 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business. The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together. It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof. In this section, we demonstrate this by showing how each the previous two sections' approaches reduces to the other logically. 672 (** Assuming axioms (like axiom K and [JMeq_eq]) is a hazardous business. The due diligence associated with it is necessarily global in scope, since two axioms may be consistent alone but inconsistent together. It turns out that all of the major axioms proposed for reasoning about equality in Coq are logically equivalent, so that we only need to pick one to assert without proof. In this section, we demonstrate this by showing how each of the previous two sections' approaches reduces to the other logically.
673 673
674 To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section. The rest of the proof is trivial. *) 674 To show that [JMeq] and its axiom let us prove [UIP_refl], we start from the lemma [UIP_refl'] from the previous section. The rest of the proof is trivial. *)
675 675
676 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x. 676 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
677 intros; rewrite (UIP_refl' pf); reflexivity. 677 intros; rewrite (UIP_refl' pf); reflexivity.