Mercurial > cpdt > repo
changeset 120:39c7894b3f7f
JMeq
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 18 Oct 2008 14:24:11 -0400 |
parents | 8df59f0b3dc0 |
children | 61e5622b1195 |
files | src/Equality.v |
diffstat | 1 files changed, 111 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Equality.v Sat Oct 18 13:52:09 2008 -0400 +++ b/src/Equality.v Sat Oct 18 14:24:11 2008 -0400 @@ -8,7 +8,7 @@ *) (* begin hide *) -Require Import Eqdep List. +Require Import Eqdep JMeq List. Require Import Tactics. @@ -470,3 +470,113 @@ reflexivity. Qed. End fhapp. + +Implicit Arguments fhapp [A B ls1 ls2]. + + +(** * Heterogeneous Equality *) + +(** There is another equality predicate, defined in the [JMeq] module of the standard library, implementing %\textit{%#<i>#heterogeneous equality#</i>#%}%. *) + +Print JMeq. +(** [[ + +Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop := + JMeq_refl : JMeq x x + ]] + +[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. *) + +Infix "==" := JMeq (at level 70, no associativity). + +Definition lemma3' (A : Type) (x : A) (pf : x = x) : pf == refl_equal x := + match pf return (pf == refl_equal _) with + | refl_equal => JMeq_refl _ + end. + +(** There is no quick way to write such a proof by tactics, but the underlying proof term that we want is trivial. + + Suppose that we want to use [lemma3'] to establish another lemma of the kind of we have run into several times so far. *) + +Lemma lemma4 : forall (A : Type) (x : A) (pf : x = x), + O = match pf with refl_equal => O end. + intros; rewrite (lemma3' pf); reflexivity. +Qed. + +(** 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: *) + +Check JMeq_eq. +(** [[ + +JMeq_eq + : forall (A : Type) (x y : A), x == y -> x = y + ]] *) + +(** It may be surprising that we cannot prove that heterogeneous equality implies normal equality. The difficulties are the same kind we have seen so far, based on limitations of [match] annotations. + + We can redo our [fhapp] associativity proof based around [JMeq]. *) + +Section fhapp'. + Variable A : Type. + Variable B : A -> Type. + + (** This time, the naive theorem statement type-checks. *) + + Theorem fhapp_ass' : forall ls1 ls2 ls3 + (hls1 : fhlist B ls1) (hls2 : fhlist B ls2) (hls3 : fhlist B ls3), + fhapp hls1 (fhapp hls2 hls3) == fhapp (fhapp hls1 hls2) hls3. + induction ls1; crush. + + (** Even better, [crush] discharges the first subgoal automatically. The second subgoal is: + + [[ + + ============================ + (a0, + fhapp (B:=B) (ls1:=ls1) (ls2:=ls2 ++ ls3) b + (fhapp (B:=B) (ls1:=ls2) (ls2:=ls3) hls2 hls3)) == + (a0, + fhapp (B:=B) (ls1:=ls1 ++ ls2) (ls2:=ls3) + (fhapp (B:=B) (ls1:=ls1) (ls2:=ls2) b hls2) hls3) + ]] + + It looks like one rewrite with the inductive hypothesis should be enough to make the goal trivial. + + [[ + + rewrite IHls1. + + [[ + +Error: Impossible to unify "fhlist B ((ls1 ++ ?1572) ++ ?1573)" with + "fhlist B (ls1 ++ ?1572 ++ ?1573)" + ]] + + We see that [JMeq] is not a silver bullet. We can use it to simplify the statements of equality facts, but the Coq type-checker uses non-trivial heterogeneous equality facts no more readily than it uses standard equality facts. Here, the problem is that the form [(e1, e2)] is syntactic sugar for an explicit application of a constructor of an inductive type. That application mentions the type of each tuple element explicitly, and our [rewrite] tries to change one of those elements without updating the corresponding type argument. + + We can get around this problem by another multiple use of [generalize]. We want to bring into the goal the proper instance of the inductive hypothesis, and we also want to generalize the two relevant uses of [fhapp]. *) + + generalize (fhapp b (fhapp hls2 hls3)) + (fhapp (fhapp b hls2) hls3) + (IHls1 _ _ b hls2 hls3). + (** [[ + + ============================ + forall (f : fhlist B (ls1 ++ ls2 ++ ls3)) + (f0 : fhlist B ((ls1 ++ ls2) ++ ls3)), f == f0 -> (a0, f) == (a0, f0) + ]] + + Now we can rewrite with append associativity, as before. *) + + rewrite app_ass. + (** [[ + + ============================ + forall f f0 : fhlist B (ls1 ++ ls2 ++ ls3), f == f0 -> (a0, f) == (a0, f0) + ]] + + From this point, the goal is trivial. *) + + intros f f0 H; rewrite H; reflexivity. + Qed. +End fhapp'.