Tree Derivation

The TreeDerivation is the tree version of the ChaseDerivation. Since we allow rules to feature disjunctions, there are multiple possible results for a given trigger. The ChaseDerivation picks one possible choice. For the TreeDerivation, we consider all possiblities at once. That is, the tree branches out for the disjunctions.

We try to mimic much of the machinery introduced for ChaseDerivation but we will see that some of this requires a different approach. Most prominently, we now need to consider addresses of nodes in the tree to be able to define a proper predecessor relation.

Chase Step

To define how one chase step follows from the previous, we introduce two auxiliary definitions that capture two cases that can occur for a given ChaseNode in a TreeDerivation. This is similar to the definitions for ChaseDerivation only that now the result is a list of ChaseNodes.

1. Case (exists_trigger_list): There still exists an Trigger.active trigger, in which case one chase node for each disjunct of the trigger is introduced and contains the facts from the previous step together with the respective head result of the trigger.

2. Case (not_exists_trigger_list): There is no active trigger. Then the successor list must be empty, i.e. the respective tree node does not have any children.

def exists_trigger_list_condition {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) (before : ChaseNode obs rules) (after : List (ChaseNode obs rules)) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : Prop

Equations

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

def exists_trigger_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) (before : ChaseNode obs rules) (after : List (ChaseNode obs rules)) : Prop

Equations

• exists_trigger_list obs rules before after = ∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), exists_trigger_list_condition obs rules before after trg

def not_exists_trigger_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) (before : ChaseNode obs rules) (after : List (ChaseNode obs rules)) : Prop

Equations

• not_exists_trigger_list obs rules before after = ((¬∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), trg.val.active before.facts) ∧ after = [])

The TreeDerivation Structure

The backbone of the TreeDerivation is a FiniteDegreeTree of ChaseNodes with a couple of conditions.

1. We enforce that there is at least an initial ChaseNode.
2. At each step in the derivation, either there exists a trigger that yields the child nodes or there is no trigger and consequently the derivation stops at this point. This is expressed by the two auxiliary definitions above.
3. No triggers are active on leaf nodes.
4. For each trigger, there exists a depth in the tree from which on the trigger is never active anymore.

Conditions 3 and 4 together are "fairness", i.e. each trigger must eventually be non-active. Fairness ensures that the chase result (or in this case each fact set in the chase result) is indeed a model.

structure TreeDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) : Type (max (max u_1 u_2) u_3)

• tree : FiniteDegreeTree (ChaseNode obs rules)
• isSome_root : self.tree.root.isSome = true
• triggers_exist (ns : List Nat) (before : ChaseNode obs rules) : before ∈ (self.tree.drop ns).root → let after := (self.tree.drop ns).childNodes; exists_trigger_list obs rules before after ∨ not_exists_trigger_list obs rules before after
• fairness_leaves (leaf : ChaseNode obs rules) : leaf ∈ self.tree.leaves → ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), ¬trg.val.active leaf.facts
• fairness_infinite_branches (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (i : Nat), ∀ (ns : List Nat), ns.length ≥ i → ∀ (node : ChaseNode obs rules), node ∈ self.tree.get? ns → ¬trg.val.active node.facts

Basic Definitions

Here we introduce some auxiliary definitions and theorems and we lift some of the machinery of the underlying FiniteDegreeTree to TreeDerivation.

def TreeDerivation.toFiniteDegreeTreeWithRoot {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : FiniteDegreeTree.FiniteDegreeTreeWithRoot (ChaseNode obs rules)

We can convert a TreeDerivation directly to a FiniteDegreeTree.FiniteDegreeTreeWithRoot.

Equations

• td.toFiniteDegreeTreeWithRoot = ⟨td.tree, ⋯⟩

@[implicit_reducible]

instance TreeDerivation.instMembershipChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} : Membership (ChaseNode obs rules) (TreeDerivation obs rules)

Membership of ChaseNodes in the TreeDerivation directly corresponds to membership in the FiniteDegreeTree.

Equations

• TreeDerivation.instMembershipChaseNode = { mem := fun (td : TreeDerivation obs rules) (node : ChaseNode obs rules) => node ∈ td.tree }

theorem TreeDerivation.mem_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {e : ChaseNode obs rules} : e ∈ td ↔ ∃ (ns : List Nat), td.tree.get? ns = some e

An element is a member of the tree iff it occurs at some address.

def TreeDerivation.derivation_for_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) (t2 : FiniteDegreeTree (ChaseNode obs rules)) (suffix : t2 <:+ td.tree) (t2_root_some : t2.root.isSome = true) : TreeDerivation obs rules

