Fix a bug in the specialization by unification tactic related to the problems

given by injection. Add the example to the test-suite for [dependent
destruction].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11551 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 36 insertions, 4 deletions

diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index d12c21b15..488b057f3 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -102,3 +102,28 @@ Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ;
 
   eapply app with τ...
 Save.
+
+(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
+
+Unset Manual Implicit Arguments.
+
+Inductive Ty :=
+ | Nat : Ty
+ | Prod : Ty -> Ty -> Ty.
+
+Inductive Exp : Ty -> Type :=
+| Const : nat -> Exp Nat
+| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2)
+| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1.
+
+Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
+| EvConst   : forall n, Ev (Const n) (Const n)
+| EvPair    : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2',
+               Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2')
+| EvFst     : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2,
+               Ev e (Pair e1 e2) ->
+               Ev (Fst e) e1.
+
+Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2).
+intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. 
+Qed.
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 4dd72b84d..6a5eafe8b 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -325,18 +325,23 @@ Proof. intros; assumption. Defined.
 Lemma simplification_heq : Π A B (x y : A), (x = y -> B) -> (JMeq x y -> B).
 Proof. intros; apply X; apply (JMeq_eq H). Defined.
 
-Lemma simplification_existT : Π A (P : A -> Type) B  (p : A) (x y : P p),
+Lemma simplification_existT2 : Π A (P : A -> Type) B (p : A) (x y : P p),
   (x = y -> B) -> (existT P p x = existT P p y -> B).
 Proof. intros. apply X. apply inj_pair2. exact H. Defined.
 
+Lemma simplification_existT1 : Π A (P : A -> Type) B (p q : A) (x : P p) (y : P q),
+  (p = q -> existT P p x = existT P q y -> B) -> (existT P p x = existT P q y -> B).
+Proof. intros. injection H. intros ; auto. Defined.
+  
 Lemma simplification_K : Π A (x : A) (B : x = x -> Type), B (refl_equal x) -> (Π p : x = x, B p).
 Proof. intros. rewrite (UIP_refl A). assumption. Defined.
 
 (** This hint database and the following tactic can be used with [autosimpl] to 
    unfold everything to [eq_rect]s. *)
 
-Hint Unfold solution_left solution_right deletion simplification_heq simplification_existT : equations.
-Hint Unfold eq_rect_r eq_rec eq_ind : equations.
+Hint Unfold solution_left solution_right deletion simplification_heq
+  simplification_existT1 simplification_existT2
+  eq_rect_r eq_rec eq_ind : equations.
 
 (** Simply unfold as much as possible. *)
 
@@ -361,7 +366,9 @@ Ltac simplify_one_dep_elim_term c :=
   match c with
     | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
     | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _)
-    | eq (existT _ _ _) (existT _ _ _) -> _ => refine (simplification_existT _ _ _ _ _ _ _)
+    | eq (existT _ _ _) (existT _ _ _) -> _ => 
+      refine (simplification_existT2 _ _ _ _ _ _ _) ||
+        refine (simplification_existT1 _ _ _ _ _ _ _ _)
     | ?x = ?y -> _ => (* variables case *)
       (let hyp := fresh in intros hyp ;
         move hyp before x ;