PreTriggers

Triggers are one of the most essential definitions for the chase. They are our primary way for modelling specific applications of rules. Quite simply, a trigger is just a pair of a rule and a substitution that tells us how variables should be replaced. For actual triggers, we will require a way to tell if they should still be applied or not. We refer to this with the notion of "obsolescence" later. However, most of the machinery around triggers can be introduced agnostic of any kind of obsolescence. Consequently, we call the "almost trigger" a PreTrigger.

A trigger is self contained in the sense that it "knows" what its result will be independant of the chase context. This would not be so simple if we considered nulls instead of Skolem terms.

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

A PreTrigger is nothing more than a pair of a Rule and a GroundSubstitution.

• rule : Rule sig
• subs : GroundSubstitution sig

def PreTrigger.mapped_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : List (GroundTerm sig)

The mapped_frontier results from applying the triggers substitution to all frontier variables.

Equations

• trg.mapped_frontier = List.map trg.subs trg.rule.frontier

@[simp]

theorem PreTrigger.length_mapped_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} : trg.mapped_frontier.length = trg.rule.frontier.length

The lenth of the mapped_frontier is exactly the length of the frontier.

theorem PreTrigger.apply_mapping_after_mapped_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {mapping : TermMapping (GroundTerm sig) (GroundTerm sig)} : List.map mapping trg.mapped_frontier = { rule := trg.rule, subs := mapping ∘ trg.subs }.mapped_frontier

Applying a term mapping after the trigger can be combined with the substitution without affecting the mapped_frontier.

def PreTrigger.skolemize_var_or_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (var_or_const : VarOrConst sig) : SkolemTerm sig

In the context of a trigger, we Skolemize a VarOrConst by passing the rule in the trigger.

Equations

• trg.skolemize_var_or_const i lt var_or_const = VarOrConst.skolemize trg.rule i lt var_or_const

def PreTrigger.apply_to_var_or_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) : TermMapping (VarOrConst sig) (GroundTerm sig)

We apply a trigger to a VarOrConst by Skolemizing and then applying the GroundSubstitution from the trigger. We need this to define the trigger result later.

Equations

• trg.apply_to_var_or_const i lt = trg.subs.apply_skolem_term ∘ trg.skolemize_var_or_const i lt

@[simp]

theorem PreTrigger.apply_to_var_or_const_for_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (c : sig.C) : trg.apply_to_var_or_const i lt (VarOrConst.const c) = GroundTerm.const c

Applying a trigger to a constant changes nothing.

@[simp]

theorem PreTrigger.apply_to_var_or_const_of_not_mem_existential_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) : ¬v ∈ trg.rule.existential_vars_for_head_disjunct i lt → trg.apply_to_var_or_const i lt (VarOrConst.var v) = trg.subs v

Applying a trigger to an non-existential variable does not skolemize but merely applied the substitution.

@[simp]

theorem PreTrigger.apply_to_var_or_const_frontier_var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) : v ∈ trg.rule.frontier → trg.apply_to_var_or_const i lt (VarOrConst.var v) = trg.subs v

Applying a trigger to a frontier variable does not skolemize but merely applied the substitution.

def PreTrigger.functional_term_for_var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) (v_mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : GroundTerm sig

A shortcut definition for how the Skolem term resulting from applying the trigger to an existential variable will look.

Equations

• trg.functional_term_for_var i lt v v_mem = GroundTerm.func { rule := trg.rule, headIdx := i, headIdx_lt := lt, v := v, v_mem := v_mem } trg.mapped_frontier ⋯

theorem PreTrigger.functional_term_for_var.inj {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i1 i2 : Nat} {lt1 : i1 < trg.rule.head.length} {lt2 : i2 < trg.rule.head.length} {v1 : sig.V} {v1_mem : v1 ∈ trg.rule.existential_vars_for_head_disjunct i1 lt1} {v2 : sig.V} {v2_mem : v2 ∈ trg.rule.existential_vars_for_head_disjunct i2 lt2} : trg.functional_term_for_var i1 lt1 v1 v1_mem = trg.functional_term_for_var i2 lt2 v2 v2_mem → i1 = i2 ∧ v1 = v2

The functional_term_for_var function is injective for a fixed trigger.

@[simp]

theorem PreTrigger.functional_term_for_var.injEq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i1 i2 : Nat} {lt1 : i1 < trg.rule.head.length} {lt2 : i2 < trg.rule.head.length} {v1 : sig.V} {v1_mem : v1 ∈ trg.rule.existential_vars_for_head_disjunct i1 lt1} {v2 : sig.V} {v2_mem : v2 ∈ trg.rule.existential_vars_for_head_disjunct i2 lt2} : trg.functional_term_for_var i1 lt1 v1 v1_mem = trg.functional_term_for_var i2 lt2 v2 v2_mem ↔ i1 = i2 ∧ v1 = v2

@[simp]

theorem PreTrigger.apply_to_var_or_const_of_mem_existential_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) (mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : trg.apply_to_var_or_const i lt (VarOrConst.var v) = trg.functional_term_for_var i lt v mem

Applying a trigger to an existential variable, yields exactly the Skolem function term from the shortcup definition functional_term_for_var.

theorem PreTrigger.apply_to_var_or_const_injective_of_mem_existential_vars {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {v : sig.V} (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v_mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) (voc : VarOrConst sig) : voc ∈ trg.rule.head[i].terms → trg.apply_to_var_or_const i lt (VarOrConst.var v) = trg.apply_to_var_or_const i lt voc → VarOrConst.var v = voc

For existential variables, applying the trigger is injective.

theorem PreTrigger.result_term_not_in_frontier_image_of_var_existential {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (v : sig.V) (v_existential : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : ¬trg.apply_to_var_or_const i lt (VarOrConst.var v) ∈ trg.mapped_frontier

Applying the trigger to non-frontier variables yields a term that cannot possibly be in the mapped frontier. In other words, terms for existential variables are fresh (although freshness entails more than that).

@[reducible, inline]

abbrev PreTrigger.apply_to_function_free_atom {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (atom : FunctionFreeAtom sig) : Fact sig

We lift the trigger application from VarOrConst to FunctionFreeAtom.

Equations

• trg.apply_to_function_free_atom i lt atom = (trg.apply_to_var_or_const i lt).apply_generalized_atom atom

@[implicit_reducible]

def PreTrigger.mapped_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : List (Fact sig)

The body does not feature any existential variables. Therefore, we mapped body merely results from applying the trigger's substitution to the body of its rule.

Equations

• trg.mapped_body = trg.subs.apply_function_free_conj trg.rule.body

@[simp]

theorem PreTrigger.length_mapped_body {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : trg.mapped_body.length = List.length trg.rule.body

The length of the mapped_body is the same as the length of the rule body.

theorem PreTrigger.mem_terms_mapped_body_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (t : GroundTerm sig) : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_body ↔ (∃ (c : sig.C), c ∈ trg.rule.body.consts ∧ GroundTerm.const c = t) ∨ ∃ (v : sig.V), v ∈ trg.rule.body.vars ∧ trg.subs v = t

A term occurs in mapped_body if and only if it is a constant in the rule body of if there exists a variable in the rule body that is mapped to the term by the substitution.

theorem PreTrigger.mem_terms_mapped_body_of_mem_mapped_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} (t : GroundTerm sig) : t ∈ trg.mapped_frontier → t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_body

If a term is in the mapped_frontier, then it is also in the mapped_body.

@[implicit_reducible]

def PreTrigger.mapped_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : List (List (Fact sig))

The mapped head is the result of the trigger and is simply the application to all head atoms. This result has a list of result facts for each of the head disjuncts. Note again that existential variables are Skolemized before the trigger's substitution is applied but this is hidden within the previously defined functions.

Equations

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

@[simp]

theorem PreTrigger.length_mapped_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) : trg.mapped_head.length = trg.rule.head.length

The length of the mapped_head is the same as the length of the rule head. That is, the trigger result indeed has one list of facts for each of the head disjuncts.

theorem PreTrigger.length_each_mapped_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (n : Nat) : Option.map List.length trg.mapped_head[n]? = Option.map List.length trg.rule.head[n]?

Also for each head disjunct, the number of result facts is equal to the number of atoms in the conjunction.

def PreTrigger.subs_for_mapped_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) : GroundSubstitution sig

For a fixed head index, we can view the trigger merely as a substitution that internally captures the Skolemization of existential variables. In other words, applying this substitution to the specified head disjunct yields exactly the trigger result for the same disjunct. Viewing the trigger as a substitution can be convenient for theorems and proofs.

Equations

• trg.subs_for_mapped_head i lt v = trg.apply_to_var_or_const i lt (VarOrConst.var v)

@[simp]

theorem PreTrigger.apply_subs_for_var_or_const_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (voc : VarOrConst sig) : (trg.subs_for_mapped_head i lt).apply_var_or_const voc = trg.apply_to_var_or_const i lt voc

Applying the subs_for_mapped_head is the same as applying the trigger on VarOrConst.

@[simp]

theorem PreTrigger.apply_subs_for_atom_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (a : FunctionFreeAtom sig) : (trg.subs_for_mapped_head i lt).apply_function_free_atom a = trg.apply_to_function_free_atom i lt a

Applying the subs_for_mapped_head is the same as applying the trigger on FunctionFreeAtom.

@[simp]

theorem PreTrigger.apply_subs_for_mapped_head_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) : (trg.subs_for_mapped_head i lt).apply_function_free_conj trg.rule.head[i] = trg.mapped_head[i]

Applying the subs_for_mapped_head on the head is exactly the trigger result (mapped_head).

def PreTrigger.fresh_terms_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) : List (GroundTerm sig)

The list of fresh terms are the function terms introduced for the existential variables.

Equations

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

theorem PreTrigger.mem_fresh_terms_of_functional_for_exis_var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} {lt : i < trg.rule.head.length} {v : sig.V} (v_mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : trg.functional_term_for_var i lt v v_mem ∈ trg.fresh_terms_for_head_disjunct i lt

The functional term produces by an existential variable is one of the fresh terms.

theorem PreTrigger.mem_fresh_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} {lt : i < trg.rule.head.length} (t : GroundTerm sig) : t ∈ trg.fresh_terms_for_head_disjunct i lt → ∃ (v : sig.V), ∃ (v_mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt), t = GroundTerm.func { rule := trg.rule, headIdx := i, headIdx_lt := lt, v := v, v_mem := v_mem } trg.mapped_frontier ⋯