Each subtree of the underlying FiniteDegreeTree is itself a TreeDerivation as long as its root is not none.

Equations

• td.derivation_for_suffix t2 suffix t2_root_some = { tree := t2, isSome_root := t2_root_some, triggers_exist := ⋯, fairness_leaves := ⋯, fairness_infinite_branches := ⋯ }

def TreeDerivation.root {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : ChaseNode obs rules

The root of the TreeDerivation is the initial ChaseNode. We know that this is never none.

Equations

• td.root = td.tree.root.get ⋯

theorem TreeDerivation.root_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : td.root ∈ td

The root is a member.

The (immediate) ChildNodes

For a TreeDerivation derivation, its childNodes are the ChaseNodes immediately following the root. We mainly introduce a couple of theorems here that abstract away the triggers_exist condition from the TreeDerivation definition.

def TreeDerivation.childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : List (ChaseNode obs rules)

Equations

• td.childNodes = td.tree.childNodes

theorem TreeDerivation.mem_of_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (n : ChaseNode obs rules) : n ∈ td.childNodes → n ∈ td

Each child node is a member.

theorem TreeDerivation.isSome_origin_of_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (n : ChaseNode obs rules) : n ∈ td.childNodes → n.origin.isSome = true

The origin of the childNodes needs to be set.

theorem TreeDerivation.active_trigger_origin_of_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {n : ChaseNode obs rules} (mem : n ∈ td.childNodes) : (n.origin.get ⋯).fst.val.active td.root.facts

The trigger used to derive the childNodes is active for head.

theorem TreeDerivation.childNodes_ne_nil_iff_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : td.childNodes ≠ [] ↔ ∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), trg.val.active td.root.facts

The childNodes are not nil if and only if some trigger is active on root.

theorem TreeDerivation.facts_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {n : ChaseNode obs rules} (mem : n ∈ td.childNodes) : n.facts = td.root.facts ∪ (n.origin_result ⋯).toSet

The fact set of each of the childNodes consists exactly of the facts from root and the result of the trigger that introduces the child node.

TreeDerivation Subtrees

We define a suffix/subtree relation on TreeDerivation simply as the subtree relation of the underlying FiniteDegreeTree.

def TreeDerivation.IsSuffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td1 td2 : TreeDerivation obs rules) : Prop

Equations

• (td1 <:+ td2) = (td1.tree <:+ td2.tree)

def TreeDerivation.«term_<:+_» : Lean.TrailingParserDescr

Equations

• TreeDerivation.«term_<:+_» = Lean.ParserDescr.trailingNode `TreeDerivation.«term_<:+_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <:+ ") (Lean.ParserDescr.cat `term 51))

theorem TreeDerivation.IsSuffix_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td1 td2 : TreeDerivation obs rules} : td1 <:+ td2 ↔ td1.tree <:+ td2.tree

theorem TreeDerivation.mem_of_mem_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : TreeDerivation obs rules} (suffix : cd1 <:+ cd2) (node : ChaseNode obs rules) : node ∈ cd1 → node ∈ cd2

Members of our subtrees are also our members.

Child Trees

We can drop the root of a TreeDerivation and obtain a (possibly empty) list of childTrees, which are again TreeDerivations.

