Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an

"injection" tactic when applied on an equality statement. Moreover,
hypotheses are now entered in the left-to-right order.

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

5 files changed, 87 insertions, 28 deletions

diff --git a/CHANGES b/CHANGES
index 00c59fa166..6e0e434782 100644
--- a/CHANGES
+++ b/CHANGES
@@ -49,7 +49,8 @@ Tactics
 - Now "appcontext" and "context" behave the same. The old buggy behaviour of
   "context" can be retrieved at parse time by setting the
   "Tactic Compat Context" flag. (possible source of incompatibilities).
-
+- Introduction patterns of the form [x1 .. xn] or (x1,..,xn) now apply
+  injection when used on an equality statement ("ssreflect" style)
 
 Program
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b0bcf57d74..16ab1ee5b4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1087,7 +1087,7 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;simpl env sigma c1;t2;simpl env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
+let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e, None,t) env in
   let filter (cpath, t1', t2') =
@@ -1109,7 +1109,7 @@ let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
   tclTHEN
     (tclMAP
       (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
-      injectors)
+      (if l2r then List.rev injectors else injectors))
     (tac (List.length injectors))
 
 exception Not_dep_pair
@@ -1119,7 +1119,7 @@ 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 ipats (eq,_,(t,t1,t2) as u) eq_clause =
+let injEq_then 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
@@ -1167,8 +1167,14 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
         end
         else raise Not_dep_pair
       with e when Errors.noncritical e ->
-	inject_at_positions env sigma u eq_clause posns
-	  (fun _ -> intros_pattern MoveLast ipats)
+	inject_at_positions env sigma l2r u eq_clause posns
+          (tac (clenv_value eq_clause))
+
+let injEq ipats =
+  injEq_then
+    (fun c _ ->
+      tclTHEN (clear_if_overwritten c ipats) (intros_pattern MoveLast ipats))
+    false
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -1179,6 +1185,8 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause [] false None gls
 let injHyp id gls = injClause [] 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 sort = pf_apply get_type_of gls (pf_concl gls) in
   let sigma =  clause.evd in
@@ -1189,7 +1197,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac 0 gls
     | Inr posns ->
-	inject_at_positions env sigma u clause (List.rev posns) ntac gls
+	inject_at_positions env sigma false u clause (List.rev posns) ntac gls
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen ntac)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 44bc4df1f7..2c96ef7e36 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1314,23 +1314,49 @@ let error_unexpected_extra_pattern loc nb pat =
        str (if Int.equal nb 1 then "was" else "were") ++
       strbrk " expected in the branch).")
 