This theorem unfolds some of the internal definitions of fresh_terms_for_head_disjunct.

theorem PreTrigger.term_functional_of_mem_fresh_terms {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} {lt : i < trg.rule.head.length} (t : GroundTerm sig) : t ∈ trg.fresh_terms_for_head_disjunct i lt → ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok

Fresh terms are always functional.

theorem PreTrigger.constant_not_mem_fresh_terms_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} {lt : i < trg.rule.head.length} {c : sig.C} : ¬GroundTerm.const c ∈ trg.fresh_terms_for_head_disjunct i lt

Constants can never be fresh.

theorem PreTrigger.frontier_term_not_mem_fresh_terms_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} {lt : i < trg.rule.head.length} {t : GroundTerm sig} : t ∈ trg.mapped_frontier → ¬t ∈ trg.fresh_terms_for_head_disjunct i lt

Mappings of frontier variables can never be fresh.

def PreTrigger.existential_var_for_fresh_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (t : GroundTerm sig) (t_mem : t ∈ trg.fresh_terms_for_head_disjunct i lt) : sig.V

For a given fresh term, we can obtain the existential variable that introduced it.

Equations

• trg.existential_var_for_fresh_term i lt t t_mem = (List.find? (fun (v : sig.V) => decide ((t.functionSymbol ⋯).v = v)) (trg.rule.existential_vars_for_head_disjunct i lt)).get ⋯

@[simp]

