diff options
Diffstat (limited to 'src/versions/standard/Tactics_standard.v')
| -rw-r--r-- | src/versions/standard/Tactics_standard.v | 127 |
1 files changed, 115 insertions, 12 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index 6ddf5a5..468de7a 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -17,11 +17,74 @@ Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances Declare ML Module "smtcoq_plugin". -Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto. -Tactic Notation "verit_bool" := verit_bool_base (@None nat); vauto. +(** Collect all the hypotheses from the context *) -Tactic Notation "verit_bool_no_check" constr(h) := verit_bool_no_check_base (Some h); vauto. -Tactic Notation "verit_bool_no_check" := verit_bool_no_check_base (@None nat); vauto. +Ltac get_hyps_acc acc k := + match goal with + | [ H : ?P |- _ ] => + let T := type of P in + match T with + | Prop => + lazymatch P with + | id _ => fail + | _ => + change P with (id P) in H; + match acc with + | Some ?t => get_hyps_acc (Some (H, t)) k + | None => get_hyps_acc (Some H) k + end + end + | _ => fail + end + | _ => k 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 k := get_hyps_acc (@None nat) ltac:(fun Hs => eliminate_id; k Hs). + + +Section Test. + Variable A : Type. + Hypothesis H1 : forall a:A, a = a. + Variable n : Z. + Hypothesis H2 : n = 17%Z. + + Goal True. + Proof. + (* get_hyps ltac:(fun acc => idtac acc). *) + Abort. +End Test. + + +(** Tactics in bool *) + +Tactic Notation "verit_bool" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_base (Some (h, Hs)) + | None => verit_bool_base (Some h) + end; + vauto). +Tactic Notation "verit_bool" := + get_hyps ltac:(fun Hs => verit_bool_base Hs; vauto). + +Tactic Notation "verit_bool_no_check" constr(h) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_no_check_base (Some (h, Hs)) + | None => verit_bool_no_check_base (Some h) + end; + vauto). +Tactic Notation "verit_bool_no_check" := + get_hyps ltac:(fun Hs => verit_bool_no_check_base Hs; vauto). (** Tactics in Prop **) @@ -29,18 +92,58 @@ Tactic Notation "verit_bool_no_check" := verit_bool_no_check_base (@No 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; [ .. | verit_bool h; bool2prop ] ]. -Tactic Notation "verit" := prop2bool; [ .. | verit_bool ; bool2prop ]. -Tactic Notation "verit_no_check" constr(h) := prop2bool; [ .. | prop2bool_hyps h; [ .. | verit_bool_no_check h; bool2prop ] ]. -Tactic Notation "verit_no_check" := prop2bool; [ .. | verit_bool_no_check ; bool2prop ]. +Tactic Notation "verit" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base (Some (h, Hs)) ] + | None => verit_bool_base (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base (Some Hs) ] + | None => verit_bool_base (@None nat) + end; vauto) + ]. +Tactic Notation "verit_no_check" constr(h) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base (Some (h, Hs)) ] + | None => verit_bool_no_check_base (Some h) + end; vauto) + ] + ]. +Tactic Notation "verit_no_check" := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base (Some Hs) ] + | None => verit_bool_no_check_base (@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 (prop2bool_hyps h; [ .. | verit_bool h ]); cvc4_bool; try (prop2bool_hyps h; [ .. | verit_bool h ]); bool2prop ]). -Tactic Notation "smt" := (prop2bool; [ .. | try verit_bool ; cvc4_bool; try verit_bool ; bool2prop ]). -Tactic Notation "smt_no_check" constr(h) := (prop2bool; [ .. | try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); cvc4_bool_no_check; try (prop2bool_hyps h; [ .. | verit_bool_no_check h ]); bool2prop]). -Tactic Notation "smt_no_check" := (prop2bool; [ .. | try verit_bool_no_check ; cvc4_bool_no_check; try verit_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]). |