WIP: no alt matches implies core

ProofLibrary/AlternativeMatches/Chase.lean

@@ -0,0 +1,82 @@
+import ProofLibrary.AlternativeMatches.Basic
+import ProofLibrary.AlternativeMatches.HomomorphismExtension
+import ProofLibrary.Models.Cores
+
+variable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
+variable {obs : ObsoletenessCondition sig} {kb : KnowledgeBase sig}
+
+namespace GroundTermMapping
+
+  def is_alt_match_at_chase_step (h : GroundTermMapping sig) (cb : ChaseBranch obs kb) (i : Nat) : Prop :=
+    match eq : cb.branch.infinite_list (i + 1) with
+    | .none => True
+    | .some node =>
+      have := eq ▸ cb.origin_is_some i
+      let origin := node.origin.get (by rw [Option.is_none_or] at this; exact this)
+      h.isAlternativeMatch origin.fst.val origin.snd cb.result
+
+end GroundTermMapping
+
+namespace ChaseBranch
+
+  def has_alt_match_at_step (cb : ChaseBranch obs kb) (i : Nat) : Prop := ∃ (h : GroundTermMapping sig), h.is_alt_match_at_chase_step cb i
+
+  def has_alt_match (cb : ChaseBranch obs kb) : Prop := ∃ i, cb.has_alt_match_at_step i
+
+  theorem result_isWeakCore_of_noAltMatch (cb : ChaseBranch obs kb) : ¬ cb.has_alt_match -> cb.result.isWeakCore := by
+    sorry
+
+  theorem result_isStrongCore_of_noAltMatch (cb : ChaseBranch obs kb) : ¬ cb.has_alt_match -> cb.result.isStrongCore := by
+    unfold FactSet.isStrongCore
+    intro noAltMatch h endo
+    have ⟨strong, inj⟩ := cb.result_isWeakCore_of_noAltMatch noAltMatch h endo
+    constructor
+    . exact strong
+    constructor
+    . exact inj
+    . apply Classical.byContradiction
+      intro contra
+      unfold Function.surjective_for_domain_and_image_set at contra
+      simp at contra
+      rcases contra with ⟨t, t_mem, contra⟩
+
+      let term_property (ts : Set (GroundTerm sig)) (t : GroundTerm sig) := ∃ j, ∀ t', t' ∈ ts -> ¬ (h.repeat_hom j) t' = t
+      let step_property (i : Nat) := (cb.branch.infinite_list i).is_none_or (fun node => ∃ t, t ∈ node.fact.val.terms ∧ term_property node.fact.val.terms t)
+
+      -- there exists a smallest chase step with such a term (not necessarily t)
+      have : ∃ i, step_property i ∧ ∀ (j : Fin i), ¬ step_property j.val := by
+        sorry
+      rcases this with ⟨step, prop_step, smallest⟩
+
+      let stronger_term_property (ts : Set (GroundTerm sig)) (t : GroundTerm sig) := ∃ j, ∀ k, j ≤ k -> ∀ t', t' ∈ ts -> ¬ (h.repeat_hom k) t' = t
+
+      have term_prop_implies_stronger (ts : Set (GroundTerm sig)) (t : GroundTerm sig) : term_property ts t -> stronger_term_property ts t := by
+        unfold term_property
+        unfold stronger_term_property
+        intro term_prop
+        /- intro s s_mem -/
+        /- specialize term_prop s s_mem -/
+        rcases term_prop with ⟨j, term_prop⟩
+        exists j
+        intro k le
+        rcases Nat.exists_eq_add_of_le le with ⟨diff, diff_eq⟩
+        induction diff generalizing k with
+        | zero => sorry
+        | succ diff ih =>
+          unfold GroundTermMapping.repeat_hom
+          rw [diff_eq]
+          simp
+          intro s s_mem contra
+          apply ih (j + diff) _ rfl (h s)
+          . sorry
+          . rw [h.repeat_hom_swap] at contra
+            exact contra
+          . simp
+
+      apply noAltMatch
+      exists step
+
+      sorry
+
+end ChaseBranch
+

ProofLibrary/ChaseSequence/Basic.lean

@@ -100,6 +100,36 @@ namespace ChaseBranch
 
   def result (branch : ChaseBranch obs kb) : FactSet sig :=
     fun f => ∃ n : Nat, (branch.branch.infinite_list n).is_some_and (fun fs => f ∈ fs.fact)
+
+  theorem origin_is_some (cb : ChaseBranch obs kb) : ∀ i, (cb.branch.infinite_list (i + 1)).is_none_or (fun node => node.origin.isSome) := by
+    intro i
+    cases eq : cb.branch.infinite_list (i + 1) with
+    | none => simp [Option.is_none_or]
+    | some node =>
+      simp only [Option.is_none_or]
+      have trg_ex := cb.triggers_exist i
+      cases eq2 : cb.branch.infinite_list i with
+      | none =>
+        have no_holes := cb.branch.no_holes (i + 1)
+        simp [eq] at no_holes
+        specialize no_holes ⟨i, by simp⟩
+        apply False.elim
+        apply no_holes
+        exact eq2
+      | some prev_node =>
+        rw [eq2, Option.is_none_or] at trg_ex
+        cases trg_ex with
+        | inl trg_ex =>
+          unfold exists_trigger_opt_fs at trg_ex
+          rcases trg_ex with ⟨trg, _, disj, trg_eq⟩
+          rw [eq] at trg_eq
+          injection trg_eq with trg_eq
+          rw [← trg_eq]
+          simp
+        | inr trg_ex =>
+          unfold not_exists_trigger_opt_fs at trg_ex
+          rw [eq] at trg_ex
+          simp at trg_ex
 end ChaseBranch
 
 structure ChaseTree (obs : ObsoletenessCondition sig) (kb : KnowledgeBase sig) where

ProofLibrary/Models/Cores.lean

@@ -282,6 +282,19 @@ namespace GroundTermMapping
       . rw [applyFact_compose]
         simp
 
+  def repeat_hom (h : GroundTermMapping sig) : Nat -> GroundTermMapping sig
+  | .zero => id
+  | .succ j => h ∘ (h.repeat_hom j)
+
+  theorem repeat_hom_swap (h : GroundTermMapping sig) (i : Nat) : ∀ t, h (h.repeat_hom i t) = (h.repeat_hom i) (h t) := by
+    intro t
+    induction i with
+    | zero => unfold repeat_hom; simp
+    | succ i ih =>
+      unfold repeat_hom
+      simp
+      rw [ih]
+
 end GroundTermMapping
 
 namespace FactSet