-let intro_or_and_pattern loc b ll l' tac id gl =
-    let c = mkVar id in
-    let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+let adjust_intro_patterns nb ipats =
+  let rec aux n = function
+  | [] when Int.equal n 0 -> []
+  | [] -> (dloc,IntroAnonymous) :: aux (n-1) []
+  | (loc',pat) :: _ when Int.equal n 0 ->
+      error_unexpected_extra_pattern loc' nb pat
+  | ip :: l -> ip :: aux (n-1) l in
+  aux nb ipats
+
+let inj_function = ref (fun _ -> failwith "Not implemented")
+
+let declare_injector f = inj_function := f
+
+let my_find_eq_data_decompose gl t =
+  try find_eq_data_decompose gl t
+  with e when is_anomaly e
+    (* Hack in case equality is not yet defined... one day, maybe,
+       known equalities will be dynamically registered *)
+      -> raise Matching.PatternMatchingFailure
+
+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 rec adjust_names_length nb n = function
-      | [] when Int.equal n 0 or not bracketed -> []
-      | [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) []
-      | (loc',pat) :: _ as l when Int.equal n 0 ->
-	  if bracketed then error_unexpected_extra_pattern loc' nb pat;
-	  l
-      | ip :: l -> ip :: adjust_names_length nb (n-1) 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 ((adjust_names_length n n l)@l'))
+      (Array.map2 (fun n l -> tac thin ((adjust n l)@l'))
 	nv (Array.of_list ll))
       gl
 
@@ -1413,8 +1439,8 @@ let rec intros_patterns b avoid ids thin destopt tac = function
         (fun ids -> intros_patterns b avoid ids thin destopt tac l)
   | (loc, IntroOrAndPattern ll) :: l' ->
       intro_then_force
-	(intro_or_and_pattern loc b ll l'
-	   (intros_patterns b avoid ids thin destopt tac))
+	(intro_or_and_pattern loc b ll 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
@@ -1452,8 +1478,8 @@ let prepare_intros s ipat gl = match ipat with
       id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | IntroOrAndPattern ll -> make_id s gl,
       onLastHypId
-	(intro_or_and_pattern loc true ll []
-	  (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards)))
+	(intro_or_and_pattern loc true ll [] []
+	  (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards)))
   | IntroForthcoming _ -> user_err_loc
       (loc,"",str "Introduction pattern for one hypothesis expected")
 
@@ -1461,18 +1487,23 @@ let ipat_of_name = function
   | Anonymous -> None
   | Name id -> Some (dloc, IntroIdentifier id)
 
-let allow_replace c gl = function (* A rather arbitrary condition... *)
+let allow_replace c = function (* A rather arbitrary condition... *)
   | Some (_, IntroIdentifier id) ->
       let c = fst (decompose_app ((strip_lam_assum c))) in
-      isVar c && Id.equal (destVar c) id
+      if isVar c && Id.equal (destVar c) id then Some id else None
   | _ ->
-      false
+      None
+
+let clear_if_overwritten c ipats =
+  match List.map_filter (fun ipat -> allow_replace c (Some ipat)) ipats with
+  | [id] -> thin [id]
+  | _ -> tclIDTAC
 
 let assert_as first ipat c gl =
   match kind_of_term (pf_hnf_type_of gl c) with
   | Sort s ->
       let id,tac = prepare_intros s ipat gl in
-      let repl = allow_replace c gl ipat in
+      let repl = allow_replace c ipat <> None in
       tclTHENS
 	((if first then internal_cut_gen else internal_cut_rev_gen) repl id c)
 	(if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl
@@ -1486,8 +1517,8 @@ let as_tac id ipat = match ipat with
   | Some (loc,IntroRewrite l2r) ->
       Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
-      intro_or_and_pattern loc true ll []
-        (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards))
+      intro_or_and_pattern loc true ll [] []
+        (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ -> clear_wildcards))
         id
   | Some (loc,
       (IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7c0fee5c78..99d41a4873 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -105,6 +105,12 @@ val onInductionArg :
   (constr with_bindings -> tactic) ->
     constr with_bindings induction_arg -> tactic
 
+(** Complete intro_patterns up to some length; fails if more patterns
+   than required *)
+
+val adjust_intro_patterns : int -> intro_pattern_expr located list ->
+  intro_pattern_expr located list
+
 (** {6 Introduction tactics with eliminations. } *)
 
 val intro_pattern  : Id.t move_location -> intro_pattern_expr -> tactic
@@ -162,6 +168,7 @@ val unfold_constr     : global_reference -> tactic
 val clear         : Id.t list -> tactic
 val clear_body    : Id.t list -> tactic
 val keep          : Id.t list -> tactic
+val clear_if_overwritten : constr -> intro_pattern_expr located list -> tactic
 
 val specialize    : int option -> constr with_bindings -> tactic
 
@@ -390,3 +397,8 @@ val general_multi_rewrite :
 
 val subst_one :
   (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
+
+val declare_injector :
+  ((int -> tactic) -> Coqlib.coq_eq_data * types *
+   (types * constr * constr) ->
+   clausenv -> tactic) -> unit
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index c5cd7380a2..9847e09872 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -66,6 +66,13 @@ einjection (H O).
 instantiate (1:=O).
 Abort.
 
+(* Test the injection intropattern *)
+
+Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
+intros * (H1,H2).
+exact H1.
+Qed.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.