comparison src/Equality.v @ 121:61e5622b1195

Interconvertibility
author Adam Chlipala <adamc@hcoop.net>
date Sat, 18 Oct 2008 14:55:52 -0400
parents 39c7894b3f7f
children 7cbf0376702f
comparison
equal deleted inserted replaced
120:39c7894b3f7f 121:61e5622b1195
487 487
488 [JMeq] stands for "John Major equality," a name coined by Conor McBride as a sort of pun about British politics. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *) 488 [JMeq] stands for "John Major equality," a name coined by Conor McBride as a sort of pun about British politics. [JMeq] starts out looking a lot like [eq]. The crucial difference is that we may use [JMeq] %\textit{%#<i>#on arguments of different types#</i>#%}%. For instance, a lemma that we failed to establish before is trivial with [JMeq]. It makes for prettier theorem statements to define some syntactic shorthand first. *)
489 489
490 Infix "==" := JMeq (at level 70, no associativity). 490 Infix "==" := JMeq (at level 70, no associativity).
491 491
492 Definition lemma3' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x := 492 Definition UIP_refl' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x :=
493 match pf return (pf == refl_equal _) with 493 match pf return (pf == refl_equal _) with
494 | refl_equal => JMeq_refl _ 494 | refl_equal => JMeq_refl _
495 end. 495 end.
496 496
497 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial. 497 (** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial.
498 498
499 Suppose that we want to use [lemma3'] to establish another lemma of the kind of we have run into several times so far. *) 499 Suppose that we want to use [UIP_refl'] to establish another lemma of the kind of we have run into several times so far. *)
500 500
501 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x), 501 Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x),
502 O = match pf with refl_equal => O end. 502 O = match pf with refl_equal => O end.
503 intros; rewrite (lemma3' pf); reflexivity. 503 intros; rewrite (UIP_refl' pf); reflexivity.
504 Qed. 504 Qed.
505 505
506 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch. The use of [rewrite] is implemented in terms of an axiom: *) 506 (** All in all, refreshingly straightforward, but there really is no such thing as a free lunch. The use of [rewrite] is implemented in terms of an axiom: *)
507 507
508 Check JMeq_eq. 508 Check JMeq_eq.
578 From this point, the goal is trivial. *) 578 From this point, the goal is trivial. *)
579 579
580 intros f f0 H; rewrite H; reflexivity. 580 intros f f0 H; rewrite H; reflexivity.
581 Qed. 581 Qed.
582 End fhapp'. 582 End fhapp'.
583
584
585 (** * Equivalence of Equality Axioms *)
586
587 (** 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.
588
589 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. *)
590
591 Lemma UIP_refl'' : forall (A : Type) (x : A) (pf : x = x), pf = refl_equal x.
592 intros; rewrite (UIP_refl' pf); reflexivity.
593 Qed.
594
595 (** The other direction is perhaps more interesting. Assume that we only have the axiom of the [Eqdep] module available. We can define [JMeq] in a way that satisfies the same interface as the combination of the [JMeq] module's inductive definition and axiom. *)
596
597 Definition JMeq' (A : Type) (x : A) (B : Type) (y : B) : Prop :=
598 exists pf : B = A, x = match pf with refl_equal => y end.
599
600 Infix "===" := JMeq' (at level 70, no associativity).
601
602 (** We say that, by definition, [x] and [y] are equal if and only if there exists a proof [pf] that their types are equal, such that [x] equals the result of casting [y] with [pf]. This statement can look strange from the standpoint of classical math, where we almost never mention proofs explicitly with quantifiers in formulas, but it is perfectly legal Coq code.
603
604 We can easily prove a theorem with the same type as that of the [JMeq_refl] constructor of [JMeq]. *)
605
606 (** remove printing exists *)
607 Theorem JMeq_refl' : forall (A : Type) (x : A), x === x.
608 intros; unfold JMeq'; exists (refl_equal A); reflexivity.
609 Qed.
610
611 (** printing exists $\exists$ *)
612
613 (** The proof of an analogue to [JMeq_eq] is a little more interesting, but most of the action is in appealing to [UIP_refl]. *)
614
615 Theorem JMeq_eq' : forall (A : Type) (x y : A),
616 x === y -> x = y.
617 unfold JMeq'; intros.
618 (** [[
619
620 H : exists pf : A = A,
621 x = match pf in (_ = T) return T with
622 | refl_equal => y
623 end
624 ============================
625 x = y
626 ]] *)
627
628 destruct H.
629 (** [[
630
631 x0 : A = A
632 H : x = match x0 in (_ = T) return T with
633 | refl_equal => y
634 end
635 ============================
636 x = y
637 ]] *)
638
639 rewrite H.
640 (** [[
641
642 x0 : A = A
643 ============================
644 match x0 in (_ = T) return T with
645 | refl_equal => y
646 end = y
647 ]] *)
648
649 rewrite (UIP_refl _ _ x0); reflexivity.
650 Qed.
651
652 (** We see that, in a very formal sense, we are free to switch back and forth between the two styles of proofs about equality proofs. One style may be more convenient than the other for some proofs, but we can always intercovert between our results. The style that does not use heterogeneous equality may be preferable in cases where many results do not require the tricks of this chapter, since then the use of axioms is avoided altogether for the simple cases, and a wider audience will be able to follow those "simple" proofs. On the other hand, heterogeneous equality often makes for shorter and more readable theorem statements. *)