Chase Derivation Skeleton

It is time to define the chase [BV84]. We are going to introduce slightly different representations and the ChaseDerivationSkeleton is arguably the most basic but also most versatile one.

We only demand a PossiblyInfiniteList of ChaseNodes that is non-empty such that the next ChaseNode always results from a trigger application. However, we do not care so far if the trigger is active or even loaded. We also do not care here whether the derivation is "fair".

Chase Step

To define how one chase step follows from the previous, we introduce an auxiliary definitions that capture that the next ChaseNode in a ChaseDerivationSkeleton always follows from the previous from a trigger application, given that a next node still exists.

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

Equations

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

The ChaseDerivation Structure

The backbone of the ChaseDerivationSkeleton is a PossiblyInfiniteList of ChaseNodes with two 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 next node or there is no next node.

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

• branch : PossiblyInfiniteList (ChaseNode obs rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (n : Nat) (before : ChaseNode obs rules) : before ∈ (self.branch.drop n).head → let after := (self.branch.drop n).tail.head; exists_trigger_opt_fs obs rules before after

Basic Definitions

Here we introduce some auxiliary definitions and theorems and we lift some of the machinery of the underlying PossiblyInfiniteList to ChaseDerivationSkeleton.

@[implicit_reducible]

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

Membership of ChaseNodes in the ChaseDerivationSkeleton directly corresponds to membership in the PossiblyInfiniteList.

Equations

• ChaseDerivationSkeleton.instMembershipChaseNode = { mem := fun (cd : ChaseDerivationSkeleton obs rules) (node : ChaseNode obs rules) => node ∈ cd.branch }

theorem ChaseDerivationSkeleton.mem_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {e : ChaseNode obs rules} : e ∈ cd ↔ ∃ (n : Nat), cd.branch.get? n = some e

An element is a member of the derivation iff it occurs at some index in the underlying branch.

def ChaseDerivationSkeleton.derivation_for_branch_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivationSkeleton obs rules) (l2 : PossiblyInfiniteList (ChaseNode obs rules)) (suffix : l2 <:+ cd.branch) (l2_head_some : l2.head.isSome = true) : ChaseDerivationSkeleton obs rules

Each suffix of the underlying PossiblyInfiniteList is itself a ChaseDerivationSkeleton as long as its head is not none.

Equations

• cd.derivation_for_branch_suffix l2 suffix l2_head_some = { branch := l2, isSome_head := l2_head_some, triggers_exist := ⋯ }

def ChaseDerivationSkeleton.head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivationSkeleton obs rules) : ChaseNode obs rules

The head of the ChaseDerivationSkeleton is the initial ChaseNode. We know that this is never none.

Equations

• cd.head = cd.branch.head.get ⋯

theorem ChaseDerivationSkeleton.head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} : cd.head ∈ cd

The head is a member.

The "next" ChaseNode

For a ChaseDerivationSkeleton derivation, its next node is the ChaseNode immediately following the head. We mainly introduce a couple of theorems here that abstract away the triggers_exist condition from the ChaseDerivationSkeleton definition.

def ChaseDerivationSkeleton.next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivationSkeleton obs rules) : Option (ChaseNode obs rules)

Equations

• cd.next = cd.branch.tail.head

theorem ChaseDerivationSkeleton.next_mem_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (next : ChaseNode obs rules) : next ∈ cd.next → next ∈ cd

The next node is a member.

theorem ChaseDerivationSkeleton.isSome_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next : ChaseNode obs rules} (eq : cd.next = some next) : next.origin.isSome = true

The origin of the next ChaseNode needs to be set.

theorem ChaseDerivationSkeleton.facts_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next : ChaseNode obs rules} (eq : cd.next = some next) : next.facts = cd.head.facts ∪ (next.origin_result ⋯).toSet

The fact set of the next ChaseNode consists exactly of the facts from head and the result of the trigger that introduces next.

ChaseDerivationSkeleton Suffixes

We define a suffix relation on ChaseDerivationSkeleton simply as the suffix relation of the underlying PossiblyInfiniteList.

def ChaseDerivationSkeleton.IsSuffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd1 cd2 : ChaseDerivationSkeleton obs rules) : Prop

Equations

• (cd1 <:+ cd2) = (cd1.branch <:+ cd2.branch)

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

Equations

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

theorem ChaseDerivationSkeleton.IsSuffix_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivationSkeleton obs rules} : cd1 <:+ cd2 ↔ ∃ (m : Nat), cd2.branch.drop m = cd1.branch

