Chase Tree Result is Universal Model Set

This whole file is dedicated to showing that the result of a ChaseTree is a universal model set [BMMP16]. More precisely, we want to show the universality part as we have already shown in ChaseTree.result_models_kb that each element of the result is a model. So what exactly remains to be shown?

We aim to show that for a given ChaseTree for a KnowledgeBase and any model $M$ of the KnowledgeBase, we can pick a fact set $F$ from the result of the chase tree such that there is a homomorphism from $F$ to $M$. This result is shown in RegularChaseTree.universal_result.

The proof works by step-wise construction of both a branch in the chase tree as well as a suitable homomorphism. The constructions builds both at the same time. One step of the construction is done by the hom_step function below, which calls hom_step_of_trg_ex for the heavy lifting. The base of the construction is simply an empty branch and the id mapping. In each step of the construction, we consider an InductiveHomomorphismResult, which we define to be a pair of a node in the chase tree and a GroundTermMapping such that the mapping is a homomorphism from the node into the model $M$.

In the proof of RegularChaseTree.universal_result, we leverage the TreeDerivation.generate_subderivation function with hom_step as the generator function. Besides that, all the homomorphisms from the individual steps need to be combined into a single function. The definition is not too hard and all relevant properties are also not too hard to show once we can establish that the homomorphisms for each step always extend the previous one.

@[reducible, inline]

abbrev AuxiliaryDefsAndTheoremsForUniversalityProof.InductiveHomomorphismResult {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (ct : ChaseTree N obs kb) (m : FactSet sig) : Type (max 0 (max (max u u_3) u_2) u_1)

The InductiveHomomorphismResult is used for the step-wise construction is forms the element that is the input and output of the generator function used in TreeDerivation.generate_subderivation later. It consists of a node in the chase tree and a GroundTermMapping that is a homomorphism from the node to the target model. The generated branch is the chain of all the generated nodes.

Equations

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

noncomputable def AuxiliaryDefsAndTheoremsForUniversalityProof.hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (out_sub_in : ChaseNode.out_sub_in) (ct : ChaseTree N obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (node : ct.NodeWithAddress) (prev_hom : GroundTermMapping sig) (prev_hom_is_homomorphism : prev_hom.isHomomorphism (ChaseNode.outgoingFacts obs kb.rules node.node) m) (children_ne_nil : node.subderivation.childNodes ≠ []) (trg_inactive_of_fresh_term_present : ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)) : InductiveHomomorphismResult ct m

Consider any node in the chase tree together with a homomorphism from this node to the target model. Given that the list of child nodes is not empty, we return one of child node together with an extended homomorphism. How do we know that such a node and homomorphism exist? If the list of children is not empty, there needs to exists a trigger that has been used to derive them. The existing trigger is loaded for the target model but since it is a model, we can also show that it also needs to be satisfied for the model. The way in which the trigger is satisfied in the model dictates which child node we pick and how we define the homomorphisms for the fresh terms introduced by the trigger. This is already all that happens here but it is not quite trivial to show that the constructed GroundTermMapping is indeed a homomorphism.

Equations

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

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.mem_childNodes_of_mem_hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {node : ct.NodeWithAddress} {prev_hom : GroundTermMapping sig} {prev_hom_is_homomorphism : prev_hom.isHomomorphism (ChaseNode.outgoingFacts obs kb.rules node.node) m} {children_ne_nil : node.subderivation.childNodes ≠ []} {trg_inactive_of_fresh_term_present : ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} : (hom_step_of_trg_ex ⋯ ct m m_is_model node prev_hom prev_hom_is_homomorphism children_ne_nil trg_inactive_of_fresh_term_present).val.fst ∈ node.childNodes

The node that we pick in hom_step_of_trg_ex is in the childNodes of the previous node. This is trivial.

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.hom_extends_prev_in_hom_step_of_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {node : ct.NodeWithAddress} {prev_hom : GroundTermMapping sig} {prev_hom_is_homomorphism : prev_hom.isHomomorphism (ChaseNode.outgoingFacts obs kb.rules node.node) m} {children_ne_nil : node.subderivation.childNodes ≠ []} {trg_inactive_of_fresh_term_present : ∀ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} (t : GroundTerm sig) : t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → prev_hom t = (hom_step_of_trg_ex ⋯ ct m m_is_model node prev_hom prev_hom_is_homomorphism children_ne_nil trg_inactive_of_fresh_term_present).val.snd t

The homomorphisms that we construct in hom_step_of_trg_ex agrees with the previous one on all terms in the previous node. This is also trivial.

noncomputable def AuxiliaryDefsAndTheoremsForUniversalityProof.hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (out_sub_in : ChaseNode.out_sub_in) (ct : ChaseTree N obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)) (prev_res : InductiveHomomorphismResult ct m) : Option (InductiveHomomorphismResult ct m)

When extending the InductiveHomomorphismResult from one step to the next, we do not necessarily know that a trigger is active for the current node. Indeed the chase might just have already finished. So we do a simple case distinction here and return an Option either with the result from hom_step_of_trg_ex or simply none.

Equations

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

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.mem_childNodes_of_mem_hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} {prev_res : InductiveHomomorphismResult ct m} (res : InductiveHomomorphismResult ct m) : res ∈ hom_step ⋯ ct m m_is_model trg_inactive_of_fresh_term_present prev_res → res.val.fst ∈ prev_res.val.fst.childNodes

