wip: proof production (incl. better tracking of proofs in CC)

src/cc/Sidekick_cc.ml

@@ -96,7 +96,7 @@ module Make (A: CC_ARG)
     | E_merge_t of term * term
     | E_congruence of node * node (* caused by normal congruence *)
     | E_and of explanation * explanation
-    | E_theory of explanation
+    | E_theory of proof_step * explanation list
 
   type repr = node
 
@@ -167,7 +167,7 @@ module Make (A: CC_ARG)
       | E_congruence (n1,n2) -> Fmt.fprintf out "(@[congruence@ %a@ %a@])" N.pp n1 N.pp n2
       | E_merge (a,b) -> Fmt.fprintf out "(@[merge@ %a@ %a@])" N.pp a N.pp b
       | E_merge_t (a,b) -> Fmt.fprintf out "(@[<hv>merge@ @[:n1 %a@]@ @[:n2 %a@]@])" Term.pp a Term.pp b
-      | E_theory e -> Fmt.fprintf out "(@[th@ %a@])" pp e
+      | E_theory (_p,es) -> Fmt.fprintf out "(@[th@ %a@])" (Util.pp_list pp) es
       | E_and (a,b) ->
         Format.fprintf out "(@[<hv1>and@ %a@ %a@])" pp a pp b
 
@@ -176,7 +176,7 @@ module Make (A: CC_ARG)
     let[@inline] mk_merge a b : t = if N.equal a b then mk_reduction else E_merge (a,b)
     let[@inline] mk_merge_t a b : t = if Term.equal a b then mk_reduction else E_merge_t (a,b)
     let[@inline] mk_lit l : t = E_lit l
-    let mk_theory e = E_theory e
+    let[@inline] mk_theory p es = E_theory (p,es)
 
     let rec mk_list l =
       match l with
