Quelques améliorations des intro patterns:

- ajout de -> et <- pour substitution immédiate d'une égalité 
  (comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
  cas "[[|] H]" (cf CHANGES)

Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?





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

10 files changed, 84 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index ed4f1fa6e2..704a1d5e34 100644
--- a/CHANGES
+++ b/CHANGES
@@ -66,7 +66,8 @@ Libraries
   statement in "sigT" (including the completeness axiom) are now in "sig" (in
   case of incompatibility, use sigT_of_sig or sig_of_sigT), identifiers in 
   French moved to English, useless hypothesis of ln_exists1 dropped, new
-  Rlogic.v states a few logical properties about R axioms.
+  Rlogic.v states a few logical properties about R axioms; RIneq.v made more
+  uniform.
 - Slight restructuration of the Logic library regarding choice and classical
   logic. Addition of files providing intuitionistic axiomatizations of
   descriptions: Epsilon.v, Description.v and IndefiniteDescription.v
@@ -345,6 +346,13 @@ Tactics
 - Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses.
 - New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns.
 - New introduction pattern "?" for letting Coq choose a name.
+- Introduction patterns now support side hypotheses (e.g. intros [|] on 
+  "(nat -> nat) -> nat" works).
+- New introduction patterns "->" and "<-" for immediate rewriting of
+  introduced hypotheses.
+- Introduction patterns coming after non trivial introduction patterns now
+  force full introduction of the first pattern (e.g. "intros [[|] p]" on
+  "nat->nat->nat" now behaves like "intros [[|?] p]")
 - Added "eassumption".
 - Added option 'using lemmas' to auto, trivial and eauto.
 - Tactic "congruence" is now complete for its intended scope (ground
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index f442bf75ff..63efd543aa 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -633,6 +633,7 @@ let rec xlate_intro_pattern =
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
   | IntroFresh _ -> xlate_error "TODO: IntroFresh"
+  | IntroRewrite _ -> xlate_error "TODO: IntroRewrite"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
diff --git a/interp/genarg.ml b/interp/genarg.ml
index fc93f455a2..ac45bfe8dd 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -79,6 +79,7 @@ type intro_pattern_expr =
   | IntroWildcard
   | IntroIdentifier of identifier
   | IntroAnonymous
+  | IntroRewrite of bool
   | IntroFresh of identifier
 and case_intro_pattern_expr = intro_pattern_expr list list
 
@@ -87,6 +88,8 @@ let rec pr_intro_pattern = function
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
   | IntroAnonymous -> str "?"
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
   | IntroFresh id -> str "?" ++ pr_id id
 
 and pr_case_intro_pattern = function
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 0df4e66a01..9773082181 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -36,6 +36,7 @@ type intro_pattern_expr =
   | IntroWildcard
   | IntroIdentifier of identifier
   | IntroAnonymous
+  | IntroRewrite of bool
   | IntroFresh of identifier
 and case_intro_pattern_expr = intro_pattern_expr list list
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 64062765a0..5e50e9859d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -193,6 +193,8 @@ GEXTEND Gram
       | prefix = pattern_ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
+      | "->" -> IntroRewrite true
+      | "<-" -> IntroRewrite false
       ] ]
   ;
   simple_binding:
@@ -268,14 +270,15 @@ GEXTEND Gram
   ;
   clause:
     [ [ "in"; "*"; occs=occurrences ->
-        {onhyps=None;onconcl=true;concl_occs=occs}
+          {onhyps=None; onconcl=true; concl_occs=occs}
       | "in"; "*"; "|-"; (b,occs)=concl_occ ->
           {onhyps=None; onconcl=b; concl_occs=occs}
       | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ ->
           {onhyps=Some hl; onconcl=b; concl_occs=occs}
       | "in"; hl=LIST0 hypident_occ SEP"," ->
           {onhyps=Some hl; onconcl=false; concl_occs=[]}
-      | -> {onhyps=Some[];onconcl=true; concl_occs=[]} ] ]
+      | ->
+	  {onhyps=Some[]; onconcl=true; concl_occs=[]} ] ]
   ;
   concl_occ:
     [ [ "*"; occs = occurrences -> (true,occs)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 214389f18f..60acd90925 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1302,3 +1302,4 @@ let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp)
 
 let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl ->  replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl)
 let _ = Setoid_replace.register_general_rewrite general_rewrite
+let _ = Tactics.register_general_multi_rewrite general_multi_rewrite
diff --git a/tactics/inv.ml b/tactics/inv.ml
index baa77f9c4b..55b8d08c6a 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -382,6 +382,8 @@ let rec get_names allow_conj = function
       error "Anonymous pattern not allowed for inversion equations"
   | IntroFresh _->
       error "Fresh pattern not allowed for inversion equations"
+  | IntroRewrite _->
+      error "Rewriting pattern not allowed for inversion equations"
   | IntroOrAndPattern [l] -> 
       if allow_conj then
 	if l = [] then (None,[]) else
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 719307b116..9a2c2097c6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -445,7 +445,7 @@ let rec intern_intro_pattern lf ist = function
       IntroOrAndPattern (intern_case_intro_pattern lf ist l)
   | IntroIdentifier id ->
       IntroIdentifier (intern_ident lf ist id)
-  | IntroWildcard | IntroAnonymous | IntroFresh _ as x -> x
+  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
 
 and intern_case_intro_pattern lf ist =
   List.map (List.map (intern_intro_pattern lf ist))
