More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).

4 files changed, 91 insertions, 58 deletions

diff --git a/CHANGES b/CHANGES
index 66d5a0e0f..a3c8bf6f0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -102,6 +102,10 @@ Tactics
   independently of the number of ipats, which has itself to be less
   than the number of new hypotheses (possible source of incompatibilities;
   former behavior obtainable by "Unset Injection L2R Pattern Order").
+- Tactic "injection" now automatically simplifies subgoals
+  "existT n p = exists n p'" into "p = p'" when "n" is in an inductive type for
+  which a decidable equality scheme has been generated with "Scheme Equality"
+  (possible source of incompatibilities).
 - New tactic "rewrite_strat" for generalized rewriting with user-defined
   strategies, subsumming autorewrite.
 - Injection can now also deduce equality of arguments of sort Prop, by using
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9873a541a..b79d28138 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2096,14 +2096,13 @@ injection H0.
 Abort.
 \end{coq_eval}
 
-Beware that \texttt{injection} yields always an equality in a sigma type
-whenever the injected object has a dependent type.
-
-\Rem There is a special case for dependent pairs. If we have a decidable
-equality over the type of the first argument, then it is safe to do
-the projection on the second one, and so {\tt injection} will work fine.
-To define such an equality, you have to use the {\tt Scheme} command
-(see \ref{Scheme}).
+Beware that \texttt{injection} yields an equality in a sigma type
+whenever the injected object has a dependent type $P$ with its two
+instances in different types $(P~t_1~...~t_n)$ and
+$(P~u_1~...~u_n)$. If $t_1$ and $u_1$ are the same and have for type
+an inductive type for which a decidable equality has been declared
+using the command {\tt Scheme Equality} (see \ref{Scheme}), the use of
+a sigma type is avoided.
 
 \Rem If some quantified hypothesis of the goal is named {\ident}, then
 {\tt injection {\ident}} first introduces the hypothesis in the local
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 14bdc1786..fcf954668 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1196,6 +1196,49 @@ let try_delta_expand env sigma t =
   hd_rec whdt
 *)
 
+let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
+let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
+
+let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
+
+let inject_if_homogenous_dependent_pair ty =
+  Proofview.Goal.raw_enter begin fun gl ->
+  try
+    let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
+    (* fetch the informations of the  pair *)
+    let ceq = Universes.constr_of_global Coqlib.glob_eq in
+    let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
+    (* check whether the equality deals with dep pairs or not *)
+    let eqTypeDest = fst (decompose_app t) in
+    if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit;
+    let _,ar1 = decompose_app_vect t1 and
+        _,ar2 = decompose_app_vect t2 in
+    let ind,_ = try pf_apply find_mrectype gl ar1.(0) with Not_found -> raise Exit in
+    (* check if the user has declared the dec principle *)
+    (* and compare the fst arguments of the dep pair *)
+    (* Note: should work even if not an inductive type, but the table only *)
+    (* knows inductive types *)
+    if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) &&
+      pf_apply is_conv gl ar1.(2) ar2.(2)) then raise Exit;
+    Library.require_library [Loc.ghost,eqdep_dec] (Some false);
+    let new_eq_args = [|pf_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
+    let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
+      ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
+    (* cut with the good equality and prove the requested goal *)
+    tclTHENLIST
+      [Proofview.tclEFFECTS eff;
+       intro;
+       onLastHyp (fun hyp ->
+        tclTHENS (cut (mkApp (ceq,new_eq_args)))
+          [clear [destVar hyp];
+           Proofview.V82.tactic (refine
+             (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+          ])]
+  with Exit ->
+    Proofview.tclUNIT ()
+  end
+
 (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it
    expands then only when the whdnf has a constructor of an inductive type
    in hd position, otherwise delta expansion is not done *)
@@ -1233,51 +1276,12 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
     Proofview.tclTHEN (Proofview.V82.tclEVARS !evdref)
     (Proofview.tclBIND
       (Proofview.Monad.List.map
-         (fun (pf,ty) -> tclTHENS (cut ty) [Proofview.tclUNIT (); Proofview.V82.tactic (refine pf)])
+         (fun (pf,ty) -> tclTHENS (cut ty)
+           [inject_if_homogenous_dependent_pair ty;
+            Proofview.V82.tactic (refine pf)])
          (if l2r then List.rev injectors else injectors))
       (fun _ -> tac (List.length injectors)))
 
-exception Not_dep_pair
-
-let eq_dec_scheme_kind_name = ref (fun _ -> failwith "eq_dec_scheme undefined")
-let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
-
-let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
-
-let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
-  Proofview.Goal.raw_enter begin fun gl ->
-  (* fetch the informations of the  pair *)
-  let ceq = Universes.constr_of_global Coqlib.glob_eq in
-  let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
-  let eqTypeDest = fst (destApp t) in
-  let _,ar1 = destApp t1 and
-      _,ar2 = destApp t2 in
-  let ind = destInd ar1.(0) in
-	(* check whether the equality deals with dep pairs or not *)
-	(* if yes, check if the user has declared the dec principle *)
-	(* and compare the fst arguments of the dep pair *)
-  let new_eq_args = [|type_of env sigma ar1.(3);ar1.(3);ar2.(3)|] in
-  if (Globnames.is_global (sigTconstr()) eqTypeDest) &&
-    (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind)) &&
-    (is_conv env sigma ar1.(2) ar2.(2))
-  then begin
-    Library.require_library [Loc.ghost,eqdep_dec] (Some false);
-    let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
-      ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
-    let scheme, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in
-      (* cut with the good equality and prove the requested goal *)
-    tclTHENS (tclTHEN (Proofview.tclEFFECTS eff) (cut (mkApp (ceq,new_eq_args))))
-      [tclIDTAC;
-       pf_constr_of_global (ConstRef scheme) (fun c ->
-       tclTHEN (Proofview.V82.tactic (apply (
-        mkApp(inj2,[|ar1.(0);c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
-       ))) (Auto.trivial [] [])
-       )]
-  (* not a dep eq or no decidable type found *)
-  end
-  else raise Not_dep_pair
-  end
-
 let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
@@ -1290,14 +1294,8 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
      Proofview.tclZERO (Errors.UserError ("Equality.inj" , str"Nothing to inject."))
   | Inr posns ->
-     Proofview.tclORELSE
-       (inject_if_homogenous_dependent_pair env sigma u)
-       begin function
-         | Not_dep_pair as e |e when Errors.noncritical e ->
-			       inject_at_positions env sigma l2r u eq_clause posns
-						   (tac (clenv_value eq_clause))
-         | reraise -> Proofview.tclZERO reraise
-       end
+      inject_at_positions env sigma l2r u eq_clause posns
+	(tac (clenv_value eq_clause))
 
 let postInjEqTac ipats c n =
   match ipats with
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 9d5047fdc..6a4882443 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -84,6 +84,38 @@ injection H.
 intro H0. exact H0.
 Abort.
 
+(* Test injection using K, knowing that an equality is decidable *)
+(* Basic case, using sigT, with "as" clause *)
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT *)
+
+Inductive my_sig (A : Type) (P : A -> Type) : Type :=
+    my_exist : forall x : A, P x -> my_sig A P.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  my_exist _ _ n H1 = my_exist _ _ n H2 -> H1 = H2.
+intros.
+injection H as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT deeply nested *)
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  (my_exist _ _ n H1,0) = (my_exist _ _ n H2,0) -> H1 = H2.
+intros * [= H].
+exact H.
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.