From ccc3c7d5c7e82e8f3038ef3c3ca6f35af79b51a0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 12 Feb 2026 20:16:02 -0800 Subject: [PATCH] Add meet/join operation and some properties Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 108 +++++++++++++++++++++++++++++++++++++------ Utils.agda | 9 ++++ 2 files changed, 104 insertions(+), 13 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 330a53a..ff8e03b 100644 --- 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₂)) diff --git a/Utils.agda b/Utils.agda index 49b8ec1..5f8437e 100644 --- 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)