Substitutions and other mappings on Terms

In this file, we define mainly GroundSubstitution and GroundTermMapping. The latter is used to define homomorphisms on FactSets. Both kinds of mapping are based on a (very general) TermMapping.

TermMapping

The TermMapping is really just a function between two types but we define a bit of machinery on it that captures how remapping terms in such a general way behaves in the context of a GeneralizedAtom or lists or sets thereof.

@[reducible, inline]

abbrev TermMapping (S : Type u) (T : Type v) : Type (max u v)

A TermMapping is nothing more than a function from one term type to another.

Equations

• TermMapping S T = (S → T)

def TermMapping.apply_generalized_atom {sig : Signature} [DecidableEq sig.P] {S : Type u_4} {T : Type u_5} (h : TermMapping S T) (a : GeneralizedAtom sig S) : GeneralizedAtom sig T

A TermMapping is applied to a GeneralizedAtom by simply applying it to each term.

Equations

• h.apply_generalized_atom a = { predicate := a.predicate, terms := List.map h a.terms, arity_ok := ⋯ }

def TermMapping.apply_generalized_atom_list {sig : Signature} [DecidableEq sig.P] {S : Type u_4} {T : Type u_5} (h : TermMapping S T) (l : List (GeneralizedAtom sig S)) : List (GeneralizedAtom sig T)

A TermMapping is applied to a list of GeneralizedAtoms by applying it to each atom.

Equations

• h.apply_generalized_atom_list l = List.map h.apply_generalized_atom l

def TermMapping.apply_generalized_atom_set {sig : Signature} [DecidableEq sig.P] {S : Type u_4} {T : Type u_5} (h : TermMapping S T) (s : Set (GeneralizedAtom sig S)) : Set (GeneralizedAtom sig T)

A TermMapping is applied to a set of GeneralizedAtoms by applying it to each atom.

Equations

• h.apply_generalized_atom_set s = s.map h.apply_generalized_atom

theorem TermMapping.length_terms_apply_generalized_atom {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} (h : TermMapping S T) (a : GeneralizedAtom sig S) : (h.apply_generalized_atom a).terms.length = a.terms.length

Applying a TermMapping to a GeneralizedAtom does not change the number of terms.

theorem TermMapping.apply_generalized_atom_compose {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) : apply_generalized_atom (h ∘ g) = h.apply_generalized_atom ∘ g.apply_generalized_atom

We can split the application of a composed TermMapping on an atom.

theorem TermMapping.apply_generalized_atom_compose' {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) (a : GeneralizedAtom sig S) : apply_generalized_atom (h ∘ g) a = h.apply_generalized_atom (g.apply_generalized_atom a)

We can split the application of a composed TermMapping on an atom.

theorem TermMapping.apply_generalized_atom_congr_left {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} (g h : TermMapping S T) (a : GeneralizedAtom sig S) : (∀ (t : S), t ∈ a.terms → g t = h t) → g.apply_generalized_atom a = h.apply_generalized_atom a

To show that applying two TermMappings on the same atom yields the same result, it is enough to show that the mappings behave identical on each term.

theorem TermMapping.apply_generalized_atom_eq_self_of_id_on_terms {sig : Signature} [DecidableEq sig.P] {T : Type u_1} (h : TermMapping T T) (a : GeneralizedAtom sig T) (id_on_terms : ∀ (t : T), t ∈ a.terms → h t = t) : h.apply_generalized_atom a = a

Applying a TermMapping on a GeneralizedAtom is the identity if the mapping is the identity on each term.

theorem TermMapping.apply_generalized_atom_list_compose {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) : apply_generalized_atom_list (h ∘ g) = h.apply_generalized_atom_list ∘ g.apply_generalized_atom_list

We can split the application of a composed TermMapping on a list of atoms.

theorem TermMapping.apply_generalized_atom_list_compose' {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) (l : List (GeneralizedAtom sig S)) : apply_generalized_atom_list (h ∘ g) l = h.apply_generalized_atom_list (g.apply_generalized_atom_list l)

We can split the application of a composed TermMapping on a list of atoms.

theorem TermMapping.apply_generalized_atom_set_compose {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) : apply_generalized_atom_set (h ∘ g) = h.apply_generalized_atom_set ∘ g.apply_generalized_atom_set

We can split the application of a composed TermMapping on a set of atoms.

theorem TermMapping.apply_generalized_atom_set_compose' {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {U : Type u_3} (g : TermMapping S T) (h : TermMapping T U) (s : Set (GeneralizedAtom sig S)) : apply_generalized_atom_set (h ∘ g) s = h.apply_generalized_atom_set (g.apply_generalized_atom_set s)

We can split the application of a composed TermMapping on a set of atoms.

