diff options
Diffstat (limited to 'src/Tactics.v')
-rw-r--r-- | src/Tactics.v | 162 |
1 files changed, 162 insertions, 0 deletions
diff --git a/src/Tactics.v b/src/Tactics.v new file mode 100644 index 0000000..edf2f19 --- /dev/null +++ b/src/Tactics.v @@ -0,0 +1,162 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2021 *) +(* *) +(* See file "AUTHORS" for the list of authors *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +Require Import PropToBool. +Require Import Int63 List PArray Bool ZArith. +Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances QInst. + +Declare ML Module "smtcoq_plugin". + + +(** Collect all the hypotheses from the context *) + +Ltac get_hyps_acc acc := + match goal with + | [ H : ?P |- _ ] => + let T := type of P in + lazymatch T with + | Prop => + lazymatch P with + | id _ => fail + | _ => + let _ := match goal with _ => change P with (id P) in H end in + match acc with + | Some ?t => get_hyps_acc (Some (H, t)) + | None => get_hyps_acc (Some H) + end + end + | _ => fail + end + | _ => acc + end. + +Ltac eliminate_id := + repeat match goal with + | [ H : ?P |- _ ] => + lazymatch P with + | id ?Q => change P with Q in H + | _ => fail + end + end. + +Ltac get_hyps := + let Hs := get_hyps_acc (@None nat) in + let _ := match goal with _ => eliminate_id end in + Hs. + + +(* Section Test. *) +(* Variable A : Type. *) +(* Hypothesis H1 : forall a:A, a = a. *) +(* Variable n : Z. *) +(* Hypothesis H2 : n = 17%Z. *) + +(* Goal True. *) +(* Proof. *) +(* let Hs := get_hyps in idtac Hs. *) +(* Abort. *) +(* End Test. *) + + +(** Tactics in bool *) + +Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; auto with typeclass_instances. + +Tactic Notation "verit_bool" constr(h) := + let Hs := get_hyps in + match Hs with + | Some ?Hs => verit_bool_base_auto (Some (h, Hs)) + | None => verit_bool_base_auto (Some h) + end; + vauto. +Tactic Notation "verit_bool" := + let Hs := get_hyps in + verit_bool_base_auto Hs; vauto. + +Tactic Notation "verit_bool_no_check" constr(h) := + let Hs := get_hyps in + match Hs with + | Some ?Hs => verit_bool_no_check_base_auto (Some (h, Hs)) + | None => verit_bool_no_check_base_auto (Some h) + end; + vauto. +Tactic Notation "verit_bool_no_check" := + let Hs := get_hyps in + fun Hs => verit_bool_no_check_base_auto Hs; vauto. + + +(** Tactics in Prop **) + +Ltac zchaff := prop2bool; zchaff_bool; bool2prop. +Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. + +Tactic Notation "verit" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto (Some (h, Hs)) ] + | None => verit_bool_base_auto (Some h) + end; vauto + ] + ]. +Tactic Notation "verit" := + prop2bool; + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto (Some Hs) ] + | None => verit_bool_base_auto (@None nat) + end; vauto + ]. +Tactic Notation "verit_no_check" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto (Some (h, Hs)) ] + | None => verit_bool_no_check_base_auto (Some h) + end; vauto + ] + ]. +Tactic Notation "verit_no_check" := + prop2bool; + [ .. | let Hs := get_hyps in + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto (Some Hs) ] + | None => verit_bool_no_check_base_auto (@None nat) + end; vauto + ]. + +Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. +Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. + +Tactic Notation "smt" constr(h) := (prop2bool; [ .. | try verit h; cvc4_bool; try verit h; bool2prop ]). +Tactic Notation "smt" := (prop2bool; [ .. | try verit ; cvc4_bool; try verit ; bool2prop ]). +Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try verit_no_check h; cvc4_bool_no_check; try verit_no_check h; bool2prop]). +Tactic Notation "smt_no_check" := (prop2bool; [ .. | try verit_no_check ; cvc4_bool_no_check; try verit_no_check ; bool2prop]). + + + +(* + Local Variables: + coq-load-path: ((rec "." "SMTCoq")) + End: +*) |