simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

proofs: remove with_defs

Browse source
This commit is contained in:
Simon Cruanes 2021-05-07 18:31:51 -04:00
parent e90b3ec76b
commit 7507a7f0b1
3 changed files with 6 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/base-term/Proof.ml
View file

@ -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) =

1
src/core/Sidekick_core.ml
View file

@ -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] *)

12
src/th-bool-static/Sidekick_th_bool_static.ml
View file

@ -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 =