WIP: Show that determinsitic Chase Branch has Tree

monsterkrampe · Dec 10, 2024 · 4c4ea97 · 4c4ea97
1 parent f13b717
commit 4c4ea97
Show file tree

Hide file tree

Showing 2 changed files with 114 additions and 0 deletions.
diff --git a/ProofLibrary/ChaseSequence/Deterministic.lean b/ProofLibrary/ChaseSequence/Deterministic.lean
@@ -394,3 +394,115 @@ theorem deterministicChaseTreeResultUniversallyModelsKb (ct : ChaseTree obs kb)
         rw [← h'.left]
         exact h'.right
 
+theorem deterministicChaseBranchResultUniversallyModelsKb (cb : ChaseBranch obs kb) : kb.isDeterministic -> cb.result.universallyModelsKb kb := by
+  intro deterministic
+
+  have : ∃ (ct : ChaseTree obs kb), ct.firstResult = cb.result := by
+    let ct : ChaseTree obs kb := {
+      tree := {
+        tree := {
+          infinite_tree := fun l => if l.all (fun e => e = 0) then cb.branch.infinite_list l.length else none
+          no_orphans := by sorry
+          /-   intro l -/
+          /-   cases eq : l.all (fun e => e = 0) with -/
+          /-   | false => simp [eq] -/
+          /-   | true => -/
+          /-     simp only [eq] -/
+          /-     intro not_none -/
+          /-     intro parent -/
+          /-     rcases parent.property with ⟨diff, l_eq⟩ -/
+          /-     have : parent.val.all (fun e => e = 0) := by -/
+          /-       rw [← l_eq] at eq -/
+          /-       rw [List.all_append] at eq -/
+          /-       rw [Bool.and_eq_true] at eq -/
+          /-       exact eq.right -/
+          /-     simp [this] -/
+          /-     cases diff with -/
+          /-     | nil => simp at l_eq; rw [l_eq]; apply not_none -/
+          /-     | cons _ _ => -/
+          /-       let parent_len_fin : Fin l.length := ⟨parent.val.length, by simp [← l_eq]; apply Nat.lt_add_one_of_le; simp⟩ -/
+          /-       have := cb.branch.no_holes l.length not_none parent_len_fin -/
+          /-       exact this -/
+          no_holes_in_children := by sorry
+            /- intro l n -/
+            /- unfold InfiniteTreeSkeleton.children -/
+            /- cases n with -/
+            /- | succ n => -/
+            /-   have all_eq_false : ((n+1)::l).all (fun e => e = 0) = false := by rw [List.all_eq_false]; exists n+1; simp -/
+            /-   simp [all_eq_false] -/
+            /- | zero => -/
+            /-   intro _ m -/
+            /-   have isLt := m.isLt -/
+            /-   simp at isLt -/
+        }
+        finitely_many_children := by sorry
+          /- intro l -/
+          /- cases eq : cb.branch.infinite_list (l.length + 1) with -/
+          /- | none => -/
+          /-   exists 0 -/
+          /-   rw [PossiblyInfiniteTree.getElem_children_eq_get_tree] -/
+          /-   unfold PossiblyInfiniteTree.get -/
+          /-   cases eq2 : l.all (fun e => e = 0) with -/
+          /-   | false => simp [eq2, eq]; intro k; have isLt := k.isLt; simp at isLt -/
+          /-   | true => simp [eq2, eq]; intro k; have isLt := k.isLt; simp at isLt -/
+          /- | some _ => -/
+          /-   cases eq2 : l.all (fun e => e = 0) with -/
+          /-   | false => -/
+          /-     exists 0 -/
+          /-     rw [PossiblyInfiniteTree.getElem_children_eq_get_tree] -/
+          /-     unfold PossiblyInfiniteTree.get -/
+          /-     simp [eq2] -/
+          /-     intro k; have isLt := k.isLt; simp at isLt -/
+          /-   | true => -/
+          /-     exists 1 -/
+          /-     rw [PossiblyInfiniteTree.getElem_children_eq_get_tree] -/
+          /-     unfold PossiblyInfiniteTree.get -/
+          /-     simp -/
+          /-     rw [PossiblyInfiniteTree.getElem_children_eq_get_tree] -/
+          /-     unfold PossiblyInfiniteTree.get -/
+          /-     simp -/
+          /-     constructor -/
+          /-     . simp at eq2; apply eq2 -/
+          /-     . rw [eq]; simp -/
+      }
+      database_first := by sorry
+        /- simp only [FiniteDegreeTree.get, PossiblyInfiniteTree.get] -/
+        /- exact cb.database_first -/
+      triggers_exist := by
+        simp only [FiniteDegreeTree.get, PossiblyInfiniteTree.get]
+        intro l
+        cases eq : l.all (fun e => e = 0) with
+        | false => simp [Option.is_none_or]
+        | true =>
+          simp only [reduceIte]
+          have cb_trgs := cb.triggers_exist l.length
+          sorry
+      fairness_leaves := by sorry
+      fairness_infinite_branches := by sorry
+    }
+
+    exists ct
+    unfold ChaseBranch.result
+    unfold ChaseTree.firstResult
+    apply funext
+    intro f
+    rw [eq_iff_iff]
+    simp only [FiniteDegreeTree.get, PossiblyInfiniteTree.get]
+    constructor
+    . intro h
+      rcases h with ⟨n, h⟩
+      rw [List.all_eq_val_repeat 0, List.length_repeat] at h
+      simp at h
+      exists n
+    . intro h
+      rcases h with ⟨n, h⟩
+      exists n
+      rw [List.all_eq_val_repeat 0, List.length_repeat]
+      simp
+      exact h
+
+  rcases this with ⟨ct, eq⟩
+  rw [← eq]
+  apply deterministicChaseTreeResultUniversallyModelsKb
+  exact deterministic
+
diff --git a/ProofLibrary/List.lean b/ProofLibrary/List.lean
@@ -370,6 +370,8 @@ theorem List.length_repeat (val : α) : ∀ n, (List.repeat val n).length = n :=
   | zero => simp [List.repeat]
   | succ n ih => simp [List.repeat]; exact ih
 
+theorem List.all_eq_val_repeat [DecidableEq α] (val : α) : ∀ n, (List.repeat val n).all (fun e => e = val) = true := by sorry
+
 theorem List.repeat_split : ∀ (n k l : Nat), n = k + l -> List.repeat val n = List.repeat val k ++ List.repeat val l := by
   intro n k l h
   induction k generalizing n with