theorem PreTrigger.existential_var_for_fresh_term_after_functional_term_for_var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {i : Nat} (lt : i < trg.rule.head.length) {v : sig.V} (v_mem : v ∈ trg.rule.existential_vars_for_head_disjunct i lt) : trg.existential_var_for_fresh_term i lt (trg.functional_term_for_var i lt v v_mem) ⋯ = v

Indeed getting the existential variable for a functional term introduced for a variable yields exactly this variable (as expected).

def PreTrigger.atom_for_result_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) {f : Fact sig} (i : Nat) (lt : i < trg.rule.head.length) (f_mem : f ∈ trg.mapped_head[i]) : FunctionFreeAtom sig

For a fact in the trigger result, we can obtain the head atom that yields the fact.

Equations

• trg.atom_for_result_fact i lt f_mem = trg.rule.head[i][List.idxOf f trg.mapped_head[i]]

@[simp]

theorem PreTrigger.apply_on_atom_for_result_fact_is_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) {f : Fact sig} (i : Nat) (lt : i < trg.rule.head.length) (f_mem : f ∈ trg.mapped_head[i]) : trg.apply_to_function_free_atom i lt (trg.atom_for_result_fact i lt f_mem) = f

Applying the trigger on the atom from atom_for_result_fact indeed yields the correct fact.

theorem PreTrigger.atom_for_result_fact_mem_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {f : Fact sig} {i : Nat} {lt : i < trg.rule.head.length} {f_mem : f ∈ trg.mapped_head[i]} : trg.atom_for_result_fact i lt f_mem ∈ trg.rule.head[i]

The atom from atom_for_result_fact occurs in the correct rule head disjunct.

def PreTrigger.var_or_const_for_result_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) {f : Fact sig} {t : GroundTerm sig} (i : Nat) (lt : i < trg.rule.head.length) (f_mem : f ∈ trg.mapped_head[i]) (t_mem : t ∈ f.terms) : VarOrConst sig

For any term in the result (not just fresh ones), we can obtain the corresponding VarOrConst from the rule.

Equations

• trg.var_or_const_for_result_term i lt f_mem t_mem = (trg.atom_for_result_fact i lt f_mem).terms[List.idxOf t f.terms]

@[simp]

theorem PreTrigger.apply_on_var_or_const_for_result_term_is_term {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) {f : Fact sig} {t : GroundTerm sig} (i : Nat) (lt : i < trg.rule.head.length) (f_mem : f ∈ trg.mapped_head[i]) (t_mem : t ∈ f.terms) : trg.apply_to_var_or_const i lt (trg.var_or_const_for_result_term i lt f_mem t_mem) = t

Applying the trigger on the VarOrConst from var_or_const_for_result_term indeed yields the correct term.

