Chase Derivation

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

As briefly discussed for the ChaseNode already, the chase starts on an initial fact set and then applies triggers until all triggers are obsolete, which might only be the case after infinitely many steps. This whole process needs to be "fair", i.e. a trigger that is active needs to be not active after finitely many steps. This can happen by applying the trigger itself or another trigger that will make the former obsolete.

We should note that chase derivations usually start on a Database, i.e. a finite fact set where all terms are constants. This is what we demand for a ChaseBranch later but for now it is more convenient for us to relax this condition since it is not relevant for most basic definitions and results. What we gain by relaxing the condition is that we can drop an abitrary number of ChaseNodes from the beginning of a derivation and still be left with a derivation. This gives the ChaseDerivation a more coinductive behavior that conveniently alignes with the PossiblyInfiniteList that is used to provide the basic structure of the derivation.

The goal of the chase is to eventually build a most general (i.e. universal) model of a given KnowledgeBase by iteratively satisfying all triggers and thereby all rules. For the more generic ChaseDerivation, we cannot quite expect this as a result but we can already show that the ChaseDerivation.result models all of the rules in ChaseDerivation.result_models_rules.

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 ChaseDerivation.

1. Case: There still exists an active trigger, in which case the next ChaseNode shall be defined accordingly. That is, we add the facts introduced by the trigger to the facts from the previous step and we set the origin of the ChaseNode to the trigger.

2. Case: There is no active trigger. Then the next chase step must be undefined (none), i.e. the ChaseDerivation stops at this point.

def exists_trigger_opt_fs {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsoletenessCondition 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.

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

Equations

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

The ChaseDerivation Structure

The backbone of the ChaseDerivation is a PossiblyInfiniteList 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 next node or there is no trigger and consequently the derivation stops at this point. This is expressed by the two auxiliary definitions above.
3. The derivation needs to be fair. That is, for each trigger, there exists a step in the derivation from which on the trigger is not active.

Expressing the conditions in terms of the machinery available form the PossiblyInfiniteList is admittedly quite convoluted. As part of the framework built around the ChaseDerivation, we will also restate these conditions in a more accessible way. See e.g. ChaseDerivation.fairness'.

structure ChaseDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsoletenessCondition 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 ∨ not_exists_trigger_opt_fs obs rules before after
• fairness (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (i : Nat), (∃ (node : ChaseNode obs rules), node ∈ (self.branch.drop i).head ∧ ¬trg.val.active node.facts) ∧ ∀ (j : Nat) (node2 : ChaseNode obs rules), node2 ∈ (self.branch.drop i).tail.get? j → ¬trg.val.active node2.facts

Basic Definitions

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

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

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

Equations

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

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

Each suffix of the underlying PossiblyInfiniteList is itself a ChaseDerivation 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 := ⋯, fairness := ⋯ }

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

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

Equations

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

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

The head is a member.

The "next" ChaseNode

For a ChaseDerivation 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 ChaseDerivation definition.

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

Equations

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

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

The next node is a member.

theorem ChaseDerivation.isSome_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.active_trigger_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next : ChaseNode obs rules} (eq : cd.next = some next) : (next.origin.get ⋯).fst.val.active cd.head.facts

The trigger used to derive next is active for head.

theorem ChaseDerivation.isSome_next_iff_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} : cd.next.isSome = true ↔ ∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), trg.val.active cd.head.facts

The next node is not none if and only if some trigger is active on head.

theorem ChaseDerivation.facts_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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.

ChaseDerivation Suffixes

We define a suffix relation on ChaseDerivation simply as the suffix relation of the underlying PossiblyInfiniteList. We also use this to state the fairness condition more nicely.

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

Equations

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

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

Equations

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

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

Members of our suffix are also our members.

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

Each ChaseNode in the ChaseDerivation induces a subderivation.

theorem ChaseDerivation.fairness' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (cd2 : ChaseDerivation obs rules), cd2 <:+ cd ∧ ∀ (node : ChaseNode obs rules), node ∈ cd2 → ¬trg.val.active node.facts

Fairness can be stated as: For each trigger, there exists a subderivation such that the trigger is not active for all nodes in the subderivation.

Tail

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

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

Equations

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

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

The head of the tail is next.

theorem ChaseDerivation.head_tail' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.next_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.mem_iff_eq_head_or_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.suffix_iff_eq_or_suffix_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation 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 ChaseDerivation. For this, we introduce ChaseDerivatio.Node as the subtype of ChaseNode that features a membership proof.

@[reducible, inline]

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

Equations

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

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

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

Equations

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

theorem ChaseDerivation.mem_rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {motive : cd.Node → Prop} (head : motive ⟨cd.head, ⋯⟩) (step : ∀ (cd2 : ChaseDerivation 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 ChaseDerivation.mem_tail_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next_some : cd.next.isSome = true} {node : ChaseNode obs rules} : node ∈ cd.tail next_some ↔ ∃ (cd2 : ChaseDerivation 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 ChaseDerivation. This has a couple of convenient implications. For example, we can never see the same ChaseNode twice as otherwise the trigger in second occurrence would already be obsolete.

theorem ChaseDerivation.facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.mem_suffix_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation 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.

theorem ChaseDerivation.head_not_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (h : cd.next.isSome = true) : ¬cd.head ∈ cd.tail h

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

theorem ChaseDerivation.eq_of_suffix_of_head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation obs rules} (suffix : cd1 <:+ cd2) (head_mem : cd2.head ∈ cd1) : cd1 = cd2

By head_not_mem_tail, if we have a suffix but our head occurs in the suffix, then our suffix is equal to us.

theorem ChaseDerivation.suffix_of_suffix_of_suffix_of_head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd cd1 cd2 : ChaseDerivation obs rules} : cd1 <:+ cd → cd2 <:+ cd → cd2.head ∈ cd1 → cd2 <:+ cd1

