From 7507a7f0b11c325fb1d8bfec538e9b1d388f0daa Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 7 May 2021 18:31:51 -0400 Subject: [PATCH] proofs: remove `with_defs` --- src/base-term/Proof.ml | 5 ----- src/core/Sidekick_core.ml | 1 - src/th-bool-static/Sidekick_th_bool_static.ml | 12 ++++++------ 3 files changed, 6 insertions(+), 12 deletions(-) diff --git a/src/base-term/Proof.ml b/src/base-term/Proof.ml index b9ed732a..ea8c3852 100644 --- a/src/base-term/Proof.ml +++ b/src/base-term/Proof.ml @@ -52,7 +52,6 @@ type t = | Bool_c of clause (* boolean tautology *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term - | With_def of term list * t (* [with_def ts p] is [p] using definitions of [ts] *) | LRA of clause | Composite of { (* some named (atomic) assumptions *) @@ -111,7 +110,6 @@ let cc_imply2 h1 h2 t u : t = CC_lemma_imply ([h1; h2], t, u) let assertion t = Assertion t let assertion_c c = Assertion_c (Iter.to_rev_list c) let assertion_c_l c = Assertion_c c -let with_defs ts p = match ts with [] -> p | _ -> With_def (ts, p) let composite_a ?(assms=[]) steps : t = Composite {assumptions=assms; steps} let composite_l ?(assms=[]) steps : t = @@ -166,7 +164,6 @@ let iter_p (p:t) ~f_t ~f_step ~f_clause ~f_p : unit = | Bool_eq (t, u) -> f_t t; f_t u | Bool_c c -> f_clause c | Ite_true t | Ite_false t -> f_t t - | With_def (ts, p) -> List.iter f_t ts; f_p p | LRA c -> f_clause c | Composite { assumptions; steps } -> List.iter (fun (_,lit) -> iter_lit ~f_t lit) assumptions; @@ -319,8 +316,6 @@ module Quip = struct i Cstor.pp c (pp_l pp_t) ts Cstor.pp c (pp_l pp_t) us | Ite_true t -> Fmt.fprintf out "(@[ite-true@ %a@])" pp_t t | Ite_false t -> Fmt.fprintf out "(@[ite-false@ %a@])" pp_t t - | With_def (ts,p) -> - Fmt.fprintf out "(@[with-defs (@[%a@])@ %a@])" (pp_l pp_t) ts pp_rec p | LRA c -> Fmt.fprintf out "(@[lra@ %a@])" pp_cl c | Composite {steps; assumptions} -> let pp_ass out (n,a) = diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml index f5063462..96cea297 100644 --- a/src/core/Sidekick_core.ml +++ b/src/core/Sidekick_core.ml @@ -195,7 +195,6 @@ module type PROOF = sig val refl : term -> t (* proof of [| t=t] *) val true_is_true : t (* proof of [|- true] *) val true_neq_false : t (* proof of [|- not (true=false)] *) - val with_defs : term list -> t -> t (* proof under definition of given terms *) val cc_lemma : lit Iter.t -> t (* equality tautology, unsigned *) val cc_imply2 : t -> t -> term -> term -> t (* tautology [p1, p2 |- t=u] *) val cc_imply_l : t list -> term -> term -> t (* tautology [hyps |- t=u] *) diff --git a/src/th-bool-static/Sidekick_th_bool_static.ml b/src/th-bool-static/Sidekick_th_bool_static.ml index 5809ecac..67435845 100644 --- a/src/th-bool-static/Sidekick_th_bool_static.ml +++ b/src/th-bool-static/Sidekick_th_bool_static.ml @@ -198,20 +198,20 @@ module Make(A : ARG) : S with module A = A = struct SI.define_const si ~const:t_ite ~rhs:t; let lit_a = mk_lit a in add_clause [Lit.neg lit_a; mk_lit (eq self.tst t_ite b)] - SI.P.(with_defs [t_ite] (A.proof_ite_true t)); + (A.proof_ite_true t); add_clause [lit_a; mk_lit (eq self.tst t_ite c)] - SI.P.(with_defs [t_ite] (A.proof_ite_false t)); - Some (t_ite, SI.P.(with_defs [t_ite] (refl t))) + (A.proof_ite_false t); + Some (t_ite, SI.P.(refl t)) end | _ -> None let[@inline] pr_lit lit = SI.P.(lit_st (Lit.signed_term lit)) - let[@inline] pr_def_refl proxy t = SI.P.(with_defs [proxy] (refl t)) + let[@inline] pr_def_refl _proxy t = SI.P.(refl t) (* prove clause [l] by boolean lemma *) - let pr_bool_c proxy l : SI.P.t = + let pr_bool_c _proxy l : SI.P.t = let cl = List.rev_map pr_lit l in - SI.P.(with_defs [proxy] (A.proof_bool_c cl)) + (A.proof_bool_c cl) (* TODO: polarity? *) let cnf (self:state) (si:SI.t) ~mk_lit ~add_clause (t:T.t) : (T.t * SI.P.t) option =