Cores

In this file, we define cores of fact sets. Namely, we define FactSet.isWeakCore and FactSet.isStrongCore. FactSets that are models and cores are interesting since there are (intuitively speaking) the smallest possible models. Under certain condition, the chase is able to produce a core directly, which is very desirable since the result of the chase is also always a universal model. But this is discussed in other files. Here, we are only concerned with the definition of cores on FactSets and some of their properties.

Some Auxiliary Definitions and Theorems on Lists and Functions

Before we can go into the actual definitions, we need a lot of machinery, mainly about functions to be able to state properties like injectivity and surjectivity possibly only about a list of set of elements and not the whole domain of the function.

Auxiliary Theorems on Lists

theorem List.length_le_of_nodup_of_all_mem {α : Type u_1} [DecidableEq α] (as bs : List α) (nodup : as.Nodup) (all_mem : ∀ (e : α), e ∈ as → e ∈ bs) : as.length ≤ bs.length

If a list is duplicate free and the sublist of another list, then the second list is at least as long as the first.

theorem List.equiv_of_nodup_of_length_eq_of_all_mem {α : Type u_1} [DecidableEq α] (as bs : List α) (nodup : as.Nodup) (eq_length : as.length = bs.length) (all_mem : ∀ (e : α), e ∈ as → e ∈ bs) (e : α) : e ∈ as ↔ e ∈ bs

If a list is duplicate free and the sublist of another list that has the same length, then both lists have exactly the same elements.

Injectivity and Surjectivity

We define what it means for a function to be injective or surjective restricted to a given domain and image, given as either a list or set. Intuitively, results involving the list versions most likely have an implicit requirement for domain and image being finite whereas results stated for the set version do not have this requirement.

We found our more suitable than using Function.Injective and Function.Sufjective because this would require us to consider appropriate subtypes and also since there barely seem to be theorems in the standard library (outside Mathlib). We might rework those definitions in the future though. I think a couple of (small) things can be cleaned up here but this is not the highest priprity. Maybe this should even move to the BasicLeanDatastructures repo since there are really just general results over functions.

def Function.image_set {α : Type u_1} {β : Type u_2} (f : α → β) (A : Set α) : Set β

The image of a function for a given domain set.

Equations

• Function.image_set f A = A.map f

def Function.injective_for_domain_set {α : Type u_1} {β : Sort u_2} (f : α → β) (domain : Set α) : Prop

A function is injective on a given domain set if for each two elements of the given domain, the mapping of both elements being the same implies the elements being the same.

Equations