def TreeDerivation.childTrees {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : List (TreeDerivation obs rules)

We obtain the child trees of the FiniteDegreeTree and convert each of them into a TreeDerivation using derivation_for_suffix. We know that all of those trees have non-none roots.

Equations

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

theorem TreeDerivation.mem_childTrees_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (c : TreeDerivation obs rules) : c ∈ td.childTrees ↔ c.toFiniteDegreeTreeWithRoot ∈ td.tree.childTrees

Membership in childTrees can be boiled down to membership in FiniteDegreeTree.childTrees.

theorem TreeDerivation.childNodes_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : td.childNodes = List.map root td.childTrees

childNodes can be expressed by mapping each childTrees to its root.

theorem TreeDerivation.IsSuffix_of_mem_childTrees {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (td2 : TreeDerivation obs rules) : td2 ∈ td.childTrees → td2 <:+ td

Each childTrees is a suffix.

theorem TreeDerivation.suffix_iff_eq_or_suffix_childTree {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td1 td2 : TreeDerivation obs rules} : td1 <:+ td2 ↔ td1 = td2 ∨ ∃ (td3 : TreeDerivation obs rules), td3 ∈ td2.childTrees ∧ td1 <:+ td3

A derivation is a subtree of another if and only if both are the same or the first is a suffix of one of the second's child trees.

Induction Principle for Members

Similar to FiniteDegreeTree.mem_rec, we define an induction principle to show properties of ChaseNodes in a TreeDerivation.

Looking ahead a bit, we will also want to define a predecessor relation on nodes in the tree as we did for nodes in a ChaseDerivation. This is not so elegant here though as the same node might indeed occur multiple times in the tree. Therefore, we are going to associate each node with its address in the tree to tell them apart. Since we are doing this anyway, it makes sense to define the induction principle already with respect to this kind of node.

NodeWithAddress

The NodeWithAddress is a structure of a ChaseNode, an address (i.e. a List Nat), and a proof that the chase node is indeed at the given address. We also introduce a couple of covenience functions and theorems for the NodeWithAddress.

structure TreeDerivation.NodeWithAddress {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : Type (max (max u_1 u_2) u_3)

• node : ChaseNode obs rules
• address : List Nat
• eq : td.tree.get? self.address = some self.node

def TreeDerivation.NodeWithAddress.subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) : TreeDerivation obs rules

Each NodeWithAddress induces a subderivation in the TreeDerivation.

Equations

• node.subderivation = td.derivation_for_suffix (td.tree.drop node.address) ⋯ ⋯

def TreeDerivation.NodeWithAddress.cast_for_new_root_node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (new_root : td.NodeWithAddress) (node : new_root.subderivation.NodeWithAddress) : td.NodeWithAddress

We can cast a node for one of our subderivations into our own node.

Equations

• new_root.cast_for_new_root_node node = { node := node.node, address := new_root.address ++ node.address, eq := ⋯ }

def TreeDerivation.NodeWithAddress.root {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : td.NodeWithAddress

The NodeWithAddress version of TreeDerivation.root.

Equations

• TreeDerivation.NodeWithAddress.root td = { node := td.root, address := [], eq := ⋯ }

def TreeDerivation.NodeWithAddress.childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) : List td.NodeWithAddress

The child nodes of a given NodeWithAddress.

Equations

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

theorem TreeDerivation.NodeWithAddress.mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) : node.node ∈ td

The NodeWithAddress is a member.

theorem TreeDerivation.NodeWithAddress.eq_of_address_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {n1 n2 : td.NodeWithAddress} : n1.address = n2.address → n1 = n2

Two NodeWithAddress are equal if their addresses are.

theorem TreeDerivation.NodeWithAddress.IsSuffix_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node.subderivation <:+ td

subderivation is indeed a subtree.

theorem TreeDerivation.NodeWithAddress.root_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : root node.subderivation = { node := node.node, address := [], eq := ⋯ }

The root of the subderivation is the node itself with empty address.

@[simp]

theorem TreeDerivation.NodeWithAddress.root_subderivation' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node.subderivation.root = node.node

The root of the subderivation is the node itself.

@[simp]

theorem TreeDerivation.NodeWithAddress.subderivation_root {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : (root td).subderivation = td

The subderivation of the root is the original TreeDerivation.

theorem TreeDerivation.NodeWithAddress.childNodes_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node.subderivation.childNodes = (td.tree.drop node.address).childNodes

Unfolds the childNodes and subderivation definitions to an expression on the underlying tree.

@[simp]

theorem TreeDerivation.NodeWithAddress.length_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node.childNodes.length = node.subderivation.childNodes.length

NodeWithAddress.childNodes has the same length as TreeDerivation.childNodes.

theorem TreeDerivation.NodeWithAddress.childNodes_eq_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node.subderivation.childNodes = List.map NodeWithAddress.node node.childNodes

NodeWithAddress.childNodes and TreeDerivation.childNodes are (almost) equal.

theorem TreeDerivation.NodeWithAddress.mem_childNodes_of_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node n : td.NodeWithAddress} : n ∈ node.childNodes → n.node ∈ node.subderivation.childNodes

Membership for NodeWithAddress.childNodes and TreeDerivation.childNodes is (almost) the same.

@[simp]

theorem TreeDerivation.NodeWithAddress.node_getElem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} (i : Nat) (lt : i < node.childNodes.length) : node.childNodes[i].node = node.subderivation.childNodes[i]