If there is a new node returned by hom_step, then it is in the childNodes of the current node.

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.childNodes_empty_of_hom_step_none {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} {prev_res : InductiveHomomorphismResult ct m} : hom_step ⋯ ct m m_is_model trg_inactive_of_fresh_term_present prev_res = none → prev_res.val.fst.childNodes = []

If hom_step returns none, then the current node does not have any children.

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.hom_extends_prev_in_hom_step {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} {prev_res : InductiveHomomorphismResult ct m} (pair : InductiveHomomorphismResult ct m) : pair ∈ hom_step ⋯ ct m m_is_model trg_inactive_of_fresh_term_present prev_res → ∀ (t : GroundTerm sig), t ∈ (ChaseNode.outgoingFacts obs kb.rules prev_res.val.fst.node).terms → prev_res.val.snd t = pair.val.snd t

The homomorphism returns in hom_step agrees with the current one on all terms from the current node.

noncomputable def AuxiliaryDefsAndTheoremsForUniversalityProof.start_for_infinite_list_of_derivations_and_homomorphisms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (ct : ChaseTree N obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) : InductiveHomomorphismResult ct m

We define the first InductiveHomomorphismResult to be used in the following infinite construction.

Equations

• AuxiliaryDefsAndTheoremsForUniversalityProof.start_for_infinite_list_of_derivations_and_homomorphisms ct m m_is_model = ⟨(TreeDerivation.NodeWithAddress.root ct.toTreeDerivation, id), ⋯⟩

noncomputable def AuxiliaryDefsAndTheoremsForUniversalityProof.infinite_list_of_derivations_and_homomorphisms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (out_sub_in : ChaseNode.out_sub_in) (ct : ChaseTree N obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)) : PossiblyInfiniteList (ChaseDerivation N obs kb.rules × GroundTermMapping sig)

We use the inductive constructor to generate an infinite list of derivations together with their respective homomorphisms.

Equations

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

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.each_step_isHomomorphism_in_infinite_list_of_derivations_and_homomorphisms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} (step : ChaseDerivation N obs kb.rules × GroundTermMapping sig) : step ∈ infinite_list_of_derivations_and_homomorphisms ⋯ ct m m_is_model trg_inactive_of_fresh_term_present → step.snd.isHomomorphism (ChaseNode.outgoingFacts obs kb.rules step.fst.head) m

In every step of the infinite list, the associated mapping is indeed a homomorphism from the step's derivation to the target model.

noncomputable def AuxiliaryDefsAndTheoremsForUniversalityProof.head_infinite_list_of_derivations_and_homomorphisms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] (out_sub_in : ChaseNode.out_sub_in) (ct : ChaseTree N obs kb) (m : FactSet sig) (m_is_model : m.modelsKb kb) (trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)) : ChaseDerivation N obs kb.rules × GroundTermMapping sig

The infinite list always has a first element that we unwrap here.

Equations

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

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.mem_branches_fst_head_infinite_list_of_derivations_and_homomorphisms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} : (head_infinite_list_of_derivations_and_homomorphisms ⋯ ct m m_is_model trg_inactive_of_fresh_term_present).fst ∈ ct.branches

The first derivation in the generated list is a branch in the chase tree.

theorem AuxiliaryDefsAndTheoremsForUniversalityProof.fst_head_infinite_list_of_derivations_and_homomorphisms_eq_list_of_all_heads {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} {N : Type u} [CN : ChaseNode N obs kb.rules] {out_sub_in : ChaseNode.out_sub_in} {ct : ChaseTree N obs kb} {m : FactSet sig} {m_is_model : m.modelsKb kb} {trg_inactive_of_fresh_term_present : ∀ (node : ct.NodeWithAddress) (trg : RTrigger { cond := obs.cond, monotone := ⋯ } kb.rules) (i : Nat) (lt : i < trg.val.rule.head.length) (t : GroundTerm sig), t ∈ trg.val.fresh_terms_for_head_disjunct i lt → t ∈ (ChaseNode.outgoingFacts obs kb.rules node.node).terms → ¬trg.val.active (ChaseNode.outgoingFacts obs kb.rules node.node)} : (head_infinite_list_of_derivations_and_homomorphisms ⋯ ct m m_is_model trg_inactive_of_fresh_term_present).fst.branch = (infinite_list_of_derivations_and_homomorphisms ⋯ ct m m_is_model trg_inactive_of_fresh_term_present).map fun (step : ChaseDerivation N obs kb.rules × GroundTermMapping sig) => step.fst.head

The first derivation in the generated list is equal to taking the heads of each derivation.

theorem RegularChaseTree.universal_result {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} (ct : RegularChaseTree obs kb) (m : FactSet sig) : m.modelsKb kb → ∃ (fs : FactSet sig), ∃ (h : GroundTermMapping sig), fs ∈ ct.result ∧ h.isHomomorphism fs m

As outlined at the very top of this file, we now use TreeDerivation.generate_subderivation with the hom_step generator to obtain the branch in the tree that yields the result FactSet for which the combined GroundTermMappings form a homomorphism into the target model.