Shared Extraction Lemmas for the Certificate Induction #
The per-operator soundness lemmas all start the same way: read the parent ids off the node,
show the parent boxes and values exist because the node produced some, and fetch the parent
enclosure from the induction hypothesis. This file packages the induction hypothesis as
ParentsEnclosed and provides the small lookup lemmas each operator case needs.
def
NN.MLTheory.CROWN.Graph.CertSoundness.ParentsEnclosed
(nodes : Array Node)
(cert : Array (Option (FlatBox ℝ)))
(vals : Array (Option Val))
(k : ℕ)
:
Induction hypothesis at node k: every parent whose certificate box and semantic value both
exist is enclosed. Phrased through getBox?/getVal? so operator cases never need array sizes
or the topological order.
Instances For
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.parents_enclosed_unary
{nodes : Array Node}
{cert : Array (Option (FlatBox ℝ))}
{vals : Array (Option Val)}
{k p1 : ℕ}
{B1 : FlatBox ℝ}
{v1 : Val}
(hpe : ParentsEnclosed nodes cert vals k)
(hparents : IR.unaryParent? nodes[k]!.parents = some p1)
(hgb : getBox? cert p1 = some B1)
(hgv : getVal? vals p1 = some v1)
:
EnclosesBox B1 v1
Parent enclosure for the single parent of a unary node.
theorem
NN.MLTheory.CROWN.Graph.CertSoundness.parents_enclosed_binary
{nodes : Array Node}
{cert : Array (Option (FlatBox ℝ))}
{vals : Array (Option Val)}
{k p1 p2 : ℕ}
{B1 B2 : FlatBox ℝ}
{v1 v2 : Val}
(hpe : ParentsEnclosed nodes cert vals k)
(hparents : IR.binaryParents? nodes[k]!.parents = some (p1, p2))
(hgb1 : getBox? cert p1 = some B1)
(hgb2 : getBox? cert p2 = some B2)
(hgv1 : getVal? vals p1 = some v1)
(hgv2 : getVal? vals p2 = some v2)
:
Parent enclosure for both parents of a binary node.