Chase Termination for Linear (Multi-Head) Rules

This file contains an attempt of formalizing reductions from one of our recent papers where we show that chase termination is decidable for linear existential rules [GLMON25].

The file contains code contributed by Laila in a student project covering preliminary definitions from the paper up until the mixed derivation. The contents are in an early stage of development. The code will be extended in the future and likely be reworked in the process.

The following definitions around Atom Positions aren't used in the rest of this file yet but could hopefully make some definitions and proofs for linear chase termination a bit easier.

structure AtomPos (sig : Signature) (T : Type u) [DecidableEq sig.P] : Type (max u u_1)

An AtomPos consists of a GeneralizedAtom and a Number i that refers to the term at Position i in that Atom

• a : GeneralizedAtom sig T
• i : Fin self.a.terms.length

def AtomPos.term {sig : Signature} {T : Type u} [DecidableEq sig.P] (pos : AtomPos sig T) : T

Returns the term at the position referred by AtomPos

Equations

• pos.term = pos.a.terms[pos.i]

def AtomPos.idx_valid {sig : Signature} {T : Type u} [DecidableEq sig.P] (a : GeneralizedAtom sig T) (i : Nat) : Bool

i is a valid index for a GeneralizedAtom a if it refers to an actual term of the atom a

Equations

• AtomPos.idx_valid a i = if i < a.terms.length then true else false

def AtomPos.mapping {sig : Signature} {T : Type u} [DecidableEq sig.P] {S : Type u_4} (h : TermMapping T S) (pos : AtomPos sig T) : AtomPos sig S

We apply a TermMapping to an AtomPos by applying the Mapping to the Atom and keeping the same positional Number

Equations

• AtomPos.mapping h pos = { a := h.apply_generalized_atom pos.a, i := Fin.cast ⋯ pos.i }

theorem AtomPos.term_map_eq {sig : Signature} {T : Type u} [DecidableEq sig.P] {S : Type u_1} (pos : AtomPos sig T) (h : TermMapping T S) : h pos.term = (mapping h pos).term

It doesn't matter if we first get the term from a AtomPos and then apply a TermMapping or if we first apply the mapping on the AtomPos and the retrieve the Term

theorem AtomPos.termMapping_AtomPos_eq {sig : Signature} {T : Type u} [DecidableEq sig.P] {S : Type u_1} (h : TermMapping T S) (a : GeneralizedAtom sig T) (i : Fin a.terms.length) : { a := h.apply_generalized_atom a, i := Fin.cast ⋯ i } = mapping h { a := a, i := i }

We get the same result if we first apply a TermMapping to an atom and then build an AtomPos from the result or vice versa

@[implicit_reducible]

instance instInhabitedPreGroundTermOfC {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] : Inhabited (PreGroundTerm sig)

Equations

• instInhabitedPreGroundTermOfC = { default := FiniteTree.leaf default }

@[implicit_reducible]

instance instInhabitedGroundTermOfC {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] : Inhabited (GroundTerm sig)

Equations

• instInhabitedGroundTermOfC = { default := ⟨default, ⋯⟩ }

Linear Existential Rule

A linear rule is an existential Rule that has only a single atom in the body. Here we additionally restrict the rule heads to be a conjunction of exactly two head atoms (usually linear rule heads admit conjunctions of an arbitrary numberof atoms).

def Rule.isLinear {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : Rule sig) : Prop

A Rule is linear if it's body consists of exactli one atom

Equations

• rule.isLinear = (List.length rule.body = 1)

def Rule.exactlyTwoHeadAtoms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : Rule sig) (det : rule.isDeterministic = true) : Prop

Equations

• rule.exactlyTwoHeadAtoms det = (List.length rule.head[0] = 2)

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

• rule : Rule sig
• linear : self.rule.isLinear
• deterministic : self.rule.isDeterministic = true
• exactlyTwoHeadAtoms : self.rule.exactlyTwoHeadAtoms ⋯

def LinearRule.body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : LinearRule sig) : FunctionFreeAtom sig

This function returns the body of a linear rule

Equations

• rule.body = rule.rule.body[0]

def LinearRule.head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : LinearRule sig) : FunctionFreeAtom sig × FunctionFreeAtom sig

This function returns the head of a linear rule as a Pair of the two head-atoms

Equations

• rule.head = (rule.rule.head[0][0], rule.rule.head[0][1])

theorem LinearRule.body_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : LinearRule sig} : rule.rule.body = [rule.body]

theorem LinearRule.head_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : LinearRule sig} : rule.rule.head = [[rule.head.fst, rule.head.snd]]

def is_frontier_position_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : LinearRule sig) (i : Nat) (i_valid : i < rule.body.terms.length) : Prop

An integer i is frontier position in the body of a rule, if the term at the i'th position in the body atom is a frontier variable

Equations

• is_frontier_position_body rule i i_valid = ∃ (v : sig.V), rule.body.terms[i] = VarOrConst.var v ∧ v ∈ rule.rule.frontier

theorem frontier_occus_in_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : LinearRule sig} (i : Nat) (i_valid : i < rule.body.terms.length) : is_frontier_position_body rule i i_valid → rule.body.terms[i] ∈ rule.head.fst.terms ∨ rule.body.terms[i] ∈ rule.head.snd.terms

If i is a frontier position in the body of a rule r, then the term at this position occurs in the head of the rule

theorem frontier_occurs_in_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (r : Rule sig) (v : sig.V) : v ∈ r.frontier → ∃ (f : FunctionFreeAtom sig), f ∈ r.body ∧ VarOrConst.var v ∈ f.terms

if v is a frontier variable of rule r, then v occurs in the body of r

def is_frontier_position_fst {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : LinearRule sig) (i : Nat) (i_valid : i < rule.head.fst.terms.length) : Prop

i is frontier position in the first head atom of a rule, if the term at the i'th position in that atom is a frontier variable

Equations

• is_frontier_position_fst rule i i_valid = ∃ (v : sig.V), rule.head.fst.terms[i] = VarOrConst.var v ∧ v ∈ rule.rule.frontier

theorem frontier_pos_fst_iff_in_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : LinearRule sig} {i : Nat} {i_valid : i < rule.head.fst.terms.length} : is_frontier_position_fst rule i i_valid ↔ ∃ (j : Nat), ∃ (h : j < rule.body.terms.length), rule.head.fst.terms[i].isVar = true ∧ rule.head.fst.terms[i] = rule.body.terms[j]

i is frontier position in the first head atom of a rule iff the term at this position is a variable and also occurs in the rulebody

def is_frontier_position_snd {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rule : LinearRule sig) (i : Nat) (i_valid : i < rule.head.snd.terms.length) : Prop

i is frontier position in the second head atom of a rule, if the term at the i'th position in that atom is a frontier variable

Equations

• is_frontier_position_snd rule i i_valid = ∃ (v : sig.V), rule.head.snd.terms[i] = VarOrConst.var v ∧ v ∈ rule.rule.frontier

theorem frontier_pos_snd_iff_in_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rule : LinearRule sig} {i : Nat} {i_valid : i < rule.head.snd.terms.length} : is_frontier_position_snd rule i i_valid ↔ ∃ (j : Nat), ∃ (h : j < rule.body.terms.length), rule.head.snd.terms[i].isVar = true ∧ rule.head.snd.terms[i] = rule.body.terms[j]

i is frontier position in the second head atom of a rule iff the term at this position is a variable and also occurs in the rulebody

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

• rules : Set (LinearRule sig)
• id_unique (r1 r2 : LinearRule sig) : r1 ∈ self.rules ∧ r2 ∈ self.rules ∧ r1.rule.id = r2.rule.id → r1 = r2

def extend_Substitutution {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (s : GroundSubstitution sig) (v : sig.V) (c : GroundTerm sig) : GroundSubstitution sig

This function modifies the Substitution s such that v ↦ c and otherwise s is the same as before

Equations

• extend_Substitutution s v c x = if x = v then c else s x

def matchVarorConst {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (s : GroundSubstitution sig) (t : VarOrConst sig) (gt : GroundTerm sig) (vars : List sig.V) : Option (GroundSubstitution sig)

This function modifies the Substitution s such that t ↦ gt and returns the modified substitution if possible. Otherwise it returns Option.none The parameter 'vars' serves as a list of variables for which the substition is already 'properly' defined and cannot be changed anymore

Equations

• matchVarorConst s (VarOrConst.const c) gt vars = if gt = GroundTerm.const c then some s else none
• matchVarorConst s (VarOrConst.var v) gt vars = if v ∈ vars then if gt = s v then some s else none else some (extend_Substitutution s v gt)

theorem matchVarorConst.apply_var_or_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {s : GroundSubstitution sig} {t : VarOrConst sig} {gt : GroundTerm sig} {vars : List sig.V} (subs : GroundSubstitution sig) : subs ∈ matchVarorConst s t gt vars → subs.apply_var_or_const t = gt

if 'matchVarOrConst s t gt' returns an actual substitution (Option.some subs) then subs applied on t will return gt

theorem matchVarorConst.noChange_vars {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {v : sig.V} {s : GroundSubstitution sig} {t : VarOrConst sig} {gt : GroundTerm sig} {vars : List sig.V} (subs : GroundSubstitution sig) : subs ∈ matchVarorConst s t gt vars → v ∈ vars → subs v = s v

If a variable v occurs in vars, then the resulting substitution from any call of matchVarorConst (with vars) will behave on v exactly as the substituion before the call

def matchTermList {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (s : GroundSubstitution sig) (vars : List sig.V) (l : List (VarOrConst sig × GroundTerm sig)) : Option (GroundSubstitution sig)

If possible, this function returns substitution subs s.t. subs the List of VarOrConst to the List of GroundTerms (elementwise). Variables in 'vars' need to be mapped exactly as in Substitution s. If such a substitution is not possible, the function returns Option.none

Equations

• One or more equations did not get rendered due to their size.
• matchTermList s vars [] = some s

theorem matchTermList.v_in_vars_noChange {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {ls : List (VarOrConst sig × GroundTerm sig)} {v : sig.V} (s : GroundSubstitution sig) (vars : List sig.V) : v ∈ vars → ∀ (s' : GroundSubstitution sig), s' ∈ matchTermList s vars ls → s' v = s v

Variables that occur in vars are (in the resulting substitution from matchTermList) mapped exactly as in Substitution s

theorem matchTermList.apply_lists {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {l : List (VarOrConst sig × GroundTerm sig)} (s : GroundSubstitution sig) (vars : List sig.V) (subs : GroundSubstitution sig) : subs ∈ matchTermList s vars l → List.map subs.apply_var_or_const l.unzip.fst = l.unzip.snd

The resulting substitution s from matchTermList (if there is one) will map for each pair of l the first element(VarOrConst) to the second one (GroundTerm) when s is applied to l

theorem matchTermList.some_if {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {vars : List sig.V} {s : GroundSubstitution sig} {l : List (VarOrConst sig × GroundTerm sig)} {subs : GroundSubstitution sig} (map_unzip_eq : List.map subs.apply_var_or_const l.unzip.fst = l.unzip.snd) (subs_agrees_on_vars : ∀ (x : sig.V), x ∈ vars → s x = subs x) : ∃ (subs : GroundSubstitution sig), matchTermList s vars l = some subs

If there exists a substitution than maps the first element to the second in each pair of l, then matchTermList will find such a substitution

def GroundSubstitution.from_atom_and_fact {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] (atom : FunctionFreeAtom sig) (fact : Fact sig) : Option (GroundSubstitution sig)

A ground substitution is a homomorphism from an atom to a fact. This function returns such a GroundSubstitution if there exists one. (Otherwise returns Option.none)

Equations

• GroundSubstitution.from_atom_and_fact atom fact = if atom.predicate = fact.predicate then matchTermList (fun (x : sig.V) => default) [] (atom.terms.zip fact.terms) else none

theorem GroundSubstitution.apply_function_free_atom_from_atom_and_fact {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {atom : FunctionFreeAtom sig} {fact : Fact sig} (subs : GroundSubstitution sig) : subs ∈ from_atom_and_fact atom fact → subs.apply_function_free_atom atom = fact

If GroundSubstitution.from_atom_and_fact finds a Substitution s, then s applied on the atom retruns exactly the fact

theorem GroundSubstitution.atom_terms_len_eq_fact_terms_len {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {atom : FunctionFreeAtom sig} {fact : Fact sig} (subs : GroundSubstitution sig) : subs ∈ from_atom_and_fact atom fact → atom.terms.length = fact.terms.length

If a substitution is returned by GroundSubstitution.from_atom_and_fact,then the atom and fact have the same number of terms.

theorem GroundSubstitution.i_lt_atom_terms_len_iff_fact_terms_len {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {atom : FunctionFreeAtom sig} {fact : Fact sig} (subs : GroundSubstitution sig) : subs ∈ from_atom_and_fact atom fact → ∀ (i : Nat), i < atom.terms.length ↔ i < fact.terms.length

If a substitution is returned by GroundSubstitution.from_atom_and_fact,then every number i is less than than the length of the term list of the atomm iff it is also less than the term list lenght of the fact

theorem GroundSubstitution.from_atom_and_fact_some_iff {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {atom : FunctionFreeAtom sig} {fact : Fact sig} : (∃ (subs : GroundSubstitution sig), from_atom_and_fact atom fact = some subs) ↔ ∃ (subs : GroundSubstitution sig), subs.apply_function_free_atom atom = fact

GroundSubstitution.from_atom_and_fact finds a substituition iff there exists one that maps the atom to the fact

def PreTrigger.from_rule_and_fact {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] (rule : LinearRule sig) (fact : Fact sig) : Option (PreTrigger sig)

A PreTrigger consists of a rule and a substitution form the rulebody to a fact. Here we get this substitution via GroundSubstitution.from_atom_and_fact

Equations

• PreTrigger.from_rule_and_fact rule fact = Option.map (fun (subs : GroundSubstitution sig) => { rule := rule.rule, subs := subs }) (GroundSubstitution.from_atom_and_fact rule.body fact)

theorem PreTrigger.from_rule_and_fact_some_implies {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} (trg : PreTrigger sig) : trg ∈ from_rule_and_fact rule fact → trg.rule = rule.rule ∧ GroundSubstitution.from_atom_and_fact rule.body fact = some trg.subs

def ruleApply {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] (rule : LinearRule sig) (fact : Fact sig) : Option (Fact sig × Fact sig)

A rule can be appiled to a fact, if there exists a homomorphism from the rulebody to the fact (iff PreTrigger.from_rule_and_fact is some). The result of the Rule Applycation is then given by trg.mapped_head and consist of two facts (that are obtained from the rulehaed by applying the substitution and skolemization)

Equations

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

theorem ruleApply_eq {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} : have trg_opt := PreTrigger.from_rule_and_fact rule fact; ruleApply rule fact = Option.map (fun (trg : PreTrigger sig) => (trg.apply_to_function_free_atom 0 rule.head.fst, trg.apply_to_function_free_atom 0 rule.head.snd)) trg_opt

theorem ruleApply.some_implies_PreTrigger_some {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} : (ruleApply rule fact).isSome = true → (PreTrigger.from_rule_and_fact rule fact).isSome = true

If ruleApply returns some value for a rule and a fact, then PreTrigger.from_rule_and_fact also returns some value for the same rule and fact

theorem ruleApply.body_length_eq_fact_length {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} (ruleApply_some : (ruleApply rule fact).isSome = true) : rule.body.terms.length = fact.terms.length

If ruleApply returns some for a rule and a fact, then this means, that rulebody and fact have the same number of terms in their resp. atom

theorem ruleApply_fst_term_lenght_eq_rule_head_length {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {ruleApply_some : (ruleApply rule fact).isSome = true} : ((ruleApply rule fact).get ruleApply_some).fst.terms.length = rule.head.fst.terms.length

The resulting first Atom from ruleApply (if it doesn'r return none) hase the same number of terms as the first head atom of the rule

theorem ruleApply_snd_term_lenght_eq_rule_head_length {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {ruleApply_some : (ruleApply rule fact).isSome = true} : ((ruleApply rule fact).get ruleApply_some).snd.terms.length = rule.head.snd.terms.length

The resulting second Atom from ruleApply (if it doesn'r return none) hase the same number of terms as the second head atom of the rule

theorem ruleApply_frontierPos_fstHead {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {i : Nat} (i_valid : i < rule.head.fst.terms.length) (h_frontier : is_frontier_position_fst rule i i_valid) (ruleApplySome : (ruleApply rule fact).isSome = true) : ∃ (j : Nat), ∃ (j_valid : j < fact.terms.length), ((ruleApply rule fact).get ruleApplySome).fst.terms[i] = fact.terms[j]

If i is a frontier-Position in the first head of the rule, then there exists some position j in fact such that ruleApply rule fact will map the term at the frontier-Position to the term at position j in the fact.

theorem rule_terms_eq_implies_ruleApply_terms_eq_fstHead {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {idxH idxB : Nat} (idxH_valid : idxH < rule.head.fst.terms.length) (idxB_valid : idxB < rule.body.terms.length) (ruleApplySome : (ruleApply rule fact).isSome = true) : rule.head.fst.terms[idxH] = rule.body.terms[idxB] → ((ruleApply rule fact).get ruleApplySome).fst.terms[idxH] = fact.terms[idxB]

If some positions in the first atom of the rule head and the body contain the same term, then the heads position of the second fact produced by ruleApply will contain the term that occurs at the rule bodies position in the fact that is given as parameter to ruleApply.

theorem rule_terms_eq_implies_ruleApply_terms_eq_sndHead {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {idxH idxB : Nat} (idxH_valid : idxH < rule.head.snd.terms.length) (idxB_valid : idxB < rule.body.terms.length) (ruleApplySome : (ruleApply rule fact).isSome = true) : rule.head.snd.terms[idxH] = rule.body.terms[idxB] → ((ruleApply rule fact).get ruleApplySome).snd.terms[idxH] = fact.terms[idxB]

If some positions in rule head and body contain the same term, then the heads position of the second fact produced by ruleApply will contain the term that occurs at the rule bodies position in the fact that is given as parameter to ruleApply.

theorem ruleApply_frontierPos_sndHead {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {i : Nat} (i_valid : i < rule.head.snd.terms.length) (h_frontier : is_frontier_position_snd rule i i_valid) (ruleApplySome : (ruleApply rule fact).isSome = true) : ∃ (j : Nat), ∃ (j_valid : j < fact.terms.length), ((ruleApply rule fact).get ruleApplySome).snd.terms[i] = fact.terms[j]

theorem ruleApply_non_frontier_var_fstHead_is_fun {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {i : Nat} (i_valid : i < rule.head.fst.terms.length) (ruleApplySome : (ruleApply rule fact).isSome = true) : (∃ (v : sig.V), rule.head.fst.terms[i] = VarOrConst.var v ∧ ¬v ∈ rule.rule.frontier) → ∃ (a : SkolemFS sig), ∃ (b : List (GroundTerm sig)), ∃ (c : b.length = a.arity), ((ruleApply rule fact).get ruleApplySome).fst.terms[i] = GroundTerm.func a b c

If i is a position in the first rule head containing a non-frontier-variable (i.e. an existential variable),then ruleApply will map the term at this position to a functional term (a SkolemFunction)

theorem ruleApply_non_frontier_var_sndHead_is_fun {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [Inhabited sig.C] {rule : LinearRule sig} {fact : Fact sig} {i : Nat} (i_valid : i < rule.head.snd.terms.length) (ruleApplySome : (ruleApply rule fact).isSome = true) : (∃ (v : sig.V), rule.head.snd.terms[i] = VarOrConst.var v ∧ ¬v ∈ rule.rule.frontier) → ∃ (a : SkolemFS sig), ∃ (b : List (GroundTerm sig)), ∃ (c : b.length = a.arity), ((ruleApply rule fact).get ruleApplySome).snd.terms[i] = GroundTerm.func a b c

If i is a position in the second rule head containing a non-frontier-variable (i.e. an existential variable),then ruleApply will map the term at this position to a functional term (a SkolemFunction)

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

an AddressSymbol consists of a Linear Rule and a Number 0 or 1 that references the first(0) or second(1) head of that rule

• rule : LinearRule sig
• headIndex : Fin 2

def addressSymbols {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (rs : LinearRuleSet sig) : Set (AddressSymbol sig)

This function defines the set of all possible Address symbols of a rule set

Equations

• addressSymbols rs sym = (sym.rule ∈ rs.rules)

structure Address {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_1 u_2) u_3)

An Address consists of an initial fact from the fat set and a list of address symbols from the rule set. The paper considers them a a word wu ∈ (fact set)(addressSymbols)* which allows talking about prefixes of addresses

• initialAtom : { f : Fact sig // f ∈ fs }
• path : List { sym : AddressSymbol sig // sym ∈ addressSymbols rs }

def immed_prefix_address_in_set {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} {fs : FactSet sig} (a : Address fs rs) (f : Set (Address fs rs)) : Prop

This definition returns true iff the immediate prefix of an address (i.e. the same Address just with the Address-path being shortend by the first symbol) is contained is Set f

Equations

• immed_prefix_address_in_set a f = match a.path with | [] => true = true | head :: ls => have b := { initialAtom := a.initialAtom, path := ls }; b ∈ f

structure Forest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_1 u_2) u_3)

A forest is a set of addresses with the following two properties: (1) the fact set is fully contained in the forest and (2) for each addresses all its prefixae are in the forest too

• f : Set (Address fs rs)
• fs_contained (fact : Fact sig) : fact ∈ fs → ∃ (a : Address fs rs), a ∈ self.f ∧ fact = a.initialAtom.val ∧ a.path = []
• isPrefixClosed (a : Address fs rs) : a ∈ self.f → immed_prefix_address_in_set a self.f

def Forest.subforest_of {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} {fs : FactSet sig} (g f : Forest fs rs) : Prop

A forest is subforest of another one if it is a subset

Equations

• g.subforest_of f = (g.f ⊆ f.f)

theorem Forest.subforest_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} {fs : FactSet sig} {f : Forest fs rs} : f.subforest_of f

The subforest relation is reflexive

theorem Forest.subforest_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} {fs : FactSet sig} {f g h : Forest fs rs} : f.subforest_of g → g.subforest_of h → f.subforest_of h

def FactSet.toForest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} (fs : FactSet sig) : Forest fs rs

A Fact set can be seen as a forest too where all adresses have an empty path

Equations

• fs.toForest = { f := fun (x : Address fs rs) => x.path = [], fs_contained := ⋯, isPrefixClosed := ⋯ }

@[irreducible]

def labellingFunction {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {fs : FactSet sig} {rs : LinearRuleSet sig} (w : Address fs rs) : Option (Fact sig)

The Labelling Function maps an address to a fact if possible. The fact is created by successively applying the rules of the address symbols. Starting from the initial atom of the address, the rule of the first address symbol is applied then from the result one takes the head atom that is referenced by the address symbol and applies the naxt rule onto that. As rule applycation may fail (if there is no homomorphism) the labelling can also return none

Equations

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

def oblivious_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (fs : FactSet sig) (rs : LinearRuleSet sig) : Forest fs rs

The oblivious chase representation is the forest of all addresses where the labelling function returns Option.some fact

Equations

• oblivious_chase fs rs = { f := fun (addr : Address fs rs) => (labellingFunction addr).isSome = true, fs_contained := ⋯, isPrefixClosed := ⋯ }

def materialization_labelling {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (g : Forest fs rs) : FactSet sig

The materialization of a forest is the set of all facts that can be produced by labellings from addresses of the forest

Equations

• materialization_labelling g a = ∃ (b : Address fs rs), b ∈ g.f ∧ labellingFunction b = some a

theorem subforest_of_oblivious_chase_labelling_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {h : g.subforest_of (oblivious_chase fs rs)} (a : Address fs rs) : a ∈ g.f → (labellingFunction a).isSome = true

For all Addresses that are part of a subforest of the obllivious chase the labbeling function returns some fact

structure LinearRuleTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_1 u_2) u_3)

A trigger consists of a Linear rule from the rule set and an address such that there exists an homomorphism from the rulebody to the labelling of the address

• rule : { r : LinearRule sig // r ∈ rs.rules }
• addr : { u : Address fs rs // (labellingFunction u).isSome = true }
• hom_exists : (GroundSubstitution.from_atom_and_fact self.rule.val.body ((labellingFunction self.addr.val).get ⋯)).isSome = true

def LinearRuleTrigger.apply {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (pi : LinearRuleTrigger fs rs) : Address fs rs × Address fs rs

from the trigger's rule on can bild two address symbols (one for each head). The Appplication of the trigger produces the two addresses that arise from adding one of those address symbols each to the trigger's address

Equations

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

theorem LinearRuleTrigger.ruleApply_of_trigger_labelling_is_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : (ruleApply pi.rule.val ((labellingFunction pi.addr.val).get ⋯)).isSome = true

If you call ruleApply on the trigger's rule and labelling of the address, then you get Option.some value

theorem LinearRuleTrigger.labellingFunction_trg_apply_is_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : (labellingFunction pi.apply.fst).isSome = true ∧ (labellingFunction pi.apply.snd).isSome = true

The labelling of the addresses produced by the trigger applicstion is some

def LinearRuleTrigger.labelling_of_apply {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (pi : LinearRuleTrigger fs rs) : Fact sig × Fact sig

this function gives a shortcut for retrieving the actual labellings for the addresses created by the trigger application

Equations

• pi.labelling_of_apply = (ruleApply pi.rule.val ((labellingFunction pi.addr.val).get ⋯)).get ⋯

theorem LinearRuleTrigger.labelling_of_apply_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : Prod.map some some pi.labelling_of_apply = (labellingFunction pi.apply.fst, labellingFunction pi.apply.snd)

this shows that the schortcut of labelling_of_apply is actually correct

theorem LinearRuleTrigger.trg_apply_labelling_fst_predicate_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : pi.rule.val.head.fst.predicate = pi.labelling_of_apply.fst.predicate

The predicates of the first atom of the trigger'st rule head and the first fact produced by labelling_of_apply are the same

theorem LinearRuleTrigger.trg_apply_labelling_snd_predicate_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : pi.rule.val.head.snd.predicate = pi.labelling_of_apply.snd.predicate

The predicates of the second atom of the rule head and the second fact produced by labelling_of_apply are the same

theorem LinearRuleTrigger.trg_apply_labelling_fst_terms_len {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : pi.rule.val.head.fst.terms.length = pi.labelling_of_apply.fst.terms.length

The number of terms in the first atom of the trigger's rule head and in the first fact produced by labelling_of_apply are the same

theorem LinearRuleTrigger.trg_apply_labelling_snd_terms_len {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : pi.rule.val.head.snd.terms.length = pi.labelling_of_apply.snd.terms.length

The number of terms in the second atom of the trigger's rule head and in the second fact produced by labelling_of_apply are the same

theorem LinearRuleTrigger.rule_body_terms_len_eq_addr_labelling_terms_len {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} : pi.rule.val.body.terms.length = ((labellingFunction pi.addr.val).get ⋯).terms.length

The atom in the trigger's rule's body has the same number of terms ar the fact produced by the labelling of the trigger's address

theorem LinearRuleTrigger.term_in_rule_eq_implies_in_labelling_eq_fstHead {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} {idxB idxH : Nat} (idxB_valid : idxB < pi.rule.val.body.terms.length) (idxH_valid : idxH < pi.rule.val.head.fst.terms.length) : pi.rule.val.body.terms[idxB] = pi.rule.val.head.fst.terms[idxH] → ((labellingFunction pi.addr.val).get ⋯).terms[idxB] = pi.labelling_of_apply.fst.terms[idxH]

If some positions idxH,idxB in the trigger's first rule head and body (resp.) contain the same term (this is then either a frontier variable or constant), then the first fact produced by labelling_of_apply contains the same term at position idxH, as the labelling of the trigger's address contains at idxB.

theorem LinearRuleTrigger.term_in_rule_eq_implies_in_labelling_eq_sndHead {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {pi : LinearRuleTrigger fs rs} {idxB idxH : Nat} (idxB_valid : idxB < pi.rule.val.body.terms.length) (idxH_valid : idxH < pi.rule.val.head.snd.terms.length) : pi.rule.val.body.terms[idxB] = pi.rule.val.head.snd.terms[idxH] → ((labellingFunction pi.addr.val).get ⋯).terms[idxB] = pi.labelling_of_apply.snd.terms[idxH]

If some positions idxH,idxB in the trigger's second rule head and body (resp.) contain the same term (this is then either a frontier variable or constant), then the second fact produced by labelling_of_apply contains the same term at position idxH, as the labelling of the trigger's address contains at idxB.

def LinearRuleTrigger.appears_in_forest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (pi : LinearRuleTrigger fs rs) (g : Forest fs rs) : Prop

A trigger appears in a forest, if it's address is part of the forest

Equations

• pi.appears_in_forest g = (pi.addr.val ∈ g.f)

def LinearRuleTrigger.isActive_in_forest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (pi : LinearRuleTrigger fs rs) (g : Forest fs rs) : Prop

A trigger is active in a forest, if it's address is part of that forest, but at least one of the addresses that are produced by trigger application isn't part of the forest.

Equations

• pi.isActive_in_forest g = (pi.appears_in_forest g ∧ ¬(pi.apply.fst ∈ g.f ∧ pi.apply.snd ∈ g.f))

def LinearRuleTrigger.forest_Address {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {rs : LinearRuleSet sig} {fs : FactSet sig} (g : Forest fs rs) : Type (max 0 (max u_3 u_2) u_1)

A forest-address is just an address that occurs in a specific forest

Equations

• LinearRuleTrigger.forest_Address g = { addr : Address fs rs // addr ∈ g.f }

theorem LinearRuleTrigger.forest_addr_label_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {g_sub : g.subforest_of (oblivious_chase fs rs)} {b : forest_Address g} : (labellingFunction b.val).isSome = true

every forest address where the forest is subforest of the oblivious chase is labelled to Option.some ... by the labellingFunction

def LinearRuleTrigger.forest_Trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (g : Forest fs rs) : Type (max 0 (max u_3 u_2) u_1)

A forest_trigger of a forest is a trigger that appears in that specific forest

Equations

• LinearRuleTrigger.forest_Trigger g = { trg : LinearRuleTrigger fs rs // trg.appears_in_forest g }

def LinearRuleTrigger.blockingTeam {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} (g_sub : g.subforest_of (oblivious_chase fs rs)) (b1 b2 : forest_Address g) (pi : forest_Trigger g) : Prop

Two addresses b1, b2 are Blocking team for a trigger iff ...(See definition 11 in the paper). Note that this definition slighliy differs from the definition in the paper in the sense that we don't requite h to be the identity on ⟨u⟩ but only on the frontier-positional terms in ⟨u⟩

Equations

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

structure LinearRuleTrigger.Conditions {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} (g_sub : g.subforest_of (oblivious_chase fs rs)) (b1 b2 : forest_Address g) (pi : forest_Trigger g) : Type (max (max u_1 u_2) u_3)

these are the three conditions from the alternative blocking-team definition. If they hold true then b1 and b2 are a plocking team for the trigger (see Observation 12 in the paper). Note that we needed to add the treatment of constants at condition two.

• b1_label : Fact sig
• b2_label : Fact sig
• b1_label_eq : self.b1_label = (labellingFunction b1.val).get ⋯
• b2_label_eq : self.b2_label = (labellingFunction b2.val).get ⋯
• first : self.b1_label.predicate = pi.val.labelling_of_apply.fst.predicate ∧ self.b2_label.predicate = pi.val.labelling_of_apply.snd.predicate
• second : (∀ (j : Nat) (lt_fst : j < pi.val.rule.val.head.fst.terms.length), (is_frontier_position_fst pi.val.rule.val j lt_fst ∨ ∃ (c : sig.C), pi.val.rule.val.head.fst.terms[j] = VarOrConst.const c) → pi.val.labelling_of_apply.fst.terms[j] = self.b1_label.terms[j]) ∧ ∀ (j : Nat) (lt_snd : j < pi.val.rule.val.head.snd.terms.length), (is_frontier_position_snd pi.val.rule.val j lt_snd ∨ ∃ (c : sig.C), pi.val.rule.val.head.snd.terms[j] = VarOrConst.const c) → pi.val.labelling_of_apply.snd.terms[j] = self.b2_label.terms[j]
• third : (∀ (i j : Nat), pi.val.labelling_of_apply.fst.terms[i]? = pi.val.labelling_of_apply.fst.terms[j]? → self.b1_label.terms[i]? = self.b1_label.terms[j]?) ∧ (∀ (i j : Nat), pi.val.labelling_of_apply.fst.terms[i]? = pi.val.labelling_of_apply.snd.terms[j]? → self.b1_label.terms[i]? = self.b2_label.terms[j]?) ∧ ∀ (i j : Nat), pi.val.labelling_of_apply.snd.terms[i]? = pi.val.labelling_of_apply.snd.terms[j]? → self.b2_label.terms[i]? = self.b2_label.terms[j]?

theorem LinearRuleTrigger.b1_label_terms_idxOf_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {g_sub : g.subforest_of (oblivious_chase fs rs)} {b1 b2 : forest_Address g} {pi : forest_Trigger g} {cond : Conditions g_sub b1 b2 pi} (i : Nat) (i_lt : i < pi.val.labelling_of_apply.fst.terms.length) : cond.b1_label.terms[List.idxOf pi.val.labelling_of_apply.fst.terms[i] pi.val.labelling_of_apply.fst.terms] = cond.b1_label.terms[i]

this is just a helper theorem to simplify the expression cond.b1_label.terms[List.idxOf pi.val.labelling_of_apply.fst.terms[i] pi.val.labelling_of_apply.fst.terms] Maybe this could be stated in a more general result (?)

theorem LinearRuleTrigger.b2_label_terms_idxOf_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {g_sub : g.subforest_of (oblivious_chase fs rs)} {b1 b2 : forest_Address g} {pi : forest_Trigger g} {cond : Conditions g_sub b1 b2 pi} (i : Nat) (i_lt : i < pi.val.labelling_of_apply.snd.terms.length) : cond.b2_label.terms[List.idxOf pi.val.labelling_of_apply.snd.terms[i] pi.val.labelling_of_apply.snd.terms] = cond.b2_label.terms[i]

this is just a helper theorem to simplify the expression cond.b2_label.terms[List.idxOf pi.val.labelling_of_apply.snd.terms[i] pi.val.labelling_of_apply.snd.terms]

theorem LinearRuleTrigger.blockingTeam.iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {g_sub : g.subforest_of (oblivious_chase fs rs)} {b1 b2 : forest_Address g} {pi : forest_Trigger g} : blockingTeam g_sub b1 b2 pi ↔ ∃ (x : Conditions g_sub b1 b2 pi), True

this shows the equivalence of the two definitons for blocking teams (This is the proof for observation 12 in the paper)

def LinearRuleTrigger.active_trigger_apply_resulting_forest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (pi : LinearRuleTrigger fs rs) (g : Forest fs rs) (pi_active : pi.isActive_in_forest g) : Forest fs rs

returns the resulting forest that arises if one adds the result of pi.apply to forest g if pi is a Trigger that is active in g

Equations

• pi.active_trigger_apply_resulting_forest g pi_active = { f := fun (x : Address fs rs) => x ∈ g.f ∨ x = pi.apply.fst ∨ x = pi.apply.snd, fs_contained := ⋯, isPrefixClosed := ⋯ }

theorem LinearRuleTrigger.forest_subforest_trigger_apply_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {g : Forest fs rs} {pi : LinearRuleTrigger fs rs} {pi_active : pi.isActive_in_forest g} : g.subforest_of (pi.active_trigger_apply_resulting_forest g pi_active)

the original forest g is a subforest of the one produced by active_trigger_apply_resulting_forest

@[reducible, inline]

abbrev PreChaseDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_3 u_2) u_1)

A PossiblyInfiniteList of triggers is called PreChaseDerivation

Equations

• PreChaseDerivation fs rs = PossiblyInfiniteList (LinearRuleTrigger fs rs)

structure PreChaseDerivation.trg_application_cond {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (trg : LinearRuleTrigger fs rs) (before : Forest fs rs) (after : Option (Forest fs rs)) : Prop

This structure defines two conditions that must hold for the correspondence between a trigger and two forests. It is be needed to define chase derivations. (1) the trigger must be active in the forest 'before' (2) adding the application of the trigger to forest 'before' results in the forest 'after'

• active : trg.isActive_in_forest before
• result : after = some (trg.active_trigger_apply_resulting_forest before ⋯)

def PreChaseDerivation.forest_seq_valid {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (trg_seq : PreChaseDerivation fs rs) (forest_seq : PossiblyInfiniteList (Forest fs rs)) : Prop

A forest sequence is valid for a PreChaseDerivation-trigger sequence, if it (1) starts with the fact set and then (2) for each number n on which the trigger sequence is defined, the trg_application_condition holds for that trigger together with the forests at positions n and n+1 in the forest-sequence

Equations

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

theorem PreChaseDerivation.forest_seq_valid_implies_unique {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {trg_seq : PreChaseDerivation fs rs} (forest_seq_1 forest_seq_2 : PossiblyInfiniteList (Forest fs rs)) : trg_seq.forest_seq_valid forest_seq_1 ∧ trg_seq.forest_seq_valid forest_seq_2 → forest_seq_1 = forest_seq_2

if two forest sequences are both valid for the same trigger-sequence, then they are equal

theorem PreChaseDerivation.forest_seq_valid_subset_oblivious_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {trg_seq : PreChaseDerivation fs rs} (forest_seq : PossiblyInfiniteList (Forest fs rs)) : trg_seq.forest_seq_valid forest_seq → ∀ (n : Nat), (forest_seq.get? n).elim True fun (f : Forest fs rs) => f.subforest_of (oblivious_chase fs rs)

every forest that occurs in a valid forest-sequence is subforest of the oblivious chase

structure LChaseDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_1 u_2) u_3)

A chase derivation consists of a Possibly infinite trigger sequence, together with a forest sequence that is valid for the trigger sequence

• trigger_seq : PreChaseDerivation fs rs
• forest_seq : PossiblyInfiniteList (Forest fs rs)
• cond : self.trigger_seq.forest_seq_valid self.forest_seq

theorem LChaseDerivation.trg_seq_n_some_then_forest_seq_n_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) : (PossiblyInfiniteList.get? deriv.trigger_seq n).isSome = true → (deriv.forest_seq.get? n).isSome = true

If the trigger sequence of a chasederivation is defined (Option.isSome) at position n the so is the forest sequence

theorem LChaseDerivation.forest_succc_n_some_then_trg_n_some {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) : (deriv.forest_seq.get? (n + 1)).isSome = true → (PossiblyInfiniteList.get? deriv.trigger_seq n).isSome = true

if the forest sequence is defined (Option.isSome) at position n+1 then the trigger sequence is defined at position n

theorem LChaseDerivation.trg_n_active {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) (trg : LinearRuleTrigger fs rs) (trg_n : trg ∈ PossiblyInfiniteList.get? deriv.trigger_seq n) : trg.isActive_in_forest ((deriv.forest_seq.get? n).get ⋯)

for every n, the trigger in the trigger sequence at position n (if there is some) is active in the forest of the forest-sequence at position n

theorem LChaseDerivation.trg_n_forest_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) (trg : LinearRuleTrigger fs rs) (trg_n : trg ∈ PossiblyInfiniteList.get? deriv.trigger_seq n) : trg.appears_in_forest ((deriv.forest_seq.get? n).get ⋯)

for every n, the trigger in the trigger sequence at position n (if there is some) appears in the forest of the forest-sequence at position n

theorem LChaseDerivation.forest_n_subforest_succ {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) (f : Forest fs rs) : f ∈ deriv.forest_seq.get? n → ∀ (f2 : Forest fs rs), f2 ∈ deriv.forest_seq.get? n.succ → f.subforest_of f2

every forest in the forest sequence is subforest of its successor forest in that sequence

theorem LChaseDerivation.forest_n_subforest_all_succ {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} (n : Nat) (f : Forest fs rs) : f ∈ deriv.forest_seq.get? n → ∀ (n2 : Nat), n2 ≥ n → ∀ (f2 : Forest fs rs), f2 ∈ deriv.forest_seq.get? n2 → f.subforest_of f2

every forest in the forest sequence is subforest of all its successor forests in that sequence

def LChaseDerivation.chaseForest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (deriv : LChaseDerivation fs rs) : Forest fs rs

a chase forest is defined as the union of all forests that occur in the forest sequence of the chase derivation. This is also a forest.

Equations

• deriv.chaseForest = { f := fun (addr : Address fs rs) => ∃ (forest : Forest fs rs), addr ∈ forest.f ∧ forest ∈ deriv.forest_seq, fs_contained := ⋯, isPrefixClosed := ⋯ }

theorem LChaseDerivation.chaseForest_subforest_obliviousChase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} {deriv : LChaseDerivation fs rs} : deriv.chaseForest.subforest_of (oblivious_chase fs rs)

the chase forest is subforest of the oblivious chase

def LChaseDerivation.is_oblivious {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (deriv : LChaseDerivation fs rs) : Prop

a chase derivation is called oblivous, if its chase forest equals the oblivious chase representation (defined by oblivious_chase)

Equations

• deriv.is_oblivious = (deriv.chaseForest = oblivious_chase fs rs)

def LChaseDerivation.trg_n_not_blocked_in_forest {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (n : Nat) (deriv : LChaseDerivation fs rs) : Prop

In a chase derivation, the trigger at position n in the trigger sequence is not blocked in forest at position n (in the forest sequence), if there doesn't exist a blocking team for the trigger in that forest.

Equations

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

def LChaseDerivation.is_resricted {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (deriv : LChaseDerivation fs rs) : Prop

a chese derivation is called restricted if no trigger of the trigger-sequence is blocked in its corresponding forest

Equations

• deriv.is_resricted = ∀ (n : Nat), LChaseDerivation.trg_n_not_blocked_in_forest n deriv

def LChaseDerivation.is_fair {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (deriv : LChaseDerivation fs rs) : Prop

a chase derivation is called fair, if every trigger that is active in the chaseForest of that derivation also has a blocking team in the chaseForest

Equations

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

def LChaseDerivation.subsequence {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] {rs : LinearRuleSet sig} {fs : FactSet sig} (deriv1 deriv2 : LChaseDerivation fs rs) : Prop

Derivation deriv1 is a subsequence of deriv2, if it can be created from deriv2 by dropping 'unneccessary' elements.

Equations

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

structure LChaseDerivation.mixedDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [Inhabited sig.C] (fs : FactSet sig) (rs : LinearRuleSet sig) : Type (max (max u_1 u_2) u_3)

A mixed derivation consists of a oblivious chase derivation m, a restricted chase derivation r that is subsequence of m and we additionally have the condition that every trigger of m at position n that also occurs somewhere in r is not blocked in the forest at position n from m

• m : LChaseDerivation fs rs
• m_obliv : self.m.is_oblivious ∧ ¬PossiblyInfiniteList.finite self.m.trigger_seq
• r : LChaseDerivation fs rs
• r_restr : self.r.is_resricted ∧ self.r.is_fair ∧ ¬PossiblyInfiniteList.finite self.r.trigger_seq
• sub : self.r.subsequence self.m
• trg_blocked (n : Nat) : ∃ (trg : LinearRuleTrigger fs rs), PossiblyInfiniteList.get? self.m.trigger_seq n = some trg ∧ trg ∈ self.r.trigger_seq → trg_n_not_blocked_in_forest n self.m