Getting specific elements from child nodes can be translated between NodeWithAddress.childNodes and TreeDerivation.childNodes.

@[simp]

theorem TreeDerivation.NodeWithAddress.address_getElem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} (i : Nat) (lt : i < node.childNodes.length) : node.childNodes[i].address = node.address ++ [i]

Getting specific element addresses from child nodes can be translated between NodeWithAddress.childNodes and TreeDerivation.childNodes.

theorem TreeDerivation.NodeWithAddress.subderivation_mem_childTrees_of_mem_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node node2 : td.NodeWithAddress} : node2 ∈ node.childNodes → node2.subderivation ∈ node.subderivation.childTrees

The subderivation for a child node is a child tree.

Now we are ready for the actual induction principle on NodeWithAddresss in a TreeDerivation.

theorem TreeDerivation.mem_rec_address {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {motive : td.NodeWithAddress → Prop} (root : motive (NodeWithAddress.root td)) (step : ∀ (new_root : td.NodeWithAddress), motive new_root → ∀ (c : td.NodeWithAddress), c ∈ new_root.childNodes → motive c) (node : td.NodeWithAddress) : motive node

If we want to show a motive for all nodes in a derivation, it is enough to show the motive for the root and for each arbitrary child node in each abitrary subderivation where the motive in turn already holds for the root. This can be used with the induction tactic.

theorem TreeDerivation.mem_some_childTree_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : ChaseNode obs rules} : (∃ (t : TreeDerivation obs rules), t ∈ td.childTrees ∧ node ∈ t) ↔ ∃ (td2 : TreeDerivation obs rules), td2 <:+ td ∧ node ∈ td2.childNodes

A node is a member of some element of childTrees if and only if there is a subderivation where the node occurs in the childNodes. Part of this proof uses the induction principle defined above.

Subset Monotonicity of Facts in ChaseNodes

Since ChaseNodes always extend the previous facts, the fact sets can only be growing along the branches of the TreeDerivation. This has a couple of convenient implications. For example, the root of a TreeDerivation can never occur in its childTrees.

theorem TreeDerivation.facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : ChaseNode obs rules) : node ∈ td → td.root.facts ⊆ node.facts

Each member's facts contain the root facts.

theorem TreeDerivation.root_not_mem_childTrees {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : ¬∃ (t : TreeDerivation obs rules), t ∈ td.childTrees ∧ td.root ∈ t

The root cannot occur in the childTrees. Otherwise, it would be introduced using a trigger but then this trigger is already obsolete since all the facts from root already occur in the very beginning. We use ObsolescenceCondition.contains_trg_result_implies_cond here.

theorem TreeDerivation.eq_of_suffix_of_root_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td1 td2 : TreeDerivation obs rules} (suffix : td1 <:+ td2) (root_mem : td2.root ∈ td1) : td1 = td2

By root_not_mem_childTrees, if we have a subtree but our root occurs in the subtree, then our subtree is equal to us.

Predecessor Relation

Opposed to the ChaseDerivation, we define the predecessor relation direclty using addresses here. This is because ChaseNodes may indeed occur multiple times in a TreeDerivation (just not in the same branch) and therefore the approach used in ChaseDerivation would not quite work. In particular, note that the TreeDerivation has no equivalent for ChaseDerivation.suffix_of_suffix_of_suffix_of_head_mem.