Unfolds the definition of the suffix relation.

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

Members of our suffix are also our members.

theorem ChaseDerivationSkeleton.subderivation_of_node_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {node : ChaseNode obs rules} (node_mem : node ∈ cd) : ∃ (cd2 : ChaseDerivationSkeleton obs rules), cd2.head = node ∧ cd2 <:+ cd

Each ChaseNode in the ChaseDerivationSkeleton induces a subderivation.

Tail

If next exists, we can drop the first element from the ChaseDerivationSkeleton and obtain a new ChaseDerivationSkeleton, which, inspired by the PossiblyInfiniteList, we call the tail.

def ChaseDerivationSkeleton.tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivationSkeleton obs rules) (next_some : cd.next.isSome = true) : ChaseDerivationSkeleton obs rules

Equations

• cd.tail next_some = cd.derivation_for_branch_suffix cd.branch.tail ⋯ next_some

theorem ChaseDerivationSkeleton.head_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next_some : cd.next.isSome = true} : some (cd.tail next_some).head = cd.next

The head of the tail is next.

@[simp]

theorem ChaseDerivationSkeleton.head_tail' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next_some : cd.next.isSome = true} : (cd.tail next_some).head = cd.next.get next_some

The head of the tail is next.

theorem ChaseDerivationSkeleton.next_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next_some : cd.next.isSome = true} (next : ChaseNode obs rules) : next ∈ cd.next → next ∈ cd.tail next_some

next is a member of the tail.

theorem ChaseDerivationSkeleton.mem_iff_eq_head_or_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {node : ChaseNode obs rules} : node ∈ cd ↔ node = cd.head ∨ ∃ (h : cd.next.isSome = true), node ∈ cd.tail h

A node is a member if and only if it is either the head or it is a member of the tail.

theorem ChaseDerivationSkeleton.suffix_iff_eq_or_suffix_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivationSkeleton obs rules} : cd1 <:+ cd2 ↔ cd1 = cd2 ∨ ∃ (h : cd2.next.isSome = true), cd1 <:+ cd2.tail h

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

Induction Principle for Members

Similar to PossiblyInfiniteList.mem_rec, we define an induction principle to show properties of ChaseNodes in a ChaseDerivationSkeleton. For this, we introduce ChaseDerivationSkeleton.Node as the subtype of ChaseNode that features a membership proof.

@[reducible, inline]

abbrev ChaseDerivationSkeleton.Node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivationSkeleton obs rules) : Type (max 0 (max u_3 u_2) u_1)

Equations

• cd.Node = { node : ChaseNode obs rules // node ∈ cd }

def ChaseDerivationSkeleton.Node.cast_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivationSkeleton obs rules} (suffix : cd <:+ cd2) (node : cd.Node) : cd2.Node

A Node of our suffix can be cast into our Node type.

Equations

• ChaseDerivationSkeleton.Node.cast_suffix suffix node = ⟨node.val, ⋯⟩

theorem ChaseDerivationSkeleton.mem_rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {motive : cd.Node → Prop} (head : motive ⟨cd.head, ⋯⟩) (step : ∀ (cd2 : ChaseDerivationSkeleton obs rules) (suffix : cd2 <:+ cd), motive ⟨cd2.head, ⋯⟩ → ∀ (next : ChaseNode obs rules) (next_mem : next ∈ cd2.next), motive ⟨next, ⋯⟩) (node : cd.Node) : motive node

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

theorem ChaseDerivationSkeleton.mem_tail_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next_some : cd.next.isSome = true} {node : ChaseNode obs rules} : node ∈ cd.tail next_some ↔ ∃ (cd2 : ChaseDerivationSkeleton obs rules), cd2 <:+ cd ∧ cd2.next = some node

A node is a member of the tail if and only if there is a subderivation where the node is in the next position. 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 ChaseDerivationSkeleton.

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

Each member's facts contain the head facts. Note that this extends to arbitrary pairs of members since each member always induces a subderivation where it acts as the head.

theorem ChaseDerivationSkeleton.mem_suffix_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivationSkeleton obs rules} (suffix : cd1 <:+ cd2) (node : ChaseNode obs rules) : node ∈ cd2 → node.facts ⊆ cd1.head.facts ∨ node ∈ cd1

A first implication of facts_node_subset_every_mem is that, considering one of our subderivations, each of our members either has all of its facts contained in the head of the subderivation or it is itself a member of the subderivation.

Predecessor Relation

