From 4a2ef2747950e8a28bfce7ca641bedd7ef71bea1 Mon Sep 17 00:00:00 2001 From: ckeller Date: Wed, 21 Apr 2021 09:46:30 +0200 Subject: Convert hypotheses from Prop to bool (#89) * This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed. * Some current limitations are detailed in src/PropToBool.v. * Partially enhances #30 . --- src/BoolToProp.v | 74 -------- src/PropToBool.v | 250 +++++++++++++++++++++++++++- src/SMTCoq.v | 2 +- src/classes/SMT_classes_instances.v | 1 + src/trace/coqTerms.ml | 25 ++- src/trace/coqTerms.mli | 4 + src/trace/smtMisc.ml | 2 +- src/verit/verit.ml | 10 ++ src/verit/verit.mli | 4 +- src/versions/standard/Tactics_standard.v | 40 ++--- src/versions/standard/_CoqProject | 1 - src/versions/standard/g_smtcoq_standard.ml4 | 4 +- 12 files changed, 304 insertions(+), 113 deletions(-) delete mode 100644 src/BoolToProp.v (limited to 'src') diff --git a/src/BoolToProp.v b/src/BoolToProp.v deleted file mode 100644 index 8a3b134..0000000 --- a/src/BoolToProp.v +++ /dev/null @@ -1,74 +0,0 @@ -(**************************************************************************) -(* *) -(* SMTCoq *) -(* Copyright (C) 2011 - 2019 *) -(* *) -(* See file "AUTHORS" for the list of authors *) -(* *) -(* This file is distributed under the terms of the CeCILL-C licence *) -(* *) -(**************************************************************************) - -Require Import - Bool ZArith BVList Logic BVList FArray - SMT_classes SMT_classes_instances ReflectFacts. -Import BVList.BITVECTOR_LIST. - -Local Coercion is_true : bool >-> Sortclass. - -Infix "--->" := implb (at level 60, right associativity) : bool_scope. -Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope. - -Ltac bool2prop := - repeat - match goal with - | [ |- forall _ : bitvector _, _] => intro - | [ |- forall _ : farray _ _, _] => intro - | [ |- forall _ : _ -> _, _] => intro - | [ |- forall _ : Z, _] => intro - | [ |- forall _ : bool, _] => intro - | [ |- forall _ : Type, _] => intro - | [ p: Type |- context[ forall _ : ?t, _ ] ] => intro - - | [ |- forall t : Type, CompDec t -> _ ] => intro - | [ |- CompDec _ -> _ ] => intro - - | [ |- context[ bv_ult _ _ ] ] => unfold is_true; rewrite bv_ult_B2P - | [ |- context[ bv_slt _ _ ] ] => unfold is_true; rewrite bv_slt_B2P - | [ |- context[ bv_eq _ _ ] ] => unfold is_true; rewrite bv_eq_reflect - | [ |- context[ equal _ _ ] ] => unfold is_true; rewrite equal_iff_eq - | [ |- context[ Z.ltb _ _ ] ] => unfold is_true; rewrite Z.ltb_lt - | [ |- context[ Z.gtb _ _ ] ] => unfold is_true; rewrite Z.gtb_lt - | [ |- context[ Z.leb _ _ ] ] => unfold is_true; rewrite Z.leb_le - | [ |- context[ Z.geb _ _ ] ] => unfold is_true; rewrite Z.geb_le - | [ |- context[ Z.eqb _ _ ] ] => unfold is_true; rewrite Z.eqb_eq - - | [ |- context[?G0 ---> ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true -> G1 = true) (G0 ---> G1)); - [ | apply implyP] - - | [ |- context[?G0 || ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (G0 || G1)); - [ | apply orP] - - | [ |- context[?G0 && ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (G0 && G1)); - [ | apply andP] - - | [ |- context[?G0 <---> ?G1 ] ] => - unfold is_true; rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (G0 <---> G1)); - [ | apply iffP] - - | [ |- context[ negb ?G ] ] => - unfold is_true; rewrite <- (@reflect_iff (G <> true) (negb G)); - [ | apply negP] - - | [R : CompDec ?t |- context[ CompDec ?t ] ] => exact R - - | [R : EqbType ?t |- context[ EqbType ?t ] ] => exact R - - | [ |- context[ false = true ] ] => rewrite FalseB - - | [ |- context[ true = true ] ] => rewrite TrueB - - end. diff --git a/src/PropToBool.v b/src/PropToBool.v index a9cbded..25662ad 100644 --- a/src/PropToBool.v +++ b/src/PropToBool.v @@ -13,7 +13,13 @@ Require Import Bool ZArith BVList Logic BVList FArray SMT_classes SMT_classes_instances ReflectFacts. -Import BVList.BITVECTOR_LIST. +Import BVList.BITVECTOR_LIST. + + +Lemma geb_ge (n m : Z) : (n >=? m)%Z = true <-> (n >= m)%Z. +Proof. + now rewrite Z.geb_le, Z.ge_le_iff. +Qed. Ltac prop2bool := repeat @@ -27,9 +33,9 @@ Ltac prop2bool := | [ |- context[ bv_ultP _ _ ] ] => rewrite <- bv_ult_B2P | [ |- context[ bv_sltP _ _ ] ] => rewrite <- bv_slt_B2P | [ |- context[ Z.lt _ _ ] ] => rewrite <- Z.ltb_lt - | [ |- context[ Z.gt _ _ ] ] => rewrite Z.gt_lt_iff; rewrite <- Z.ltb_lt + | [ |- context[ Z.gt _ _ ] ] => rewrite Zgt_is_gt_bool | [ |- context[ Z.le _ _ ] ] => rewrite <- Z.leb_le - | [ |- context[ Z.ge _ _ ] ] => rewrite Z.ge_le_iff; rewrite <- Z.leb_le + | [ |- context[ Z.ge _ _ ] ] => rewrite <- geb_ge | [ |- context[ Z.eq _ _ ] ] => rewrite <- Z.eqb_eq | [ |- context[ @Logic.eq ?t _ _ ] ] => @@ -77,7 +83,243 @@ Ltac prop2bool := | [ |- context[ True ] ] => rewrite <- TrueB | [ |- context[ False ] ] => rewrite <- FalseB + end. - (* | [ |- _ : (CompDec _ )] => try easy *) + +Ltac bool2prop_true := + repeat + match goal with + | [ |- forall _ : ?t, _ ] => + lazymatch type of t with + | Prop => fail + | _ => intro + end + + | [ |- context[ bv_ult _ _ = true ] ] => rewrite bv_ult_B2P + | [ |- context[ bv_slt _ _ = true ] ] => rewrite bv_slt_B2P + | [ |- context[ Z.ltb _ _ = true ] ] => rewrite Z.ltb_lt + | [ |- context[ Z.gtb _ _ ] ] => rewrite <- Zgt_is_gt_bool + | [ |- context[ Z.leb _ _ = true ] ] => rewrite Z.leb_le + | [ |- context[ Z.geb _ _ ] ] => rewrite geb_ge + | [ |- context[ Z.eqb _ _ = true ] ] => rewrite Z.eqb_eq + + | [ |- context[ eqb_of_compdec ?p _ _ = true ] ] => rewrite <- (@compdec_eq_eqb _ p) + + | [ |- context[ ?G0 || ?G1 = true ] ] => + rewrite <- (@reflect_iff (G0 = true \/ G1 = true) (orb G0 G1)); + [ | apply orP] + + | [ |- context[ implb ?G0 ?G1 = true ] ] => + rewrite <- (@reflect_iff (G0 = true -> G1 = true) (implb G0 G1)); + [ | apply implyP] + + | [ |- context[?G0 && ?G1 = true ] ] => + rewrite <- (@reflect_iff (G0 = true /\ G1 = true) (andb G0 G1)); + [ | apply andP] + + | [ |- context[Bool.eqb ?G0 ?G1 = true ] ] => + rewrite <- (@reflect_iff (G0 = true <-> G1 = true) (Bool.eqb G0 G1)); + [ | apply iffP] + + | [ |- context[ negb ?G = true ] ] => + rewrite <- (@reflect_iff (~ G = true) (negb G)); + [ | apply negP] + + | [ |- context[ true = true ] ] => rewrite TrueB + + | [ |- context[ false = true ] ] => rewrite FalseB end. +Ltac bool2prop := unfold is_true; bool2prop_true. + + +Ltac prop2bool_hyp H := + let TH := type of H in + + (* Add a CompDec hypothesis if needed *) + let prop2bool_t := fresh "prop2bool_t" in epose (prop2bool_t := ?[prop2bool_t_evar] : Type); + let prop2bool_comp := fresh "prop2bool_comp" in epose (prop2bool_comp := ?[prop2bool_comp_evar] : bool); + let H' := fresh in + assert (H':False -> TH); + [ let HFalse := fresh "HFalse" in intro HFalse; + repeat match goal with + | [ |- forall _ : ?t, _ ] => + lazymatch type of t with + | Prop => fail + | _ => intro + end + | [ |- context[@eq ?A _ _] ] => instantiate (prop2bool_t_evar := A); instantiate (prop2bool_comp_evar := true) + | _ => instantiate (prop2bool_t_evar := nat); instantiate (prop2bool_comp_evar := false) + end; + destruct HFalse + | ]; + clear H'; + match (eval compute in prop2bool_comp) with + | true => + let A := eval cbv in prop2bool_t in + match goal with + | [ _ : CompDec A |- _ ] => idtac + | _ => + let Hcompdec := fresh "Hcompdec" in + assert (Hcompdec: CompDec A); + [ auto with typeclass_instances | ] + end + | false => idtac + end; + clear prop2bool_t; clear prop2bool_comp; + + (* Compute the bool version of the lemma *) + [ .. | + let prop2bool_Hbool := fresh "prop2bool_Hbool" in epose (prop2bool_Hbool := ?[prop2bool_Hbool_evar] : Prop); + assert (H':False -> TH); + [ let HFalse := fresh "HFalse" in intro HFalse; + let rec tac_rec := + match goal with + | [ |- forall _ : ?t, _ ] => + lazymatch type of t with + | Prop => fail + | _ => + let H := fresh in + intro H; tac_rec; revert H + end + | _ => prop2bool + end in + tac_rec; + match goal with + | [ |- ?g ] => only [prop2bool_Hbool_evar]: refine g + end; + destruct HFalse + | ]; + clear H'; + + (* Assert and prove the bool version of the lemma *) + assert (H':prop2bool_Hbool); subst prop2bool_Hbool; + [ bool2prop; apply H | ]; + + (* Replace the Prop version with the bool version *) + clear H; assert (H:=H'); clear H' + ]. + +Ltac prop2bool_hyps Hs := + match Hs with + | (?Hs, ?H) => try prop2bool_hyp H; [ .. | prop2bool_hyps Hs] + | ?H => try prop2bool_hyp H + end. + + + +Section Test. + Variable A : Type. + + Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2. + Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z. + Hypothesis uninterpreted_type : forall (a:A), a = a. + + Goal True. + Proof. + prop2bool_hyp basic. + prop2bool_hyp no_eq. + prop2bool_hyp uninterpreted_type. + Abort. + + Goal True. + Proof. + prop2bool_hyps (basic, no_eq, uninterpreted_type). + Abort. +End Test. + +Section Group. + + Variable G : Type. + Variable HG : CompDec G. + Variable op : G -> G -> G. + Variable inv : G -> G. + Variable e : G. + + Hypothesis associative : + forall a b c : G, op a (op b c) = op (op a b) c. + Hypothesis identity : + forall a : G, (op e a = a) /\ (op a e = a). + Hypothesis inverse : + forall a : G, (op a (inv a) = e) /\ (op (inv a) a = e). + + Variable e' : G. + Hypothesis other_id : forall e' z, op e' z = z. + + Goal True. + Proof. + prop2bool_hyp associative. + prop2bool_hyp identity. + prop2bool_hyp inverse. + prop2bool_hyp other_id. + exact I. + Qed. + + Goal True. + Proof. + prop2bool_hyps (associative, identity, inverse, other_id). + exact I. + Qed. + +End Group. + + +Section MultipleCompDec. + + Variables A B : Type. + Hypothesis multiple : forall (a1 a2:A) (b1 b2:B), a1 = a2 -> b1 = b2. + + Goal True. + Proof. + Fail prop2bool_hyp multiple. + Abort. + +End MultipleCompDec. + + +(* We can assume that we deal only with monomorphic hypotheses, since + polymorphism will be removed before *) +Section Poly. + Hypothesis basic : forall (A:Type) (l1 l2:list A), + length (l1++l2) = length l1 + length l2. + Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a. + + Goal True. + Proof. + prop2bool_hyp basic. + Fail prop2bool_hyp uninterpreted_type. + Abort. + +End Poly. + + + + + +Infix "--->" := implb (at level 60, right associativity) : bool_scope. +Infix "<--->" := Bool.eqb (at level 60, right associativity) : bool_scope. + + + +(* Does not fail since 8.10 *) + +Goal True. + evar (t:Type). + assert (H:True). + - instantiate (t:=nat). exact I. + - exact I. +Qed. + +Goal True. + evar (t:option Set). + assert (H:True). + - instantiate (t:=Some nat). exact I. + - exact I. +Qed. + +Goal True. + evar (t:option Type). + assert (H:True). + - Fail instantiate (t:=Some nat). exact I. + - exact I. +Abort. diff --git a/src/SMTCoq.v b/src/SMTCoq.v index 6b69058..398d066 100644 --- a/src/SMTCoq.v +++ b/src/SMTCoq.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Export PropToBool BoolToProp. (* Before SMTCoq.State *) +Require Export PropToBool. Require Export Int63 List PArray. Require Export SMTCoq.State SMTCoq.SMT_terms SMTCoq.Trace SMT_classes_instances. Require Export Tactics. diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v index 89d6c62..50c02b7 100644 --- a/src/classes/SMT_classes_instances.v +++ b/src/classes/SMT_classes_instances.v @@ -764,6 +764,7 @@ End list. Hint Resolve unit_ord unit_eqbtype unit_comp unit_inh unit_compdec : typeclass_instances. Hint Resolve bool_ord bool_eqbtype bool_dec bool_comp bool_inh bool_compdec : typeclass_instances. Hint Resolve Z_ord Z_eqbtype Z_dec Z_comp Z_inh Z_compdec : typeclass_instances. +Hint Resolve Nat_ord Nat_eqbtype Nat_dec Nat_comp Nat_inh Nat_compdec : typeclass_instances. Hint Resolve Positive_ord Positive_eqbtype Positive_dec Positive_comp Positive_inh Positive_compdec : typeclass_instances. Hint Resolve BV_ord BV_eqbtype BV_dec BV_comp BV_inh BV_compdec : typeclass_instances. Hint Resolve FArray_ord FArray_eqbtype FArray_dec FArray_comp FArray_inh FArray_compdec : typeclass_instances. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index a6d0023..ca5f3cc 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -355,7 +355,6 @@ let rec mk_bv_list = function (* Reification *) - let mk_bool b = let c, args = Structures.decompose_app b in if Structures.eq_constr c (Lazy.force ctrue) then true @@ -435,3 +434,27 @@ let mk_bvsize n = else assert false | _ -> assert false else mk_N n + +(** Switches between constr and OCaml *) +(* Transform a option constr into a constr option *) +let option_of_constr_option co = + let c, args = Structures.decompose_app co in + if c = Lazy.force cSome then + match args with + | [_;c] -> Some c + | _ -> assert false + else + None + +(* Transform a tuple of constr into a (reversed) list of constr *) +let list_of_constr_tuple = + let rec list_of_constr_tuple acc t = + let c, args = Structures.decompose_app t in + if c = Lazy.force cpair then + match args with + | [_;_;t;l] -> list_of_constr_tuple (l::acc) t + | _ -> assert false + else + t::acc + in + list_of_constr_tuple [] diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli index bf626b3..b5ca6b7 100644 --- a/src/trace/coqTerms.mli +++ b/src/trace/coqTerms.mli @@ -261,3 +261,7 @@ val mk_nat : Structures.constr -> int val mk_N : Structures.constr -> int val mk_Z : Structures.constr -> int val mk_bvsize : Structures.constr -> int + +(* Switches between constr and OCaml *) +val option_of_constr_option : Structures.constr -> Structures.constr option +val list_of_constr_tuple : Structures.constr -> Structures.constr list diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml index 92f0f09..aad8b07 100644 --- a/src/trace/smtMisc.ml +++ b/src/trace/smtMisc.ml @@ -23,8 +23,8 @@ let mkInt i = (** Generic representation of shared object *) type 'a gen_hashed = { index : int; hval : 'a } -(** Functions over constr *) +(** Functions over constr *) let mklApp f args = Structures.mkApp (Lazy.force f, args) let string_of_name_def d n = try Structures.string_of_name n with | _ -> d diff --git a/src/verit/verit.ml b/src/verit/verit.ml index fbc04e3..3080372 100644 --- a/src/verit/verit.ml +++ b/src/verit/verit.ml @@ -218,6 +218,16 @@ let verit_logic = SL.of_list [LUF; LLia] let tactic_gen vm_cast lcpl lcepl = + (* Transform the tuple of lemmas given by the user into a list *) + let lcpl = + let lcpl = EConstr.Unsafe.to_constr lcpl in + let lcpl = CoqTerms.option_of_constr_option lcpl in + match lcpl with + | Some lcpl -> CoqTerms.list_of_constr_tuple lcpl + | None -> [] + in + + (* Core tactic *) clear_all (); let rt = SmtBtype.create () in let ro = Op.create () in diff --git a/src/verit/verit.mli b/src/verit/verit.mli index 6fa62d8..4b84b58 100644 --- a/src/verit/verit.mli +++ b/src/verit/verit.mli @@ -19,5 +19,5 @@ val parse_certif : val checker : string -> string -> unit val checker_debug : string -> string -> unit val theorem : Structures.id -> string -> string -> unit -val tactic : Structures.constr list -> Structures.constr_expr list -> Structures.tactic -val tactic_no_check : Structures.constr list -> Structures.constr_expr list -> Structures.tactic +val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic +val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic diff --git a/src/versions/standard/Tactics_standard.v b/src/versions/standard/Tactics_standard.v index 4162f13..6ddf5a5 100644 --- a/src/versions/standard/Tactics_standard.v +++ b/src/versions/standard/Tactics_standard.v @@ -10,18 +10,18 @@ (**************************************************************************) -Require Import PropToBool BoolToProp. (* Before SMTCoq.State *) +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". -Tactic Notation "verit_bool" constr_list(h) := - verit_bool_base h; vauto. +Tactic Notation "verit_bool" constr(h) := verit_bool_base (Some h); vauto. +Tactic Notation "verit_bool" := verit_bool_base (@None nat); vauto. -Tactic Notation "verit_bool_no_check" constr_list(h) := - verit_bool_no_check_base h; vauto. +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. (** Tactics in Prop **) @@ -29,32 +29,18 @@ Tactic Notation "verit_bool_no_check" constr_list(h) := Ltac zchaff := prop2bool; zchaff_bool; bool2prop. Ltac zchaff_no_check := prop2bool; zchaff_bool_no_check; bool2prop. -Tactic Notation "verit" constr_list(h) := prop2bool; [ .. | verit_bool h; bool2prop ]. -Tactic Notation "verit_no_check" constr_list(h) := prop2bool; [ .. | verit_bool_no_check h; 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 ]. Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. - -(* Ltac smt := prop2bool; *) -(* repeat *) -(* match goal with *) -(* | [ |- context[ CompDec ?t ] ] => try assumption *) -(* | [ |- _ : bool] => verit_bool *) -(* | [ |- _ : bool] => try (cvc4_bool; verit_bool) *) -(* end; *) -(* bool2prop. *) -(* Ltac smt_no_check := prop2bool; *) -(* repeat *) -(* match goal with *) -(* | [ |- context[ CompDec ?t ] ] => try assumption *) -(* | [ |- _ : bool] => verit_bool_no_check *) -(* | [ |- _ : bool] => try (cvc4_bool_no_check; verit_bool_no_check) *) -(* end; *) -(* bool2prop. *) - -Tactic Notation "smt" constr_list(h) := (prop2bool; [ .. | try verit_bool h; cvc4_bool; try verit_bool h; bool2prop ]). -Tactic Notation "smt_no_check" constr_list(h) := (prop2bool; [ .. | try verit_bool_no_check h; cvc4_bool_no_check; try verit_bool_no_check h; 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]). diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject index e067da8..86dd443 100644 --- a/src/versions/standard/_CoqProject +++ b/src/versions/standard/_CoqProject @@ -149,7 +149,6 @@ Misc.v SMTCoq.v ReflectFacts.v PropToBool.v -BoolToProp.v QInst.v Tactics.v SMT_terms.v diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 index 6c3b8cf..2411316 100644 --- a/src/versions/standard/g_smtcoq_standard.ml4 +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -109,8 +109,8 @@ END TACTIC EXTEND Tactic_verit -| [ "verit_bool_base" constr_list(lpl) ] -> [ Verit.tactic (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ] -| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ Verit.tactic_no_check (List.map EConstr.Unsafe.to_constr lpl) (get_lemmas ()) ] +| [ "verit_bool_base" constr(lpl) ] -> [ Verit.tactic lpl (get_lemmas ()) ] +| [ "verit_bool_no_check_base" constr(lpl) ] -> [ Verit.tactic_no_check lpl (get_lemmas ()) ] END TACTIC EXTEND Tactic_cvc4 -- cgit