# HG changeset patch # User Adam Chlipala # Date 1334247089 14400 # Node ID bef6fb896eddcbb9746e471ce916f45124d1ae0c # Parent eb0fa506d04c03346f10bada9314ea47b9696fb1 More discussion of axiom avoidance and tactic pitfalls for JMeq diff -r eb0fa506d04c -r bef6fb896edd src/Equality.v --- a/src/Equality.v Sun Apr 08 11:11:27 2012 -0400 +++ b/src/Equality.v Thu Apr 12 12:11:29 2012 -0400 @@ -739,9 +739,118 @@ intros f f0 H; rewrite H; reflexivity. Qed. (* end thide *) -End fhapp'. -(** This example illustrates a general pattern: heterogeneous equality often simplifies theorem statements, but we still need to do some work to line up some dependent pattern matches that tactics will generate for us. *) +End fhapp'. + +(** This example illustrates a general pattern: heterogeneous equality often simplifies theorem statements, but we still need to do some work to line up some dependent pattern matches that tactics will generate for us. + + The proof we have found relies on the [JMeq_eq] axiom, which we can verify with a command%\index{Vernacular commands!Print Assumptions}% that we will discuss more in two chapters. *) + +Print Assumptions fhapp_ass'. +(** %\vspace{-.15in}%[[ +Axioms: +JMeq_eq : forall (A : Type) (x y : A), x == y -> x = y +]] + +It was the [rewrite H] tactic that implicitly appealed to the axiom. By restructuring the proof, we can avoid axiom dependence. A general lemma about pairs provides the key element. (Our use of [generalize] above can be thought of as reducing the proof to another, more complex and specialized lemma.) *) + +Lemma pair_cong : forall A1 A2 B1 B2 (x1 : A1) (x2 : A2) (y1 : B1) (y2 : B2), + x1 == x2 + -> y1 == y2 + -> (x1, y1) == (x2, y2). + intros until y2; intros Hx Hy; rewrite Hx; rewrite Hy; reflexivity. +Qed. + +Hint Resolve pair_cong. + +Section fhapp''. + Variable A : Type. + Variable B : A -> Type. + + 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. + Qed. +End fhapp''. + +Print Assumptions fhapp_ass''. +(** << +Closed under the global context +>> + +One might wonder exactly which elements of a proof involving [JMeq] imply that [JMeq_eq] must be used. For instance, above we noticed that [rewrite] had brought [JMeq_eq] into the proof of [fhap_ass'], yet here we have also used [rewrite] with [JMeq] hypotheses while avoiding axioms! One illuminating exercise is comparing the types of the lemmas that [rewrite] uses under the hood to implement the rewrites. Here is the normal lemma for [eq] rewriting:%\index{Gallina terms!eq\_ind\_r}% *) + +Check eq_ind_r. +(** %\vspace{-.15in}%[[ +eq_ind_r + : forall (A : Type) (x : A) (P : A -> Prop), + P x -> forall y : A, y = x -> P y +]] + +The corresponding lemma used for [JMeq] in the proof of [pair_cong] is %\index{Gallina terms!JMeq\_rew\_r}%[JMeq_rew_r], which, confusingly, is defined by [rewrite] as needed, so it is not available for checking until after we apply it. *) + +Check JMeq_rew_r. +(** %\vspace{-.15in}%[[ +JMeq_rew_r + : forall (A : Type) (x : A) (B : Type) (b : B) + (P : forall B0 : Type, B0 -> Type), P B b -> x == b -> P A x +]] + +The key difference is that, where the [eq] lemma is parametrized on a predicate of type [A -> Prop], the [JMeq] lemma is parameterized on a predicate of type more like [forall A : Type, A -> Prop]. To apply [eq_ind_r] with a proof of [x = y], it is only necessary to rearrange the goal into an application of a [fun] abstraction to [y]. In contrast, to apply [JMeq_rew_r], it is necessary to rearrange the goal to an application of a [fun] abstraction to both [y] and %\emph{%##its type##%}%. In other words, the predicate must be %\emph{%##polymorphic##%}% in [y]'s type; any type must make sense, from a type-checking standpoint. There may be cases where the former rearrangement is easy to do in a type-correct way, but the second rearrangement done naively leads to a type error. + +When [rewrite] cannot figure out how to apply [JMeq_rew_r] for [x == y] where [x] and [y] have the same type, the tactic can instead use an alternate theorem, which is easy to prove as a composition of [eq_ind_r] and [JMeq_eq]. *) + +Check JMeq_ind_r. +(** %\vspace{-.15in}%[[ +JMeq_ind_r + : forall (A : Type) (x : A) (P : A -> Prop), + P x -> forall y : A, y == x -> P y +]] + +Ironically, where in the proof of [fhapp_ass'] we used [rewrite app_ass] to make it clear that a use of [JMeq] was actually homogeneously typed, we created a situation where [rewrite] applied the axiom-based [JMeq_ind_r] instead of the axiom-free [JMeq_rew_r]! + +For another simple example, consider this theorem that applies a heterogeneous equality to prove a congruence fact. *) + +Theorem out_of_luck : forall n m : nat, + n == m + -> S n == S m. + intros n m H. + + (** Applying [JMeq_ind_r] is easy, as the %\index{tactics!pattern}%[pattern] tactic will transform the goal into an application of an appropriate [fun] to a term that we want to abstract. *) + + pattern n. + (** %\vspace{-.15in}%[[ + n : nat + m : nat + H : n == m + ============================ + (fun n0 : nat => S n0 == S m) n +]] +*) + apply JMeq_ind_r with (x := m); auto. + + (** However, we run into trouble trying to get the goal into a form compatible with [JMeq_rew_r.] *) + Undo 2. +(** %\vspace{-.15in}%[[ + pattern nat, n. +]] +<< +Error: The abstracted term "fun (P : Set) (n0 : P) => S n0 == S m" +is not well typed. +Illegal application (Type Error): +The term "S" of type "nat -> nat" +cannot be applied to the term + "n0" : "P" +This term has type "P" which should be coercible to +"nat". +>> + +In other words, the successor function [S] is insufficiently polymorphic. If we try to generalize over the type of [n], we find that [S] is no longer legal to apply to [n]. *) + +Abort. + +(** Why did we not run into this problem in our proof of [fhapp_ass'']? The reason is that the pair constructor is polymorphic in the types of the pair components, while functions like [S] are not polymorphic at all. Use of such non-polymorphic functions with [JMeq] tends to push toward use of axioms. The example with [nat] here is a bit unrealistic; more likely cases would involve functions that have %\emph{%##some##%}% polymorphism, but not enough to allow abstractions of the sort we attempted above with [pattern]. For instance, we might have an equality between two lists, where the goal only type-checks when the terms involved really are lists, though everything is polymorphic in the types of list data elements. The ##Heq%\footnote{\url{http://www.mpi-sws.org/~gil/Heq/}}%## library builds up a slightly different foundation to help avoid such problems. *) (** * Equivalence of Equality Axioms *)