theorem PreTrigger.var_or_const_for_result_term_mem_atom_for_result_fact {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {f : Fact sig} {t : GroundTerm sig} {i : Nat} {lt : i < trg.rule.head.length} {f_mem : f ∈ trg.mapped_head[i]} {t_mem : t ∈ f.terms} : trg.var_or_const_for_result_term i lt f_mem t_mem ∈ (trg.atom_for_result_fact i lt f_mem).terms

For a term in a result fact, var_or_const_for_result_term returns a VarOrConst that is in atom_for_result_fact.

theorem PreTrigger.var_or_const_for_result_term_mem_terms_head {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {f : Fact sig} {t : GroundTerm sig} {i : Nat} {lt : i < trg.rule.head.length} {f_mem : f ∈ trg.mapped_head[i]} {t_mem : t ∈ f.terms} : trg.var_or_const_for_result_term i lt f_mem t_mem ∈ trg.rule.head[i].terms

For a term in a result fact, var_or_const_for_result_term occurs in the correct head disjunct.

theorem PreTrigger.mem_terms_mapped_head_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) (t : GroundTerm sig) : t ∈ List.flatMap GeneralizedAtom.terms trg.mapped_head[i] ↔ (∃ (c : sig.C), c ∈ trg.rule.head[i].consts ∧ GroundTerm.const c = t) ∨ t ∈ List.map trg.subs (trg.rule.frontier_for_head i lt) ∨ t ∈ trg.fresh_terms_for_head_disjunct i lt

A term occurs in the trigger result for a given head index if and only if one of the following three cases holds. 1. The term is a constant in the head. 2. The term results from mapping a frontier variable in the head. 3. The term is a fresh term of the head.

theorem PreTrigger.mapped_head_constants_subset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (lt : i < trg.rule.head.length) : FactSet.constants trg.mapped_head[i].toSet ⊆ (List.flatMap GroundTerm.constants trg.mapped_frontier ++ trg.rule.head[i].consts).toSet

The constants in the trigger result are a subset of the constants from the mapped frontier terms and the constants that occur directly in the rule head.

def PreTrigger.loaded {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (fs : FactSet sig) : Prop

The trigger is loaded for a FactSet if its mapped body occurs in the fact set.

Equations

• trg.loaded fs = (trg.mapped_body.toSet ⊆ fs)

theorem PreTrigger.term_mapping_preserves_loadedness {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (fs : FactSet sig) (h : GroundTermMapping sig) (h_id : h.isIdOnConstants) : trg.loaded fs → { rule := trg.rule, subs := h ∘ trg.subs }.loaded (h.applyFactSet fs)

Applying a GroundTermMapping that is the id on constants after the trigger substitution and on the fact set preserves loadedness.

def PreTrigger.satisfied_for_disj {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (fs : FactSet sig) (i : Nat) (lt : i < trg.rule.head.length) : Prop

A trigger head is satisfied for a FactSet if there exists a substitution that agrees with the trigger substitution on all frontier variable such that the mapping of the head occurs in the fact set. This corresponds to FOL semantics. It is important to note here that a trigger being satisfied in this sense does not necessarily mean that it is obsolete! Obsolescence might be defined almost arbitrarily and for example in the Skolem chase, a satisfied trigger is often not obsolete. However, for the restricted (aka. standard) chase, obsolescence is defined via satisfaction.

Equations

• trg.satisfied_for_disj fs i lt = ∃ (s : GroundSubstitution sig), (∀ (v : sig.V), v ∈ trg.rule.frontier → s v = trg.subs v) ∧ (s.apply_function_free_conj trg.rule.head[i]).toSet ⊆ fs

theorem PreTrigger.satisfied_for_disj_of_mapped_head_contained {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (fs : FactSet sig) (i : Nat) (lt : i < trg.rule.head.length) : trg.mapped_head[i].toSet ⊆ fs → trg.satisfied_for_disj fs i lt

If the exact trigger result is contained in the fact set, then the trigger is also satisfied.

def PreTrigger.satisfied {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (fs : FactSet sig) : Prop

The trigger is satisfied if it is satisfied for some head. Note that this checks out with FOL semantics since the heads are part of a big disjunction.

Equations

• trg.satisfied fs = ∃ (i : Nat), ∃ (lt : i < trg.rule.head.length), trg.satisfied_for_disj fs i lt

theorem PreTrigger.satisfied_of_satisfied_subset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} {fs fs2 : FactSet sig} (sub : fs ⊆ fs2) : trg.satisfied fs → trg.satisfied fs2

If a trigger is satisfied, then it is also satisfied on all supersets.

def PreTrigger.equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg1 trg2 : PreTrigger sig) : Prop

We consider two trigger to be equivalent if they share the same rule and their substitutions agree on the frontier variables. This entails that they have the same result.

Equations

• trg1.equiv trg2 = (trg1.rule = trg2.rule ∧ ∀ (v : sig.V), v ∈ trg1.rule.frontier → trg1.subs v = trg2.subs v)

theorem PreTrigger.equiv_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} : trg.equiv trg

Trigger equivalence is reflexive.

theorem PreTrigger.equiv_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.equiv trg2 → trg2.equiv trg1

Trigger equivalence is symmetric.

theorem PreTrigger.equiv_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 trg3 : PreTrigger sig} : trg1.equiv trg2 → trg2.equiv trg3 → trg1.equiv trg3

Trigger equivalence is transitive.

theorem PreTrigger.mapped_frontier_eq_of_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} (equiv : trg1.equiv trg2) : trg1.mapped_frontier = trg2.mapped_frontier

Equivalent triggers have the same mapped_frontier.

theorem PreTrigger.equiv_of_rule_eq_of_mapped_frontier_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} (rule_eq : trg1.rule = trg2.rule) (mapped_front_eq : trg1.mapped_frontier = trg2.mapped_frontier) : trg1.equiv trg2