theorem TermMapping.apply_generalized_atom_mem_apply_generalized_atom_set {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} (h : TermMapping S T) (a : GeneralizedAtom sig S) (as : Set (GeneralizedAtom sig S)) : a ∈ as → h.apply_generalized_atom a ∈ h.apply_generalized_atom_set as

Applying a TermMapping to both an atom and a set of atoms retains membership of the atom in the set.

theorem TermMapping.apply_generalized_atom_set_subset_of_subset {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} (h : TermMapping S T) (as bs : Set (GeneralizedAtom sig S)) : as ⊆ bs → h.apply_generalized_atom_set as ⊆ h.apply_generalized_atom_set bs

Applying the same TermMapping to two sets of atoms retains their subset relation.

theorem TermMapping.apply_generalized_atom_set_toSet {sig : Signature} [DecidableEq sig.P] {S : Type u_1} {T : Type u_2} {g : TermMapping S T} (l : List (GeneralizedAtom sig S)) : g.apply_generalized_atom_set l.toSet = (g.apply_generalized_atom_list l).toSet

When mapping a set of atoms that results from the list, we can instead map on the list and then convert to the set.

GroundSubstitution

GroundSubstitution is used mainly on rules to map the variables to some actual ground terms. This is a key ingredient of PrTriggers that model "rule applications" in the chase.

@[reducible, inline]

abbrev GroundSubstitution (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max u_2 u_3 u_2)

A GroundSubstitution is merely a TermMapping from variables to GroundTerms.

Equations

• GroundSubstitution sig = TermMapping sig.V (GroundTerm sig)

def GroundSubstitution.apply_var_or_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (σ : GroundSubstitution sig) : TermMapping (VarOrConst sig) (GroundTerm sig)

We lift GroundSubstitutions to mappings from VarOrConst to GroundTerm in the obvious way.

Equations

• σ.apply_var_or_const (VarOrConst.var v) = σ v
• σ.apply_var_or_const (VarOrConst.const c) = GroundTerm.const c