Also, even with the address approach, the relation is not total here (which is expected for a tree).

def TreeDerivation.predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (n1 n2 : td.NodeWithAddress) : Prop

Node $n$ is a predecessor of node $m$ if the address of $n$ is a prefix of the address of $m$. Predecessor can therefore also be understood as ancestor in the tree.

Equations

• (n1 ≼ n2) = (n1.address <+: n2.address)

def TreeDerivation.«term_≼_» : Lean.TrailingParserDescr

Equations

• TreeDerivation.«term_≼_» = Lean.ParserDescr.trailingNode `TreeDerivation.«term_≼_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≼ ") (Lean.ParserDescr.cat `term 51))

theorem TreeDerivation.predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {new_root : td.NodeWithAddress} {n1 n2 : new_root.subderivation.NodeWithAddress} : n1 ≼ n2 → new_root.cast_for_new_root_node n1 ≼ new_root.cast_for_new_root_node n2

The predecessor relation is stable across suffixes. That is, predecessor in our suffix are also predecessor for us. We only need to cast the nodes.

theorem TreeDerivation.predecessor_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} : node ≼ node

The predecessor relation is reflexive.

theorem TreeDerivation.predecessor_antisymm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {n1 n2 : td.NodeWithAddress} : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem TreeDerivation.predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {n1 n2 n3 : td.NodeWithAddress} : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

theorem TreeDerivation.node_prec_childNodes {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : td.NodeWithAddress} (n : td.NodeWithAddress) : n ∈ node.childNodes → node ≼ n

Each node is the predecessor of its childNodes.

theorem TreeDerivation.facts_node_subset_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node1 node2 : td.NodeWithAddress} : node1 ≼ node2 → node1.node.facts ⊆ node2.node.facts

The facts of our predecessor are a subset of our facts.

Branches and Chase Result

Here, we define the result of a TreeDerivation, which requires us to also define the branches of the TreeDerivation. It should be no surprise that these are ChaseDerivations. The result is then just the set of the results of all the ChaseDerivations in the tree. We already know from the ChaseDerivation that each element of TreeDerivation.result is therefore a model of the rules.

def TreeDerivation.derivation_for_branch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) (branch : PossiblyInfiniteList (ChaseNode obs rules)) (branch_mem : branch ∈ td.tree.branches) : ChaseDerivation obs rules

Each branch of the underlying tree can be transformed into a proper ChaseDerivation.

Equations

• td.derivation_for_branch branch branch_mem = { branch := branch, isSome_head := ⋯, triggers_exist := ⋯, triggers_active := ⋯, fairness := ⋯ }

def TreeDerivation.branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : Set (ChaseDerivation obs rules)

The branches of the TreeDerivation are defined as all the ChaseDerivation that occur as branches in the tree.

Equations

• td.branches branch = (branch.branch ∈ td.tree.branches)

theorem TreeDerivation.branches_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} : td.branches = fun (b : ChaseDerivation obs rules) => b.head = td.root ∧ (td.childTrees = [] ∧ b.next = none ∨ ∃ (td2 : TreeDerivation obs rules), td2 ∈ td.childTrees ∧ ∃ (next : ChaseNode obs rules), ∃ (next_eq : next ∈ b.next), b.tail ⋯ ∈ td2.branches)

We lift FiniteDegreeTree.branches_eq to a similar version for TreeDerivations.

theorem TreeDerivation.derivation_for_branch_mem_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {branch : PossiblyInfiniteList (ChaseNode obs rules)} {branch_mem : branch ∈ td.tree.branches} : td.derivation_for_branch branch branch_mem ∈ td.branches

Each ChaseDerivation constructed using derivation_for_branch occurs in branches.

def TreeDerivation.result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (td : TreeDerivation obs rules) : Set (FactSet sig)

The result is the set of FactSets that correspond to the results of the branches.

Equations

• td.result = td.branches.map fun (deriv : ChaseDerivation obs rules) => deriv.result

theorem TreeDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (fs : FactSet sig) : fs ∈ td.result → fs.modelsRules rules

Each element of the result models the rules.

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some node.

theorem TreeDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} {node : ChaseNode obs rules} (node_mem : node ∈ td) : node.facts.constants ⊆ td.root.facts.constants ∪ rules.head_constants

