notations <>, Assumption avec existentiel, replace term

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

8 files changed, 112 insertions, 10 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index df2aabdf8..1c19352b2 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -148,7 +148,7 @@ let pr_var_decl env (id,c,typ) =
     | Some c ->
 	(* Force evaluation *) 
 	let pb = prterm_env env c in
-	(str" := " ++ pb) in
+	(str" := " ++ pb ++ cut () ) in
   let pt = prtype_env env typ in
   let ptyp = (str" : " ++ pt) in
   (pr_id id ++ hov 0 (pbody ++ ptyp))
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 9094b0395..0b111a69f 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -137,10 +137,10 @@ Syntax constr
 
 
   | arrow [ << (ARROW $A [<>]$B) >> ] ->
-       [ [<hv 0> $A:L [0 0] "->" (ARROWBOX $B) ] ]
+       [ [<hv 0> $A:L " ->" [0 0] (ARROWBOX $B) ] ]
   | arrow_stop [ << (ARROWBOX $c) >> ] -> [ $c:E ]
   | arrow_again [ << (ARROWBOX (PROD $A [<>]$B)) >> ] ->
-	 [ $A:L [0 0] "->" (ARROWBOX $B) ]
+	 [ $A:L " ->" [0 0] (ARROWBOX $B) ]
 
 (* These are synonymous *)
 (* redundant
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                      *)
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index 7fd29d595..8326de6f8 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -18,6 +18,7 @@ Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1).
 Notation "~ x" := (not x) (at level 5, right associativity)
   V8only (at level 55, right associativity).
 Notation "x = y" := (eq ? x y) (at level 5, no associativity).
+Notation "x <> y" := (not (eq ? x y)) (at level 5, no associativity).
 
 Infix RIGHTA 6 "/\\" and.
 Infix RIGHTA 7 "\\/" or.
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index a0610b56d..81c0d9817 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -260,7 +260,10 @@ Notation  "x = y = z" := x=y/\y=z
   (at level 5, y at level 4) : Z_scope
   V8only (at level 50, y at level 49).
 
+(* Now a polymorphic notation
 Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope.
+*)
+
 (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*)
 
 V7only[