WIP: Basic Termination Result for Trees (now working on (essentially)…

… Koenigs Lemma...)

ProofLibrary/ChaseSequence/Basic.lean

@@ -85,6 +85,7 @@ def not_exists_trigger_opt_fs (obs : ObsoletenessCondition sig) (rules : RuleSet
 def not_exists_trigger_list (obs : ObsoletenessCondition sig) (rules : RuleSet sig) (before : ChaseNode obs rules) (after : List (ChaseNode obs rules)) : Prop :=
   ¬(∃ trg : (RTrigger obs rules), trg.val.active before.fact) ∧ after = []
 
+@[ext]
 structure ChaseBranch (obs : ObsoletenessCondition sig) (kb : KnowledgeBase sig) where
   branch : PossiblyInfiniteList (ChaseNode obs kb.rules)
   database_first : branch.infinite_list 0 = some { fact := kb.db.toFactSet, origin := none, fact_contains_origin_result := by simp [Option.is_none_or] }
@@ -378,8 +379,8 @@ theorem chaseTreeSetIsSubsetOfResult (ct : ChaseTree obs kb) : ∀ node : List N
       unfold PossiblyInfiniteTree.branches_through at branch_through_node
       unfold InfiniteTreeSkeleton.branches_through at branch_through_node
       simp [Set.element] at branch_through_node
-      rw [branch_through_node.right ⟨node.length, by simp⟩]
-      simp
+      rcases branch_through_node with ⟨nodes, eq, eq2⟩
+      rw [eq node.length, eq2]
       rfl
 
     have branch_subs_result := chaseBranchSetIsSubsetOfResult branch node.length

ProofLibrary/ChaseSequence/Deterministic.lean

@@ -175,22 +175,25 @@ theorem ChaseTree.firstResult_is_in_result (ct : ChaseTree obs kb) : ct.firstRes
     unfold FiniteDegreeTree.branches
     unfold PossiblyInfiniteTree.branches
     unfold InfiniteTreeSkeleton.branches
+    unfold InfiniteTreeSkeleton.branches_through
     simp [firstBranch, Set.element]
     let nodes : InfiniteList Nat := fun _ => 0
     exists nodes
-    intro n
-    unfold FiniteDegreeTree.get
-    unfold PossiblyInfiniteTree.get
-    have : List.repeat 0 n = (nodes.take n).reverse := by
-      simp only [nodes]
-      induction n with
-      | zero => simp [List.repeat, InfiniteList.take]
-      | succ n ih =>
-        unfold List.repeat
-        unfold InfiniteList.take
-        simp
-        exact ih
-    rw [this]
+    constructor
+    . intro n
+      unfold FiniteDegreeTree.get
+      unfold PossiblyInfiniteTree.get
+      have : List.repeat 0 n = (nodes.take n).reverse := by
+        simp only [nodes]
+        induction n with
+        | zero => simp [List.repeat, InfiniteList.take]
+        | succ n ih =>
+          unfold List.repeat
+          unfold InfiniteList.take
+          simp
+          exact ih
+      rw [this]
+    . rfl
   . unfold ChaseBranch.result
     rfl
 
@@ -218,11 +221,11 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
           | some node =>
             have trg_ex := ct.triggers_exist (nodes.take n).reverse
             simp [Option.is_none_or]
-            have n_succ_in_ct := branch_in_ct (n+1)
+            have n_succ_in_ct := branch_in_ct.left (n+1)
             rw [eq] at n_succ_in_ct
             unfold FiniteDegreeTree.get at trg_ex
             unfold PossiblyInfiniteTree.get at trg_ex
-            rw [← branch_in_ct] at trg_ex
+            rw [← branch_in_ct.left] at trg_ex
             cases eq_prev : branch.branch.infinite_list n with
             | none =>
               have no_holes := branch.branch.no_holes (n+1) (by rw [eq]; simp) ⟨n, by simp⟩
@@ -260,7 +263,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
               | inr trg_ex =>
                 unfold not_exists_trigger_list at trg_ex
                 have contra := ct.tree.children_empty_means_all_following_none (nodes.take n).reverse trg_ex.right (nodes n)
-                specialize branch_in_ct (n+1)
+                have branch_in_ct := branch_in_ct.left (n+1)
                 unfold InfiniteList.take at branch_in_ct
                 simp at branch_in_ct
                 unfold FiniteDegreeTree.get at contra
@@ -310,7 +313,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
               have eq' := eq
               unfold FiniteDegreeTree.get at eq
               unfold PossiblyInfiniteTree.get at eq
-              rw [← branch_in_ct] at eq
+              rw [← branch_in_ct.left] at eq
               specialize this n
               rw [eq] at this; simp [Option.is_none_or] at this
               rw [this] at eq'
@@ -322,7 +325,7 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
                 cases trg_ex with | intro _ trg_ex => cases trg_ex.right with | intro _ trg_ex =>
                   unfold FiniteDegreeTree.get at h
                   unfold PossiblyInfiniteTree.get at h
-                  rw [← branch_in_ct] at h
+                  rw [← branch_in_ct.left] at h
                   rw [h] at trg_ex
                   contradiction
               | inr trg_ex =>
@@ -357,16 +360,16 @@ theorem ChaseTree.firstResult_is_result_when_deterministic (ct : ChaseTree obs k
             rw [eq] at this
             simp [Option.is_none_or] at this
             rw [← this]
-            unfold FiniteDegreeTree.get; unfold PossiblyInfiniteTree.get; rw [← branch_in_ct]; exact h
+            unfold FiniteDegreeTree.get; unfold PossiblyInfiniteTree.get; rw [← branch_in_ct.left]; exact h
         . intro h; cases h with | intro n h =>
           exists n
-          rw [branch_in_ct]
+          rw [branch_in_ct.left]
           cases eq : branch.branch.infinite_list n with
           | none =>
             rw [nodes_none_means_first_branch_none n (by
               unfold FiniteDegreeTree.get
               unfold PossiblyInfiniteTree.get
-              rw [← branch_in_ct]
+              rw [← branch_in_ct.left]
               exact eq
             )] at h
             simp [Option.is_some_and] at h

ProofLibrary/ChaseSequence/Termination.lean

@@ -197,5 +197,157 @@ section GeneralResults
 
   end ChaseBranch
 
+  namespace ChaseTree
+
+    theorem finitely_many_branch_of_terminates (ct : ChaseTree obs kb) : ct.terminates -> ct.branches.finite := by
+      unfold terminates
+      unfold ChaseBranch.terminates
+      intro each_b_term
+
+      have : ∀ b, b ∈ ct.tree.branches -> ∃ i, b.infinite_list i = none := by
+        intro b b_mem
+        rcases b_mem with ⟨nodes, b_mem, _⟩
+
+        -- It might seem like byContradiction is not needed but we need the contra hypothesis to show that cb is a proper chase branch
+        apply Classical.byContradiction
+        intro contra
+
+        let cb : ChaseBranch obs kb := {
+          branch := b
+          database_first := by rw [← ct.database_first]; rw [b_mem]; simp [InfiniteList.take]; rfl
+          triggers_exist := by
+            intro n
+            cases eq : b.infinite_list n with
+            | none => simp [Option.is_none_or]
+            | some node =>
+              simp [Option.is_none_or]
+              have trgs_ex := ct.triggers_exist (nodes.take n).reverse
+              unfold FiniteDegreeTree.get at trgs_ex
+              unfold PossiblyInfiniteTree.get at trgs_ex
+              rw [← b_mem, eq] at trgs_ex
+              simp [Option.is_none_or] at trgs_ex
+              cases trgs_ex with
+              | inr trgs_ex =>
+                unfold not_exists_trigger_list at trgs_ex
+                have all_none := ct.tree.children_empty_means_all_following_none _ trgs_ex.right
+                specialize all_none (nodes n)
+                apply False.elim
+                apply contra
+                exists (n+1)
+                rw [b_mem]
+                unfold InfiniteList.take
+                simp
+                exact all_none
+              | inl trgs_ex =>
+                apply Or.inl
+                unfold exists_trigger_list at trgs_ex
+                unfold exists_trigger_opt_fs
+                sorry
+          fairness := by sorry
+        }
+
+        apply contra
+        specialize each_b_term cb (by exists nodes)
+        exact each_b_term
+
+      -- Koenig's Lemma
+      have : ct.tree.branches.finite := by
+        apply ct.tree.branches_finite_of_each_finite
+        apply this
+
+      rcases this with ⟨l, l_nodup, l_eq⟩
+
+      let cb_for_b (b : PossiblyInfiniteList (ChaseNode obs kb.rules)) : Option (ChaseBranch obs kb) :=
+        match (Classical.propDecidable (∃ (cb : ChaseBranch obs kb), cb.branch = b)) with
+        | .isTrue p => some (Classical.choose p)
+        | .isFalse _ => none
+
+      have := Classical.typeDecidableEq (ChaseBranch obs kb)
+      let filtered := (l.filterMap (fun b => cb_for_b b)).eraseDupsKeepRight
+
+      exists filtered
+      constructor
+      . apply List.nodup_eraseDupsKeepRight
+      . intro e
+        unfold filtered
+        rw [List.mem_eraseDupsKeepRight_iff]
+        unfold branches
+        simp
+        constructor
+        . intro h
+          rcases h with ⟨b, b_mem, b_eq⟩
+          unfold cb_for_b at b_eq
+          split at b_eq
+          case h_1 _ p _ =>
+            have spec := Classical.choose_spec p
+            injection b_eq with b_eq
+            rw [← b_eq]
+            simp [Set.element]
+            rw [spec]
+            apply (l_eq b).mp
+            exact b_mem
+          case h_2 _ p _ =>
+            simp at b_eq
+        . intro h
+          exists e.branch
+          rw [l_eq]
+          constructor
+          . exact h
+          . unfold cb_for_b
+            split
+            case h_1 _ p _ =>
+              have spec := Classical.choose_spec p
+              simp
+              apply ChaseBranch.ext
+              exact spec
+            case h_2 _ p _ =>
+              apply False.elim
+              apply p
+              exists e
+
+    theorem result_finite_of_branches_finite (ct : ChaseTree obs kb) : ct.branches.finite -> ct.result.finite := by
+      intro bs_finite
+      unfold Set.finite at bs_finite
+      rcases bs_finite with ⟨l, _, iff⟩
+      have : DecidableEq (FactSet sig) := Classical.typeDecidableEq (FactSet sig)
+      exists (l.map ChaseBranch.result).eraseDupsKeepRight
+      constructor
+      . apply List.nodup_eraseDupsKeepRight
+      . intro fs
+        rw [List.mem_eraseDupsKeepRight_iff]
+        simp
+        constructor
+        . intro h
+          rcases h with ⟨b, mem, eq⟩
+          exists b
+          constructor
+          . rw [← iff]; exact mem
+          . exact eq
+        . intro h
+          rcases h with ⟨b, mem, eq⟩
+          exists b
+          constructor
+          . rw [iff]; exact mem
+          . exact eq
+
+    theorem terminates_iff_result_finite (ct : ChaseTree obs kb) : ct.terminates ↔ ∀ fs, fs ∈ ct.result -> fs.finite := by
+      unfold terminates
+      unfold result
+      constructor
+      . intro each_b_term
+        intro res res_mem
+        rcases res_mem with ⟨b, mem, eq⟩
+        rw [← eq]
+        rw [← ChaseBranch.terminates_iff_result_finite]
+        apply each_b_term
+        exact mem
+      . intro each_b_term
+        intro b mem
+        rw [ChaseBranch.terminates_iff_result_finite]
+        apply each_b_term
+        exists b
+
+  end ChaseTree
+
 end GeneralResults
 

ProofLibrary/ChaseSequence/Universality.lean

@@ -868,15 +868,18 @@ theorem chaseTreeResultIsUniversal (ct : ChaseTree obs kb) : ∀ (m : FactSet si
     unfold FiniteDegreeTree.branches
     unfold PossiblyInfiniteTree.branches
     unfold InfiniteTreeSkeleton.branches
+    unfold InfiniteTreeSkeleton.branches_through
     unfold Set.element
     simp
     exists indices
-    intro n
-    simp only [path]
-    rw [indices_aux_result]
-    unfold FiniteDegreeTree.get
-    unfold PossiblyInfiniteTree.get
-    rfl
+    constructor
+    . intro n
+      simp only [path]
+      rw [indices_aux_result]
+      unfold FiniteDegreeTree.get
+      unfold PossiblyInfiniteTree.get
+      rfl
+    . rfl
   . constructor
     . intro gt
       split

ProofLibrary/PossiblyInfiniteList.lean

@@ -7,6 +7,9 @@ namespace InfiniteList
   | 0 => []
   | n+1 => (l.take n) ++ [l n]
 
+  theorem length_take (l : InfiniteList α) (n : Nat) : (l.take n).length = n := by
+    induction n ; simp [take] ; simpa [take]
+
   def skip (l : InfiniteList α) (m : Nat) : InfiniteList α := fun n => l (n + m)
 
   theorem skip_zero_eq (l : InfiniteList α) : l.skip 0 = l := by unfold skip; simp only [Nat.add_zero]
@@ -39,6 +42,30 @@ namespace InfiniteList
         have : m = k := by cases Nat.lt_or_eq_of_le (Nat.le_of_lt_succ m.isLt); contradiction; assumption
         rw [this]
         simp [take]
+
+  theorem take_after_take (l : InfiniteList α) (n m : Nat) : (l.take n).take m = l.take (n.min m) := by
+    induction n with
+    | zero => simp [take]
+    | succ n ih =>
+      simp [take]
+      rw [List.take_append_eq_append_take]
+      rw [ih]
+      rw [length_take]
+      cases Decidable.em (n ≤ m) with
+      | inl le =>
+        simp [Nat.min_eq_left le]
+        cases Nat.eq_or_lt_of_le le with
+        | inl eq =>
+          rw [eq]
+          simp
+        | inr lt =>
+          simp [Nat.min_eq_left (Nat.succ_le_of_lt lt)]
+          conv => right; unfold InfiniteList.take
+          rw [List.take_of_length_le (by apply Nat.le_sub_of_add_le; rw [Nat.add_comm, List.length_singleton]; apply Nat.succ_le_of_lt; exact lt)]
+      | inr lt =>
+        simp at lt
+        simp [Nat.min_eq_right (Nat.le_of_lt lt), Nat.min_eq_right (Nat.le_succ_of_le (Nat.le_of_lt lt))]
+        apply Nat.sub_eq_zero_of_le (Nat.le_of_lt lt)
 end InfiniteList
 
 @[ext]