notations <>, Assumption avec existentiel, replace term

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

4 files changed, 105 insertions, 7 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index dbff4f520..3eee019ba 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1233,3 +1233,57 @@ let subst_all gl =
   let ids = map_succeed test (pf_hyps_types gl) in
   let ids = list_uniquize ids in
   subst ids gl
+
+(* Rewrite the first assumption for which the condition faildir does not fail 
+   and gives the direction of the rewrite *)
+
+let rewrite_assumption_cond faildir gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest -> 
+	  (try let dir = faildir t gl in 
+	       general_rewrite dir (mkVar id) gl
+	   with Failure _ | UserError _  ->  arec rest)
+   in arec (pf_hyps gl)
+
+
+let rewrite_assumption_cond_in faildir hyp gl =
+   let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest -> 
+	  (try let dir = faildir t gl in 
+	       general_rewrite_in dir hyp ((mkVar id),NoBindings) gl
+	   with Failure _ | UserError _ ->  arec rest)
+   in arec (pf_hyps gl)
+
+let cond_eq_term_left c t gl = 
+ let eqpat = build_coq_eq_pattern ()
+ in if not (is_matching eqpat t) then failwith "not an equality";
+    let (_,x,_) = match_eq eqpat t in
+    if pf_conv_x gl c x then true else failwith "not convertible"
+
+let cond_eq_term_right c t gl = 
+ let eqpat = build_coq_eq_pattern ()
+ in if not (is_matching eqpat t) then failwith "not an equality";
+    let (_,_,x) = match_eq eqpat t in
+    if pf_conv_x gl c x then false else failwith "not convertible"
+
+let cond_eq_term c t gl = 
+ let eqpat = build_coq_eq_pattern ()
+ in if not (is_matching eqpat t) then failwith "not an equality";
+    let (_,x,y) = match_eq eqpat t in
+    if pf_conv_x gl c x then true 
+    else if pf_conv_x gl c y then false
+    else failwith "not convertible"
+
+let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t)
+
+let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t)
+   
+let replace_term t = rewrite_assumption_cond (cond_eq_term t)
+   
+let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t)
+
+let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t)
+   
+let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e37e2d29b..88e286e51 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -96,3 +96,10 @@ val unfold_body : identifier -> tactic
 val subst : identifier list -> tactic
 val subst_all : tactic
 
+(* Replace term *)
+val replace_term_left : constr -> tactic
+val replace_term_right : constr -> tactic
+val replace_term : constr -> tactic
+val replace_term_in_left : constr -> identifier -> tactic
+val replace_term_in_right : constr -> identifier -> tactic
+val replace_term_in : constr -> identifier -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index cc61d4ea8..0915a2d9d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -41,6 +41,33 @@ TACTIC EXTEND ReplaceIn
   -> [ failwith "Replace in: TODO" ]
 END
 
+TACTIC EXTEND Replacetermleft
+  [ "Replace" "->" constr(c)  ] -> [ replace_term_left c ]
+END
+
+TACTIC EXTEND Replacetermright
+  [ "Replace" "<-" constr(c)  ] -> [ replace_term_right c ]
+END
+
+TACTIC EXTEND Replaceterm
+  [ "Replace" constr(c)  ] -> [ replace_term c ]
+END
+
+TACTIC EXTEND ReplacetermInleft
+  [ "Replace"  "->" constr(c) "in" ident(h) ]
+  -> [ replace_term_in_left c h ]
+END
+
+TACTIC EXTEND ReplacetermInright
+  [ "Replace"  "<-" constr(c) "in" ident(h) ]
+  -> [ replace_term_in_right c h ]
+END
+
+TACTIC EXTEND ReplacetermIn
+  [ "Replace" constr(c) "in" ident(h) ]
+  -> [ replace_term_in c h ]
+END
+
 TACTIC EXTEND DEq
   [ "Simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ]
 END
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 02c0e6591..d058ad543 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -753,13 +753,23 @@ let exact_proof c gl =
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
-  let rec arec = function
-    | [] -> error "No such assumption"
-    | (id,c,t)::rest -> 
-	if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
-	else arec rest
-  in
-  arec (pf_hyps gl)
+  if occur_existential concl then 
+    let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest -> 
+	  (try tclTHEN (unify t) (exact_check (mkVar id)) gl
+	   with UserError _ | Logic.RefinerError _ ->  arec rest)
+    in
+      arec (pf_hyps gl)
+  else
+    let rec arec = function
+      | [] -> error "No such assumption"
+      | (id,_,t)::rest -> 
+	  if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
+	  else arec rest
+    in
+      arec (pf_hyps gl)
+
 
 (*****************************************************************)
 (*          Modification of a local context                      *)