WIP: Basic Formalization for Cores

ProofLibrary/KnowledgeBaseBasics.lean

@@ -203,6 +203,34 @@ theorem Fact.toFact_after_toFunctionFreeFact_is_id : ∀ (f : Fact sig), f.toFun
           simp at h
     case isFalse _ => contradiction
 
+def FactSet.terms (fs : FactSet sig) : Set (GroundTerm sig) := fun t => ∃ f, f ∈ fs ∧ t ∈ f.terms
+
+theorem Factset.terms_finite_of_finite (fs : FactSet sig) (finite : fs.finite) : fs.terms.finite := by
+  rcases finite with ⟨l, finite⟩
+  exists (l.map Fact.terms).flatten
+  intro e
+  constructor
+  . intro in_l
+    unfold FactSet.terms
+    simp [List.mem_flatten] at in_l
+    rcases in_l with ⟨terms, ex_f, e_in_terms⟩
+    rcases ex_f with ⟨f, f_in_l, terms_eq⟩
+    exists f
+    constructor
+    . rw [← finite]; exact f_in_l
+    . rw [terms_eq]; exact e_in_terms
+  . intro in_fs
+    unfold FactSet.terms at in_fs
+    simp [List.mem_flatten]
+    rcases in_fs with ⟨f, f_in_fs, e_in_f⟩
+    exists f.terms
+    constructor
+    . exists f
+      constructor
+      . rw [finite]; exact f_in_fs
+      . rfl
+    . exact e_in_f
+
 def Database.toFactSet (db : Database sig) : { fs : FactSet sig // fs.finite } := ⟨
   fun x => match (Fact.toFunctionFreeFact x) with
     | Option.none => False

ProofLibrary/List.lean

@@ -407,6 +407,38 @@ namespace List
     cases l with
     | nil => contradiction
     | cons head tail => simp
+
+  theorem flatten_cons (l : List α) (ls : List (List α)) : (l :: ls).flatten = l ++ ls.flatten := by
+    induction ls generalizing l with
+    | nil => simp [flatten]
+    | cons hd tl ih =>
+      have : (l :: hd :: tl).flatten = ([l, hd].flatten :: tl).flatten := by
+        unfold flatten
+        simp
+      rw [this]
+      rw [ih]
+      rw [ih]
+      have : [l, hd].flatten = l ++ hd := by simp [flatten]
+      rw [this]
+      simp
+
+  theorem mem_flatten (l : List (List α)) : ∀ e, e ∈ l.flatten ↔ ∃ l', l' ∈ l ∧ e ∈ l' := by
+    induction l with
+    | nil => simp [flatten]
+    | cons hd tl ih =>
+      intro e
+      rw [flatten_cons]
+      simp
+      constructor
+      . intro h
+        cases h with
+        | inl _ => apply Or.inl; assumption
+        | inr _ => apply Or.inr; apply (ih e).mp; assumption
+      . intro h
+        cases h with
+        | inl _ => apply Or.inl; assumption
+        | inr _ => apply Or.inr; apply (ih e).mpr; assumption
+
 end List
 
 def List.repeat (val : α) : Nat -> List α

ProofLibrary/Models/Cores.lean

@@ -0,0 +1,52 @@
+import ProofLibrary.SubstitutionAndHomomorphismBasics
+
+namespace Function
+
+  def injective (f : α -> β) : Prop := ∀ a b, f a = f b -> a = b
+
+  def surjective (f : α -> β) : Prop := ∀ b, ∃ a, f a = b
+
+end Function
+
+namespace GroundTermMapping
+
+  variable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
+
+  -- TODO: do we really need this?
+  def injective (h : GroundTermMapping sig) (A : FactSet sig) : Prop :=
+    ∀ t t', (t ∈ A.terms ∧ t' ∈ A.terms) -> (h t = h t' -> t = t')
+
+  -- TODO: do we really need this?
+  def surjective (h : GroundTermMapping sig) (B : FactSet sig) : Prop :=
+    ∀ t', t' ∈ B.terms -> ∃ t, h t = t'
+
+  def strong (h : GroundTermMapping sig) (A B : FactSet sig) : Prop :=
+    ∀ e, ¬ e ∈ A -> ¬ (h.applyFact e) ∈ B
+
+end GroundTermMapping
+
+namespace FactSet
+
+  variable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
+
+  def isWeakCore (fs : FactSet sig) : Prop :=
+    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs fs ∧ h.injective fs
+
+  def isStrongCore (fs : FactSet sig) : Prop :=
+    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs fs ∧ h.injective fs ∧ h.surjective fs
+
+  theorem isStrongCore_of_isWeakCore_of_finite (fs : FactSet sig) (weakCore : fs.isWeakCore) (finite : fs.finite) : fs.isStrongCore := by
+    rcases finite with ⟨l, finite⟩
+    unfold isStrongCore
+    intro h isHom
+    specialize weakCore h isHom
+    rcases weakCore with ⟨strong, injective⟩
+    constructor
+    . exact strong
+    constructor
+    . exact injective
+    . intro b b_mem
+      sorry
+
+end FactSet
+

ProofLibrary/SubstitutionAndHomomorphismBasics.lean

@@ -102,10 +102,10 @@ namespace GroundTermMapping
     { predicate := f.predicate, terms := List.map h f.terms }
 
   def applyFactSet (h : GroundTermMapping sig) (fs : FactSet sig) : FactSet sig :=
-    fun f' : Fact sig => ∃ (f : Fact sig), (f ∈ fs) ∧ ((applyFact h f) = f')
+    fun f' : Fact sig => ∃ (f : Fact sig), (f ∈ fs) ∧ ((h.applyFact f) = f')
 
   def isHomomorphism (h : GroundTermMapping sig) (A B : FactSet sig) : Prop :=
-    isIdOnConstants h ∧ (applyFactSet h A ⊆ B)
+    isIdOnConstants h ∧ (h.applyFactSet A ⊆ B)
 
   theorem applyPreservesElement (h : GroundTermMapping sig) (f : Fact sig) (fs : FactSet sig) : f ∈ fs -> applyFact h f ∈ applyFactSet h fs := by
     intro hf