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

Add some proofs about predecessors

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

48
Lattice/Builder.agda
View File

@@ -10,21 +10,22 @@ 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.Relation.Unary.Any using (Any; here; there; any?; satisfied)
open import Data.List.Relation.Unary.Any.Properties using (¬Any[])
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.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.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 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
@@ -379,3 +380,40 @@ record Graph : Set where
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₂
Pred? : ∀ (n₁ n₂ : Node) → Decidable (Pred n₁ n₂)
Pred? n₁ n₂ n = PathExists? n n₁ ×-dec PathExists? n n₂
preds : Node → Node → List Node
preds n₁ n₂ = filter (Pred? 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-⊔? : 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)
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.