WIP: Chase w/o alt match: endo strong and injective

ProofLibrary/AlternativeMatches/Chase.lean

@@ -126,7 +126,267 @@ namespace ChaseBranch
   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
+    intro noAltMatch h_0 h_0_hom
+    apply Classical.byContradiction
+    intro contra
+    have contra := implToNotOr (notAndDeMorgan contra)
+
+    have : ∀ k, (cb.branch.infinite_list k).is_none_or (fun node => ∃ (h_k : GroundTermMapping sig), (h_k.isHomomorphism cb.result cb.result) ∧ ((∀ (f : Fact sig), (∀ (t : GroundTerm sig), t ∈ f.terms -> t ∈ cb.result.terms) -> ¬ f ∈ cb.result -> h_0.applyFact f ∈ cb.result -> h_k.applyFact f ∈ cb.result) ∧ (∀ s t, s ∈ cb.result.terms -> t ∈ cb.result.terms -> s ≠ t -> h_0 s = h_0 t -> h_k s = h_k t)) ∧ (∀ t, t ∈ node.fact.val.terms -> h_k t = t)) := by
+      intro k
+      induction k with
+      | zero =>
+        rw [cb.database_first, Option.is_none_or]
+        exists h_0
+        constructor
+        . constructor
+          . sorry
+          . sorry
+        . sorry
+      | succ k ih =>
+        cases eq : cb.branch.infinite_list (k+1) with
+        | none => simp [Option.is_none_or]
+        | some node =>
+          rw [Option.is_none_or]
+          cases eq2 : cb.branch.infinite_list k with
+          | none => sorry -- contradiction via no_holes
+          | some node2 =>
+            rw [eq2, Option.is_none_or] at ih
+            rcases ih with ⟨h_k, h_k_hom, retains, identity⟩
+
+            cases eq_origin : node.origin with
+            | none =>
+              have is_some := cb.origin_is_some k
+              rw [eq, Option.is_none_or] at is_some
+              rw [eq_origin] at is_some
+              simp at is_some
+            | some origin =>
+              have node_fact_is_prev_fact_union_origin_res := cb.origin_trg_result_yields_next_node_fact k node node2 eq eq2 origin eq_origin
+              have origin_trg_active := cb.origin_trg_is_active k node node2 eq eq2
+
+              let trg_res_terms := (origin.fst.val.result.get origin.snd).terms
+
+              have h_surj_on_trg_res : h_k.surjective_for_domain_and_image_set trg_res_terms trg_res_terms := by
+                apply Classical.byContradiction
+                intro not_surj
+                apply noAltMatch
+                exists k
+                exists h_k
+                apply Or.inr
+                exists node
+                exists origin
+                constructor
+                . exact eq
+                constructor
+                . exact eq_origin
+                . constructor
+                  . constructor
+                    . exact h_k_hom.left
+                    . apply Set.subsetTransitive _ (h_k.applyFactSet cb.result) _
+                      constructor
+                      . apply GroundTermMapping.applyFactSet_subset_of_subset
+                        apply Set.subsetTransitive _ node.fact.val _
+                        constructor
+                        . rw [node_fact_is_prev_fact_union_origin_res]
+                          apply Set.subsetUnionSomethingStillSubset'
+                          apply Set.subsetOfSelf
+                        . have subset_res := chaseBranchSetIsSubsetOfResult cb (k+1)
+                          rw [eq, Option.is_none_or] at subset_res
+                          exact subset_res
+                      . exact h_k_hom.right
+                  constructor
+                  . intro t t_mem
+                    apply identity
+                    simp at t_mem
+                    rcases t_mem with ⟨v, v_mem, v_eq⟩
+                    rcases origin.fst.val.rule.frontier_var_occurs_in_fact_in_body v v_mem with ⟨a, a_mem, v_mem⟩
+                    exists origin.fst.val.subs.apply_function_free_atom a
+                    constructor
+                    . apply origin_trg_active.left
+                      rw [← List.inIffInToSet]
+                      simp [PreTrigger.mapped_body, SubsTarget.apply, GroundSubstitution.apply_function_free_conj]
+                      exists a
+                      constructor
+                      . simp [eq_origin]; exact a_mem
+                      . simp [eq_origin]
+                    . rw [← v_eq]
+                      simp [GroundSubstitution.apply_function_free_atom]
+                      exists VarOrConst.var v
+                  . unfold Function.surjective_for_domain_and_image_set at not_surj
+                    simp at not_surj
+                    rcases not_surj with ⟨t, t_mem, no_arg_for_t⟩
+                    exists t
+                    constructor
+                    . exact t_mem
+                    . intro t_mem_image
+                      rcases t_mem_image with ⟨f, f_mem, t_mem_image⟩
+                      rcases f_mem with ⟨f', f'_mem, f_eq⟩
+                      rw [← f_eq] at t_mem_image
+                      simp [GroundTermMapping.applyFact] at t_mem_image
+                      rcases t_mem_image with ⟨t', t'_mem_image, t_eq⟩
+                      apply no_arg_for_t t'
+                      . exists f'
+                      . exact t_eq
+
+              sorry
+
+    cases contra with
+    | inl not_strong =>
+      apply not_strong
+      unfold GroundTermMapping.strong
+      intro f f_dom f_mem apply_f_mem
+
+      have step_ex : ∀ (terms : List (GroundTerm sig)), (∀ t, t ∈ terms -> t ∈ cb.result.terms) -> ∃ i, (cb.branch.infinite_list i).is_some_and (fun node => ∀ t, t ∈ terms -> t ∈ node.fact.val.terms) := by
+        intro terms id_on_terms
+        induction terms with
+        | nil => exists 0; rw [cb.database_first, Option.is_some_and]; simp
+        | cons hd tl ih =>
+          rcases ih (by intro t t_mem; apply id_on_terms; simp [t_mem]) with ⟨i_ih, ih⟩
+          specialize id_on_terms hd (by simp)
+          rcases id_on_terms with ⟨f, f_mem, hd_mem⟩
+          rcases f_mem with ⟨i_hd, f_mem⟩
+
+          cases eq_hd : cb.branch.infinite_list i_hd with
+          | none => simp [eq_hd, Option.is_some_and] at f_mem
+          | some node_hd =>
+            rw [eq_hd, Option.is_some_and] at f_mem
+            cases eq_ih : cb.branch.infinite_list i_ih with
+            | none => simp [eq_ih, Option.is_some_and] at ih
+            | some node_ih =>
+              rw [eq_ih, Option.is_some_and] at ih
+              cases Decidable.em (i_hd ≤ i_ih) with
+              | inl le =>
+                exists i_ih
+                rw [eq_ih, Option.is_some_and]
+                intro t t_mem
+                simp at t_mem
+                cases t_mem with
+                | inl t_mem =>
+                  rw [t_mem]
+                  exists f
+                  constructor
+                  . have all_following := chaseBranchSetIsSubsetOfAllFollowing cb i_hd (i_ih - i_hd)
+                    simp [eq_hd] at all_following
+                    rw [Nat.add_sub_of_le le, eq_ih, Option.is_none_or] at all_following
+                    apply all_following
+                    exact f_mem
+                  . exact hd_mem
+                | inr t_mem =>
+                  apply ih
+                  exact t_mem
+              | inr lt =>
+                simp at lt
+                exists i_hd
+                rw [eq_hd, Option.is_some_and]
+                intro t t_mem
+                simp at t_mem
+                cases t_mem with
+                | inl t_mem =>
+                  rw [t_mem]
+                  exists f
+                | inr t_mem =>
+                  specialize ih t t_mem
+                  rcases ih with ⟨f', f'_mem, t_mem⟩
+                  exists f'
+                  constructor
+                  . have all_following := chaseBranchSetIsSubsetOfAllFollowing cb i_ih (i_hd - i_ih)
+                    simp [eq_ih] at all_following
+                    rw [Nat.add_sub_of_le (Nat.le_of_lt lt), eq_hd, Option.is_none_or] at all_following
+                    apply all_following
+                    exact f'_mem
+                  . exact t_mem
+
+      specialize step_ex f.terms f_dom
+      rcases step_ex with ⟨step, step_ex⟩
+
+      cases eq : cb.branch.infinite_list step with
+      | none => rw [eq, Option.is_some_and] at step_ex; contradiction
+      | some node =>
+        rw [eq, Option.is_some_and] at step_ex
+        specialize this step
+        rw [eq, Option.is_none_or] at this
+        rcases this with ⟨h_k, _, retains, identity⟩
+        have retains := retains.left f f_dom f_mem apply_f_mem
+
+        have : h_k.applyFact f = f := by
+          unfold GroundTermMapping.applyFact
+          rw [Fact.ext_iff]
+          constructor
+          . simp
+          . simp
+            apply List.map_id_of_id_on_all_mem
+            intro t t_mem
+            apply identity
+            apply step_ex
+            exact t_mem
+        apply f_mem
+        rw [← this]
+        exact retains
+    | inr not_inj =>
+      apply not_inj
+      intro s t s_mem t_mem image_eq
+      apply Classical.byContradiction
+      intro neq
+
+      rcases s_mem with ⟨f_s, f_s_mem, s_mem⟩
+      rcases t_mem with ⟨f_t, f_t_mem, t_mem⟩
+      rcases f_s_mem with ⟨step_s, f_s_mem⟩
+      rcases f_t_mem with ⟨step_t, f_t_mem⟩
+      cases eq_s : cb.branch.infinite_list step_s with
+      | none => simp [eq_s, Option.is_some_and] at f_s_mem
+      | some node_s =>
+        rw [eq_s, Option.is_some_and] at f_s_mem
+        cases eq_t : cb.branch.infinite_list step_t with
+        | none => simp [eq_t, Option.is_some_and] at f_t_mem
+        | some node_t =>
+          rw [eq_t, Option.is_some_and] at f_t_mem
+          cases Decidable.em (step_s ≤ step_t) with
+          | inl le =>
+            specialize this step_t
+            rw [eq_t, Option.is_none_or] at this
+            rcases this with ⟨h_k, _, retains, identity⟩
+            have retains := retains.right
+            specialize retains s t
+              (by exists f_s; constructor; exists step_s; rw [eq_s, Option.is_some_and]; exact f_s_mem; exact s_mem)
+              (by exists f_t; constructor; exists step_t; rw [eq_t, Option.is_some_and]; exact f_t_mem; exact t_mem)
+              neq image_eq
+            have id_s := identity s (by
+              exists f_s
+              constructor
+              . have all_following := chaseBranchSetIsSubsetOfAllFollowing cb step_s (step_t - step_s)
+                simp [eq_s] at all_following
+                rw [Nat.add_sub_of_le le, eq_t, Option.is_none_or] at all_following
+                apply all_following
+                exact f_s_mem
+              . exact s_mem
+            )
+            have id_t := identity t (by exists f_t)
+            rw [id_s, id_t] at retains
+            apply neq
+            apply retains
+          | inr lt =>
+            simp at lt
+            specialize this step_s
+            rw [eq_s, Option.is_none_or] at this
+            rcases this with ⟨h_k, _, retains, identity⟩
+            have retains := retains.right
+            specialize retains s t
+              (by exists f_s; constructor; exists step_s; rw [eq_s, Option.is_some_and]; exact f_s_mem; exact s_mem)
+              (by exists f_t; constructor; exists step_t; rw [eq_t, Option.is_some_and]; exact f_t_mem; exact t_mem)
+              neq image_eq
+            have id_s := identity s (by exists f_s)
+            have id_t := identity t (by
+              exists f_t
+              constructor
+              . have all_following := chaseBranchSetIsSubsetOfAllFollowing cb step_t (step_s - step_t)
+                simp [eq_t] at all_following
+                rw [Nat.add_sub_of_le (Nat.le_of_lt lt), eq_s, Option.is_none_or] at all_following
+                apply all_following
+                exact f_t_mem
+              . exact t_mem
+            )
+            rw [id_s, id_t] at retains
+            apply neq
+            apply retains
 
   theorem result_isStrongCore_of_noAltMatch (cb : ChaseBranch obs kb) : ¬ cb.has_alt_match -> cb.result.isStrongCore := by
     unfold FactSet.isStrongCore

