Add meet/join operation and some properties

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2026-02-12 20:16:02 -08:00
parent 05c55498ce
commit ccc3c7d5c7
2 changed files with 104 additions and 13 deletions
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -2,12 +2,11 @@ module Lattice.Builder where

 open import Lattice
 open import Equivalence
-open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬; ∈-cartesianProduct)
+open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬; ∈-cartesianProduct; foldr₁; x∷xs≢[])
 open import Data.Nat as Nat using (ℕ)
 open import Data.Fin as Fin using (Fin; suc; zero; _≟_)
 open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
 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⁺; ∈-filter⁻ to ∈ˡ-filter⁻; ∈-filter⁺ to ∈ˡ-filter⁺; ∈-lookup to ∈ˡ-lookup)
@@ -19,7 +18,7 @@ open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProduct
 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 Data.Empty using (⊥-elim)
 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)
@@ -34,11 +33,11 @@ record Graph : Set where
        size : ℕ

    Node : Set
-    Node = Fin size
+    Node = Fin (Nat.suc size)

-    nodes = fins size
+    nodes = fins (Nat.suc size)

-    nodes-complete = fins-complete size
+    nodes-complete = fins-complete (Nat.suc size)

    Edge : Set
    Edge = Node × Node
@@ -46,6 +45,9 @@ record Graph : Set where
    field
        edges : List Edge