And now by eq_of_suffix_of_head_mem, if we have two suffixes $C$ and $D$, and the head of $D$ occurs in $C$, then $D$ is a suffix of $C$. This may seem obvious even without the above results but it is really not even though it aligns well with one's intuition. Imagine that a ChaseNode could occur multiple times in a ChaseDerivation. Then we may have a case where $C$ is a subderivation of $D$, $D$ is not a subderivation of $C$ but $D$ occurs in $C$.

Predecessor Relation

Since we learned that ChaseNodes cannot occur multiple times in the same ChaseDerivation, we can define predecessor relation (≼), which is a total order on ChaseDerivation.Node. This is particularly nice, since we can do this while completely ignoring indices of the nodes in the underlying PossiblyInfiniteList.

def ChaseDerivation.predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 : ChaseDerivation obs rules), cd2 <:+ cd ∧ cd2.head = n1.val ∧ n2.val ∈ cd2

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

Equations

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

theorem ChaseDerivation.predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivation 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 ChaseDerivation.predecessor_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {node : cd.Node} : node ≼ node

The predecessor relation is reflexive.

theorem ChaseDerivation.predecessor_antisymm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem ChaseDerivation.predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 n3 : cd.Node} : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

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

The predecessor relation is total.

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

The head is a predecessor of next.

theorem ChaseDerivation.facts_node_subset_of_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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.

theorem ChaseDerivation.fairness_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (node : cd.Node), ∀ (node2 : cd.Node), node ≼ node2 → ¬trg.val.active node2.val.facts

We can express fairness in terms of the predecessor relation: For each trigger, there is a node such that the trigger is not active for each of the node's successors.

We also define a strict version of the predecessor relation (≺) in the obvious way. By that, we obtain a strict total order on ChaseDerivation.Node.

def ChaseDerivation.strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.«term_≺_» : Lean.TrailingParserDescr

Equations

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

theorem ChaseDerivation.strict_predecessor_of_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivation 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 ChaseDerivation.strict_predecessor_irreflexive {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n : cd.Node} : ¬n ≺ n

The strict predecessor relation is irreflexive.

theorem ChaseDerivation.strict_predecessor_asymmetric {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≺ n2 → ¬n2 ≺ n1

The strict predecessor relation is asymmetric.

theorem ChaseDerivation.strict_predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 n3 : cd.Node} : n1 ≺ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive.

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

The strict predecessor relation is total.

theorem ChaseDerivation.head_strict_prec_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next : ChaseNode obs rules} (mem : next ∈ cd.next) : ⟨cd.head, ⋯⟩ ≺ ⟨next, ⋯⟩

The head is a strict predecessor of next.

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

A predecessor is either equal or a strict predecessor.

theorem ChaseDerivation.facts_not_subset_of_strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≺ n2 → ¬n2.val.facts ⊆ n1.val.facts

The facts of a strict successor cannot be a subset of our facts. This is because strict successor nodes can only be introduced by active triggers. But if a trigger only produces facts that already exist, then it cannot be active.

Chase Result

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

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

Equations

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

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

Every node's facts occur in the result.

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

The result of our suffix is the same our result.

theorem ChaseDerivation.facts_mem_some_node_of_mem_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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 ChaseDerivation.trg_loaded_for_some_node_of_trg_loaded_for_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation 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.

theorem ChaseDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} : cd.result.modelsRules rules

The result is a model of all rules. This is true because otherwise, there would be an active trigger on the result. But then, this trigger needs to be active for some node and the hence it needs to become inactive at some point due to fairness. Hence it cannot be active on the result. Contradiction!

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 ChaseNode.

theorem ChaseDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {node : ChaseNode obs rules} (node_mem : node ∈ cd) : node.facts.constants ⊆ cd.head.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 ChaseDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {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.val.facts.terms) : t ∈ cd.head.facts.terms ∨ ∃ (node2 : cd.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.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 ChaseDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.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 ∈ cd.head.facts.terms ∨ ∃ (node2 : cd.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.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 ChaseDerivation.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.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 ∈ cd.head.facts.terms ∨ trg.val.mapped_head[disj_idx].toSet ⊆ node.val.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.

Minimal Nodes with given Properties

If a property hold for a given node in the chase, then there must be a "first" node for which this property holds. That means that this node is minimal with respect to the ≺ relation. The result itself is prop_for_node_has_minimal_such_node and is shown via Nat.prop_for_nat_has_minimal_such_nat. This forces us to take into account specific node indices and therefore requires auxiliary theorems, mainly get?_branch_injective, which is shown using node_has_unique_position.

theorem ChaseDerivation.node_has_unique_position {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (node : ChaseNode obs rules) (i j : Nat) : i < j → cd.branch.get? i = some node → cd.branch.get? j ≠ some node

theorem ChaseDerivation.get?_branch_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (node : ChaseNode obs rules) (i j : Nat) : cd.branch.get? i = some node → cd.branch.get? j = some node → i = j

theorem ChaseDerivation.prop_for_node_has_minimal_such_node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsoletenessCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (prop : cd.Node → Prop) (n : cd.Node) : prop n → ∃ (n2 : cd.Node), prop n2 ∧ ∀ (n3 : cd.Node), n3 ≺ n2 → ¬prop n3