Add meet/join operation and some properties

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Lattice/Builder.agda

@@ -2,29 +2,29 @@ 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-¬)
+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⁺)
+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 using (Any; here; there; any?; satisfied)
+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[])
+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 using (All; []; _∷_; map; lookup; zipWith; tabulate; universal; 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 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
@@ -33,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
@@ -45,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₃
@@ -252,10 +255,10 @@ record Graph : Set where
     ...  | yes refl | yes refl = f (adj n₁ n₂)
     ...  | _        | _        = adj n₁' n₂'
 
-    Adjecency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
+    Adjacency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
-    Adjecency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_)
+    Adjacency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_)
 
-    Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjecency-append ps adj n₁' n₂'
+    Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjacency-append ps adj n₁' n₂'
     Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj
         with n₁ ≟ n₁' | n₂ ≟ n₂'
     ...   | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj
@@ -371,11 +374,172 @@ record Graph : Set where
     Has-⊤ : Set
     Has-⊤ = Any Is-⊤ (proj₁ nodes)
 
-    Has-T? : Dec Has-⊤
+    Has-⊤? : Dec Has-⊤
-    Has-T? = findUniversal (proj₁ nodes) PathExists?
+    Has-⊤? = findUniversal (proj₁ nodes) PathExists?
 
     Has-⊥ : Set
     Has-⊥ = Any Is-⊥ (proj₁ nodes)
 
     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₂
+
+    Succ : Node → Node → Node → Set
+    Succ 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₂
+
+    Suc? : ∀ (n₁ n₂ : Node) → Decidable (Succ n₁ n₂)
+    Suc? n₁ n₂ n = PathExists? n₁ n ×-dec PathExists? n₂ n
+
+    preds : Node → Node → List Node
+    preds n₁ n₂ = filter (Pred? n₁ n₂) (proj₁ nodes)
+
+    sucs : Node → Node → List Node
+    sucs n₁ n₂ = filter (Suc? 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-⊓ : Node → Node → Set
+    Have-⊓ n₁ n₂ = Σ Node (λ n →  Succ n₁ n₂ n × (∀ n' →  Succ n₁ n₂ n' → PathExists n n'))
+
+    -- when filtering nodes by a predicate P, then trying to find a universal
+    -- element according to another predicate Q, the universality can be
+    -- extended from "element of the filtered list for to which all other elements relate" to
+    -- "node satisfying P to which all other nodes satisfying P relate".
+    filter-nodes-universal : ∀ {P : Node → Set} (P? : Decidable P) -- e.g. Pred n₁ n₂
+                               {Q : Node → Node → Set} (Q? : Decidable² Q) -- e.g. PathExists? n' n
+                               → Dec (Σ Node λ n → P n × (∀ n' → P n' → Q n n'))
+    filter-nodes-universal {P = P} P? {Q = Q} Q?
+        with findUniversal (filter P? (proj₁ nodes)) Q?
+    ...   | yes founduni =
+            let idx = index founduni
+                n = Any.lookup founduni
+                n∈filter = ∈ˡ-lookup idx
+                (_ , Pn) = ∈ˡ-filter⁻ P? {xs = proj₁ nodes} n∈filter
+                nuni = lookup-result founduni
+            in yes (n , (Pn , λ n' Pn' →
+                                    let n'∈filter = ∈ˡ-filter⁺ P? (nodes-complete n') Pn'
+                                    in lookup nuni n'∈filter))
+    ...   | no nouni = no λ (n , (Pn , nuni')) →
+                           let n∈filter = ∈ˡ-filter⁺ P? (nodes-complete n) Pn
+                               nuni = tabulate {xs = filter P? (proj₁ nodes)} (λ {n'} n'∈filter →  nuni' n' (proj₂ (∈ˡ-filter⁻ P? {xs = proj₁ nodes} n'∈filter)))
+                           in nouni (lose n∈filter nuni)
+
+    Have-⊔? : Decidable² Have-⊔
+    Have-⊔? n₁ n₂ = filter-nodes-universal (Pred? n₁ n₂) (λ n₁ n₂ → PathExists? n₂ n₁)
+
+    Have-⊓? : Decidable² Have-⊓
+    Have-⊓? n₁ n₂ = filter-nodes-universal (Suc? n₁ n₂) PathExists?
+
+    Total-⊔ : Set
+    Total-⊔ = ∀ n₁ n₂ → Have-⊔ n₁ n₂
+
+    Total-⊓ : Set
+    Total-⊓ = ∀ n₁ n₂ → Have-⊓ n₁ n₂
+
+    P-Total? : ∀ {P : Node → Node → Set} (P? : Decidable² P) → Dec (∀ n₁ n₂ → P n₁ n₂)
+    P-Total? {P} P?
+        with all? (λ (n₁ , n₂) → P? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
+    ...   | yes allP = yes λ n₁ n₂ →
+            let n₁n₂∈prod = ∈-cartesianProduct (nodes-complete n₁) (nodes-complete n₂)
+            in lookup allP n₁n₂∈prod
+    ...   | no ¬allP = no λ allP → ¬allP (universal (λ (n₁ , n₂) → allP n₁ n₂) _)
+
+    Total-⊔? : Dec Total-⊔
+    Total-⊔? = P-Total? Have-⊔?
+
+    Total-⊓? : Dec Total-⊓
+    Total-⊓? = P-Total? Have-⊓?
+
+    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₂))

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)