HeadChoice

Here we define HeadChoices, which are merely functions from triggers to head indices. We also define machinery to get a branch from a tree that corresponds to a given HeadChoice.

@[reducible, inline]

abbrev HeadChoice (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] : Type (max (max u_3 u_2) u_1)

A HeadChoice is a function that maps each trigger to one of its head indices.

Equations

• HeadChoice sig = ((trg : PreTrigger sig) → Fin trg.rule.head.length)

def HeadChoice.consistent_for_equivalent_triggers {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (hc : HeadChoice sig) : Prop

Often we want to assume that a HeadChoice for equivalent triggers returns the same index.

Equations

• hc.consistent_for_equivalent_triggers = ∀ {trg trg2 : PreTrigger sig}, trg.equiv trg2 → ↑(hc trg) = ↑(hc trg2)

def PreTrigger.output_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (hc : HeadChoice sig) : List (Fact sig)

A shortcut for the trigger output dictaded by a head choice.

Equations

• trg.output_for_headChoice hc = trg.mapped_head[↑(hc trg)]

theorem PreTrigger.output_for_headChoice_eq_of_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg trg2 : PreTrigger sig} {hc : HeadChoice sig} (hc_consistent : hc.consistent_for_equivalent_triggers) (equiv : trg.equiv trg2) : trg.output_for_headChoice hc = trg2.output_for_headChoice hc

The head choice output for equivalent triggers is the same given that the head choice is consistent_for_equivalent_triggers.

def ChaseNode.adheres_to_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (node : N) (hc : HeadChoice sig) : Prop

A ChaseNode adheres to a HeadChoice if its origin uses the index that is the head choice of its trigger.

Equations

• One or more equations did not get rendered due to their size.

theorem ChaseNode.origin_result_eq_of_adheres_to_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {node : N} (isSome : (origin node).isSome = true) {hc : HeadChoice sig} (adheres : adheres_to_headChoice node hc) : origin_result node isSome = ((origin node).get isSome).fst.val.output_for_headChoice hc

def ChaseDerivationSkeleton.adheres_to_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (cd : ChaseDerivationSkeleton N obs rules) (hc : HeadChoice sig) : Prop

A ChaseDerivationSkeleton adheres to a HeadChoice if every node adheres to the HeadChoice.

Equations

• cd.adheres_to_headChoice hc = ∀ (n : N), n ∈ cd → ChaseNode.adheres_to_headChoice n hc

def TreeDerivation.generator_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (td : TreeDerivation N obs rules) (hc : HeadChoice sig) (n : td.NodeWithAddress) : Option td.NodeWithAddress

The generator function used to generate the tree branch corresponding to the given HeadChoice.

Equations

• One or more equations did not get rendered due to their size.

theorem TreeDerivation.generator_for_headChoice_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} (n next : td.NodeWithAddress) : next ∈ td.generator_for_headChoice hc n → next ∈ n.childNodes

The generator function produces a child node if it produces a value at all.

theorem TreeDerivation.generator_for_headChoice_eq_none_iff_childNodes_eq_nil {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} (n : td.NodeWithAddress) : td.generator_for_headChoice hc n = none ↔ n.childNodes = []

The generator function does not yield a new value if and only if the childNodes are empty.

theorem TreeDerivation.generator_for_headChoice_adheres_to_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} (n next : td.NodeWithAddress) : next ∈ td.generator_for_headChoice hc n → ChaseNode.adheres_to_headChoice next.node hc

The node produced by generator_for_headChoice adheres to the head choice.

def TreeDerivation.subderivation_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] (td : TreeDerivation N obs rules) (hc : HeadChoice sig) : ChaseDerivation N obs rules

This function generates the tree branch that corresponds to the given HeadChoice.

Equations

• td.subderivation_for_headChoice hc = td.generate_subderivation (TreeDerivation.NodeWithAddress.root td) (td.generator_for_headChoice hc) id ⋯ ⋯

theorem TreeDerivation.subderivation_for_headChoice_mem_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} : td.subderivation_for_headChoice hc ∈ td.branches

The subderivation_for_headChoice is a branch, which follows since we use TreeDerivation.generate_subderivation to build it.

theorem TreeDerivation.head_subderivation_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} : (td.subderivation_for_headChoice hc).head = td.root

The head of subderivation_for_headChoice is the root of the tree derivation.

theorem TreeDerivation.subderivation_for_headChoice_adheres_to_headChoice_of_root_adheres {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {N : Type u} [CN : ChaseNode N obs rules] {td : TreeDerivation N obs rules} {hc : HeadChoice sig} : ChaseNode.adheres_to_headChoice td.root hc → (td.subderivation_for_headChoice hc).adheres_to_headChoice hc

The subderivation for a head choice adheres to that head choice.

def ChaseTree.subderivation_for_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (ct : ChaseTree N obs kb) (hc : HeadChoice sig) : ChaseBranch N obs kb

This function generates the tree branch that corresponds to the given HeadChoice.

Equations

• ct.subderivation_for_headChoice hc = { toChaseDerivation := ct.subderivation_for_headChoice hc, database_first := ⋯ }

theorem ChaseTree.subderivation_for_headChoice_adheres_to_headChoice {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {ct : ChaseTree N obs kb} {hc : HeadChoice sig} : (ct.subderivation_for_headChoice hc).adheres_to_headChoice hc

The subderivation for a head choice adheres to that head choice.