diff options
Diffstat (limited to 'tactics/tauto.ml4')
| -rw-r--r-- | tactics/tauto.ml4 | 209 |
1 files changed, 209 insertions, 0 deletions
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 new file mode 100644 index 00000000..553acc91 --- /dev/null +++ b/tactics/tauto.ml4 @@ -0,0 +1,209 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "parsing/grammar.cma" i*) + +(*i $Id: tauto.ml4,v 1.62.2.1 2004/07/16 19:30:55 herbelin Exp $ i*) + +open Ast +open Coqast +open Hipattern +open Names +open Libnames +open Pp +open Proof_type +open Tacticals +open Tacinterp +open Tactics +open Util + +let assoc_last ist = + match List.assoc (Names.id_of_string "X1") ist.lfun with + | VConstr c -> c + | _ -> failwith "Tauto: anomaly" + +let is_empty ist = + if is_empty_type (assoc_last ist) then + <:tactic<idtac>> + else + <:tactic<fail>> + +let is_unit ist = + if is_unit_type (assoc_last ist) then + <:tactic<idtac>> + else + <:tactic<fail>> + +let is_conj ist = + let ind = assoc_last ist in + if (is_conjunction ind) && (is_nodep_ind ind) then + <:tactic<idtac>> + else + <:tactic<fail>> + +let is_disj ist = + if is_disjunction (assoc_last ist) then + <:tactic<idtac>> + else + <:tactic<fail>> + +let not_dep_intros ist = + <:tactic< + repeat match goal with + | |- (?X1 -> ?X2) => intro + | |- (Coq.Init.Logic.iff _ _) => unfold Coq.Init.Logic.iff + | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not + | H:(Coq.Init.Logic.iff _ _)|- _ => unfold Coq.Init.Logic.iff in H + | H:(Coq.Init.Logic.not _)|-_ => unfold Coq.Init.Logic.not in H + | H:(Coq.Init.Logic.iff _ _)->_|- _ => unfold Coq.Init.Logic.iff in H + | H:(Coq.Init.Logic.not _)->_|-_ => unfold Coq.Init.Logic.not in H + end >> + +let axioms ist = + let t_is_unit = tacticIn is_unit + and t_is_empty = tacticIn is_empty in + <:tactic< + match reverse goal with + | |- ?X1 => $t_is_unit; constructor 1 + | _:?X1 |- _ => $t_is_empty; elimtype X1; assumption + | _:?X1 |- ?X1 => assumption + end >> + + +let simplif ist = + let t_is_unit = tacticIn is_unit + and t_is_conj = tacticIn is_conj + and t_is_disj = tacticIn is_disj + and t_not_dep_intros = tacticIn not_dep_intros in + <:tactic< + $t_not_dep_intros; + repeat + (match reverse goal with + | id: (?X1 _ _) |- _ => + $t_is_conj; elim id; do 2 intro; clear id + | id: (?X1 _ _) |- _ => $t_is_disj; elim id; intro; clear id + | id0: ?X1-> ?X2, id1: ?X1|- _ => + (* generalize (id0 id1); intro; clear id0 does not work + (see Marco Maggiesi's bug PR#301) + so we instead use Assert and exact. *) + assert X2; [exact (id0 id1) | clear id0] + | id: ?X1 -> ?X2|- _ => + $t_is_unit; cut X2; + [ intro; clear id + | (* id : ?X1 -> ?X2 |- ?X2 *) + cut X1; [exact id| constructor 1; fail] + ] + | id: (?X1 ?X2 ?X3) -> ?X4|- _ => + $t_is_conj; cut (X2-> X3-> X4); + [ intro; clear id + | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X3 -> ?X4 *) + intro; intro; cut (X1 X2 X3); [exact id| split; assumption] + ] + | id: (?X1 ?X2 ?X3) -> ?X4|- _ => + $t_is_disj; + cut (X3-> X4); + [cut (X2-> X4); + [intro; intro; clear id + | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X2 -> ?X4 *) + intro; cut (X1 X2 X3); [exact id| left; assumption] + ] + | (* id: (?X1 ?X2 ?X3) -> ?X4 |- ?X3 -> ?X4 *) + intro; cut (X1 X2 X3); [exact id| right; assumption] + ] + | |- (?X1 _ _) => $t_is_conj; split + end; + $t_not_dep_intros) >> + +let rec tauto_intuit t_reduce solver ist = + let t_axioms = tacticIn axioms + and t_simplif = tacticIn simplif + and t_is_disj = tacticIn is_disj + and t_tauto_intuit = tacticIn (tauto_intuit t_reduce solver) in + let t_solver = Tacexpr.TacArg (valueIn (VTactic (dummy_loc,solver))) in + <:tactic< + ($t_simplif;$t_axioms + || match reverse goal with + | id:(?X1-> ?X2)-> ?X3|- _ => + cut X3; + [ intro; clear id; $t_tauto_intuit + | cut (X1 -> X2); + [ exact id + | generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id; + solve [ $t_tauto_intuit ]]] + | |- (?X1 _ _) => + $t_is_disj; solve [left;$t_tauto_intuit | right;$t_tauto_intuit] + end + || + (* NB: [|- _ -> _] matches any product *) + match goal with | |- _ -> _ => intro; $t_tauto_intuit + | |- _ => $t_reduce;$t_solver + end + || + $t_solver + ) >> + +let reduction_not_iff=interp + <:tactic<repeat + match goal with + | |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff + | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H + end >> + + +let t_reduction_not_iff = + Tacexpr.TacArg (valueIn (VTactic (dummy_loc,reduction_not_iff))) + +let intuition_gen tac = + interp (tacticIn (tauto_intuit t_reduction_not_iff tac)) + +let simplif_gen = interp (tacticIn simplif) + +let tauto g = + try intuition_gen (interp <:tactic<fail>>) g + with + Refiner.FailError _ | UserError _ -> + errorlabstrm "tauto" [< str "Tauto failed" >] + +let default_intuition_tac = interp <:tactic< auto with * >> + +let q_elim tac= + <:tactic< + match goal with + x : ?X1, H : ?X1 -> _ |- _ => generalize (H x); clear H; $tac + end >> + +let rec lfo n gl= + if n=0 then (tclFAIL 0 "LinearIntuition failed" gl) else + let p=if n<0 then n else (n-1) in + let lfo_rec=q_elim (Tacexpr.TacArg (valueIn (VTactic(dummy_loc,lfo p)))) in + intuition_gen (interp lfo_rec) gl + +let lfo_wrap n gl= + try lfo n gl + with + Refiner.FailError _ | UserError _ -> + errorlabstrm "LinearIntuition" [< str "LinearIntuition failed." >] + +TACTIC EXTEND Tauto +| [ "Tauto" ] -> [ tauto ] +END +(* Obsolete sinve V8.0 +TACTIC EXTEND TSimplif +| [ "Simplif" ] -> [ simplif_gen ] +END +*) +TACTIC EXTEND Intuition +| [ "Intuition" ] -> [ intuition_gen default_intuition_tac ] +| [ "Intuition" tactic(t) ] -> [ intuition_gen (snd t) ] +END +(* Obsolete since V8.0 +TACTIC EXTEND LinearIntuition +| [ "LinearIntuition" ] -> [ lfo_wrap (-1)] +| [ "LinearIntuition" integer(n)] -> [ lfo_wrap n] +END +*) |