Revising r16550 about providing intro patterns for applying injection:

- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

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

7 files changed, 108 insertions, 89 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 842ce67a0d..20e7f2b2ce 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1134,7 +1134,38 @@ 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 injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
+  (* fetch the informations of the  pair *)
+  let ceq = 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 (eq_constr eqTypeDest (sigTconstr())) &&
+    (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) 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
+      (* cut with the good equality and prove the requested goal *)
+    tclTHENS (cut (mkApp (ceq,new_eq_args)))
+      [tclIDTAC; tclTHEN (apply (
+        mkApp(inj2,
+              [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
+                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
+
+let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
   match find_positions env sigma t1 t2 with
@@ -1147,64 +1178,32 @@ let injEq_then tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
     | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
         errorlabstrm "Equality.inj" (str"Nothing to inject.")
     | Inr posns ->
-(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ?
-	let t1 = try_delta_expand env sigma t1 in
-	let t2 = try_delta_expand env sigma t2 in
-*)
-      try
-(* fetch the informations of the  pair *)
-        let ceq = 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 (eq_constr eqTypeDest (sigTconstr())) &&
-           (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) 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
-          (* cut with the good equality and prove the requested goal *)
-          tclTHENS (cut (mkApp (ceq,new_eq_args)) )
-            [tclIDTAC; tclTHEN (apply (
-              mkApp(inj2,
-                    [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
-                      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
-      with e when Errors.noncritical e ->
-	inject_at_positions env sigma l2r u eq_clause posns
+        try inject_if_homogenous_dependent_pair env sigma u
+        with e when (Errors.noncritical e || e = Not_dep_pair) ->
+        inject_at_positions env sigma l2r u eq_clause posns
           (tac (clenv_value eq_clause))
 
+let postInjEqTac ipats c n =
+  match ipats with
+  | Some ipats ->
+      let clear_tac =
+        if use_injection_pattern_l2r_order () && isVar c
+        then tclTRY (clear [destVar c])
+        else tclIDTAC in
+      let ipats =
+        if use_injection_pattern_l2r_order ()
+        then adjust_intro_patterns n ipats
+        else ipats in
+      tclTHEN
+        (clear_tac)
+        (intros_pattern MoveLast ipats)
+  | None -> tclIDTAC
+
 let injEq ipats =
   let l2r =
     if use_injection_pattern_l2r_order () & ipats <> None then true else false
   in
-  injEq_then
-    (fun c n -> match ipats with
-      | Some ipats ->
-          let clear_tac =
-            if use_injection_pattern_l2r_order () && isVar c
-            then tclTRY (clear [destVar c])
-            else tclIDTAC in
-          let ipats =
-            if use_injection_pattern_l2r_order ()
-            then adjust_intro_patterns n ipats
-            else ipats in
-          tclTHEN
-            (clear_tac)
-            (intros_pattern MoveLast ipats)
-      | None -> tclIDTAC)
-    l2r
+  injEqThen (postInjEqTac ipats) l2r
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -1215,25 +1214,26 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause None false None gls
 let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls
 
-let _ = declare_injector (fun tac -> injEq_then (fun _ -> tac) true)
-
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
+let decompEqThen ntac l2r (lbeq,_,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in
-  let sigma =  clause.evd in
+  let sigma = clause.evd in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
     | Inl (cpath, (_,dirn), _) ->
 	discr_positions env sigma u clause cpath dirn sort gls
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-        ntac 0 gls
+        ntac (clenv_value clause) 0 gls
     | Inr posns ->
-	inject_at_positions env sigma false u clause (List.rev posns) ntac gls
+	inject_at_positions env sigma l2r u clause (List.rev posns)
+          (ntac (clenv_value clause)) gls
 
 let dEqThen with_evars ntac = function
-  | None -> onNegatedEquality with_evars (decompEqThen ntac)
-  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
+  | None -> onNegatedEquality with_evars (decompEqThen ntac false)
+  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac false)) c
+
+let dEq with_evars = dEqThen with_evars (fun c x -> tclIDTAC)
 
-let dEq with_evars = dEqThen with_evars (fun x -> tclIDTAC)
+let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac) true)
 
 let swap_equality_args = function
   | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1413c1b70f..70480d26e7 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -99,7 +99,7 @@ val injHyp       : Id.t -> tactic
 val injConcl     : tactic
 
 val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic
-val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings induction_arg option -> tactic
+val dEqThen : evars_flag -> (constr -> int -> tactic) -> constr with_bindings induction_arg option -> tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b508fb83b6..ed22ab0e18 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -308,7 +308,7 @@ let projectAndApply thin id eqname names depids gls =
     | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2 gls
     | _ -> tac id gls
   in
-  let deq_trailer id neqns =
+  let deq_trailer id _ neqns =
     tclTHENSEQ
       [(if not (List.is_empty names) then clear [id] else tclIDTAC);
        (tclMAP_i neqns (fun idopt ->
@@ -387,6 +387,8 @@ let rec get_names allow_conj (loc,pat) = match pat with
         (Some n, n :: List.map get_name l)
       end else
 	error"Nested conjunctive patterns not allowed for inversion equations."
+  | IntroInjection l ->
+      error "Injection patterns not allowed for inversion equations."
   | IntroOrAndPattern l ->
       error "Disjunctive patterns not allowed for inversion equations."
   | IntroIdentifier id ->
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index dbe8b8dd73..503888c380 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -278,6 +278,8 @@ let intern_message ist = List.map (intern_message_token ist)
 let rec intern_intro_pattern lf ist = function
   | loc, IntroOrAndPattern l ->
       loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l)
+  | loc, IntroInjection l ->
+      loc, IntroInjection (List.map (intern_intro_pattern lf ist) l)
   | loc, IntroIdentifier id ->
       loc, IntroIdentifier (intern_ident lf ist id)
   | loc, IntroFresh id ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a7cfc08e98..08b165b872 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -431,6 +431,8 @@ let rec intropattern_ids (loc,pat) = match pat with
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll ->
       List.flatten (List.map intropattern_ids (List.flatten ll))
+  | IntroInjection l ->
+      List.flatten (List.map intropattern_ids l)
   | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _
   | IntroForthcoming _ -> []
 
@@ -717,6 +719,8 @@ let interp_message ist gl l =
 let rec interp_intro_pattern ist gl = function
   | loc, IntroOrAndPattern l ->
       loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l)
+  | loc, IntroInjection l ->
+      loc, IntroInjection (interp_intro_pattern_list_as_list ist gl l)
   | loc, IntroIdentifier id ->
       loc, interp_intro_pattern_var loc ist (pf_env gl) id
   | loc, IntroFresh id ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cee98b7c54..f357da8178 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1323,9 +1323,9 @@ let adjust_intro_patterns nb ipats =
   | ip :: l -> ip :: aux (n-1) l in
   aux nb ipats
 
-let inj_function = ref (fun _ -> failwith "Not implemented")
+let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented")
 
-let declare_injector f = inj_function := f
+let declare_intro_decomp_eq f = intro_decomp_eq_function := f
 
 let my_find_eq_data_decompose gl t =
   try find_eq_data_decompose gl t
@@ -1334,31 +1334,28 @@ let my_find_eq_data_decompose gl t =
        known equalities will be dynamically registered *)
       -> raise Matching.PatternMatchingFailure
 
+let intro_decomp_eq loc b l l' thin tac id gl =
+  let c = mkVar id in
+  let _,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+  let eq,eq_args = my_find_eq_data_decompose gl t in
+  let eq_clause = make_clenv_binding gl (c,t) NoBindings in
+  !intro_decomp_eq_function
+    (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
+    (eq,t,eq_args) eq_clause gl
+
 let intro_or_and_pattern loc b ll l' thin tac id gl =
   let c = mkVar id in
   let ind,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
-  try
-    (* Use injection if an equality type *)
-    let eq,eq_args = my_find_eq_data_decompose gl t in
-    match fix_empty_or_and_pattern 1 ll with
-    | [l] ->
-        let eq_clause = make_clenv_binding gl (c,t) NoBindings in
-        !inj_function
-          (fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
-          (eq,t,eq_args) eq_clause gl
-    | ll -> check_or_and_pattern_size loc ll 1; assert false
-  with Matching.PatternMatchingFailure ->
-    (* Use "destruct" otherwise *)
-    let nv = mis_constr_nargs ind in
-    let bracketed = b || not (List.is_empty l') in
-    let adjust n l = if bracketed then adjust_intro_patterns n l else l in
-    let ll = fix_empty_or_and_pattern (Array.length nv) ll in
-    check_or_and_pattern_size loc ll (Array.length nv);
-    tclTHENLASTn
-      (tclTHEN (simplest_case c) (clear [id]))
-      (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
-	nv (Array.of_list ll))
-      gl
+  let nv = mis_constr_nargs ind in
+  let bracketed = b || not (List.is_empty l') in
+  let adjust n l = if bracketed then adjust_intro_patterns n l else l in
+  let ll = fix_empty_or_and_pattern (Array.length nv) ll in
+  check_or_and_pattern_size loc ll (Array.length nv);
+  tclTHENLASTn
+    (tclTHEN (simplest_case c) (clear [id]))
+    (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
+       nv (Array.of_list ll))
+    gl
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
@@ -1393,6 +1390,8 @@ let rec explicit_intro_names = function
       | IntroRewrite _ | IntroForthcoming _)) :: l -> explicit_intro_names l
 | (_, IntroOrAndPattern ll) :: l' ->
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
+| (_, IntroInjection l) :: l' ->
+    explicit_intro_names (l@l')
 | [] ->
     []
 
@@ -1441,6 +1440,10 @@ let rec intros_patterns b avoid ids thin destopt tac = function
       intro_then_force
 	(intro_or_and_pattern loc b ll l' thin
 	   (fun thin -> intros_patterns b avoid ids thin destopt tac))
+  | (loc, IntroInjection l) :: l' ->
+      intro_then_force
+	(intro_decomp_eq loc b l l' thin
+	   (fun thin -> intros_patterns b avoid ids thin destopt tac))
   | (loc, IntroRewrite l2r) :: l ->
       intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
 	MoveLast true false
@@ -1480,6 +1483,10 @@ let prepare_intros s ipat gl = match ipat with
       onLastHypId
 	(intro_or_and_pattern loc true ll [] []
 	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards)))
+  | IntroInjection l -> make_id s gl,
+      onLastHypId
+	(intro_decomp_eq loc true l [] []
+	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards)))
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected")
 
@@ -1520,6 +1527,10 @@ let as_tac id ipat = match ipat with
       intro_or_and_pattern loc true ll [] []
         (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards))
         id
+  | Some (loc,IntroInjection l) ->
+      intro_decomp_eq loc true l [] []
+        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards))
+        id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
        IntroWildcard | IntroForthcoming _)) ->
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 99d41a4873..cdc8eb3757 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -398,7 +398,7 @@ val general_multi_rewrite :
 val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
 
-val declare_injector :
+val declare_intro_decomp_eq :
   ((int -> tactic) -> Coqlib.coq_eq_data * types *
    (types * constr * constr) ->
    clausenv -> tactic) -> unit