We can define a predecessor relation (≼) on ChaseDerivation.Node. At this point, it does not have many properties. On Proper ChaseDerivations it will be a total order.

def ChaseDerivationSkeleton.predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (n1 n2 : cd.Node) : Prop

A node $n$ is a predecessor of a node $m$ if there is a subderivation there $n$ is the head and $m$ is an arbitrary member.

Equations

• (n1 ≼ n2) = ∃ (cd2 : ChaseDerivationSkeleton obs rules), cd2 <:+ cd ∧ cd2.head = n1.val ∧ n2.val ∈ cd2

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

Equations

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

theorem ChaseDerivationSkeleton.predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivationSkeleton obs rules} {n1 n2 : cd.Node} (suffix : cd <:+ cd2) : n1 ≼ n2 → Node.cast_suffix suffix n1 ≼ Node.cast_suffix suffix 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 ChaseDerivationSkeleton.predecessor_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {node : cd.Node} : node ≼ node

The predecessor relation is reflexive.

theorem ChaseDerivationSkeleton.predecessor_total {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (n1 n2 : cd.Node) : n1 ≼ n2 ∨ n2 ≼ n1

The predecessor relation is total.

theorem ChaseDerivationSkeleton.head_prec_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {next : ChaseNode obs rules} (mem : next ∈ cd.next) : ⟨cd.head, ⋯⟩ ≼ ⟨next, ⋯⟩

The head is a predecessor of next.

theorem ChaseDerivationSkeleton.facts_node_subset_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {node1 node2 : cd.Node} : node1 ≼ node2 → node1.val.facts ⊆ node2.val.facts

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

We also define a strict version of the predecessor relation (≺) in the obvious way.

def ChaseDerivationSkeleton.strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (n1 n2 : cd.Node) : Prop

A node is a strict predecessor of another if it is a predecessor but not equal.

Equations

• (n1 ≺ n2) = (n1 ≼ n2 ∧ n1 ≠ n2)

def ChaseDerivationSkeleton.«term_≺_» : Lean.TrailingParserDescr

Equations

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

theorem ChaseDerivationSkeleton.strict_predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivationSkeleton obs rules} {n1 n2 : cd.Node} (suffix : cd <:+ cd2) : n1 ≺ n2 → Node.cast_suffix suffix n1 ≺ Node.cast_suffix suffix n2

As for the predecessor relation, we can show that the relation is stable across suffixes given that we cast the nodes.

theorem ChaseDerivationSkeleton.strict_predecessor_irreflexive {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {n : cd.Node} : ¬n ≺ n

The strict predecessor relation is irreflexive.

theorem ChaseDerivationSkeleton.strict_predecessor_total {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {n1 n2 : cd.Node} : n1 ≠ n2 → n1 ≺ n2 ∨ n2 ≺ n1

The strict predecessor relation is total.

theorem ChaseDerivationSkeleton.eq_or_strict_of_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} {n1 n2 : cd.Node} : n1 ≼ n2 → n1 = n2 ∨ n1 ≺ n2

A predecessor is either equal or a strict predecessor.

Chase Result

Here, we define the result of a ChaseDerivationSkeleton, which is simply the FactSet that is the union of all facts of all ChaseNodes.

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

Equations

• cd.result f = ∃ (node : ChaseNode obs rules), node ∈ cd ∧ f ∈ node.facts

theorem ChaseDerivationSkeleton.facts_node_subset_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (node : ChaseNode obs rules) : node ∈ cd → node.facts ⊆ cd.result

Every node's facts occur in the result.

theorem ChaseDerivationSkeleton.result_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivationSkeleton obs rules} (suffix : cd1 <:+ cd2) : cd1.result = cd2.result

The result of our suffix is the same our result.

theorem ChaseDerivationSkeleton.facts_mem_some_node_of_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (l : List (Fact sig)) : l.toSet ⊆ cd.result → ∃ (node : ChaseNode obs rules), node ∈ cd ∧ l.toSet ⊆ node.facts

For each (finite) list of facts in the result, there is a node that that contains all of them.

theorem ChaseDerivationSkeleton.trg_loaded_for_some_node_of_trg_loaded_for_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivationSkeleton obs rules} (trg : Trigger { cond := obs.cond, monotone := ⋯ }) : trg.loaded cd.result → ∃ (node : ChaseNode obs rules), node ∈ cd ∧ trg.loaded node.facts

If a trigger is loaded for the result, then it is loaded for some node in the derivation.