Certified Programming with Dependent Types: src/Equality.v comparison

comparison src/Equality.v @ 385:bef6fb896edd

More discussion of axiom avoidance and tactic pitfalls for JMeq

author	Adam Chlipala <adam@chlipala.net>
date	Thu, 12 Apr 2012 12:11:29 -0400
parents	549d604c3d16
children	05efde66559d

comparison

equal deleted inserted replaced

-:eb0fa506d04c
+:bef6fb896edd
 From this point, the goal is trivial. *)
 intros f f0 H; rewrite H; reflexivity.
 Qed.
 (* end thide *)
-End fhapp'.
+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. *)
+(** 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{%#<i>#its type#</i>#%}%.  In other words, the predicate must be %\emph{%#<i>#polymorphic#</i>#%}% 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{%#<i>#some#</i>#%}% 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 #<a href="http://www.mpi-sws.org/~gil/Heq/">#Heq%\footnote{\url{http://www.mpi-sws.org/~gil/Heq/}}%#</a># library builds up a slightly different foundation to help avoid such problems. *)
 (** * Equivalence of Equality Axioms *)
 (* EX: Show that the approaches based on K and JMeq are equivalent logically. *)

Mercurial > cpdt > repo

comparison src/Equality.v @ 385:bef6fb896edd