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

Extend proofs to meet as well as join

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

75
Lattice/Builder.agda
View File

@@ -384,42 +384,75 @@ record Graph : Set where
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₂
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)
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-⊔? : Dec Total-⊔
Total-⊔?
with all? (λ (n₁ , n₂) → Have-⊔? n₁ n₂) (cartesianProduct (proj₁ nodes) (proj₁ nodes))
... | yes all⊔ = yes λ 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 all⊔ n₁n₂∈prod
... | no ¬all⊔ = no λ all⊔ → ¬all⊔ (universal (λ (n₁ , n₂) → all⊔ n₁ 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 AssumeNoCycles (noCycles : NoCycles) where
-- TODO: technically, the decidability of existing paths is separate