+    nodes-nonempty : ¬ (proj₁ nodes ≡ [])
+    nodes-nonempty ()
+
    data Path : Node → Node → Set where
        done : ∀ {n : Node} → Path n n
        step : ∀ {n₁ n₂ n₃ : Node} →  (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
@@ -454,10 +456,90 @@ record Graph : Set where
    Total-⊓? : Dec Total-⊓
    Total-⊓? = P-Total? Have-⊓?

-    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.
+    module AssumeWellFormed (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
+        n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂
+        n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁
+            with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁)
+        ...   | done | done | _ = refl
+        ...   | step _ _ | done | _ = refl
+        ...   | done | step _ _ | _ = refl
+        ...   | step _ _ | step _ _ | ()
+
+        _⊔_ : Node → Node → Node
+        _⊔_ n₁ n₂ = proj₁ (total-⊔ n₁ n₂)
+
+        _⊓_ : Node → Node → Node
+        _⊓_ n₁ n₂ = proj₁ (total-⊓ n₁ n₂)
+
+        ⊤ : Node
+        ⊤ = foldr₁ nodes-nonempty _⊔_
+
+        ⊥ : Node
+        ⊥ = foldr₁ nodes-nonempty _⊓_
+
+        _≼_ : Node → Node → Set
+        _≼_ n₁ n₂ = n₁ ⊔ n₂ ≡ n₂
+
+        n₁≼n₂→PathExistsn₂n₁ : ∀ n₁ n₂ → (n₁ ≼ n₂) → PathExists n₂ n₁
+        n₁≼n₂→PathExistsn₂n₁ n₁ n₂ n₁⊔n₂≡n₂
+            with total-⊔ n₁ n₂ | n₁⊔n₂≡n₂
+        ...   | (_ , ((n₂→n₁ , _) , _)) | refl = n₂→n₁
+
+        PathExistsn₂n₁→n₁≼n₂ : ∀ n₁ n₂ → PathExists n₂ n₁ → (n₁ ≼ n₂)
+        PathExistsn₂n₁→n₁≼n₂ n₁ n₂ n₂→n₁
+            with total-⊔ n₁ n₂
+        ...   | (n , ((n→n₁ , n→n₂) , n'→n₁×n'→n₂⇒n'→n))
+                rewrite n₁→n₂×n₂→n₁⇒n₁≡n₂ n→n₂ (n'→n₁×n'→n₂⇒n'→n n₂ (n₂→n₁ , done)) = refl
+
+        foldr₁⊔-Pred : ∀ {ns : List Node} (ns≢[] : ¬ (ns ≡ [])) → let n = foldr₁ ns≢[] _⊔_ in All (PathExists n) ns
+        foldr₁⊔-Pred {ns = []} []≢[] = ⊥-elim ([]≢[] refl)
+        foldr₁⊔-Pred {ns = n₁ ∷ []} _ = done ∷ []
+        foldr₁⊔-Pred {ns = n₁ ∷ ns'@(n₂ ∷ ns'')} ns≢[] =
+            let
+                ns'≢[] = x∷xs≢[] n₂ ns''
+                n' = foldr₁ ns'≢[] _⊔_
+                (n , ((n→n₁ , n→n') , r)) = total-⊔ n₁ n'
+            in
+                n→n₁ ∷ map (n→n' ++_) (foldr₁⊔-Pred ns'≢[])
+
+        -- TODO: this is very similar structurally to foldr₁⊔-Pred
+        foldr₁⊓-Suc : ∀ {ns : List Node} (ns≢[] : ¬ (ns ≡ [])) → let n = foldr₁ ns≢[] _⊓_ in All (λ n' → PathExists n' n) ns
+        foldr₁⊓-Suc {ns = []} []≢[] = ⊥-elim ([]≢[] refl)
+        foldr₁⊓-Suc {ns = n₁ ∷ []} _ = done ∷ []
+        foldr₁⊓-Suc {ns = n₁ ∷ ns'@(n₂ ∷ ns'')} ns≢[] =
+            let
+                ns'≢[] = x∷xs≢[] n₂ ns''
+                n' = foldr₁ ns'≢[] _⊓_
+                (n , ((n₁→n , n'→n) , r)) = total-⊓ n₁ n'
+            in
+                n₁→n ∷ map (_++ n'→n) (foldr₁⊓-Suc ns'≢[])
+
+        ⊤-is-⊤ : Is-⊤ ⊤
+        ⊤-is-⊤ = foldr₁⊔-Pred nodes-nonempty
+
+        ⊥-is-⊥ : Is-⊥ ⊥
+        ⊥-is-⊥ = foldr₁⊓-Suc nodes-nonempty
+
+        ⊔-refl : ∀ n → n ⊔ n ≡ n
+        ⊔-refl n
+            with (n' , ((n'→n , _) , n''→n×n''→n⇒n''→n')) ← total-⊔ n n
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ n'→n (n''→n×n''→n⇒n''→n' n (done , done))
+
+        ⊓-refl : ∀ n → n ⊓ n ≡ n
+        ⊓-refl n
+            with (n' , ((n→n' , _) , n→n''×n→n''⇒n'→n'')) ← total-⊓ n n
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n→n''×n→n''⇒n'→n'' n (done , done)) n→n'
+
+        ⊔-comm : ∀ n₁ n₂ → n₁ ⊔ n₂ ≡ n₂ ⊔ n₁
+        ⊔-comm n₁ n₂
+            with (n₁₂ , ((n₁n₂→n₁ , n₁n₂→n₂) , n'→n₁×n'→n₂⇒n'→n₁₂)) ← total-⊔ n₁ n₂
+            with (n₂₁ , ((n₂n₁→n₂ , n₂n₁→n₁) , n'→n₂×n'→n₁⇒n'→n₂₁)) ← total-⊔ n₂ n₁
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n'→n₂×n'→n₁⇒n'→n₂₁ n₁₂ (n₁n₂→n₂ , n₁n₂→n₁))
+                                (n'→n₁×n'→n₂⇒n'→n₁₂ n₂₁ (n₂n₁→n₁ , n₂n₁→n₂))
+
+        ⊓-comm : ∀ n₁ n₂ → n₁ ⊓ n₂ ≡ n₂ ⊓ n₁
+        ⊓-comm n₁ n₂
+            with (n₁₂ , ((n₁→n₁n₂ , n₂→n₁n₂) , n₁→n'×n₂→n'⇒n₁₂→n')) ← total-⊓ n₁ n₂
+            with (n₂₁ , ((n₂→n₂n₁ , n₁→n₂n₁) , n₂→n'×n₁→n'⇒n₂₁→n')) ← total-⊓ n₂ n₁
+            = n₁→n₂×n₂→n₁⇒n₁≡n₂ (n₁→n'×n₂→n'⇒n₁₂→n' n₂₁ (n₁→n₂n₁ , n₂→n₂n₁))
+                                (n₂→n'×n₁→n'⇒n₂₁→n' n₁₂ (n₂→n₁n₂ , n₁→n₁n₂))
--- a/Utils.agda
+++ b/Utils.agda
@@ -2,6 +2,7 @@ module Utils where

 open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
 open import Data.Product as Prod using (Σ; _×_; _,_; proj₁; proj₂)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat using (ℕ; suc)
 open import Data.Fin as Fin using (Fin; suc; zero)
 open import Data.Fin.Properties using (suc-injective)
@@ -166,3 +167,11 @@ findUniversal-unique : ∀ {p c} {C : Set c} (R : C → C → Set p) (l : List C
                       ∀ x₁ x₂ → x₁ ∈ l → x₂ ∈ l → All (R x₁) l → All (R x₂) l →
                       x₁ ≡ x₂
 findUniversal-unique R l Rantisym x₁ x₂ x₁∈l x₂∈l Allx₁ Allx₂ = Rantisym (lookup Allx₁ x₂∈l) (lookup Allx₂ x₁∈l)
+
+x∷xs≢[] : ∀ {a} {A : Set a} (x : A) (xs : List A) → ¬ (x ∷ xs ≡ [])
+x∷xs≢[] x xs ()
+
+foldr₁ : ∀ {a} {A : Set a} {l : List A} → ¬ (l ≡ []) → (A → A → A) → A
+foldr₁ {l = x ∷ []} _ _ = x
+foldr₁ {l = x ∷ x' ∷ xs} _ f = f x (foldr₁ {l = x' ∷ xs} (x∷xs≢[] x' xs) f)
+foldr₁ {l = []} l≢[] _ = ⊥-elim (l≢[] refl)