WIP: Basic Formalization for Cores

ProofLibrary/KnowledgeBaseBasics.lean

@@ -201,6 +201,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

@@ -334,6 +334,7 @@ namespace List
     cases l with
     | nil => contradiction
     | cons head tail => simp
+
 end List
 
 def List.repeat (val : α) : Nat -> List α

ProofLibrary/Models/Cores.lean

@@ -0,0 +1,70 @@
+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) (terms : Set (GroundTerm sig)) : Prop :=
+    ∀ t t', (t ∈ terms ∧ t' ∈ terms) -> (h t = h t' -> t = t')
+
+  -- TODO: do we really need this?
+  def surjective (h : GroundTermMapping sig) (terms : Set (GroundTerm sig)) : Prop :=
+    ∀ t', t' ∈ terms -> ∃ t, h t = t'
+
+  def strong (h : GroundTermMapping sig) (A B : FactSet sig) : Prop :=
+    ∀ e, ¬ e ∈ A -> ¬ (h.applyFact e) ∈ B
+
+  -- TODO: is this really usable?
+  theorem surjective_of_injective_of_closed_on_list (h : GroundTermMapping sig) (terms : List (GroundTerm sig)) (inj : h.injective terms.toSet) (closed : ∀ (l : List _), ∀ t, t ∈ l -> h t ∈ l) : h.surjective terms.toSet := by
+    induction terms with
+    | nil => sorry
+    | cons hd tl ih =>
+      specialize ih (sorry)
+      unfold surjective
+      intro b b_mem
+      rw [← List.inIffInToSet] at b_mem
+      simp at b_mem
+      cases b_mem with
+      | inl b_mem => sorry
+      | inr b_mem =>
+        unfold surjective at ih
+        rw [List.inIffInToSet] at b_mem
+        specialize ih b b_mem
+        exact ih
+
+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.terms
+
+  def isStrongCore (fs : FactSet sig) : Prop :=
+    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs fs ∧ h.injective fs.terms ∧ h.surjective fs.terms
+
+  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