Two triggers with same rule and same mapped_frontier are equivalent.

def PreTrigger.strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg1 trg2 : PreTrigger sig) : Prop

We consider two trigger to be strongly equivalent if they share the same rule and their substitutions agree not only on the frontier variables but on all body variables.

Equations

• trg1.strong_equiv trg2 = (trg1.rule = trg2.rule ∧ ∀ (v : sig.V), v ∈ trg1.rule.body.vars → trg1.subs v = trg2.subs v)

theorem PreTrigger.strong_equiv_refl {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg : PreTrigger sig} : trg.strong_equiv trg

Strong equivalence is reflexive.

theorem PreTrigger.strong_equiv_symm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.strong_equiv trg2 → trg2.strong_equiv trg1

Strong equivalence is symmetric.

theorem PreTrigger.strong_equiv_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 trg3 : PreTrigger sig} : trg1.strong_equiv trg2 → trg2.strong_equiv trg3 → trg1.strong_equiv trg3

strong equivalence is transitive.

theorem PreTrigger.equiv_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.strong_equiv trg2 → trg1.equiv trg2

Strong equivalence implies equivalence.

theorem PreTrigger.subs_apply_function_free_atom_eq_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.strong_equiv trg2 → ∀ (a : FunctionFreeAtom sig), a ∈ trg1.rule.body → trg1.subs.apply_function_free_atom a = trg2.subs.apply_function_free_atom a

Applying the substitutions of strongly equivalent triggers to a body atom yields the same result. (This is not necessarily true if the triggers are only equivalent.)

theorem PreTrigger.mapped_body_eq_of_strong_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.strong_equiv trg2 → trg1.mapped_body = trg2.mapped_body

Strongly equivalent triggers have the same mapped_body. Again, this is not necessarily true for triggers that are only equivalent.

theorem PreTrigger.apply_to_function_free_atom_eq_of_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} (equiv : trg1.equiv trg2) (i : Nat) (lt : i < trg1.rule.head.length) (a : FunctionFreeAtom sig) : a ∈ trg1.rule.head[i] → trg1.apply_to_function_free_atom i lt a = trg2.apply_to_function_free_atom i ⋯ a

Applying two equivalent triggers to the same (head) atom yields the same result.

theorem PreTrigger.result_eq_of_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.equiv trg2 → trg1.mapped_head = trg2.mapped_head

As intended, equivalent triggers have the same result.

theorem PreTrigger.satisfied_preserved_of_equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} : trg1.equiv trg2 → ∀ {fs : FactSet sig}, trg1.satisfied fs ↔ trg2.satisfied fs

Equivalent triggers are satisfied on the same fact sets.

theorem PreTrigger.equiv_of_term_mem_fresh_terms_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {trg1 trg2 : PreTrigger sig} {i1 i2 : Nat} {lt1 : i1 < trg1.rule.head.length} {lt2 : i2 < trg2.rule.head.length} {t : GroundTerm sig} : t ∈ trg1.fresh_terms_for_head_disjunct i1 lt1 → t ∈ trg2.fresh_terms_for_head_disjunct i2 lt2 → trg1.equiv trg2 ∧ i1 = i2

If a ground term is fresh in two PreTriggers for two head indices, then actually these two PreTriggers (and indices) need to be equivalent (the same)! Why is this the case? Fresh terms are always Skolem function terms. Therefore they contain a rule, which needs to be the same for both triggers. The head indices are also part of the functional term so a similar argument can be made to show that these need to be equal. To see why the triggers also need to agree on their frontier mapping, we only need to remind ourselves that the Skolem term contains all the mapped frontier terms as arguments.