@@ -242,6 +242,7 @@ module Make (A: CC_ARG)
   type t = {
     tst: term_store;
     tbl: node T_tbl.t;
+    proof: proof;
     (* internalization [term -> node] *)
     signatures_tbl : node Sig_tbl.t;
     (* map a signature to the corresponding node in some equivalence class.
@@ -288,6 +289,7 @@ module Make (A: CC_ARG)
   let[@inline] n_false cc = Lazy.force cc.false_
   let n_bool cc b = if b then n_true cc else n_false cc
   let[@inline] term_store cc = cc.tst
+  let[@inline] proof cc = cc.proof
   let allocate_bitfield ~descr cc =
     Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr);
     Bits.mk_field cc.bitgen
@@ -456,8 +458,16 @@ module Make (A: CC_ARG)
           assert false
       end
     | E_lit lit -> lit :: acc
-    | E_theory e' ->
+    | E_theory (_pr, sub_l) ->
-      th := true; explain_decompose_expl cc ~th acc e'
+      (* FIXME: use pr as a subproof. We need to accumulate subproofs too, because
+         there is some amount of resolution done inside the congruence closure
+         itself to resolve Horn clauses produced by theories.
+
+         maybe we need to store [t=u] where [pr] is the proof of [Gamma |- t=u],
+         add [t=u] to the explanation, and use a subproof to resolve
+         it away using [pr] and add [Gamma] to the mix *)
+      th := true;
+      List.fold_left (explain_decompose_expl cc ~th) acc sub_l
     | E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b
     | E_merge_t (a,b) ->
       (* find nodes for [a] and [b] on the fly *)
@@ -878,12 +888,12 @@ module Make (A: CC_ARG)
       ?(on_pre_merge=[]) ?(on_post_merge=[]) ?(on_new_term=[])
       ?(on_conflict=[]) ?(on_propagate=[]) ?(on_is_subterm=[])
       ?(size=`Big)
-      (tst:term_store) : t =
+      (tst:term_store) (proof:proof) : t =
     let size = match size with `Small -> 128 | `Big -> 2048 in
     let bitgen = Bits.mk_gen () in
     let field_marked_explain = Bits.mk_field bitgen in
     let rec cc = {
-      tst;
+      tst; proof;
       tbl = T_tbl.create size;
       signatures_tbl = Sig_tbl.create size;
       bitgen;

src/core/Sidekick_core.ml

@@ -230,6 +230,10 @@ module type PROOF = sig
       and [p2] proves [C \/ t], is the rule that produces [C \/ u],
       i.e unit paramodulation. *)
 
+  val with_defs : proof_step -> proof_step Iter.t -> proof_rule
+  (** [with_defs pr defs] specifies that [pr] is valid only in
+      a context where the definitions [defs] are present. *)
+
   val lemma_true : term -> proof_rule
   (** [lemma_true (true) p] asserts the clause [(true)] *)
 
@@ -244,9 +248,9 @@ module type PROOF = sig
       From now on, [t] and [u] will be used interchangeably.
       @return a proof_rule ID for the clause [(t=u)]. *)
 
-  val lemma_rw_clause : proof_step -> lit_rw:proof_step Iter.t -> proof_rule
+  val lemma_rw_clause : proof_step -> using:proof_step Iter.t -> proof_rule
-  (** [lemma_rw_clause prc ~lit_rw], where [prc] is the proof of [|- c],
+  (** [lemma_rw_clause prc ~using], where [prc] is the proof of [|- c],
-      uses the equations [|- p_i = q_i] from [lit_rw]
+      uses the equations [|- p_i = q_i] from [using]
       to rewrite some literals of [c] into [c']. This is used to preprocess
       literals of a clause (using {!lemma_preprocess} individually). *)
 end
@@ -476,7 +480,14 @@ module type CC_S = sig
     val mk_merge_t : term -> term -> t
     val mk_lit : lit -> t
     val mk_list : t list -> t
-    val mk_theory : t -> t (* TODO: indicate what theory, or even provide a lemma *)
+    val mk_theory : proof_step -> t list -> t
+    (* FIXME: this should probably take [t, u, proof(Gamma |- t=u), expls],
+       where [expls] is a list of explanation of the equations in [Gamma].
+
+       For example for the lemma [a=b] deduced by injectivity from [Some a=Some b]
+       in the theory of datatypes,
+       the arguments would be [a, b, proof(Some a=Some b |- a=b), e0]
+       where [e0] is an explanation of [Some a=Some b] *)
   end
 
   type node = N.t
@@ -491,6 +502,8 @@ module type CC_S = sig
 
   val term_store : t -> term_store
 
+  val proof : t -> proof
+
   val find : t -> node -> repr
   (** Current representative *)
 
@@ -547,6 +560,7 @@ module type CC_S = sig
     ?on_is_subterm:ev_on_is_subterm list ->
     ?size:[`Small | `Big] ->
     term_store ->
+    proof ->
     t
   (** Create a new congruence closure.
 
@@ -709,13 +723,6 @@ module type SOLVER_INTERNAL = sig
 
   type lit = Lit.t
 
-  (** {3 Proof helpers} *)
-
-  val define_const : t -> const:term -> rhs:term -> unit
-  (** [define_const si ~const ~rhs] adds the definition [const := rhs]
-      to the (future) proof. [const] should be a fresh constant that
-      occurs nowhere else, and [rhs] a term defined without [const]. *)
-
   (** {3 Congruence Closure} *)
 
   (** Congruence closure instance *)
@@ -723,6 +730,7 @@ module type SOLVER_INTERNAL = sig
     with module T = T
      and module Lit = Lit
      and type proof = proof
+     and type proof_step = proof_step
      and type P.t = proof
      and type P.lit = lit
      and type Actions.t = theory_actions

src/lra/sidekick_arith_lra.ml

@@ -60,7 +60,7 @@ module type ARG = sig
   val has_ty_real : term -> bool
   (** Does this term have the type [Real] *)
 
-  val lemma_lra : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_lra : S.Lit.t Iter.t -> S.P.proof_rule
 
   module Gensym : sig
     type t
@@ -82,6 +82,7 @@ module type S = sig
   type state
 
   val create : ?stat:Stat.t ->
+    A.S.P.t ->
     A.S.T.Term.store ->
     A.S.T.Ty.store ->
     state
@@ -140,6 +141,7 @@ module Make(A : ARG) : S with module A = A = struct
   type state = {
     tst: T.store;
     ty_st: Ty.store;
+    proof: SI.P.t;
     simps: T.t T.Tbl.t; (* cache *)
     gensym: A.Gensym.t;
     encoded_eqs: unit T.Tbl.t; (* [a=b] gets clause [a = b <=> (a >= b /\ a <= b)] *)
@@ -150,8 +152,9 @@ module Make(A : ARG) : S with module A = A = struct
     stat_th_comb: int Stat.counter;
   }
 
-  let create ?(stat=Stat.create()) tst ty_st : state =
+  let create ?(stat=Stat.create()) proof tst ty_st : state =
     { tst; ty_st;
+      proof;
       simps=T.Tbl.create 128;
       gensym=A.Gensym.create tst;
       encoded_eqs=T.Tbl.create 8;
@@ -232,18 +235,25 @@ module Make(A : ARG) : S with module A = A = struct
         );
         proxy
 
-  let add_clause_lra_ (module PA:SI.PREPROCESS_ACTS) lits =
+  let add_clause_lra_ ?using (module PA:SI.PREPROCESS_ACTS) lits =
-    let pr = A.lemma_lra (Iter.of_list lits) in
+    let pr = A.lemma_lra (Iter.of_list lits) PA.proof in
+    let pr = match using with
+      | None -> pr
+      | Some using -> SI.P.lemma_rw_clause pr ~using PA.proof in
     PA.add_clause lits pr
 
   (* preprocess linear expressions away *)
   let preproc_lra (self:state) si (module PA:SI.PREPROCESS_ACTS)
-      (t:T.t) : T.t option =
+      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     Log.debugf 50 (fun k->k "(@[lra.preprocess@ %a@])" T.pp t);
     let tst = SI.tst si in
 
     (* preprocess subterm *)
-    let preproc_t t = SI.preprocess_term si (module PA) t in
+    let preproc_t ~steps t =
+      let u, pr = SI.preprocess_term si (module PA) t in
+      CCOpt.iter (fun s -> steps := s :: !steps) pr;
+      u
+    in
 
     (* tell the CC this term exists *)
     let declare_term_to_cc t =
@@ -262,9 +272,9 @@ module Make(A : ARG) : S with module A = A = struct
         T.Tbl.add self.encoded_eqs t ();
 
         (* encode [t <=> (u1 /\ u2)] *)
-        let lit_t = PA.mk_lit t in
+        let lit_t = PA.mk_lit_nopreproc t in
-        let lit_u1 = PA.mk_lit u1 in
+        let lit_u1 = PA.mk_lit_nopreproc u1 in
-        let lit_u2 = PA.mk_lit u2 in
+        let lit_u2 = PA.mk_lit_nopreproc u2 in
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u1];
         add_clause_lra_ (module PA) [SI.Lit.neg lit_t; lit_u2];
         add_clause_lra_ (module PA)
@@ -273,8 +283,9 @@ module Make(A : ARG) : S with module A = A = struct
       None
 
     | LRA_pred (pred, t1, t2) ->
-      let l1 = as_linexp ~f:preproc_t t1 in
+      let steps = ref [] in
-      let l2 = as_linexp ~f:preproc_t t2 in
+      let l1 = as_linexp ~f:(preproc_t ~steps) t1 in
+      let l2 = as_linexp ~f:(preproc_t ~steps) t2 in
       let le = LE.(l1 - l2) in
       let le_comb, le_const = LE.comb le, LE.const le in
       let le_const = A.Q.neg le_const in
@@ -284,6 +295,8 @@ module Make(A : ARG) : S with module A = A = struct
         | None, _ ->
           (* non trivial linexp, give it a fresh name in the simplex *)
           let proxy = var_encoding_comb self ~pre:"_le" le_comb in
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
           declare_term_to_cc proxy;
 
           let op =
@@ -297,14 +310,13 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (proxy, op, le_const)) in
           begin
-            let lit = PA.mk_lit new_t in
+            let lit = PA.mk_lit_nopreproc new_t in
             let constr = SimpSolver.Constraint.mk proxy op le_const in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess:@ %a@ :into %a" T.pp t T.pp new_t);
-          (* FIXME: emit proof: by def proxy + LRA *)
+          Some (new_t, Iter.of_list !steps)
-          Some new_t
 
         | Some (coeff, v), pred ->
           (* [c . v <= const] becomes a direct simplex constraint [v <= const/c] *)
@@ -323,28 +335,31 @@ module Make(A : ARG) : S with module A = A = struct
 
           let new_t = A.mk_lra tst (LRA_simplex_pred (v, op, q)) in
           begin
-            let lit = PA.mk_lit new_t in
+            let lit = PA.mk_lit_nopreproc new_t in
             let constr = SimpSolver.Constraint.mk v op q in
             SimpSolver.declare_bound self.simplex constr (Tag.Lit lit);
           end;
 
           Log.debugf 10 (fun k->k "lra.preprocess@ :%a@ :into %a" T.pp t T.pp new_t);
-          (* FIXME: preprocess proof *)
+          Some (new_t, Iter.of_list !steps)
-          Some new_t
       end
 
     | LRA_op _ | LRA_mult _ ->
-      let le = as_linexp ~f:preproc_t t in
+      let steps = ref [] in
+      let le = as_linexp ~f:(preproc_t ~steps) t in
       let le_comb, le_const = LE.comb le, LE.const le in
 
       if A.Q.(le_const = zero) then (
         (* if there is no constant, define [proxy] as [proxy := le_comb] and
            return [proxy] *)
         let proxy = var_encoding_comb self ~pre:"_le" le_comb in
+        begin
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
+        end;
         declare_term_to_cc proxy;
 
-        (* FIXME: proof by def of proxy *)
+        Some (proxy, Iter.of_list !steps)
-        Some proxy
       ) else (
         (* a bit more complicated: we cannot just define [proxy := le_comb]
            because of the coefficient.
@@ -352,7 +367,14 @@ module Make(A : ARG) : S with module A = A = struct
            variable [proxy2 := le_comb - proxy]
            and asserting [proxy2 = -le_const] *)
         let proxy = fresh_term self ~pre:"_le" (T.ty t) in
+        begin
+          let pr_def = SI.P.define_term proxy t PA.proof in
+          steps := pr_def :: !steps;
+        end;
         let proxy2 = fresh_term self ~pre:"_le_diff" (T.ty t) in
+        let pr_def2 =
+          SI.P.define_term proxy (A.mk_lra tst (LRA_op (Minus, t, proxy))) PA.proof
+        in
 
         SimpSolver.add_var self.simplex proxy;
         LE_.Comb.iter (fun v _ -> SimpSolver.add_var self.simplex v) le_comb;
@@ -367,29 +389,39 @@ module Make(A : ARG) : S with module A = A = struct
         declare_term_to_cc proxy;
         declare_term_to_cc proxy2;
 
-        PA.add_clause [
+        add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
-          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
+          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Leq, A.Q.neg le_const)))
-        ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
+        ];
-        PA.add_clause [
+        add_clause_lra_ ~using:Iter.(return pr_def2) (module PA) [
-          PA.mk_lit (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
+          PA.mk_lit_nopreproc (A.mk_lra tst (LRA_simplex_pred (proxy2, Geq, A.Q.neg le_const)))
-        ] (fun _ -> ()); (* TODO: by-def proxy2 + LRA *)
+        ];
 
-        (* FIXME: actual proof *)
+        Some (proxy, Iter.of_list !steps)
-        Some proxy
       )
 
     | LRA_other t when A.has_ty_real t -> None
     | LRA_const _ | LRA_simplex_pred _ | LRA_simplex_var _ | LRA_other _ ->
       None
 
-  let simplify (self:state) (_recurse:_) (t:T.t) : T.t option =
+  let simplify (self:state) (_recurse:_) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+
+    let proof_eq t u =
+      A.lemma_lra
+        (Iter.return (SI.Lit.atom self.tst (A.mk_eq self.tst t u))) self.proof
+    in
+    let proof_bool t ~sign:b =
+      let lit = SI.Lit.atom ~sign:b self.tst t in
+      A.lemma_lra (Iter.return lit) self.proof
+    in
+
     match A.view_as_lra t with
     | LRA_op _ | LRA_mult _ ->
       let le = as_linexp_id t in
       if LE.is_const le then (
         let c = LE.const le in
-        (* FIXME: proof *)
+        let u = A.mk_lra self.tst (LRA_const c) in
-        Some (A.mk_lra self.tst (LRA_const c))
+        let pr = proof_eq t u in
+        Some (u, Iter.return pr)
       ) else None
     | LRA_pred (pred, l1, l2) ->
       let le = LE.(as_linexp_id l1 - as_linexp_id l2) in
@@ -403,8 +435,9 @@ module Make(A : ARG) : S with module A = A = struct
           | Eq -> A.Q.(c = zero)
           | Neq -> A.Q.(c <> zero)
         in
-        (* FIXME: proof *)
+        let u = A.mk_bool self.tst is_true in
-        Some (A.mk_bool self.tst is_true)
+        let pr = proof_bool t ~sign:is_true in
+        Some (u, Iter.return pr)
       ) else None
     | _ -> None
 
@@ -418,7 +451,7 @@ module Make(A : ARG) : S with module A = A = struct
       |> CCList.flat_map (Tag.to_lits si)
       |>  List.rev_map SI.Lit.neg
     in
-    let pr = A.lemma_lra (Iter.of_list confl) in
+    let pr = A.lemma_lra (Iter.of_list confl) (SI.proof si) in
     SI.raise_conflict si acts confl pr
 
   let on_propagate_ si acts lit ~reason =
@@ -428,7 +461,7 @@ module Make(A : ARG) : S with module A = A = struct
       SI.propagate si acts lit
         ~reason:(fun() ->
            let lits = CCList.flat_map (Tag.to_lits si) reason in
-           let pr = A.lemma_lra Iter.(cons lit (of_list lits)) in
+           let pr = A.lemma_lra Iter.(cons lit (of_list lits)) (SI.proof si) in
            CCList.flat_map (Tag.to_lits si) reason, pr)
     | _ -> ()
 
@@ -604,7 +637,7 @@ module Make(A : ARG) : S with module A = A = struct
   let create_and_setup si =
     Log.debug 2 "(th-lra.setup)";
     let stat = SI.stats si in
-    let st = create ~stat (SI.tst si) (SI.ty_st si) in
+    let st = create ~stat (SI.proof si) (SI.tst si) (SI.ty_st si) in
     SI.add_simplifier si (simplify st);
     SI.on_preprocess si (preproc_lra st);
     SI.on_final_check si (final_check_ st);

src/smt-solver/Sidekick_smt_solver.ml

@@ -235,9 +235,6 @@ module Make(A : ARG)
     let[@inline] proof self = self.proof
     let stats t = t.stat
 
-    let define_const (self:t) ~const ~rhs : unit =
-      self.t_defs <- (const,rhs) :: self.t_defs
-
     let simplifier self = self.simp
     let simplify_t self (t:Term.t) : _ option = Simplify.normalize self.simp t
     let simp_t self (t:Term.t) : Term.t * _ = Simplify.normalize_t self.simp t
@@ -397,8 +394,7 @@ module Make(A : ARG)
             let steps = ref [] in
             let c' = CCList.map (preprocess_lit ~steps) c in
             let pr_c' =
-              if !steps=[] then pr_c
+              A.P.lemma_rw_clause pr_c ~using:(Iter.of_list !steps) proof
-              else A.P.lemma_rw_clause pr_c ~lit_rw:(Iter.of_list !steps) proof
             in
             A0.add_clause c' pr_c'
 
@@ -459,10 +455,7 @@ module Make(A : ARG)
       let pacts = preprocess_acts_of_acts self acts in
       let c = CCList.map (preprocess_lit_ ~steps self pacts) c in
       let pr =
-        if !steps=[] then proof
+        P.lemma_rw_clause proof ~using:(Iter.of_list !steps) self.proof
-        else (
-          P.lemma_rw_clause proof ~lit_rw:(Iter.of_list !steps) self.proof
-        )
       in
       c, pr
 
@@ -785,9 +778,7 @@ module Make(A : ARG)
     (* TODO: if c != c0 then P.emit_redundant_clause c
        because we jsut preprocessed it away? *)
     let pr = P.emit_input_clause (Iter.of_list c) self.proof in
-    let pr = if !steps=[] then pr
+    let pr = P.lemma_rw_clause pr ~using:(Iter.of_list !steps) self.proof in
-      else P.lemma_rw_clause pr ~lit_rw:(Iter.of_list !steps) self.proof
-    in
     add_clause_l self c pr
 
   let assert_term self t = assert_terms self [t]

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -46,11 +46,11 @@ module type ARG = sig
   val lemma_bool_equiv : term -> term -> S.P.proof_rule
   (** Boolean tautology lemma (equivalence) *)
 
-  val lemma_ite_true : a:term -> ite:term -> S.P.proof_rule
+  val lemma_ite_true : ite:term -> S.P.proof_rule
-  (** lemma [a => ite a b c = b] *)
+  (** lemma [a ==> ite a b c = b] *)
 
-  val lemma_ite_false : a:term -> ite:term -> S.P.proof_rule
+  val lemma_ite_false : ite:term -> S.P.proof_rule
-  (** lemma [¬a => ite a b c = c] *)
+  (** lemma [¬a ==> ite a b c = c] *)
 
   (** Fresh symbol generator.
 
@@ -118,6 +118,8 @@ module Make(A : ARG) : S with module A = A = struct
 
   let simplify (self:state) (simp:SI.Simplify.t) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     let tst = self.tst in
+
+    let proof = SI.Simplify.proof simp in
     let steps = ref [] in
     let add_step_ s = steps := s :: !steps in
 
@@ -155,11 +157,15 @@ module Make(A : ARG) : S with module A = A = struct
       CCOpt.iter add_step_ prf_a;
       begin match A.view_as_bool a with
         | B_bool true ->
-          add_step_ @@ A.lemma_ite_true ~a ~ite:t @@ SI.Simplify.proof simp;
+          add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a)
+            (A.lemma_ite_true ~ite:t proof) proof;
           ret b
+
         | B_bool false ->
-          add_step_ @@ A.lemma_ite_false ~a ~ite:t @@ SI.Simplify.proof simp;
+          add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt prf_a)
+            (A.lemma_ite_false ~ite:t proof) proof;
           ret c
+
         | _ ->
           None
       end
@@ -195,7 +201,8 @@ module Make(A : ARG) : S with module A = A = struct
   let pr_p1 p s1 s2 = SI.P.proof_p1 s1 s2 p
 
   (* preprocess "ite" away *)
-  let preproc_ite self si (module PA:SI.PREPROCESS_ACTS) (t:T.t) : (T.t * SI.proof_step Iter.t) option =
+  let preproc_ite self si (module PA:SI.PREPROCESS_ACTS)
+      (t:T.t) : (T.t * SI.proof_step Iter.t) option =
     let steps = ref [] in
     let add_step_ s = steps := s :: !steps in
 
@@ -207,25 +214,27 @@ module Make(A : ARG) : S with module A = A = struct
       CCOpt.iter add_step_ pr_a;
       begin match A.view_as_bool a' with
         | B_bool true ->
-          (* [a=true |- ite a b c=b], [|- a=true] ==> [|- t=b] *)
+          (* [a |- ite a b c=b],  [a=true] implies [ite a b c=b] *)
-          add_step_ @@ A.lemma_ite_true ~a:a' ~ite:t PA.proof;
+          add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a)
+            (A.lemma_ite_true ~ite:t PA.proof) PA.proof;
           ret b
+
         | B_bool false ->
-          (* [a=false |- ite a b c=c], [|- a=false] ==> [|- t=c] *)
+          (* [¬a |- ite a b c=c],  [a=false] implies [ite a b c=c] *)
-          add_step_ @@ A.lemma_ite_false ~a:a' ~ite:t PA.proof;
+          add_step_ @@ SI.P.lemma_rw_clause ~using:(Iter.of_opt pr_a)
+            (A.lemma_ite_false ~ite:t PA.proof) PA.proof;
           ret c
+
         | _ ->
           let t_ite = fresh_term self ~for_t:t ~pre:"ite" (T.ty b) in
-          SI.define_const si ~const:t_ite ~rhs:t;
           let pr_def = SI.P.define_term t_ite t PA.proof in
           let lit_a = PA.mk_lit_nopreproc a' in
-          (* TODO: use unit paramod on each clause with side t=t_ite and on a=a' *)
           PA.add_clause [Lit.neg lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite b)]
-            (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@
+            (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a))
-             A.lemma_ite_true ~a:a' ~ite:t PA.proof);
+               (A.lemma_ite_true ~ite:t PA.proof) PA.proof);
           PA.add_clause [lit_a; PA.mk_lit_nopreproc (eq self.tst t_ite c)]
-            (pr_p1 PA.proof pr_def @@ pr_p1_opt PA.proof pr_a @@
+            (SI.P.lemma_rw_clause ~using:Iter.(append (return pr_def) (of_opt pr_a))
-             A.lemma_ite_false ~a:a' ~ite:t PA.proof);
+               (A.lemma_ite_false ~ite:t PA.proof) PA.proof);
           ret t_ite
       end
     | _ -> None
@@ -238,13 +247,12 @@ module Make(A : ARG) : S with module A = A = struct
     let[@inline] add_step s = steps := s :: !steps in
 
     (* handle boolean equality *)
-    let equiv_ si ~is_xor ~for_t t_a t_b : Lit.t =
+    let equiv_ _si ~is_xor ~for_t t_a t_b : Lit.t =
       let a = PA.mk_lit_nopreproc t_a in
       let b = PA.mk_lit_nopreproc t_b in
       let a = if is_xor then Lit.neg a else a in (* [a xor b] is [(¬a) = b] *)
       let t_proxy, proxy = fresh_lit ~for_t ~mk_lit:PA.mk_lit_nopreproc ~pre:"equiv_" self in
 
-      SI.define_const si ~const:t_proxy ~rhs:for_t;
       let pr_def = SI.P.define_term t_proxy for_t PA.proof in
       add_step pr_def;
 
@@ -284,7 +292,6 @@ module Make(A : ARG) : S with module A = A = struct
         let t_subs = Iter.to_list l in
         let subs = List.map PA.mk_lit_nopreproc t_subs in
         let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"and_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
         let pr_def = SI.P.define_term t_proxy t PA.proof in
         add_step pr_def;
 
@@ -303,7 +310,6 @@ module Make(A : ARG) : S with module A = A = struct
         let t_subs = Iter.to_list l in
         let subs = List.map PA.mk_lit_nopreproc t_subs in
         let t_proxy, proxy = fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"or_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
         let pr_def = SI.P.define_term t_proxy t PA.proof in
         add_step pr_def;
 
@@ -328,7 +334,6 @@ module Make(A : ARG) : S with module A = A = struct
         (* now the or-encoding *)
         let t_proxy, proxy =
           fresh_lit ~for_t:t ~mk_lit:PA.mk_lit_nopreproc ~pre:"implies_" self in
-        SI.define_const si ~const:t_proxy ~rhs:t;
         let pr_def = SI.P.define_term t_proxy t PA.proof in
         add_step pr_def;
 
@@ -377,11 +382,15 @@ module Make(A : ARG) : S with module A = A = struct
       all_terms
         (fun t -> match cnf_of t with
            | None -> ()
-           | Some u ->
+           | Some (u, pr_t_u) ->
              Log.debugf 5
                (fun k->k "(@[th-bool-static.final-check.cnf@ %a@ :yields %a@])"
                    T.pp t T.pp u);
-             SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_list []);
+
+             (* produce a single step proof of [|- t=u] *)
+             let proof = SI.proof si in
+             let pr = SI.P.lemma_preprocess t u ~using:pr_t_u proof in
+             SI.CC.merge_t cc_ t u (SI.CC.Expl.mk_theory pr []);
              ());
     end;
     ()

src/th-data/Sidekick_th_data.ml

@@ -71,9 +71,17 @@ module type ARG = sig
   val ty_is_finite : S.T.Ty.t -> bool
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
 
-  val lemma_isa_split : S.Lit.t Iter.t -> S.proof -> unit
+  val lemma_isa_cstor : S.T.Term.t -> S.P.proof_rule
-  val lemma_isa_disj : S.Lit.t Iter.t -> S.proof -> unit
+  (** [lemma_isa_cstor (is-c (c …))]
-  val lemma_cstor_inj : S.Lit.t Iter.t -> S.proof -> unit
+      or [lemma_isa_cstor (is-c (d …))] returns a unit clause *)
+
+  val lemma_select_cstor : S.T.Term.t -> S.P.proof_rule
+  (** [lemma_select_cstor (sel-c-i (c t1…tn))]
+      returns a proof of [(sel-c-i (c t1…tn)) = ti] *)
+
+  val lemma_isa_split : S.T.Term.t -> S.Lit.t Iter.t -> S.P.proof_rule
+  val lemma_isa_disj : S.T.Term.t -> S.T.Term.t -> S.P.proof_rule
+  val lemma_cstor_inj : Cstor.t -> S.T.Term.t -> S.T.Term.t -> int -> S.P.proof_rule
 end
 
 (** Helper to compute the cardinality of types *)
@@ -231,26 +239,36 @@ module Make(A : ARG) : S with module A = A = struct
       Log.debugf 5
         (fun k->k "(@[%s.merge@ (@[:c1 %a@ %a@])@ (@[:c2 %a@ %a@])@])"
             name N.pp n1 pp c1 N.pp n2 pp c2);
-      (* build full explanation of why the constructor terms are equal *)
+
-      (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *)
+      let mk_expl pr =
-      let expl =
+        Expl.mk_theory pr @@ [
-        Expl.mk_theory @@ Expl.mk_list [
           e_n1_n2;
           Expl.mk_merge n1 c1.c_n;
           Expl.mk_merge n2 c2.c_n;
         ]
       in
+
       if A.Cstor.equal c1.c_cstor c2.c_cstor then (
         (* same function: injectivity *)
-        (* FIXME proof *)
+
+        let expl_merge i =
+          mk_expl @@
+          A.lemma_cstor_inj c1.c_cstor (N.term c1.c_n) (N.term c2.c_n) i (SI.CC.proof cc)
+        in
+
         assert (IArray.length c1.c_args = IArray.length c2.c_args);
-        IArray.iter2
+        IArray.iteri2
-          (fun u1 u2 -> SI.CC.merge cc u1 u2 expl)
+          (fun i u1 u2 -> SI.CC.merge cc u1 u2 (expl_merge i))
           c1.c_args c2.c_args;
         Ok c1
       ) else (
         (* different function: disjointness *)
-        (* FIXME proof *)
+
+        let expl =
+          mk_expl @@
+          A.lemma_isa_disj (N.term c1.c_n) (N.term c2.c_n) (SI.CC.proof cc)
+        in
+
         Error expl
       )
   end
@@ -379,8 +397,10 @@ module Make(A : ARG) : S with module A = A = struct
           Log.debugf 5
             (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])"
                 name T.pp t is_true N.pp n Monoid_cstor.pp cstor);
+          (* FIXME: needs [nu = cstor.c_n] as hyp? *)
+          let pr = A.lemma_isa_cstor (N.term cstor.c_n) (SI.CC.proof cc) in
           SI.CC.merge cc n (SI.CC.n_bool cc is_true)
-            Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
+            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
       end
     | T_select (c_t, i, u) ->
       let n_u = SI.CC.add_term cc u in
@@ -392,7 +412,10 @@ module Make(A : ARG) : S with module A = A = struct
                 name N.pp n i A.Cstor.pp c_t);
           assert (i < IArray.length cstor.c_args);
           let u_i = IArray.get cstor.c_args i in
-          SI.CC.merge cc n u_i Expl.(mk_theory @@ mk_merge n_u cstor.c_n)
+          (* FIXME: needs [nu = cstor.c_n] as hyp? *)
+          let pr = A.lemma_select_cstor (N.term cstor.c_n) (SI.CC.proof cc) in
+          SI.CC.merge cc n u_i
+            Expl.(mk_theory pr [mk_merge n_u cstor.c_n])
         | Some _ -> ()
         | None ->
           N_tbl.add self.to_decide repr_u (); (* needs to be decided *)