ProofLibrary/List.lean

@@ -360,6 +360,18 @@ namespace List
         rcases h with ⟨as, bs, eq, _⟩
         simp [eq]
 
+  theorem map_id_of_id_on_all_mem (l : List α) (f : α -> α) (id_on_all_mem : ∀ e, e ∈ l -> f e = e) : l.map f = l := by
+    induction l with
+    | nil => simp
+    | cons hd tl ih =>
+      unfold map
+      rw [id_on_all_mem hd]
+      . rw [ih]
+        intro e e_mem
+        apply id_on_all_mem
+        simp [e_mem]
+      . simp
+
 end List
 
 def List.repeat (val : α) : Nat -> List α

ProofLibrary/Models/Cores.lean

@@ -232,6 +232,15 @@ namespace Function
       apply h
       exact b_mem
 
+  theorem injective_of_surjective_of_nodup [DecidableEq α] (f : α -> α) (l : List α) (nodup : l.Nodup) : f.surjective_for_domain_and_image_list l l -> f.injective_for_domain_list l := by
+    intro surj
+    rw [surjective_on_target_iff_all_in_image] at surj
+    rw [injective_iff_length_image_eq_of_nodup _ _ nodup]
+    rw [Nat.eq_iff_le_and_ge]
+    constructor
+    . exact length_image f l
+    . exact List.length_le_of_nodup_of_all_mem l (image f l) nodup surj
+
   theorem injective_iff_surjective_of_nodup_of_closed [DecidableEq α] (f : α -> α) (l : List α) (nodup : l.Nodup) (closed : ∀ e, e ∈ l -> f e ∈ l) : f.injective_for_domain_list l ↔ f.surjective_for_domain_and_image_list l l := by
     constructor
     . intro inj