Constants in the chase can only come from the initial fact set or from a constant in a rule.

theorem TreeDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.node.facts.terms) : t ∈ td.root.facts.terms ∨ ∃ (node2 : td.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.node.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger if it was not already part of the initial fact set.

theorem TreeDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ td.root.facts.terms ∨ ∃ (node2 : td.NodeWithAddress), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.node.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase, unless the term already occurs in the initial fact set.

theorem TreeDerivation.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {td : TreeDerivation obs rules} (node : td.NodeWithAddress) {t : GroundTerm sig} (t_mem_node : t ∈ node.node.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ td.root.facts.terms ∨ trg.val.mapped_head[disj_idx].toSet ⊆ node.node.facts

If a functional term occurs in the chase, then the result of the trigger that introduces this term is contained in the current node, unless the functional term already occurs in the initial fact set.

Derivation Generation

We lift FiniteDegreeTree.generate_branch to TreeDerivation using a generator over NodeWithAddress and combine it with FiniteDegreeTree.generate_branch_mem_branches to obtain a ChaseDerivation directly.

def TreeDerivation.generate_branch {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_4} (td : TreeDerivation obs rules) (start : β) (generator : β → Option β) (mapper : β → td.NodeWithAddress) : PossiblyInfiniteList (ChaseNode obs rules)

We lift FiniteDegreeTree.generate_branch to TreeDerivation.

Equations

• td.generate_branch start generator mapper = FiniteDegreeTree.generate_branch (some start) generator fun (b : β) => (mapper b).subderivation.toFiniteDegreeTreeWithRoot

theorem TreeDerivation.generate_branch_mem_tree_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_1} {td : TreeDerivation obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes) (maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []) : td.generate_branch start generator mapper ∈ (mapper start).subderivation.tree.branches

We lift FiniteDegreeTree.generate_branch_mem_branches to TreeDerivation.

def TreeDerivation.generate_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_4} (td : TreeDerivation obs rules) (start : β) (generator : β → Option β) (mapper : β → td.NodeWithAddress) (next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes) (maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []) : ChaseDerivation obs rules

We can genearte a ChaseDerivation within a TreeDerivation using a generator function that ensures that the cnsecutive elements are children of each other and that the genearted derivation is maximal.

Equations

• td.generate_subderivation start generator mapper next_is_child maximal = (mapper start).subderivation.derivation_for_branch (td.generate_branch start generator mapper) ⋯

theorem TreeDerivation.generate_subderivation_mem_branches {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_1} {td : TreeDerivation obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} (start_eq : mapper start = NodeWithAddress.root td) : td.generate_subderivation start generator mapper next_is_child maximal ∈ td.branches

The result of generate_subderivation occurs in TreeDerivation.branches if it starts on the root of the tree.

@[simp]

theorem TreeDerivation.head_generate_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_1} {td : TreeDerivation obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} : (td.generate_subderivation start generator mapper next_is_child maximal).head = (mapper start).node

The head for the derivation produced by generate_subderivation is exactly the mapped start value.

@[simp]

theorem TreeDerivation.next_generate_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_1} {td : TreeDerivation obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} : (td.generate_subderivation start generator mapper next_is_child maximal).next = Option.map NodeWithAddress.node (Option.map mapper (generator start))

The next node for the derivation produced by generate_subderivation is exactly the mapped value after the first generator application.

theorem TreeDerivation.tail_generate_subderivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {β : Type u_1} {td : TreeDerivation obs rules} {start : β} {generator : β → Option β} {mapper : β → td.NodeWithAddress} {next_is_child : ∀ (b b' : β), b' ∈ generator b → mapper b' ∈ (mapper b).childNodes} {maximal : ∀ (b : β), generator b = none → (mapper b).subderivation.childTrees = []} (next : β) (next_mem : next ∈ generator start) : (td.generate_subderivation start generator mapper next_is_child maximal).tail ⋯ = td.generate_subderivation next generator mapper next_is_child maximal

The tail for the derivation produced by generate_subderivation is exactly the generated derivation when applying the generator once initially.