mirror of
https://github.com/c-cube/sidekick.git
synced 2026-01-21 16:56:41 -05:00
7 lines
6.1 KiB
HTML
7 lines
6.1 KiB
HTML
<!DOCTYPE html>
|
||
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Expl (sidekick.Sidekick_cc.Expl)</title><link rel="stylesheet" href="../../../odoc.support/odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc v2.3.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../odoc.support/highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> » <a href="../index.html">Sidekick_cc</a> » Expl</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_cc.Expl</span></code></h1><p>Explanations</p><p>Explanations are specialized proofs, created by the congruence closure when asked to justify why two terms are equal.</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type anchored" id="type-t"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div></div><div class="odoc-include"><details open="open"><summary class="spec include"><code><span><span class="keyword">include</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html">Sidekick_sigs.PRINT</a> <span class="keyword">with</span> <span><span class="keyword">type</span> <a href="../../Sidekick_sigs/module-type-PRINT/index.html#type-t">t</a> := <a href="#type-t">t</a></span></span></code></summary><div class="odoc-spec"><div class="spec value anchored" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="#type-t">t</a> <a href="../../Sidekick_sigs/index.html#type-printer">Sidekick_sigs.printer</a></span></span></code></div></div></details></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge"><a href="#val-mk_merge" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the nodes were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_merge_t"><a href="#val-mk_merge_t" class="anchor"></a><code><span><span class="keyword">val</span> mk_merge_t : <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: the terms were explicitly merged</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_lit"><a href="#val-mk_lit" class="anchor"></a><code><span><span class="keyword">val</span> mk_lit : <span><a href="../../Sidekick_core/Lit/index.html#type-t">Sidekick_core.Lit.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Explanation: we merged <code>t</code> and <code>u</code> because of literal <code>t=u</code>, or we merged <code>t</code> and <code>true</code> because of literal <code>t</code>, or <code>t</code> and <code>false</code> because of literal <code>¬t</code></p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_list"><a href="#val-mk_list" class="anchor"></a><code><span><span class="keyword">val</span> mk_list : <span><span><a href="#type-t">t</a> list</span> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>Conjunction of explanations</p></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_congruence"><a href="#val-mk_congruence" class="anchor"></a><code><span><span class="keyword">val</span> mk_congruence : <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <span><a href="../E_node/index.html#type-t">E_node.t</a> <span class="arrow">-></span></span> <a href="#type-t">t</a></span></code></div></div><div class="odoc-spec"><div class="spec value anchored" id="val-mk_theory"><a href="#val-mk_theory" class="anchor"></a><code><span><span class="keyword">val</span> mk_theory :
|
||
<span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> <span class="arrow">-></span></span>
|
||
<span><span><span>(<a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> * <a href="../../Sidekick_core/Term/index.html#type-t">Sidekick_core.Term.t</a> * <span><a href="#type-t">t</a> list</span>)</span> list</span> <span class="arrow">-></span></span>
|
||
<span><a href="../../Sidekick_proof/Pterm/index.html#type-delayed">Sidekick_proof.Pterm.delayed</a> <span class="arrow">-></span></span>
|
||
<a href="#type-t">t</a></span></code></div><div class="spec-doc"><p><code>mk_theory t u expl_sets pr</code> builds a theory explanation for why <code>|- t=u</code>. It depends on sub-explanations <code>expl_sets</code> which are tuples <code> (t_i, u_i, expls_i) </code> where <code>expls_i</code> are explanations that justify <code>t_i = u_i</code> in the current congruence closure.</p><p>The proof <code>pr</code> is the theory lemma, of the form <code> (t_i = u_i)_i |- t=u </code>. It is resolved against each <code>expls_i |- t_i=u_i</code> obtained from <code>expl_sets</code>, on pivot <code>t_i=u_i</code>, to obtain a proof of <code>Gamma |- t=u</code> where <code>Gamma</code> is a subset of the literals asserted into the congruence closure.</p><p>For example for the lemma <code>a=b</code> deduced by injectivity from <code>Some a=Some b</code> in the theory of datatypes, the arguments would be <code>a, b, [Some a, Some b, mk_merge_t (Some a)(Some b)], pr</code> where <code>pr</code> is the injectivity lemma <code>Some a=Some b |- a=b</code>.</p></div></div></div></body></html>
|