Fichiers tactics/*.ml4 remplacent les tactics/*.v

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

7 files changed, 910 insertions, 109 deletions

diff --git a/tactics/Equality.v b/tactics/Equality.v
index 317e11474..9f6d78264 100644
--- a/tactics/Equality.v
+++ b/tactics/Equality.v
@@ -8,91 +8,4 @@
 
 (* $Id$: *)
 
-Declare ML Module "equality".
-
-Grammar tactic simple_tactic: ast :=
-  replace [ "Replace" constrarg($c1) "with" constrarg($c2) ] -> [(Replace $c1 $c2)]
-
-| deqhyp   [ "Simplify_eq" ident_or_numarg($id) ] -> [(DEqHyp $id)]
-| deqconcl [ "Simplify_eq" ] -> [(DEqConcl)]
-
-| discr_id [ "Discriminate" ident_or_numarg($id) ] -> [(DiscrHyp $id)]
-| discr    [ "Discriminate" ] -> [(Discr)]
-
-| inj    [ "Injection" ] -> [(Inj)]
-| inj_id [ "Injection" ident_or_numarg($id) ] -> [(InjHyp $id)]
-
-| rewriteLR [ "Rewrite" "->" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
-| rewriteRL [ "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(RewriteRL ($LIST $cl))]
-| rewrite [ "Rewrite" constrarg_binding_list($cl) ] -> [(RewriteLR ($LIST $cl))]
-
-| condrewriteLR [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
-| condrewriteRL [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) ] -> [(CondRewriteRL (TACTIC $tac) ($LIST $cl))]
-| condrewrite [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) ] -> [(CondRewriteLR (TACTIC $tac) ($LIST $cl))]
-
-| rewrite_in [ "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ]
-       -> [(RewriteLRin $h ($LIST $cl))]
-| rewriteRL_in [ "Rewrite" "->" constrarg_binding_list($cl) "in" identarg($h) ]
-       -> [(RewriteLRin $h ($LIST $cl))]
-| rewriteLR_in [ "Rewrite" "<-" constrarg_binding_list($cl) "in" identarg($h) ]
-       -> [(RewriteRLin $h ($LIST $cl))]
-
-| condrewriteLRin 
-  [ "Conditional" tactic_expr($tac) "Rewrite" "->" constrarg_binding_list($cl) 
-	"in" identarg($h) ] ->
-	   [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
-| condrewriteRLin 
-  [ "Conditional" tactic_expr($tac) "Rewrite" "<-" constrarg_binding_list($cl) 
-	"in" identarg($h)] ->
-  	   [(CondRewriteRLin (TACTIC $tac) $h ($LIST $cl))]
-| condrewritein 
-  [ "Conditional" tactic_expr($tac) "Rewrite" constrarg_binding_list($cl) "in" identarg($h) ] 
-        -> [(CondRewriteLRin (TACTIC $tac) $h ($LIST $cl))]
-
-| DRewriteLR [ "Dependent" "Rewrite" "->" identarg($id) ]
-       -> [(SubstHypInConcl_LR $id)]
-| DRewriteRL [ "Dependent" "Rewrite" "<-" identarg($id) ]
-       -> [(SubstHypInConcl_RL $id)]
-
-| cutrewriteLR [ "CutRewrite" "->" constrarg($eqn) ] -> [(SubstConcl_LR $eqn)]
-| cutrewriteLRin [ "CutRewrite" "->" constrarg($eqn) "in" identarg($id) ]
-      -> [(SubstHyp_LR $eqn $id)]
-| cutrewriteRL [ "CutRewrite" "<-" constrarg($eqn) ] -> [(SubstConcl_RL $eqn)]
-| cutrewriteRLin [ "CutRewrite" "<-" constrarg($eqn) "in" identarg($id) ]
-      -> [(SubstHyp_RL $eqn $id)].
-
-Syntax tactic level 0:
-  replace [<<(Replace $c1 $c2)>>] -> ["Replace " $c1 [1 1] "with " $c2]
-
-| deqhyp [<<(DEqHyp $id)>>] -> ["Simplify_eq " $id]
-| deqconcl [<<(DEqConcl)>>] -> ["Simplify_eq"]
-
-| discr_id [<<(DiscrHyp $id)>>] -> ["Discriminate " $id]
-| discr [<<(Discr)>>] -> ["Discriminate"]
-
-| inj [<<(Inj)>>] -> ["Injection"]
-| inj_id [<<(InjHyp $id)>>] -> ["Injection " $id]
-
-| rewritelr [<<(RewriteLR $C ($LIST $bl))>>] -> ["Rewrite " $C (WITHBINDING ($LIST $bl))]
-| rewriterl [<<(RewriteRL $C ($LIST $bl))>>] -> ["Rewrite <- " $C (WITHBINDING ($LIST $bl))]
-
-| condrewritelr [<<(CondRewriteLR (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl))]
-| condrewriterl [<<(CondRewriteRL (TACTIC $tac) $C ($LIST $bl))>>] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl))]
-
-| rewriteLR_in [<<(RewriteLRin $h $c ($LIST $bl))>>] -> ["Rewrite " $c (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
-| rewriteRL_in [<<(RewriteRLin $h $c ($LIST $bl))>>] -> ["Rewrite <- " $c (WITHBINDING ($LIST $bl)) [1 1]"in " $h]
-
-| condrewritelrin [<<(CondRewriteLRin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional " $tac [1 1] "Rewrite " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
-| condrewriterlin [<<(CondRewriteRLin (TACTIC $tac) $h $C ($LIST $bl))>>] -> ["Conditional "  $tac [1 1] "Rewrite <- " $C (WITHBINDING ($LIST $bl)) [1 1] "in " $h]
-
-
-| DRewriteLR [<<(SubstHypInConcl_LR $id)>>] -> ["Dependent Rewrite -> " $id]
-| DRewriteRL [<<(SubstHypInConcl_RL $id)>>] -> ["Dependent Rewrite <- " $id]
-
-| cutrewriteLR [<<(SubstConcl_LR $eqn)>>] -> ["CutRewrite -> " $eqn]
-| cutrewriteLRin [<<(SubstHyp_LR $eqn $id)>>]
-     -> ["CutRewrite -> " $eqn:E [1 1]"in " $id]
-
-| cutrewriteRL [<<(SubstConcl_RL $eqn)>>] -> ["CutRewrite <- " $eqn:E]
-| cutrewriteRLin [<<(SubstHyp_RL $eqn $id)>>]
-      -> ["CutRewrite <- " $eqn:E [1 1]"in " $id].
+(* Command declarations are moved to the ML side *)
diff --git a/tactics/Refine.v b/tactics/Refine.v
index 4d6c117e3..72ecf89fe 100644
--- a/tactics/Refine.v
+++ b/tactics/Refine.v
@@ -8,10 +8,4 @@
 
 (* $Id$ *)
 
-Declare ML Module "refine".
-
-Grammar tactic simple_tactic: ast :=
-  tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].
-
-Syntax tactic level 0:
-  tcc [ <<(Tcc $C)>> ] -> ["Refine " $C].
+(* Command declarations are moved to the ML side *)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
new file mode 100644
index 000000000..099bfb3e5
--- /dev/null
+++ b/tactics/eauto.ml4
@@ -0,0 +1,387 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Sign
+open Reduction
+open Proof_type
+open Proof_trees
+open Tacticals
+open Tacmach
+open Evar_refiner
+open Tactics
+open Pattern
+open Clenv
+open Auto
+open Rawterm
+
+let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+  if occur_existential t1 or occur_existential t2 then 
+     tclTHEN (unify t1) (exact_no_check c) gl
+  else exact_no_check c gl
+
+let assumption id = e_give_exact (mkVar id)
+        
+let e_assumption gl = 
+  tclFIRST (List.map assumption (pf_ids_of_hyps gl)) gl
+
+let e_resolve_with_bindings_tac  (c,lbind) gl = 
+  let (wc,kONT) = startWalk gl in
+  let t = w_hnf_constr wc (w_type_of wc c) in 
+  let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in 
+  e_res_pf kONT clause gl
+
+let e_resolve_with_bindings = 
+  tactic_com_bind_list e_resolve_with_bindings_tac
+
+let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls
+let resolve_constr c gls = Tactics.apply_with_bindings (c,NoBindings) gls
+			     
+TACTIC EXTEND EExact
+| [ "EExact" constr(c) ] -> [ e_give_exact c ]
+END
+
+let e_give_exact_constr = h_eExact
+
+let registered_e_assumption gl = 
+  tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) 
+              (pf_ids_of_hyps gl)) gl
+
+TACTIC EXTEND EApply
+  [ "EApply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ]
+END
+
+let vernac_e_resolve_constr c = h_eApply (c,NoBindings)
+
+(************************************************************************)
+(*   PROLOG tactic                                                      *)
+(************************************************************************)
+
+let one_step l gl =
+  [Tactics.intro]
+  @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl)))
+  @ (List.map e_resolve_constr l)
+  @ (List.map assumption (pf_ids_of_hyps gl))
+
+let rec prolog l n gl =
+  if n <= 0 then error "prolog - failure";
+  let prol = (prolog l (n-1)) in
+  (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
+
+let prolog_tac l n gl =
+  let n =
+    match n with
+      |  Genarg.ArgArg n -> n
+      | _ -> error "Prolog called with a non closed argument"
+  in
+  try (prolog l n gl)
+  with UserError ("Refiner.tclFIRST",_) ->
+    errorlabstrm "Prolog.prolog" (str "Prolog failed")
+
+TACTIC EXTEND Prolog
+| [ "Prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ]
+END
+
+(*
+let vernac_prolog =
+  let uncom = function
+    | Constr c -> c
+    | _ -> assert false
+  in
+  let gentac = 
+    hide_tactic "Prolog"
+      (function
+	 | (Integer n) :: al -> prolog_tac (List.map uncom al) n
+	 | _ -> assert false)
+  in 
+  fun coms n -> 
+    gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
+*)
+
+open Auto
+
+(***************************************************************************)
+(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
+(***************************************************************************)
+
+let unify_e_resolve  (c,clenv) gls = 
+  let (wc,kONT) = startWalk gls in
+  let clenv' = connect_clenv wc clenv in
+  let _ = clenv_unique_resolver false clenv' gls in
+  vernac_e_resolve_constr c gls
+
+let rec e_trivial_fail_db db_list local_db goal =
+  let tacl = 
+    registered_e_assumption ::
+    (tclTHEN Tactics.intro 
+       (function g'->
+	  let d = pf_last_hyp g' in
+	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
+          (e_trivial_fail_db db_list
+	     (Hint_db.add_list hintl local_db) g'))) ::
+    (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
+  in 
+  tclFIRST (List.map tclCOMPLETE tacl) goal 
+
+and e_my_find_search db_list local_db hdc concl = 
+  let hdc = head_of_constr_reference hdc in
+  let hintl =
+    if occur_existential concl then 
+      list_map_append (Hint_db.map_all hdc) (local_db::db_list)
+    else 
+      list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)
+  in 
+  let tac_of_hint = 
+    fun ({pri=b; pat = p; code=t} as patac) -> 
+      (b, 
+       let tac =
+	 match t with
+	   | Res_pf (term,cl) -> unify_resolve (term,cl)
+	   | ERes_pf (term,cl) -> unify_e_resolve (term,cl)
+	   | Give_exact (c) -> e_give_exact_constr c
+	   | Res_pf_THEN_trivial_fail (term,cl) ->
+               tclTHEN (unify_e_resolve (term,cl)) 
+		 (e_trivial_fail_db db_list local_db)
+	   | Unfold_nth c -> unfold_constr c
+	   | Extern tacast -> conclPattern concl 
+	       (out_some p) tacast
+       in 
+       (tac,fmt_autotactic t))
+       (*i
+	 fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); 
+                     try tac gls
+		     with e when Logic.catchable_exception(e) -> 
+                            (Format.print_string "Fail\n"; 
+			     Format.print_flush (); 
+			     raise e)
+       i*)
+  in 
+  List.map tac_of_hint hintl
+    
+and e_trivial_resolve db_list local_db gl = 
+  try 
+    Auto.priority 
+      (e_my_find_search db_list local_db 
+	 (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let e_possible_resolve db_list local_db gl =
+  try List.map snd (e_my_find_search db_list local_db 
+		      (List.hd (head_constr_bound gl [])) gl)
+  with Bound | Not_found -> []
+
+let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id))
+
+let find_first_goal gls = 
+  try first_goal gls with UserError _ -> assert false
+
+(*s The following module [SearchProblem] is used to instantiate the generic
+    exploration functor [Explore.Make]. *)
+      
+module SearchProblem = struct
+
+  type state = { 
+    depth : int; (*r depth of search before failing *)
+    tacres : goal list sigma * validation;
+    last_tactic : std_ppcmds;
+    dblist : Auto.Hint_db.t list;
+    localdb :  Auto.Hint_db.t list }
+		 
+  let success s = (sig_it (fst s.tacres)) = []
+
+  let rec filter_tactics (glls,v) = function
+    | [] -> []
+    | (tac,pptac) :: tacl -> 
+	try 
+	  let (lgls,ptl) = apply_tac_list tac glls in 
+	  let v' p = v (ptl p) in
+	  ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl
+	with e when Logic.catchable_exception e ->
+	  filter_tactics (glls,v) tacl
+
+  let rec list_addn n x l = 
+    if n = 0 then l else x :: (list_addn (pred n) x l)
+
+  (* Ordering of states is lexicographic on depth (greatest first) then
+     number of remaining goals. *)
+  let compare s s' =
+    let d = s'.depth - s.depth in
+    let nbgoals s = List.length (sig_it (fst s.tacres)) in
+    if d <> 0 then d else nbgoals s - nbgoals s'
+
+  let branching s = 
+    if s.depth = 0 then 
+      []
+    else      
+      let lg = fst s.tacres in
+      let nbgl = List.length (sig_it lg) in
+      assert (nbgl > 0);
+      let g = find_first_goal lg in
+      let assumption_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (List.map 
+	       (fun id -> (e_give_exact_constr (mkVar id),
+			   (str "Exact" ++ spc () ++ pr_id id)))
+	       (pf_ids_of_hyps g))
+	in
+	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
+				    last_tactic = pp; dblist = s.dblist;
+				    localdb = List.tl s.localdb }) l
+      in
+      let intro_tac = 
+	List.map 
+	  (fun ((lgls,_) as res,pp) -> 
+	     let g' = first_goal lgls in 
+	     let hintl = 
+	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
+	     in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
+	     { depth = s.depth; tacres = res; 
+	       last_tactic = pp; dblist = s.dblist;
+	       localdb = ldb :: List.tl s.localdb })
+	  (filter_tactics s.tacres [Tactics.intro,(str "Intro")])
+      in
+      let rec_tacs = 
+	let l = 
+	  filter_tactics s.tacres
+	    (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g))
+	in
+	List.map 
+	  (fun ((lgls,_) as res, pp) -> 
+	     let nbgl' = List.length (sig_it lgls) in
+	     if nbgl' < nbgl then
+	       { depth = s.depth; tacres = res; last_tactic = pp;
+		 dblist = s.dblist; localdb = List.tl s.localdb }
+	     else 
+	       { depth = pred s.depth; tacres = res; 
+		 dblist = s.dblist; last_tactic = pp;
+		 localdb = 
+		   list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb })
+	  l
+      in
+      List.sort compare (assumption_tacs @ intro_tac @ rec_tacs)
+
+  let pp s = 
+    msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
+		  s.last_tactic ++ str "\n"))
+
+end
+
+module Search = Explore.Make(SearchProblem)
+
+let make_initial_state n gl dblist localdb =
+  { SearchProblem.depth = n;
+    SearchProblem.tacres = tclIDTAC gl;
+    SearchProblem.last_tactic = (mt ());
+    SearchProblem.dblist = dblist;
+    SearchProblem.localdb = [localdb] }
+
+let e_depth_search debug p db_list local_db gl =
+  try
+    let tac = if debug then Search.debug_depth_first else Search.depth_first in
+    let s = tac (make_initial_state p gl db_list local_db) in
+    s.SearchProblem.tacres
+  with Not_found -> error "EAuto: depth first search failed"
+
+let e_breadth_search debug n db_list local_db gl =
+  try
+    let tac = 
+      if debug then Search.debug_breadth_first else Search.breadth_first 
+    in
+    let s = tac (make_initial_state n gl db_list local_db) in
+    s.SearchProblem.tacres
+  with Not_found -> error "EAuto: breadth first search failed"
+
+let e_search_auto debug (in_depth,p) db_list gl = 
+  let local_db = make_local_hint_db gl in 
+  if in_depth then 
+    e_depth_search debug p db_list local_db gl
+  else 
+    e_breadth_search debug p db_list local_db gl
+
+let eauto debug np dbnames = 
+  let db_list =
+    List.map
+      (fun x -> 
+	 try Stringmap.find x !searchtable
+	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
+      ("core"::dbnames) 
+  in
+  tclTRY (e_search_auto debug np db_list)
+
+let full_eauto debug n gl = 
+  let dbnames = stringmap_dom !searchtable in
+  let dbnames =  list_subtract dbnames ["v62"] in
+  let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in
+  let local_db = make_local_hint_db gl in
+  tclTRY (e_search_auto debug n db_list) gl
+
+let gen_eauto d np = function
+  | None -> full_eauto d np
+  | Some l -> eauto d np l
+
+let make_depth = function
+  | None -> !default_search_depth 
+  | Some (Genarg.ArgArg d) -> d
+  | _ -> error "EAuto called with a non closed argument"
+
+let make_dimension n = function
+  | None -> (true,make_depth n)
+  | Some (Genarg.ArgArg d) -> (false,d)
+  | _ -> error "EAuto called with a non closed argument"
+
+open Genarg
+
+(* Hint bases *)
+
+let wit_hintbases, rawwit_hintbases = Genarg.create_arg "hintbases"
+let hintbases = create_generic_entry "hintbases" rawwit_hintbases
+let _ = Tacinterp.add_genarg_interp "hintbases"
+  (fun ist x ->
+    (in_gen wit_hintbases
+      (out_gen (wit_opt (wit_list0 wit_string))
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_opt (wit_list0 rawwit_string))
+	    (out_gen rawwit_hintbases x))))))
+
+GEXTEND Gram
+  GLOBAL: hintbases;
+  hintbases:
+  [ [ "with"; "*" -> None
+    | "with"; l = LIST1 IDENT -> Some l
+    | -> Some [] ] ];
+END
+
+let pr_hintbases = function 
+  | None -> str " with *"
+  | Some [] -> mt ()
+  | Some l -> str " with " ++ Util.prlist str l
+
+let _ = 
+  Pptactic.declare_extra_genarg_pprule 
+    (rawwit_hintbases, pr_hintbases)
+    (wit_hintbases, pr_hintbases)
+
+TACTIC EXTEND EAuto
+| [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
+    [ gen_eauto false (make_dimension n p) db ]
+| [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
+    [ gen_eauto true (make_dimension n p) db ]
+END
+
+
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
new file mode 100644
index 000000000..b9c6bbef8
--- /dev/null
+++ b/tactics/eqdecide.ml4
@@ -0,0 +1,194 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(***********************************************************************)
+(*                              EqDecide                               *)
+(*   A tactic for deciding propositional equality on inductive types   *)
+(*                           by Eduardo Gimenez                        *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Util
+open Names
+open Nameops
+open Term
+open Declarations
+open Tactics
+open Tacticals
+open Hiddentac
+open Equality
+open Auto
+open Pattern
+open Hipattern
+open Proof_trees
+open Proof_type
+open Tacmach
+open Coqlib
+
+(* This file containts the implementation of the tactics ``Decide
+   Equality'' and ``Compare''. They can be used to decide the
+   propositional equality of two objects that belongs to a small
+   inductive datatype --i.e., an inductive set such that all the
+   arguments of its constructors are non-functional sets.
+
+   The procedure for proving (x,y:R){x=y}+{~x=y} can be scketched as
+   follows:
+   1. Eliminate x and then y.
+   2. Try discrimination to solve those goals where x and y has
+      been introduced by different constructors.
+   3. If x and y have been introduced by the same constructor,
+      then analyse one by one the correspoing pairs of arguments.
+      If they are equal, rewrite one into the other. If they are
+      not, derive a contradiction from the injectiveness of the
+      constructor. 
+   4. Once all the arguments have been rewritten, solve the left half 
+      of the disjunction by reflexivity.
+
+   Eduardo Gimenez (30/3/98).
+*)
+
+let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
+
+let mkBranches = 
+  tclTHENSEQ
+    [intro; 
+     tclLAST_HYP h_simplest_elim;
+     clear_last;
+     intros ;
+     tclLAST_HYP h_simplest_case;
+     clear_last;
+     intros]
+
+let solveRightBranch  = 
+  tclTHEN h_simplest_right
+    (tclTHEN (intro_force true) (onLastHyp Extratactics.h_discrHyp))
+
+let h_solveRightBranch =
+  Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch
+
+(*
+let h_solveRightBranch =
+  hide_atomic_tactic "solveRightBranch" solveRightBranch
+*)
+
+(* Constructs the type {c1=c2}+{~c1=c2} *)
+
+let mkDecideEqGoal rectype c1 c2 g = 
+  let equality    = mkApp(build_coq_eq_data.eq (), [|rectype; c1; c2|]) in
+  let disequality = mkApp(build_coq_not (), [|equality|]) in
+  mkApp(build_coq_sumbool (), [|equality; disequality |])
+
+
+(* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
+
+let mkGenDecideEqGoal rectype g = 
+  let hypnames = pf_ids_of_hyps g in 
+  let xname    = next_ident_away (id_of_string "x") hypnames
+  and yname    = next_ident_away (id_of_string "y") hypnames in
+  (mkNamedProd xname rectype 
+     (mkNamedProd yname rectype 
+        (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
+
+let eqCase  tac = 
+  (tclTHEN intro  
+  (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR)
+  (tclTHEN clear_last 
+  tac)))
+
+let diseqCase = 
+  let diseq  = id_of_string "diseq" in
+  let absurd = id_of_string "absurd" in 
+  (tclTHEN (intro_using diseq)
+  (tclTHEN  h_simplest_right
+  (tclTHEN  red_in_concl
+  (tclTHEN  (intro_using absurd)
+  (tclTHEN  (h_simplest_apply (mkVar diseq))
+  (tclTHEN  (Extratactics.h_injHyp absurd)
+            full_trivial))))))
+
+let solveArg a1 a2 tac  g = 
+  let rectype = pf_type_of g a1 in
+  let decide  = mkDecideEqGoal rectype a1 a2 g in  
+  (tclTHENS
+     (h_elim_type decide) 
+     [(eqCase tac);diseqCase;default_auto]) g
+
+let solveLeftBranch rectype g =
+  match
+    try matches (Coqlib.build_coq_eqdec_partial_pattern ()) (pf_concl g)
+    with Pattern.PatternMatchingFailure -> error "Unexpected conclusion!"
+  with 
+    | _ :: lhs :: rhs :: _ -> 
+        let (mib,mip) = Global.lookup_inductive rectype in
+	let nparams   = mip.mind_nparams in
+	let getargs l = snd (list_chop nparams (snd (decompose_app l))) in
+	let rargs   = getargs (snd rhs)
+	and largs   = getargs (snd lhs) in 
+	List.fold_right2 
+	  solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
+    | _ -> anomaly "Unexpected pattern for solveLeftBranch"
+
+
+(* The tactic Decide Equality *)
+
+let hd_app c = match kind_of_term c with
+  | App (h,_) -> h
+  | _ -> c
+
+let decideGralEquality g =
+  match
+    try matches (build_coq_eqdec_pattern ()) (pf_concl g)
+    with Pattern.PatternMatchingFailure ->
+      error "The goal does not have the expected form"
+  with 
+    | (_,typ) :: _ ->
+	let headtyp = hd_app (pf_compute g typ) in
+	let rectype =
+	  match kind_of_term headtyp with
+            | Ind mi -> mi
+	    | _ -> error 
+		"This decision procedure only works for inductive objects" 
+	in 
+	(tclTHEN
+	   mkBranches 
+           (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
+    | _ -> anomaly "Unexpected pattern for decideGralEquality"
+
+
+let decideEquality c1 c2 g = 
+  let rectype = (pf_type_of g c1) in     
+  let decide  = mkGenDecideEqGoal rectype g in  
+  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
+
+
+(* The tactic Compare *)
+
+let compare c1 c2 g = 
+  let rectype = pf_type_of g c1 in
+  let decide  = mkDecideEqGoal rectype c1 c2 g in  
+  (tclTHENS (cut decide) 
+            [(tclTHEN  intro 
+             (tclTHEN (tclLAST_HYP simplest_case)
+                       clear_last));
+             decideEquality c1 c2]) g
+
+
+(* User syntax *)
+
+TACTIC EXTEND DecideEquality
+  [ "Decide" "Equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
+| [ "Decide" "Equality" ] -> [ decideGralEquality ]
+END
+
+TACTIC EXTEND Compare
+| [ "Compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+END
+
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
new file mode 100644
index 000000000..4a2917c4d
--- /dev/null
+++ b/tactics/extraargs.ml4
@@ -0,0 +1,87 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Pp
+open Pcoq
+open Genarg
+
+(* Rewriting orientation *)
+
+let wit_orient, rawwit_orient = Genarg.create_arg "orient"
+let orient = Pcoq.create_generic_entry "orient" rawwit_orient
+let _ = Tacinterp.add_genarg_interp "orient"
+  (fun ist x ->
+    (in_gen wit_orient
+      (out_gen wit_bool
+	(Tacinterp.genarg_interp ist
+	  (in_gen wit_bool
+	    (out_gen rawwit_orient x))))))
+
+let _ = Metasyntax.add_token_obj "<-"
+let _ = Metasyntax.add_token_obj "->"
+
+GEXTEND Gram
+  GLOBAL: orient;
+  orient:
+  [ [ "->" -> true
+    | "<-" -> false
+    | -> true ] ];
+END
+
+let pr_orient = function true -> Pp.str " ->" | false -> Pp.str " <-"
+
+let _ = 
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_orient, pr_orient)
+    (wit_orient, pr_orient)
+
+ 
+(* with_constr *)
+
+let wit_with_constr, rawwit_with_constr = Genarg.create_arg "with_constr"
+let with_constr = Pcoq.create_generic_entry "with_constr" rawwit_with_constr
+let _ = Tacinterp.add_genarg_interp "with_constr"
+  (fun ist x ->
+    (in_gen wit_with_constr
+      (out_gen (wit_opt wit_constr)
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_opt rawwit_constr)
+	    (out_gen rawwit_with_constr x))))))
+
+GEXTEND Gram
+  GLOBAL: with_constr;
+  with_constr:
+  [ [ "with"; c = Constr.constr -> Some c
+    | -> None ] ];
+END
+
+let pr_with_constr prc = function 
+  | None -> Pp.mt ()
+  | Some c -> Pp.str " with" ++ prc c
+
+let _ = 
+  Pptactic.declare_extra_genarg_pprule
+    (rawwit_with_constr, pr_with_constr Ppconstr.pr_constr)
+    (wit_with_constr, pr_with_constr Printer.prterm)
+
+(*
+(* Clause *)
+let wit_clause, rawwit_clause = Genarg.create_arg "clause"
+let clause = Pcoq.create_generic_entry "clause" rawwit_clause
+let _ = Tacinterp.add_genarg_interp "clause"
+  (fun ist x ->
+    (in_gen wit_clause
+      (out_gen (wit_opt wit_constr)
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_opt rawwit_constr)
+	    (out_gen rawwit_clause x))))))
+*)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
new file mode 100644
index 000000000..bef676b6a
--- /dev/null
+++ b/tactics/extratactics.ml4
@@ -0,0 +1,214 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Pp
+open Pcoq
+open Genarg
+open Extraargs
+
+(* Equality *)
+open Equality
+
+TACTIC EXTEND Rewrite
+  [ "Rewrite" orient(b) constr_with_bindings(c) ] -> [general_rewrite_bindings b c]
+END
+
+TACTIC EXTEND RewriteIn
+ [ "Rewrite" orient(b) constr_with_bindings(c) "in" ident(h) ] ->
+ [general_rewrite_in b h c]
+END
+
+let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings)
+
+TACTIC EXTEND Replace
+  [ "Replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ]
+END
+
+TACTIC EXTEND ReplaceIn
+  [ "Replace" constr(c1) "with" constr(c2) "in" ident(h) ]
+  -> [ failwith "Replace in: TODO" ]
+END
+
+TACTIC EXTEND DEq
+  [ "Simplify_eq" ident_opt(h) ] -> [ dEq h ]
+END
+
+TACTIC EXTEND Discriminate
+  [ "Discriminate" ident_opt(h) ] -> [ discr_tac h ]
+END
+
+let h_discrHyp id = h_discriminate (Some id)
+
+TACTIC EXTEND Injection
+  [ "Injection" ident_opt(h) ] -> [ injClause h ]
+END
+
+let h_injHyp id = h_injection (Some id)
+
+TACTIC EXTEND ConditionalRewrite
+  [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c) ]
+    -> [ conditional_rewrite b (Tacinterp.interp tac) c ]
+END
+
+TACTIC EXTEND ConditionalRewriteIn
+  [ "Conditional" tactic(tac) "Rewrite" orient(b) constr_with_bindings(c)
+    "in" ident(h) ]
+    -> [ conditional_rewrite_in b h (Tacinterp.interp tac) c ]
+END
+
+TACTIC EXTEND DependentRewrite
+| [ "Dependent" "Rewrite" orient(b) ident(id) ] -> [ substHypInConcl b id ]
+| [ "CutRewrite" orient(b) constr(eqn) ] -> [ substConcl b eqn ]
+| [ "CutRewrite" orient(b) constr(eqn) "in" ident(id) ]
+      -> [ substHyp b eqn id ]
+END
+
+(* Contradiction *)
+open Contradiction
+
+TACTIC EXTEND Absurd
+ [ "Absurd" constr(c) ] -> [ absurd c ]
+END
+
+TACTIC EXTEND Contradiction
+ [ "Contradiction" ] -> [ contradiction ]
+END
+
+(* Inversion *)
+
+open Inv
+open Leminv
+
+TACTIC EXTEND SimpleInversion
+| [ "Simple" "Inversion" quantified_hypothesis(id) ] -> [ inv None id ]
+| [ "Simple" "Inversion" quantified_hypothesis(id) "in" ne_ident_list(l) ]
+  -> [ invIn_gen None id l]
+| [ "Dependent" "Simple" "Inversion" quantified_hypothesis(id) with_constr(c) ]
+  -> [ dinv None c id ]
+END
+
+TACTIC EXTEND Inversion
+| [ "Inversion" quantified_hypothesis(id) ] -> [ inv (Some false) id ]
+| [ "Inversion" quantified_hypothesis(id) "in" ne_ident_list(l) ]
+      -> [ invIn_gen (Some false) id l]
+| [ "Dependent" "Inversion" quantified_hypothesis(id) with_constr(c) ]
+    -> [ dinv (Some false) c id ]
+END
+
+TACTIC EXTEND InversionClear
+| [ "Inversion_clear" quantified_hypothesis(id) ] -> [ inv (Some true) id ]
+| [ "Inversion_clear" quantified_hypothesis(id) "in" ne_ident_list(l) ]
+      -> [ invIn_gen (Some true) id l]
+| [ "Dependent" "Inversion_clear" quantified_hypothesis(id) with_constr(c) ]
+    -> [ dinv (Some true) c id ]
+END
+
+TACTIC EXTEND InversionUsing
+| [ "Inversion" quantified_hypothesis(id) "using" constr(c) ]
+     -> [ lemInv_gen id c ]
+| [ "Inversion" quantified_hypothesis(id) "using" constr(c)
+    "in" ne_ident_list(l) ]
+     -> [ lemInvIn_gen id c l ]
+END        
+
+(* AutoRewrite *)
+
+open Autorewrite
+TACTIC EXTEND Autorewrite
+  [ "AutoRewrite" "[" ne_preident_list(l) "]" ] ->
+    [ autorewrite Refiner.tclIDTAC l ]
+| [ "AutoRewrite" "[" ne_preident_list(l) "]" "using" tactic(t) ] ->
+    [ autorewrite (Tacinterp.interp t) l ]
+END
+
+let add_rewrite_hint name ort t lcsr =
+  let env = Global.env() and sigma = Evd.empty in
+  let f c = Astterm.interp_constr sigma env c, ort, t in
+  add_rew_rules name (List.map f lcsr)
+
+VERNAC COMMAND EXTEND HintRewrite
+  [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b) ] ->
+  [ add_rewrite_hint b o Tacexpr.TacId l ]
+| [ "Hint" "Rewrite" orient(o) "[" ne_constr_list(l) "]" "in" preident(b)
+    "using" tactic(t) ] ->
+  [ add_rewrite_hint b o t l ]
+END
+
+(* Refine *)
+
+open Refine
+
+TACTIC EXTEND Refine
+  [ "Refine" castedopenconstr(c) ] -> [ refine c ]
+END
+
+let refine_tac = h_refine
+
+(* Setoid_replace *)
+
+open Setoid_replace
+
+TACTIC EXTEND SetoidReplace
+  [ "Setoid_replace" constr(c1) "with" constr(c2) ]
+  -> [ setoid_replace c1 c2 None]
+END
+
+TACTIC EXTEND SetoidRewrite
+  [ "Setoid_rewrite" orient(b) constr(c) ] -> [ general_s_rewrite b c ]
+END
+
+VERNAC COMMAND EXTEND AddSetoid
+| [ "Add" "Setoid" constr(a) constr(aeq) constr(t) ] -> [ add_setoid a aeq t ]
+| [ "Add" "Morphism" constr(m) ":" ident(s) ] -> [ new_named_morphism s m ]
+END
+
+(*
+cp tactics/extratactics.ml4 toto.ml; camlp4o -I parsing pa_extend.cmo grammar.cma pr_o.cmo toto.ml 
+*)
+
+(* Inversion lemmas (Leminv) *)
+
+VERNAC COMMAND EXTEND DeriveInversionClear
+  [ "Derive" "Inversion_clear" ident(na) ident(id) ]
+  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ]
+
+| [ "Derive" "Inversion_clear" natural(n) ident(na) ident(id) ]
+  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_clear_tac ]
+
+| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+  -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
+
+| [ "Derive" "Inversion_clear"  ident(na) "with" constr(c) ]
+  -> [ add_inversion_lemma_exn na c (let loc = (0,0) in <:ast< (PROP) >>) false inv_clear_tac ]
+END
+
+VERNAC COMMAND EXTEND DeriveInversion
+| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+  -> [ add_inversion_lemma_exn na c s false half_inv_tac ]
+
+| [ "Derive" "Inversion" ident(na) "with" constr(c) ]
+  -> [ add_inversion_lemma_exn na c (let loc = (0,0) in <:ast< (PROP) >>) false half_inv_tac ]
+
+| [ "Derive" "Inversion" ident(na) ident(id) ]
+  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ]
+
+| [ "Derive" "Inversion" natural(n) ident(na) ident(id) ]
+  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false half_inv_tac ]
+END
+
+VERNAC COMMAND EXTEND DeriveDependentInversion
+| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
+  -> [ add_inversion_lemma_exn na c s true half_dinv_tac ]
+
+| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ]
+  -> [ add_inversion_lemma_exn na c s true dinv_clear_tac ]
+END
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index d971c0c1e..2e266a29d 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -16,7 +16,7 @@ open Hipattern
 open Names
 open Pp
 open Proof_type
-open Tacmach
+open Tacticals
 open Tacinterp
 open Tactics
 open Util
@@ -112,13 +112,26 @@ let rec tauto_intuit t_reduce t_solver ist =
 
 let unfold_not_iff = function
   | None -> interp <:tactic<Unfold not iff>>
-  | Some id ->
-    let ast_id = nvar id in
-    interp <:tactic<Unfold not iff in $ast_id>>
+  | Some id -> let id = (dummy_loc,id) in interp <:tactic<Unfold not iff in $id>>
 
-let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
+let reduction_not_iff =
+  Tacticals.onAllClauses (fun ido -> unfold_not_iff ido)
 
-let t_reduction_not_iff = valueIn (VTactic reduction_not_iff)
+let t_reduction_not_iff = Tacexpr.TacArg (valueIn (VTactic reduction_not_iff))
+
+(*
+let reduction_not_iff ist =
+  match ist.goalopt with 
+    | None -> anomaly "reduction_not_iff"
+    | Some gl ->
+	List.fold_right
+	(fun id tac -> 
+	  let id = (dummy_loc,id) in <:tactic<Unfold not iff in $id; $tac>>)
+	(Tacmach.pf_ids_of_hyps gl)
+	<:tactic<Unfold not iff>>
+
+let t_reduction_not_iff = tacticIn reduction_not_iff
+*)
 
 let intuition_gen tac =
   interp (tacticIn (tauto_intuit t_reduction_not_iff tac))
@@ -129,12 +142,11 @@ let tauto g =
 
 let default_intuition_tac = <:tactic< Auto with * >>
 
-let intuition args =
-  match args with
-    | [] -> intuition_gen default_intuition_tac
-    | [ Tac(_, t)] -> intuition_gen t
-    | _ -> assert false
-
-let _ = hide_atomic_tactic "Tauto" tauto
-let _ = hide_tactic "Intuition" intuition
+TACTIC EXTEND Tauto
+| [ "Tauto" ] -> [ tauto ]
+END
 
+TACTIC EXTEND Intuition
+| [ "Intuition" ] -> [ intuition_gen default_intuition_tac ]
+| [ "Intuition" tactic(t) ] -> [ intuition_gen t ]
+END