• Function.injective_for_domain_set f domain = ∀ (a a' : α), a ∈ domain → a' ∈ domain → f a = f a' → a = a'

def Function.surjective_for_domain_and_image_set {α : Type u_1} {β : Type u_2} (f : α → β) (domain : Set α) (image : Set β) : Prop

A function is surjective on a given domain set and image set if for each element of the image, there exists an element in the domain that maps to the desired image element.

Equations

• Function.surjective_for_domain_and_image_set f domain image = ∀ (b : β), b ∈ image → ∃ (a : α), a ∈ domain ∧ f a = b

def Function.image {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (l : List α) : List β

The image of a function for a given domain list.

Equations

• Function.image f l = (List.map f l).eraseDupsKeepRight

def Function.injective_for_domain_list {α : Type u_1} {β : Sort u_2} (f : α → β) (domain : List α) : Prop

A function is injective on a given domain list if for each two elements of the given domain, the mapping of both elements being the same implies the elements being the same.

Equations

• Function.injective_for_domain_list f domain = ∀ (a a' : α), a ∈ domain → a' ∈ domain → f a = f a' → a = a'

def Function.surjective_for_domain_and_image_list {α : Type u_1} {β : Type u_2} (f : α → β) (domain : List α) (image : List β) : Prop

A function is surjective on a given domain list and image list if for each element of the image, there exists an element in the domain that maps to the desired image element.

Equations

• Function.surjective_for_domain_and_image_list f domain image = ∀ (b : β), b ∈ image → ∃ (a : α), a ∈ domain ∧ f a = b

theorem Function.injective_of_injective_compose {α : Type u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β) (g : β → γ) (domain : Set α) : injective_for_domain_set (g ∘ f) domain → injective_for_domain_set f domain

If the composition of two mappings is injective, then the first one must be injective.

theorem Function.surjective_of_surjective_from_subset {α : Type u_1} {β : Type u_2} (f : α → β) (domain : Set α) (image : Set β) : surjective_for_domain_and_image_set f domain image → ∀ (domain' : Set α), domain ⊆ domain' → surjective_for_domain_and_image_set f domain' image

If a mapping is surjective for a domain and image, then the same holds for any superset of the domain.

theorem Function.surjective_of_surjective_compose {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (domain : Set α) (image : Set γ) : surjective_for_domain_and_image_set (g ∘ f) domain image → surjective_for_domain_and_image_set g (image_set f domain) image

If the composition of two mappings is surjective for a domain and image, then the second one must be surjective on the same image and the domain that is the image of the first function.

theorem Function.injective_set_list_equiv {α : Type u_1} {β : Sort u_2} (f : α → β) (domain_set : Set α) (domain_list : List α) (eq : ∀ (e : α), e ∈ domain_list ↔ e ∈ domain_set) : injective_for_domain_set f domain_set ↔ injective_for_domain_list f domain_list

The injectivity definitions for set and list are interchangeable.

theorem Function.surjective_set_list_equiv {α : Type u_1} {β : Type u_2} (f : α → β) (domain_set : Set α) (domain_list : List α) (eq_domain : ∀ (e : α), e ∈ domain_list ↔ e ∈ domain_set) (image_set : Set β) (image_list : List β) (eq_image : ∀ (e : β), e ∈ image_list ↔ e ∈ image_set) : surjective_for_domain_and_image_set f domain_set image_set ↔ surjective_for_domain_and_image_list f domain_list image_list

The surjectivity definitions for set and list are interchangeable.

theorem Function.injective_for_domain_list_cons {α : Type u_1} {β : Sort u_2} (f : α → β) (hd : α) (tl : List α) : injective_for_domain_list f (hd :: tl) → injective_for_domain_list f tl

If a mapping is injective on a domain of the form hd::tl, then it is injective on tl.

theorem Function.mapping_mem_image_of_mem {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) (a : α) : a ∈ domain → f a ∈ image f domain

The mapping of each domain element occurs in the image.

theorem Function.nodup_image {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) : (image f domain).Nodup

The image has no duplicates.

theorem Function.length_image {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) : (image f domain).length ≤ domain.length

The image has at most as many elements as the domain.

theorem Function.surjective_on_own_image {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) : surjective_for_domain_and_image_list f domain (image f domain)

Every mapping is always surjective on its own image.

theorem Function.image_contained_of_closed {α : Type u_1} [DecidableEq α] (f : α → α) (domain : List α) (closed : ∀ (e : α), e ∈ domain → f e ∈ domain) (e : α) : e ∈ image f domain → e ∈ domain

If a mapping is closed, then its image is fully contained in its domain.

theorem Function.injective_iff_length_image_eq_of_nodup {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) (nodup : domain.Nodup) : injective_for_domain_list f domain ↔ (image f domain).length = domain.length

Given a mapping and a domain list without duplicates, the mapping in injective on the domain if and only if the image contains the same number of elements as the domain.

theorem Function.surjective_on_target_iff_all_in_image {β : Type u_1} {α : Type u_2} [DecidableEq β] (f : α → β) (domain : List α) (target_image : List β) : surjective_for_domain_and_image_list f domain target_image ↔ ∀ (b : β), b ∈ target_image → b ∈ image f domain

A mapping is surjective on a given domain and image if and only if the given image is contained in the actual image of the mapping.

theorem Function.injective_of_surjective_of_nodup {α : Type u_1} [DecidableEq α] (f : α → α) (l : List α) (nodup : l.Nodup) : surjective_for_domain_and_image_list f l l → injective_for_domain_list f l

Given a single list without duplicates that represents both domain and image, if a mapping is surjective, then it is injective.

theorem Function.injective_iff_surjective_of_nodup_of_closed {α : Type u_1} [DecidableEq α] (f : α → α) (l : List α) (nodup : l.Nodup) (closed : ∀ (e : α), e ∈ l → f e ∈ l) : injective_for_domain_list f l ↔ surjective_for_domain_and_image_list f l l

Given a single list without duplicates that represents both domain and image, if a mapping closed on the list, then the mapping is injective if and only if it is surjective.

theorem Function.closed_of_injective_of_surjective_of_nodup {α : Type u_1} [DecidableEq α] (f : α → α) (l : List α) (nodup : l.Nodup) : injective_for_domain_list f l → surjective_for_domain_and_image_list f l l → ∀ (e : α), e ∈ l → f e ∈ l

Given a single list without duplicates that represents both domain and image, if a mapping both injective and surjective, then is must be closed on the list.

Strong GroundTermMappings (and Homomorphisms)

Intuitively, a homomorphism is strong if it not only retains membership but also non-membership. We define being strong as a standalone property for GroundTermMappings without requiring any additional properties for the underlying GroundTermMapping.

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

A GroundTermMapping is strong for FactSets A and B if each element not in A, its mapping is not in B. However, we only demand this for elements that only feature terms from a given domain because we do not want to care about the mapping of terms outside the domain.

Equations

• h.strong domain A B = ∀ (e : Fact sig), (∀ (t : GroundTerm sig), t ∈ e.terms → t ∈ domain) → ¬e ∈ A → ¬h.applyFact e ∈ B

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

If the composition of two mappings is strong from A to C and the second mapping is a homomorphism from B to C, then the first mapping is strong from A to B.

Repetition of GroundTermMappings (and Homomorphisms)

In general, we can define what it means to apply a function a given number of times. This is particularly useful for GroundTermMappings that are endomorphisms, i.e. homomorphisms from one structure into the same structure. We can show some nice properties for such repetitions. For example, a repeated endomorphisms is still an endomorphisms.

def GroundTermMapping.repeat_hom {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) : Nat → GroundTermMapping sig

Repetition of a GroundTermMapping defined in the obvious way. Repeating zero times is defined as the id function.

Equations

• h.repeat_hom Nat.zero = id
• h.repeat_hom j.succ = h ∘ h.repeat_hom j

theorem GroundTermMapping.repeat_hom_swap {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (i : Nat) (t : GroundTerm sig) : h (h.repeat_hom i t) = h.repeat_hom i (h t)

It does not mapper if we apply add one more repetition on the left or the right.

theorem GroundTermMapping.repeat_hom_add {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (n m : Nat) (t : GroundTerm sig) : h.repeat_hom (n + m) t = h.repeat_hom n (h.repeat_hom m t)

A (n+m)-times repetition can be split into the composition of an m-times repetition followed by an n-times repetition.

theorem GroundTermMapping.repeat_hom_cycle_mul {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (t : GroundTerm sig) (n : Nat) : h.repeat_hom n t = t → ∀ (m : Nat), h.repeat_hom (n * m) t = t

If some repetition maps a term to itself, then each multiple of the repetition count must also map the term to itself.

theorem GroundTermMapping.repeat_hom_move_cycle {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (t : GroundTerm sig) (n : Nat) : h.repeat_hom n t = t → ∀ (s : GroundTerm sig) (m : Nat), h.repeat_hom m t = s → h.repeat_hom n s = s

If some repetition maps a term to itself, then for each other term that is part of the loop, the same number of repetitions also maps that one to itself.

theorem GroundTermMapping.repeat_each_reaches_self_of_each_reachable {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (ts : List (GroundTerm sig)) (each_reachable : ∀ (t : GroundTerm sig), t ∈ ts → ∃ (k : Nat), 1 ≤ k ∧ ∃ (s : GroundTerm sig), s ∈ ts ∧ h.repeat_hom k s = t) (s : GroundTerm sig) : s ∈ ts → ∃ (l : Nat), 1 ≤ l ∧ h.repeat_hom l s = s

Consider a list of terms. If each term is reachable by some number of repetitions from some term, then for each term there is a number of repetition that maps the term to itself. Intuitively this holds by a pigeonhole principle: If for each term you need to pick a term from that you can reach it, but only finitely many terms are available, then eventually you need to complete a cycle.

theorem GroundTermMapping.repeat_globally_of_each_repeats {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (ts : List (GroundTerm sig)) (each_repeats : ∀ (s : GroundTerm sig), s ∈ ts → ∃ (l : Nat), 1 ≤ l ∧ h.repeat_hom l s = s) : ∃ (l : Nat), 1 ≤ l ∧ ∀ (s : GroundTerm sig), s ∈ ts → h.repeat_hom l s = s

If each term from a finite list is mapped to itself after some number of repetitions, then there is a global repetition number that maps each term to itself. Basically any common multiple of the individual repetition numbers works.

theorem GroundTermMapping.exists_repetition_that_is_inverse_of_surj {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (ts : List (GroundTerm sig)) (surj : Function.surjective_for_domain_and_image_list h ts ts) : ∃ (k : Nat), ∀ (t : GroundTerm sig), t ∈ ts → h.repeat_hom k (h t) = t

If a mapping is surjective for a given list of terms, then there exists a repetition count $k$ such that $k+1$ map each term from the list to itself. Note that we use $k+1$ repetitions as otherwise the result would be trivial for zero repetitions, which are the id by definition.

theorem GroundTermMapping.repeat_hom_id_on_const {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] (h : GroundTermMapping sig) (idOnConst : h.isIdOnConstants) (i : Nat) : (h.repeat_hom i).isIdOnConstants

Repeating a mapping retains the isIdOnConstants property.

theorem GroundTermMapping.repeat_hom_isHomomorphism {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] (h : GroundTermMapping sig) (fs : FactSet sig) (hom : h.isHomomorphism fs fs) (i : Nat) : (h.repeat_hom i).isHomomorphism fs fs

Repeating a mapping retains the isHomomorphism property at least for endomorphisms.

Cores Definitions and some of their Properties

Here, we finally define isWeakCore and isStrongCore and show some of their relations and additional properties. This also involves some more theorems about homomorphisms.

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

A FactSet is a weak core if every endomorphisms on the fact set is strong and injective.

Equations

• fs.isWeakCore = ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs → h.strong fs.terms fs fs ∧ Function.injective_for_domain_set h fs.terms

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

A FactSet is a strong core if every endomorphisms on the fact set is strong, injective, and surjective. (By definition, every strong core is a weak core.)

Equations

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

def FactSet.homSubset {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (c fs : FactSet sig) : Prop

We say that a fact set $C$ is a homomorphic subset of another fact set $F$ if $C$ is a subset of $F$ and there is a homomorphism from $F$ to $C$.

Equations

• c.homSubset fs = (c ⊆ fs ∧ ∃ (h : GroundTermMapping sig), h.isHomomorphism fs c)

theorem FactSet.hom_surjective_of_finite_of_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (finite : Set.finite fs) (h : GroundTermMapping sig) : h.isHomomorphism fs fs → Function.injective_for_domain_set h fs.terms → Function.surjective_for_domain_and_image_set h fs.terms fs.terms

For a homomorphism on a finite fact set, injectivity implies surjectivity.

theorem FactSet.hom_strong_of_finite_of_injective {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (finite : Set.finite fs) (h : GroundTermMapping sig) : h.isHomomorphism fs fs → Function.injective_for_domain_set h fs.terms → h.strong fs.terms fs fs

For a homomorphism on a finite fact set, injectivity implies that the homomorphisms is also strong.

theorem FactSet.isStrongCore_of_isWeakCore_of_finite {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs : FactSet sig) (weakCore : fs.isWeakCore) (finite : Set.finite fs) : fs.isStrongCore

For finite fact sets, isWeakCore implies isStrongCore. That means that isWeakCore and isStrongCore are equivalent on finite fact sets.

theorem FactSet.every_weakCore_isomorphic_to_strongCore_of_hom_both_ways {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (sc : FactSet sig) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (wc_weak : wc.isWeakCore) (h_sc_wc h_wc_sc : GroundTermMapping sig) (h_sc_wc_hom : h_sc_wc.isHomomorphism sc wc) (h_wc_sc_hom : h_wc_sc.isHomomorphism wc sc) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injective_for_domain_set iso wc.terms ∧ Function.surjective_for_domain_and_image_set iso wc.terms sc.terms

Given two fact sets A,B of which one is a weak and one is a strong core, if there are homomorphisms from A to B and B to A, then there exists an isomorphism from A to B, i.e. a strong homomorphisms that is injective and surjective.

theorem FactSet.strongCore_unique_up_to_isomorphism_with_respect_to_weak_cores {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (fs sc : FactSet sig) (sub_sc : sc.homSubset fs) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (sub_wc : wc.homSubset fs) (wc_weak : wc.isWeakCore) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injective_for_domain_set iso wc.terms ∧ Function.surjective_for_domain_and_image_set iso wc.terms sc.terms

Strong cores of fact sets are unique up to isomorphism. That is, consider a fact set $F$. A strong core $C$ for $F$ is a strong core that is also a homomorphic subset of $F$. Now every (other) homomorphic subset $C'$ of $F$ that is at least a weak core has an isomorphism into $C$.

theorem FactSet.every_universal_weakCore_isomorphic_to_universal_strongCore {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (sc : FactSet sig) (sc_universal : sc.universallyModelsKb kb) (sc_strong : sc.isStrongCore) (wc : FactSet sig) (wc_universal : wc.universallyModelsKb kb) (wc_weak : wc.isWeakCore) : ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ Function.injective_for_domain_set iso wc.terms ∧ Function.surjective_for_domain_and_image_set iso wc.terms sc.terms

Consider a KnowledgeBase and a universal model of the KB that is a strong core. Then every (other) universal model that is at least a weak core, is isomorphism to the strong core.

theorem FactSet.strong_core_of_model_is_model {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (fs : FactSet sig) (fs_model : fs.modelsKb kb) (sc : FactSet sig) (sc_sub : sc.homSubset fs) (sc_strong : sc.isStrongCore) : sc.modelsKb kb

Given a model of a KnowledgeBase, every strong core of the model is also a model. In general, this does not hold for weak cores (in the infinite setting).

theorem FactSet.strong_core_of_universal_model_is_universal_model {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {kb : KnowledgeBase sig} (fs : FactSet sig) (fs_univ_model : fs.universallyModelsKb kb) (sc : FactSet sig) (sc_sub : sc.homSubset fs) (sc_strong : sc.isStrongCore) : sc.universallyModelsKb kb

Building on top of the previous theorem, a strong core of a universal model is not only a model but also universal.