def GroundSubstitution.apply_skolem_term {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (σ : GroundSubstitution sig) : TermMapping (SkolemTerm sig) (GroundTerm sig)

We lift GroundSubstitutions to mappings from SkolemTerm to GroundTerm in the obvious way.

Equations

• σ.apply_skolem_term (SkolemTerm.var v) = σ v
• σ.apply_skolem_term (SkolemTerm.const c) = GroundTerm.const c
• σ.apply_skolem_term (SkolemTerm.func fs frontier arity_ok) = GroundTerm.func fs (List.map (fun (fv : sig.V) => σ fv) frontier) ⋯

theorem GroundSubstitution.apply_skolem_term_injective_on_func_of_frontier_eq {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] {a : SkolemFS sig} {frontier : List sig.V} {arity_a : frontier.length = a.arity} {b : SkolemFS sig} {arity_b : frontier.length = b.arity} (subs : GroundSubstitution sig) (s t : SkolemTerm sig) (hs : s = SkolemTerm.func a frontier arity_a) (ht : t = SkolemTerm.func b frontier arity_b) : subs.apply_skolem_term s = subs.apply_skolem_term t → s = t

On functional SkolemTerms that share the same frontier, applying a GroundSubstitution is injective.

@[reducible, inline]

abbrev GroundSubstitution.apply_atom {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (σ : GroundSubstitution sig) : Atom sig → Fact sig

Using the standard functionality of TermMapping, we can apply GroundSubstitutions directly to an Atom yielding a Fact.

Equations

• σ.apply_atom = σ.apply_skolem_term.apply_generalized_atom

@[reducible, inline]

abbrev GroundSubstitution.apply_function_free_atom {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (σ : GroundSubstitution sig) : FunctionFreeAtom sig → Fact sig

Using the standard functionality of TermMapping, we can apply GroundSubstitutions directly to a FunctionFreeAtom yielding a Fact.

Equations

• σ.apply_function_free_atom = σ.apply_var_or_const.apply_generalized_atom

@[reducible, inline]

abbrev GroundSubstitution.apply_function_free_conj {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (σ : GroundSubstitution sig) : FunctionFreeConjunction sig → List (Fact sig)

Using the standard functionality of TermMapping, we can apply GroundSubstitutions directly to a FunctionFreeConjunction yielding a list of Facts.

Equations

• σ.apply_function_free_conj = σ.apply_var_or_const.apply_generalized_atom_list

GroundTermMapping

A GroundTermMapping maps GroundTerms to GroundTerms and is used to define homomorphisms over FactSets.

@[reducible, inline]

abbrev GroundTermMapping (sig : Signature) [DecidableEq sig.C] [DecidableEq sig.V] : Type (max u_3 u_2)

A GroundTermMapping is merely a TermMapping over GroundTerms.

Equations

• GroundTermMapping sig = TermMapping (GroundTerm sig) (GroundTerm sig)

def GroundTermMapping.isIdOnConstants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) : Prop

Equations

• h.isIdOnConstants = ∀ {c : sig.C}, h (GroundTerm.const c) = GroundTerm.const c

@[reducible, inline]

abbrev GroundTermMapping.applyFact {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (h : GroundTermMapping sig) : Fact sig → Fact sig

Using the standard functionality of TermMapping, we can list GroundTermMappings to Facts.

Equations

• h.applyFact = TermMapping.apply_generalized_atom h

@[reducible, inline]

abbrev GroundTermMapping.applyFactSet {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (h : GroundTermMapping sig) : FactSet sig → FactSet sig

Using the standard functionality of TermMapping, we can list GroundTermMappings to FactSets.

Equations

• h.applyFactSet = TermMapping.apply_generalized_atom_set h

def GroundTermMapping.isHomomorphism {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (h : GroundTermMapping sig) (A B : FactSet sig) : Prop

A GroundTermMapping is a homomorphisms from FactSet A to B if each constant is mapped to itself and mapping A results in a subset of B.

Equations

• h.isHomomorphism A B = (h.isIdOnConstants ∧ h.applyFactSet A ⊆ B)

theorem GroundTermMapping.terms_applyFactSet {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {h : GroundTermMapping sig} {fs : FactSet sig} : (h.applyFactSet fs).terms = fs.terms.map h

The terms in a mapped FactSet are the same as the mapped terms from the original FactSet.

theorem GroundTermMapping.isHomomorphism_compose {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (g h : GroundTermMapping sig) (A B C : FactSet sig) : g.isHomomorphism A B → h.isHomomorphism B C → isHomomorphism (h ∘ g) A C

We can compose homomorphisms. That is, given a homomorphism from A to B and from B to C, we can combine both to obtain a homomorphisms from A to C.

Interactions of GroundSubstitution and GroundTermMapping

Sometimes, a GroundSubstitution and GroundTermMapping might be composed into a single GroundSubstitution. In such a case, it can be useful to be able to split them apart. But this is generally only possible if the GroundTermMapping leaves the relevant constants untouched.

theorem GroundSubstitution.apply_var_or_const_compose {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (voc : VarOrConst sig) : (∀ (d : sig.C), voc = VarOrConst.const d → h (GroundTerm.const d) = GroundTerm.const d) → apply_var_or_const (h ∘ s) voc = h (s.apply_var_or_const voc)

The application of a composed substitution on a VarOrConst can be split if the involved GroundTermMapping maps the VarOrConst to itself, in the case where it is a constant.

theorem GroundSubstitution.apply_var_or_const_compose_of_isIdOnConstants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (id_on_const : h.isIdOnConstants) : apply_var_or_const (h ∘ s) = h ∘ s.apply_var_or_const

This is a special case of the above theorem where the GroundTermMapping is simply the id on all constants.

theorem GroundSubstitution.apply_function_free_atom_compose {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (a : FunctionFreeAtom sig) : (∀ (d : sig.C), d ∈ a.constants → h (GroundTerm.const d) = GroundTerm.const d) → apply_function_free_atom (h ∘ s) a = h.applyFact (s.apply_function_free_atom a)

The application of a composed substitution on a FunctionFreeAtom can be split if the involved GroundTermMapping maps all constants from the atom to themselves.

theorem GroundSubstitution.apply_function_free_atom_compose_of_isIdOnConstants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (id_on_const : h.isIdOnConstants) : apply_function_free_atom (h ∘ s) = h.applyFact ∘ s.apply_function_free_atom

This is a special case of the above theorem where the GroundTermMapping is simply the id on all constants.

theorem GroundSubstitution.apply_function_free_conj_compose {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (ffc : FunctionFreeConjunction sig) : (∀ (d : sig.C), d ∈ ffc.consts → h (GroundTerm.const d) = GroundTerm.const d) → apply_function_free_conj (h ∘ s) ffc = TermMapping.apply_generalized_atom_list h (s.apply_function_free_conj ffc)

The application of a composed substitution on a FunctionFreeConjunction can be split if the involved GroundTermMapping maps all constants from the conjucntion to themselves.

theorem GroundSubstitution.apply_function_free_conj_compose_of_isIdOnConstants {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (s : GroundSubstitution sig) (h : GroundTermMapping sig) (id_on_const : h.isIdOnConstants) : apply_function_free_conj (h ∘ s) = TermMapping.apply_generalized_atom_list h ∘ s.apply_function_free_conj

This is a special case of the above theorem where the GroundTermMapping is simply the id on all constants.