@@ -1254,7 +1254,7 @@ let rec intropattern_ids = function
   | IntroIdentifier id -> [id]
   | IntroOrAndPattern ll -> 
       List.flatten (List.map intropattern_ids (List.flatten ll))
-  | IntroWildcard | IntroAnonymous | IntroFresh _ -> []
+  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ -> []
 
 let rec extract_ids ids = function
   | (id,VIntroPattern ipat)::tl when not (List.mem id ids) ->
@@ -1493,7 +1493,7 @@ let rec interp_message_nl ist = function
 let rec interp_intro_pattern ist gl = function
   | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l)
   | IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id
-  | IntroWildcard | IntroAnonymous | IntroFresh _ as x -> x
+  | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x
 
 and interp_case_intro_pattern ist gl =
   List.map (List.map (interp_intro_pattern ist gl))
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 08eddef96c..3a2ec3705e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -966,15 +966,54 @@ let simplest_case c = general_case_analysis false (c,NoBindings)
 (* Decomposing introductions *)
 (*****************************)
 
+let forward_general_multi_rewrite =
+  ref (fun _ -> failwith "general_multi_rewrite undefined")
+
+let register_general_multi_rewrite f =
+  forward_general_multi_rewrite := f
+
 let clear_last = tclLAST_HYP (fun c -> (clear [destVar c]))
 let case_last  = tclLAST_HYP simplest_case
 
+let fix_empty_case nv l =
+  (* The syntax does not distinguish between "[ ]" for one clause with no names
+     and "[ ]" for no clause at all; so we are a bit liberal here *)
+  if Array.length nv = 0 & l = [[]] then [] else l
+
+let intro_or_and_pattern ll l' tac =
+  tclLAST_HYP (fun c gl ->
+    let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+    let nv = mis_constr_nargs ind in
+    let rec adjust_names_length force n = function
+      | [] when n = 0 or not force -> []
+      | [] -> IntroAnonymous :: adjust_names_length force (n-1) []
+      | _ :: _ when n = 0 -> error "Too many names in some branch"
+      | ip :: l -> ip :: adjust_names_length force (n-1) l in
+    let ll = fix_empty_case nv ll in
+    if List.length ll <> Array.length nv then
+      error "Not the right number of patterns";
+    tclTHENLASTn
+      (tclTHEN case_last clear_last)
+      (array_map2 (fun n l -> tac ((adjust_names_length (l'<>[]) n l)@l'))
+	nv (Array.of_list ll))
+      gl)
+
+let clear_if_atomic l2r id gl =
+  let eq = pf_type_of gl (mkVar id) in
+  let (_,lhs,rhs) = snd (find_eq_data_decompose eq) in
+  if l2r & isVar lhs then tclTRY (clear [destVar lhs;id]) gl
+  else if not l2r & isVar rhs then tclTRY (clear [destVar rhs;id]) gl
+  else tclIDTAC gl
+
 let rec explicit_intro_names = function
-| (IntroWildcard | IntroAnonymous | IntroFresh _) :: l -> explicit_intro_names l
-| IntroIdentifier id :: l -> id :: explicit_intro_names l
+| IntroIdentifier id :: l ->
+    id :: explicit_intro_names l
+| (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l ->
+    explicit_intro_names l
 | IntroOrAndPattern ll :: l' -> 
     List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll)
-| [] -> []
+| [] ->
+    []
 
   (* We delay thinning until the completion of the whole intros tactic
      to ensure that dependent hypotheses are cleared in the right
@@ -1003,9 +1042,16 @@ let rec intros_patterns avoid thin destopt = function
   | IntroOrAndPattern ll :: l' ->
       tclTHEN
         introf
-        (tclTHENS
-	  (tclTHEN case_last clear_last)
-	  (List.map (fun l -> intros_patterns avoid thin destopt (l@l')) ll))
+        (intro_or_and_pattern ll l' (intros_patterns avoid thin destopt))
+  | IntroRewrite l2r :: l ->
+      tclTHEN 
+        (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true)
+        (onLastHyp (fun id ->
+	  tclTHENLIST [
+	    !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) 
+	      allClauses;
+	    clear_if_atomic l2r id;
+	    intros_patterns avoid thin destopt l ]))
   | [] -> clear thin
 
 let intros_pattern = intros_patterns [] []
@@ -1030,6 +1076,9 @@ let prepare_intros s ipat gl = match ipat with
   | IntroFresh id -> fresh_id [] id gl, tclIDTAC
   | IntroWildcard -> let id = make_id s gl in id, thin [id]
   | IntroIdentifier id -> id, tclIDTAC
+  | IntroRewrite l2r -> 
+      let id = make_id s gl in
+      id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses
   | IntroOrAndPattern ll -> make_id s gl, 
     (tclTHENS 
       (tclTHEN case_last clear_last)
@@ -1341,6 +1390,7 @@ let rec first_name_buggy = function
   | IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l)
   | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p
   | IntroWildcard -> None
+  | IntroRewrite _ -> None
   | IntroIdentifier id -> Some id
   | IntroAnonymous | IntroFresh _ -> assert false
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 084aba9efa..1c64e47e84 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -338,3 +338,6 @@ val tclABSTRACT : identifier option -> tactic -> tactic
 val admit_as_an_axiom : tactic
 
 val abstract_generalize : identifier -> tactic
+
+val register_general_multi_rewrite : 
+  (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit