Chase Node

The chase is a pretty simple procedure. From an initial fact set, it creates a new fact set by applying a trigger and it continues to do this until all triggers are obsolete. In this process, we obtain a (potentially infinite) sequence of fact sets. It can be very useful to also keep track of the associated triggers and this is why we capture both the fact set and used trigger of individual chase steps in a ChaseNode.

To be able to use ChaseNodes also for the core chase, we develop a general interface in form of a typeclass where the "ingoingFacts" describe all facts that initiate the new chase node, while the "outgoingFacts" describe the facts that are available going further. That is, in the core chase, the outgoingFacts are a core of the ingoingFacts. For other chase variants, ingoingFacts and outgoingFacts are the same.

class ChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (N : Type u) (obs : ObsolescenceCondition sig) (rules : RuleSet sig) : Type (max (max (max u u_1) u_2) u_3)

A ChaseNode corresponds to a chase step. It must contain two FactSets of ingoingFacts and outgoingFacts and optionally an RTrigger and a head disjunct index indicating that the current ChaseNode was obtained by applying the specified trigger and picking the indicated head disjunct. It is optional since the initial fact set does not result from a trigger but on all following nodes, this value will be set (and we will prove that it is). For convenience, the chase node also directly includes a proof that the result of its origin is indeed contained in its fact set.

• ingoingFacts : N → FactSet sig
• outgoingFacts : N → FactSet sig
• origin : N → Option ((trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length)
• facts_contain_origin_result (node : N) (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ origin node → orig.fst.val.mapped_head[↑orig.snd].toSet ⊆ ingoingFacts obs rules node

def ChaseNode.origin_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] (node : N) (isSome : (origin node).isSome = true) : List (Fact sig)

The origin_result denotes the facts that have been introduced for the chase node. That is, the mapped head index for the trigger stored in the origin field of the ChaseNode.

Equations

• ChaseNode.origin_result node isSome = ((ChaseNode.origin node).get isSome).fst.val.mapped_head[↑((ChaseNode.origin node).get isSome).snd]

theorem ChaseNode.origin_result_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] {node : N} (isSome : (origin node).isSome = true) {trg : PreTrigger sig} {i : Nat} (trg_eq : trg = ((origin node).get isSome).fst.val.toPreTrigger) (i_eq : i = ↑((origin node).get isSome).snd) : origin_result node isSome = trg.mapped_head[i]

An auxiliary theorem showing that the origin result equals the i-th mapped head of a trigger if the trigger and i match the origin.

def ChaseNode.succ {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] (n1 n2 : N) : Prop

Two ChaseNodes are in a successor relation if the second one could be created from the first one by adding the origin result of the second one to the outgoign facts of the first one. We do not enforce trigger activeness here since we can easily enforce this in the ChaseDerivation later on.

Equations

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

def ChaseNode.succ_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] (n : N) (l : List N) : Prop

A list of ChaseNode may follow from another ChaseNode if the list corresponds to a trigger output. Here we directly enforce activeness as this would be convoluted to state afterwards.

Equations

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

theorem ChaseNode.succ_of_mem_succ_list {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] {n : N} {l : List N} (s : succ_list n l) (n2 : N) : n2 ∈ l → succ n n2

Every member of a succ_list has the succ property.

def ChaseNode.out_sub_in {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {N : Type u} {obs : ObsolescenceCondition sig} {rules : RuleSet sig} [CN : ChaseNode N obs rules] : Prop

A property expressing that the outgoingFacts facts of a chase node form a subset of the ingoingFacts. We require this general property in a couple of proofs and it trivially holds true for both the regular chase node and the core chase node.

Equations

• ChaseNode.out_sub_in = ∀ {n : N}, ChaseNode.outgoingFacts obs rules n ⊆ ChaseNode.ingoingFacts obs rules n

structure RegularChaseNode {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)

The RegularChaseNode is the one we use for most chases (except the core chase). Here ingoingFacts and outgoingFacts are always the same.

• facts : FactSet sig
• origin : Option ((trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length)
• facts_contain_origin_result (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.rule.head.length) : orig ∈ self.origin → orig.fst.val.mapped_head[↑orig.snd].toSet ⊆ self.facts

@[instance_reducible]

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

The RegularChaseNode is a ChaseNode where ingoingFacts and outgoingFacts are the same.

Equations

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

theorem RegularChaseNode.ingoingFacts_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {node : RegularChaseNode obs rules} : ChaseNode.ingoingFacts obs rules node = node.facts

theorem RegularChaseNode.outgoingFacts_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {node : RegularChaseNode obs rules} : ChaseNode.outgoingFacts obs rules node = node.facts

theorem RegularChaseNode.out_sub_in {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} : ChaseNode.out_sub_in

The RegularChaseNode has the ChaseNode.out_sub_in property.