@@ -250,13 +259,7 @@ namespace Function
       rw [surjective_on_target_iff_all_in_image]
       intro b
       apply (this b).mpr
-    . intro surj
-      rw [surjective_on_target_iff_all_in_image] at surj
-      rw [injective_iff_length_image_eq_of_nodup _ _ nodup]
-      rw [Nat.eq_iff_le_and_ge]
-      constructor
-      . exact length_image f l
-      . exact List.length_le_of_nodup_of_all_mem l (image f l) nodup surj
+    . apply injective_of_surjective_of_nodup; exact nodup
 
 end Function
 
@@ -266,14 +269,15 @@ namespace GroundTermMapping
 
   variable {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P]
 
-  def strong (h : GroundTermMapping sig) (A B : FactSet sig) : Prop :=
-    ∀ e, ¬ e ∈ A -> ¬ (h.applyFact e) ∈ B
+  def strong (h : GroundTermMapping sig) (domain : Set (GroundTerm sig)) (A B : FactSet sig) : Prop :=
+    ∀ (e : Fact sig), (∀ t, t ∈ e.terms -> t ∈ domain) -> ¬ e ∈ A -> ¬ (h.applyFact e) ∈ B
 
-  theorem strong_of_compose_strong (g h : GroundTermMapping sig) (A B C : FactSet sig) :
-      h.isHomomorphism B C -> GroundTermMapping.strong (h ∘ g) A C -> g.strong A B := by
+  theorem strong_of_compose_strong (g h : GroundTermMapping sig) (domain : Set (GroundTerm sig)) (A B C : FactSet sig) :
+      h.isHomomorphism B C -> GroundTermMapping.strong (h ∘ g) domain A C -> g.strong domain A B := by
     intro h_hom compose_strong
