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

doc

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 21:29:12 -04:00
parent 6c14690fba
commit 99dc9743a3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/cc/expl.mli
View file

@ -28,20 +28,20 @@ val mk_congruence : E_node.t -> E_node.t -> t
val mk_theory : val mk_theory :
Term.t -> Term.t -> (Term.t * Term.t * t list) list -> Proof_term.step_id -> t Term.t -> Term.t -> (Term.t * Term.t * t list) list -> Proof_term.step_id -> t
(** [mk_theory t u expl_sets pr] builds a theory explanation for (** [mk_theory t u expl_sets pr] builds a theory explanation for
why [|- t=u]. It depends on sub-explanations [expl_sets] which why [|- t=u]. It depends on sub-explanations [expl_sets] which
are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are are tuples [ (t_i, u_i, expls_i) ] where [expls_i] are
explanations that justify [t_i = u_i] in the current congruence closure. explanations that justify [t_i = u_i] in the current congruence closure.
The proof [pr] is the theory lemma, of the form The proof [pr] is the theory lemma, of the form
[ (t_i = u_i)_i |- t=u ]. [ (t_i = u_i)_i |- t=u ].
It is resolved against each [expls_i |- t_i=u_i] obtained from It is resolved against each [expls_i |- t_i=u_i] obtained from
[expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u] [expl_sets], on pivot [t_i=u_i], to obtain a proof of [Gamma |- t=u]
where [Gamma] is a subset of the literals asserted into the congruence where [Gamma] is a subset of the literals asserted into the congruence
closure. closure.
For example for the lemma [a=b] deduced by injectivity For example for the lemma [a=b] deduced by injectivity
from [Some a=Some b] in the theory of datatypes, from [Some a=Some b] in the theory of datatypes,
the arguments would be the arguments would be
[a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr] [a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr]
where [pr] is the injectivity lemma [Some a=Some b |- a=b]. where [pr] is the injectivity lemma [Some a=Some b |- a=b].
*) *)