WIP: show that mfa result subsumes every chase branch

ProofLibrary/ChaseSequence/Termination/MfaLike.lean

@@ -1,7 +1,31 @@
 import ProofLibrary.ChaseSequence.Termination.Basic
 
+section Defs
+
+  variable (sig : Signature) [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
+
+  -- This is essentially the same as a GroundSubstitution only that it maps constants instead of variables
+  abbrev ConstantMapping := sig.C -> GroundTerm sig
+
+end Defs
+
+
 variable {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V]
 
+namespace ConstantMapping
+
+  def apply_ground_term (g : ConstantMapping sig) (t : GroundTerm sig) : GroundTerm sig := t.mapLeaves g
+
+  def apply_fact (g : ConstantMapping sig) (f : Fact sig) : Fact sig := {
+    predicate := f.predicate
+    terms := f.terms.map g.apply_ground_term
+    arity_ok := by rw [List.length_map]; exact f.arity_ok
+  }
+
+  def apply_fact_set (g : ConstantMapping sig) (fs : FactSet sig) : FactSet sig := fun f => ∃ f', f' ∈ fs ∧ f = g.apply_fact f'
+
+end ConstantMapping
+
 namespace KnowledgeBase
 
   def parallelSkolemChase (kb : KnowledgeBase sig) (det : kb.rules.isDeterministic) : InfiniteList (FactSet sig)
@@ -351,5 +375,74 @@ namespace RuleSet
     }
     kb.skolemChaseResult det
 
+  theorem mfaSet_contains_every_chase_step_for_every_kb_expect_for_facts_with_predicates_not_from_rs (rs : RuleSet sig) (finite : rs.rules.finite) (det : rs.isDeterministic) (special_const : sig.C) : ∀ {db : Database sig} (cb : ChaseBranch (SkolemObsoleteness sig) { rules := rs, db := db }) (n : Nat), (cb.branch.infinite_list n).is_none_or (fun node => ∀ f, f.predicate ∈ rs.predicates -> f ∈ (ConstantMapping.apply_fact_set (fun _ => GroundTerm.const special_const) node.fact.val) -> f ∈ (rs.mfaSet finite det special_const)) := by
+    intro db cb n
+    induction n with
+    | zero =>
+      rw [cb.database_first, Option.is_none_or]
+      simp only
+      intro f f_predicate f_mem
+      exists 0
+      unfold KnowledgeBase.parallelSkolemChase
+      unfold criticalInstance
+      simp only
+      unfold ConstantMapping.apply_fact_set at f_mem
+      rcases f_mem with ⟨f', f'_mem, f_eq⟩
+      simp only [Database.toFactSet, Set.element] at f'_mem
+      cases eq' : f'.toFunctionFreeFact with
+      | none => rw [eq'] at f'_mem; simp at f'_mem
+      | some fff' =>
+        unfold ConstantMapping.apply_fact at f_eq
+        simp only [Database.toFactSet, Set.element]
+        cases eq : f.toFunctionFreeFact with
+        | none =>
+          rw [f_eq] at eq
+          simp [Fact.toFunctionFreeFact] at eq
+          simp [Fact.toFunctionFreeFact] at eq'
+          rcases eq' with ⟨h, eq'⟩
+          rcases eq with ⟨t, t_mem, apply_t_func⟩
+          unfold ConstantMapping.apply_ground_term at apply_t_func
+          unfold FiniteTree.mapLeaves at apply_t_func
+          cases eq_t : t with
+          | leaf _ => simp [eq_t] at apply_t_func
+          | inner _ _ => specialize h t t_mem; simp [eq_t] at h
+        | some fff =>
+          simp only
+          unfold Fact.toFunctionFreeFact at eq
+          split at eq
+          . injection eq with eq
+            constructor
+            . rw [← eq]; exact f_predicate
+            . intro c c_mem
+              rw [← eq] at c_mem
+              simp only [List.mem_map] at c_mem
+              rcases c_mem with ⟨t, _, c_eq⟩
+              have t_mem := t.property
+              simp only [f_eq] at t_mem
+              split at c_eq
+              case h_1 d _ _ t_eq _ =>
+                rw [t_eq] at t_mem
+                simp at t_mem
+                sorry
+              case h_2 _ _ _ _ t_eq _ => sorry
+
+              rcases t_mem with ⟨s, _, t_eq⟩
+              cases eq_s : s with
+              | leaf d =>
+                simp [eq_s, ConstantMapping.apply_ground_term, FiniteTree.mapLeaves] at t_eq
+                simp only at c_eq
+                split at c_eq
+                . injection t_eq with t_eq
+                  rw [t_eq, c_eq]
+                . simp at c_eq; sorry
+              | inner _ _ => sorry
+          . simp at eq
+
+    | succ n ih =>
+      cases cb.branch.infinite_list (n+1) with
+      | none => simp [Option.is_none_or]
+      | some node =>
+        sorry
+
 end RuleSet