-    intro e e_not_mem_a e_mem_b
+    intro e e_dom e_not_mem_a e_mem_b
     apply compose_strong e
+    . exact e_dom
     . exact e_not_mem_a
     . apply h_hom.right (GroundTermMapping.applyFact (h ∘ g) e)
       exists (g.applyFact e)
@@ -289,10 +293,10 @@ 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_for_domain_set fs.terms
+    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs.terms fs fs ∧ h.injective_for_domain_set fs.terms
 
   def isStrongCore (fs : FactSet sig) : Prop :=
-    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs fs ∧ h.injective_for_domain_set fs.terms ∧ h.surjective_for_domain_and_image_set fs.terms fs.terms
+    ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.strong fs.terms fs fs ∧ h.injective_for_domain_set fs.terms ∧ h.surjective_for_domain_and_image_set fs.terms fs.terms
 
   theorem hom_surjective_of_finite_of_injective (fs : FactSet sig) (finite : fs.finite) : ∀ (h : GroundTermMapping sig), h.isHomomorphism fs fs -> h.injective_for_domain_set fs.terms -> h.surjective_for_domain_and_image_set fs.terms fs.terms := by
     rcases finite with ⟨l, finite⟩
@@ -370,7 +374,7 @@ namespace FactSet
       {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 sc ∧ iso.injective_for_domain_set wc.terms ∧ iso.surjective_for_domain_and_image_set wc.terms sc.terms := by
+      ∃ (iso : GroundTermMapping sig), iso.isHomomorphism wc sc ∧ iso.strong wc.terms wc sc ∧ iso.injective_for_domain_set wc.terms ∧ iso.surjective_for_domain_and_image_set wc.terms sc.terms := by
 
     rcases sc_universal.right wc wc_universal.left with ⟨h_sc_wc, h_sc_wc_hom⟩
     rcases wc_universal.right sc sc_universal.left with ⟨h_wc_sc, h_wc_sc_hom⟩
@@ -392,7 +396,7 @@ namespace FactSet
     . exact h_wc_sc_hom
     constructor
     -- strong since h_sc_wc ∘ h_wc_sc is strong
-    . apply GroundTermMapping.strong_of_compose_strong h_wc_sc h_sc_wc wc sc wc h_sc_wc_hom
+    . apply GroundTermMapping.strong_of_compose_strong h_wc_sc h_sc_wc wc.terms wc sc wc h_sc_wc_hom
       exact wc_weak.left
     constructor
     -- injective since h_sc_wc ∘ h_wc_sc is injetive