diff options
Diffstat (limited to 'src/versions/standard/Tactics_standard.v')
-rw-r--r-- | src/versions/standard/Tactics_standard.v | 157 |
1 files changed, 0 insertions, 157 deletions
diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v deleted file mode 100644 index f79b253..0000000 --- a/src/versions/standard/Tactics_standard.v +++ /dev/null @@ -1,157 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 k := - match goal with - | [ H : ?P |- _ ] => - let T := type of P in - lazymatch 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_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) := - get_hyps ltac:(fun Hs => - 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" := - get_hyps ltac:(fun Hs => verit_bool_base_auto 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_auto (Some (h, Hs)) - | None => verit_bool_no_check_base_auto (Some h) - end; - vauto). -Tactic Notation "verit_bool_no_check" := - get_hyps ltac:(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; - [ .. | get_hyps ltac:(fun Hs => - 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; - [ .. | get_hyps ltac:(fun Hs => - 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; - [ .. | get_hyps ltac:(fun Hs => - 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; - [ .. | get_hyps ltac:(fun Hs => - 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: -*) |