diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-04 12:05:37 +0100 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-04 12:05:37 +0100 |
commit | efdfc6a501e42d8988e5c6be0ca17315a271253c (patch) | |
tree | f907ba80c3d9c2885f792529f725ab539f4af4a1 /src | |
parent | 75dff01782c3afdaea91841f69c734eb6ab9baf8 (diff) | |
download | smtcoq-efdfc6a501e42d8988e5c6be0ca17315a271253c.tar.gz smtcoq-efdfc6a501e42d8988e5c6be0ca17315a271253c.zip |
All veriT tests go through
Diffstat (limited to 'src')
-rw-r--r-- | src/SMTCoq.v | 2 | ||||
-rw-r--r-- | src/Tactics.v | 71 |
2 files changed, 70 insertions, 3 deletions
diff --git a/src/SMTCoq.v b/src/SMTCoq.v index f3904ae..6073c7e 100644 --- a/src/SMTCoq.v +++ b/src/SMTCoq.v @@ -15,4 +15,4 @@ Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances. Require Export Tactics. Export Atom Form Sat_Checker Cnf_Checker Euf_Checker. From Trakt Require Export Trakt. -Require Export Database_trakt. +Require Export Database_trakt Conversion. diff --git a/src/Tactics.v b/src/Tactics.v index 685cfdb..08668c3 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -18,12 +18,79 @@ Require Import SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances Declare ML Module "smtcoq_plugin". -Ltac zchaff := trakt Z bool; Tactics.zchaff_bool. -Ltac zchaff_no_check := trakt Z bool; Tactics.zchaff_bool_no_check. +(** Tactics in bool *) + +(* 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. + + +(* Tactics *) Tactic Notation "verit_bool_base_auto" constr(h) := verit_bool_base h; try (exact _). Tactic Notation "verit_bool_no_check_base_auto" constr(h) := verit_bool_no_check_base h; try (exact _). +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 := trakt Z bool; Tactics.zchaff_bool. +Ltac zchaff_no_check := trakt Z bool; Tactics.zchaff_bool_no_check. + Tactic Notation "verit" constr(global) := intros; unfold is_true in *; |