(* autocontra.ml : tactic file for tactic Auto_Contra. See file autocontra.v
   for Syntax. Tactic of one argument, which is expected to be the name
   of a hypothesis. The named hypothesis should be the negation of
   a proposition that can be proved true by auto. *)

open Pattern;;
open Tactics1;;
open Tactics2;;
open Names;;
open Std;;
open Pp;;
open Ast;;
open Proof_trees;;
open Trad;;
open Tacmach;;
open Tactics;;
open Tacentries;;
open Auto;;
open List;;

let not_pattern = put_pat mmk "(not ?)";;

let ineq_pattern = put_pat mmk "(not (eq ? ? ?))";;

let auto_contra1 id gls =

let tid = try snd (lookup_sign id (pf_hyps gls))
          with Not_found -> error "No such hypothesis"
in

if matches gls tid not_pattern then
     (tHENS
     (cut_tac (constr_of_com (project gls) 
			     (gLOB (pf_hyps gls))
			     (ASTnvar (id_of_string "False"))))
     [tHEN (intro) (contradict) ;
      tHEN (resolve (ASTnvar id))
            (auto None)])
    gls
    else
    error ((string_of_id id) ^ " does not contain an apparent contradiction");;

let auto_contra id = (tRY (cOMPLETE (auto_contra1 id)));;

let auto_contra_tac = register_tactic "auto_contra"
  (fun [IDENTIFIER id] -> auto_contra id)
  (fun sigma goal (_,[IDENTIFIER id]) ->
      [< 'sTR"Auto_Contra" ; 'sPC ; print_id id>]);;

(*
let auto_contran gls =

let ineq_hyps gls ts =
    let rec ineq_hyps_rec gls ts res =
        match ts with
	      ([],_) -> res |
              (_,[]) -> res |
              (name::names,hyp::hyps) ->
	          if matches gls hyp ineq_pattern
		     then (name::res)
		     else ineq_hyps_rec gls (names,hyps) res
in ineq_hyps_rec gls ts [] in

let rec attempt_auto_contra1 ids gls =
    match ids with
          [] -> gls |
          id::ids -> (attempt (auto_contra1 id) (attempt_auto_contra1 ids) gls);;


*)