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 "obsoleteness" later. However, most of the machinery around triggers can be introduced agnostic of any kind of obsoleteness. 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.skolemize_var_or_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (disjunctIndex : Nat) (var_or_const : VarOrConst sig) : SkolemTerm sig

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

Equations

• trg.skolemize_var_or_const disjunctIndex var_or_const = VarOrConst.skolemize trg.rule.id disjunctIndex trg.rule.frontier var_or_const

def PreTrigger.apply_to_var_or_const {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (disjunctIndex : Nat) : 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 disjunctIndex = trg.subs.apply_skolem_term ∘ trg.skolemize_var_or_const disjunctIndex

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) (c : sig.C) : trg.apply_to_var_or_const i (VarOrConst.const c) = GroundTerm.const c

Applying a trigger to a constant changes nothing.

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) (v : sig.V) : v ∈ trg.rule.frontier → trg.apply_to_var_or_const i (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) (v : sig.V) : 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 v = GroundTerm.func { ruleId := trg.rule.id, disjunctIndex := i, var := v, arity := trg.rule.frontier.length } (List.map trg.subs trg.rule.frontier) ⋯

theorem PreTrigger.apply_to_var_or_const_non_frontier_var {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Nat) (v : sig.V) : ¬v ∈ trg.rule.frontier → trg.apply_to_var_or_const i (VarOrConst.var v) = trg.functional_term_for_var i v

Applying a trigger to a non-frontier variable, yields exactly the Skolem function term from the shortcup definition functional_term_for_var.

theorem PreTrigger.apply_to_var_or_const_injective_of_not_in_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {v : sig.V} (trg : PreTrigger sig) (i : Fin trg.rule.head.length) (v_not_in_frontier : ¬v ∈ trg.rule.frontier) (voc : VarOrConst sig) : trg.apply_to_var_or_const (↑i) (VarOrConst.var v) = trg.apply_to_var_or_const (↑i) voc → VarOrConst.var v = voc

For non-frontier variable, applyign the trigger is injective.

theorem PreTrigger.result_term_not_in_frontier_image_of_var_not_in_frontier {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (disj_index : Fin trg.rule.head.length) (v : sig.V) (v_not_in_frontier : ¬v ∈ trg.rule.frontier) : ¬trg.apply_to_var_or_const (↑disj_index) (VarOrConst.var v) ∈ List.map trg.subs trg.rule.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) (disjunctIndex : Nat) (atom : FunctionFreeAtom sig) : Fact sig

We lift the trigger application from VarOrConst to FunctionFreeAtom.

Equations

• trg.apply_to_function_free_atom disjunctIndex atom = (trg.apply_to_var_or_const disjunctIndex).apply_generalized_atom atom

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

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.

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

• trg.mapped_head = List.map (fun (x : FunctionFreeConjunction sig × Nat) => match x with | (h, i) => List.map (trg.apply_to_function_free_atom i) h) trg.rule.head.zipIdx

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 : Fin trg.mapped_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 v = trg.apply_to_var_or_const (↑i) (VarOrConst.var v)

theorem PreTrigger.apply_subs_for_var_or_const_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Fin trg.mapped_head.length) (voc : VarOrConst sig) : (trg.subs_for_mapped_head i).apply_var_or_const voc = trg.apply_to_var_or_const (↑i) voc

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

theorem PreTrigger.apply_subs_for_atom_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Fin trg.mapped_head.length) (a : FunctionFreeAtom sig) : (trg.subs_for_mapped_head i).apply_function_free_atom a = trg.apply_to_function_free_atom (↑i) a

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

theorem PreTrigger.apply_subs_for_mapped_head_eq {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (trg : PreTrigger sig) (i : Fin trg.mapped_head.length) : (trg.subs_for_mapped_head i).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

• trg.fresh_terms_for_head_disjunct i lt = List.map (trg.functional_term_for_var i) (trg.rule.existential_vars_for_head_disjunct i lt)

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 ∈ trg.rule.existential_vars_for_head_disjunct i lt ∧ t = GroundTerm.func { ruleId := trg.rule.id, disjunctIndex := i, var := v, arity := trg.rule.frontier.length } (List.map trg.subs trg.rule.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 ∈ List.map trg.subs trg.rule.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 (trg.functional_term_for_var i v = t)) (trg.rule.existential_vars_for_head_disjunct i lt)).get ⋯

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 v) ⋯ = 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 : Fin trg.mapped_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 f_mem = trg.rule.head[↑⟨↑i, ⋯⟩][↑⟨List.idxOf f trg.mapped_head[↑i], ⋯⟩]

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 : Fin trg.mapped_head.length) (f_mem : f ∈ trg.mapped_head[↑i]) : trg.apply_to_function_free_atom (↑i) (trg.atom_for_result_fact i 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 : Fin trg.mapped_head.length} {f_mem : f ∈ trg.mapped_head[↑i]} : trg.atom_for_result_fact i 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 : Fin trg.mapped_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 f_mem t_mem = (trg.atom_for_result_fact i f_mem).terms[↑⟨List.idxOf t f.terms, ⋯⟩]

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 : Fin trg.mapped_head.length) (f_mem : f ∈ trg.mapped_head[↑i]) (t_mem : t ∈ f.terms) : trg.apply_to_var_or_const (↑i) (trg.var_or_const_for_result_term i 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 : Fin trg.mapped_head.length} {f_mem : f ∈ trg.mapped_head[↑i]} {t_mem : t ∈ f.terms} : trg.var_or_const_for_result_term i f_mem t_mem ∈ (trg.atom_for_result_fact i 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 : Fin trg.mapped_head.length} {f_mem : f ∈ trg.mapped_head[↑i]} {t_mem : t ∈ f.terms} : trg.var_or_const_for_result_term i 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.mapped_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, ⋯⟩) ∨ t ∈ trg.fresh_terms_for_head_disjunct i ⋯

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 : Fin trg.mapped_head.length) : FactSet.constants trg.mapped_head[↑i].toSet ⊆ (List.flatMap GroundTerm.constants (List.map (trg.subs_for_mapped_head i) trg.rule.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) (F : FactSet sig) : Prop

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

Equations

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

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) (disj_index : Fin 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! Obsoleteness 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, obsoleteness is defined via satisfaction.

Equations

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

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) (disj_index : Fin trg.rule.head.length) : trg.mapped_head[↑disj_index].toSet ⊆ fs → trg.satisfied_for_disj fs disj_index

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) (F : 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 F = ∃ (disj_index : Fin trg.rule.head.length), trg.satisfied_for_disj F disj_index

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

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_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.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} : trg1.equiv trg2 → ∀ (i : Nat) (a : FunctionFreeAtom sig), trg1.apply_to_function_free_atom i 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.