DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Prove that having a total join function is decidable

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-02-05 16:54:22 -08:00
parent 7382c632bc
commit 6b462f1a83
1 changed files with 13 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
Lattice/Builder.agda
View File

@@ -2,7 +2,7 @@ module Lattice.Builder where
open import Lattice open import Lattice
open import Equivalence 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)
open import Data.Nat as Nat using (ℕ) open import Data.Nat as Nat using (ℕ)
open import Data.Fin as Fin using (Fin; suc; zero; _≟_) 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 as Maybe using (Maybe; just; nothing; _>>=_; maybe)
@@ -13,7 +13,7 @@ open import Data.List.Membership.Propositional as MemProp using (lose) renaming
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.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 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.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.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr; filter) 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.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ; ++-identityʳ to ++ˡ-identityʳ; ++-assoc to ++ˡ-assoc)
@@ -410,6 +410,17 @@ record Graph : Set where
nlast = tabulate {xs = (preds n₁ n₂)} (λ {n'} n'∈preds → nlast' n' (proj₂ (∈ˡ-filter⁻ (Pred? n₁ n₂) {xs = proj₁ nodes} n'∈preds))) 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) in nopred (lose n∈preds nlast)
Total-⊔ : Set
Total-⊔ = ∀ n₁ n₂ → Have-⊔ n₁ n₂
Total-⊔? : Dec Total-⊔
Total-⊔?
with all? (λ (n₁ , n₂) → Have-⊔? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
... | yes all⊔ = yes λ n₁ n₂ →
let n₁n₂∈prod = ∈-cartesianProduct (nodes-complete n₁) (nodes-complete n₂)
in lookup all⊔ n₁n₂∈prod
... | no ¬all⊔ = no λ all⊔ → ¬all⊔ (universal (λ (n₁ , n₂) → all⊔ n₁ n₂) _)
module AssumeNoCycles (noCycles : NoCycles) where module AssumeNoCycles (noCycles : NoCycles) where
-- TODO: technically, the decidability of existing paths is separate -- TODO: technically, the decidability of existing paths is separate
-- from cycles. Because, for every non-simple path, we can construct -- from cycles. Because, for every non-simple path, we can construct