From 7382c632bc59b91792a5bdabe33fa3aacc6aad69 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Thu, 5 Feb 2026 16:16:12 -0800
Subject: [PATCH] Add some proofs about predecessors

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 48 +++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 43 insertions(+), 5 deletions(-)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 3e0dd3c..7457f6f 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -10,21 +10,22 @@ open import Data.Maybe.Properties using (just-injective)
 open import Data.Unit using (⊤; tt)
 open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
 open import Data.List.Membership.Propositional as MemProp using (lose) renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ)
-open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺)
-open import Data.List.Relation.Unary.Any using (Any; here; there; any?; satisfied)
-open import Data.List.Relation.Unary.Any.Properties using (¬Any[])
+open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ; ∈-++⁺ˡ to ∈ˡ-++⁺ˡ; ∈-cartesianProductWith⁺ to ∈ˡ-cartesianProductWith⁺; ∈-filter⁻ to ∈ˡ-filter⁻; ∈-filter⁺ to ∈ˡ-filter⁺; ∈-lookup to ∈ˡ-lookup)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there; any?; satisfied; index)
+open import Data.List.Relation.Unary.Any.Properties using (¬Any[]; lookup-result)
 open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate; all?)
 open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
-open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
+open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr; filter) renaming (_++_ to _++ˡ_)
 open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂; uncurry)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Relation.Nullary using (¬_; Dec; yes; no; ¬?)
+open import Relation.Nullary using (¬_; Dec; yes; no; ¬?; _×-dec_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
 open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 open import Relation.Binary using () renaming (Decidable to Decidable²)
 open import Relation.Unary using (Decidable)
+open import Relation.Unary.Properties using (_∩?_)
 open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
 
 record Graph : Set where
@@ -379,3 +380,40 @@ record Graph : Set where
 
     Has-⊥? : Dec Has-⊥
     Has-⊥? = findUniversal (proj₁ nodes) (λ n₁ n₂ → PathExists? n₂ n₁)
+
+    Pred : Node → Node → Node → Set
+    Pred n₁ n₂ n = PathExists n n₁ × PathExists n n₂
+
+    Pred? : ∀ (n₁ n₂ : Node) → Decidable (Pred n₁ n₂)
+    Pred? n₁ n₂ n = PathExists? n n₁ ×-dec PathExists? n n₂
+
+    preds : Node → Node → List Node
+    preds n₁ n₂ = filter (Pred? n₁ n₂) (proj₁ nodes)
+
+    Have-⊔ : Node → Node → Set
+    Have-⊔ n₁ n₂ = Σ Node (λ n →  Pred n₁ n₂ n × (∀ n' →  Pred n₁ n₂ n' → PathExists n' n))
+
+    Have-⊔? : Decidable² Have-⊔
+    Have-⊔? n₁ n₂
+        with findUniversal (preds n₁ n₂) (λ n n' → PathExists? n' n) 
+    ...   | yes foundpred =
+            let idx = index foundpred
+                n = Any.lookup foundpred
+                n∈preds = ∈ˡ-lookup idx
+                (_ , n→n₁n₂) = ∈ˡ-filter⁻ (Pred? n₁ n₂) {xs = proj₁ nodes} n∈preds
+                nlast = lookup-result foundpred
+            in yes (n , (n→n₁n₂ , λ n' n'→n₁n₂ →
+                                    let n'∈preds = ∈ˡ-filter⁺ (Pred? n₁ n₂) (nodes-complete n') n'→n₁n₂
+                                    in lookup nlast n'∈preds))
+    ...   | no nopred = no λ (n , (n→n₁n₂ , nlast')) →
+                           let n∈preds = ∈ˡ-filter⁺ (Pred? n₁ n₂) (nodes-complete n) n→n₁n₂
+                               nlast = tabulate {xs = (preds n₁ n₂)} (λ {n'} n'∈preds →  nlast' n' (proj₂ (∈ˡ-filter⁻ (Pred? n₁ n₂) {xs = proj₁ nodes} n'∈preds)))
+                           in nopred (lose n∈preds nlast)
+
+    module AssumeNoCycles (noCycles : NoCycles) where
+        -- TODO: technically, the decidability of existing paths is separate
+        --       from cycles. Because, for every non-simple path, we can construct
+        --       a simple path by slicing out the repeat, and because the adjacency
+        --       graph has all simple paths. However, this requires additional
+        --       lemmas like splitFromInteriorʳ but for getting the _left_ hand
+        --       of a slice.