From 299938d97e838c61df8ddaf16d55fc8b41d9bff0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 7 Dec 2025 22:25:47 -0800 Subject: [PATCH] Add decidability proofs for properties Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 77 ++++++++++++++++++++++++++++++++------------ Utils.agda | 4 +++ 2 files changed, 61 insertions(+), 20 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 9a8eda0..39ea18e 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -2,28 +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) +open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal; Decidable-¬) 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 () renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ) +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) +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.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate) +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.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; ¬?) 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 Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) record Graph : Set where @@ -51,6 +52,10 @@ record Graph : Set where data IsDone : ∀ {n₁ n₂} → Path n₁ n₂ → Set where isDone : ∀ {n : Node} → IsDone (done {n}) + IsDone? : ∀ {n₁ n₂} → Decidable (IsDone {n₁} {n₂}) + IsDone? done = yes isDone + IsDone? (step _ _) = no (λ {()}) + _++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃ done ++ p = p (step e p₁) ++ p₂ = step e (p₁ ++ p₂) @@ -204,7 +209,6 @@ record Graph : Set where toSimpleWalk : ∀ {n₁ n₂} (p : Path n₁ n₂) → SimpleWalkVia (proj₁ nodes) n₁ n₂ toSimpleWalk done = (done , (empty , [])) - toSimpleWalk (step n₁,n₂∈edges done) = (step n₁,n₂∈edges done , (empty , [])) toSimpleWalk (step {n₂ = nⁱ} n₁,nⁱ∈edges p') with toSimpleWalk p' ... | (done , _) = (step n₁,nⁱ∈edges done , (empty , [])) @@ -214,12 +218,30 @@ record Graph : Set where ... | yes nⁱ∈intp'' with splitFromInteriorʳ p'' nⁱ∈intp'' ... | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ⊥-elim (¬IsDone=p''ʳ isDone) - ... | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) - rewrite intp''≡ns++intp''ʳ - rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ)) = - let intp''ʳ⊆nodes = ++ˡ⁻ʳ (ns ++ˡ nⁱ ∷ []) intp''⊆nodes + ... | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = + -- no rewrites because then I can't reason about the return value of toSimpleWalk + -- rewrite intp''≡ns++intp''ʳ + -- rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ)) = + let reassoc-intp''≡ns++intp''ʳ = subst (interior p'' ≡_) (sym (++ˡ-assoc ns (nⁱ ∷ []) (interior p''ʳ))) intp''≡ns++intp''ʳ + intp''ʳ⊆nodes = ++ˡ⁻ʳ (ns ++ˡ nⁱ ∷ []) (subst (All (_∈ˡ (proj₁ nodes))) reassoc-intp''≡ns++intp''ʳ intp''⊆nodes) + Unique-ns++intp''ʳ = subst Unique reassoc-intp''≡ns++intp''ʳ Unique-intp'' nⁱ∈p''ˡ = ∈ˡ-++⁺ʳ ns {ys = nⁱ ∷ []} (here refl) - in (step n₁,nⁱ∈edges p''ʳ , (Unique-narrow (ns ++ˡ nⁱ ∷ []) Unique-intp'' nⁱ∈p''ˡ , nodes-complete nⁱ ∷ intp''ʳ⊆nodes )) + in (step n₁,nⁱ∈edges p''ʳ , (Unique-narrow (ns ++ˡ nⁱ ∷ []) Unique-ns++intp''ʳ nⁱ∈p''ˡ , nodes-complete nⁱ ∷ intp''ʳ⊆nodes )) + + toSimpleWalk-IsDone⁻ : ∀ {n₁ n₂} (p : Path n₁ n₂) → + ¬ IsDone p → ¬ IsDone (proj₁ (toSimpleWalk p)) + toSimpleWalk-IsDone⁻ done ¬IsDone-p _ = ¬IsDone-p isDone + toSimpleWalk-IsDone⁻ (step {n₂ = nⁱ} n₁,nⁱ∈edges p') _ isDone-w + with toSimpleWalk p' + ... | (done , _) with () ← isDone-w + ... | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes)) + with nⁱ ∈ˡ? interior p'' + ... | no nⁱ∉intp'' with () ← isDone-w + ... | yes nⁱ∈intp'' + with splitFromInteriorʳ p'' nⁱ∈intp'' + ... | (done , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) = ¬IsDone=p''ʳ isDone + ... | (p''ʳ@(step _ _) , (¬IsDone=p''ʳ , (ns , intp''≡ns++intp''ʳ))) + with () ← isDone-w Adjacency : Set Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂) @@ -306,15 +328,6 @@ record Graph : Set where adj : Adjacency adj = throughAll (proj₁ nodes) - NoCycles : Set - NoCycles = ∀ (n : Node) → All IsDone (adj n n) - - NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} → p ∈ˡ adj n₁ n₂ - NoCycles⇒adj-complete noCycles {n₁} {n₂} {p} - with findCycle p - ... | inj₁ (w , w≡p) rewrite sym w≡p = paths-throughAll (proj₁ nodes) w - ... | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (lookup (noCycles nᶜ) (paths-throughAll (proj₁ nodes) wᶜ))) - PathExists : Node → Node → Set PathExists n₁ n₂ = Path n₁ n₂ @@ -325,6 +338,30 @@ record Graph : Set where ... | [] = no (λ p → let w = toSimpleWalk p in ¬Any[] (allSimplePathsNoted w)) ... | (p ∷ ps) = yes p + NoCycles : Set + NoCycles = ∀ {n} (p : Path n n) → IsDone p + + NoCycles? : Dec NoCycles + NoCycles? with any? (λ n → any? (Decidable-¬ IsDone?) (adj n n)) (proj₁ nodes) + ... | yes existsCycle = + no (λ ∀p,IsDonep → let (n , n,n-cycle) = satisfied existsCycle in + let (p , ¬IsDone-p) = satisfied n,n-cycle in + ¬IsDone-p (∀p,IsDonep p)) + ... | no noCycles = + yes (λ { done → isDone + ; p@(step {n₁ = n} _ _) → + let w = toSimpleWalk p in + let ¬IsDone-w = toSimpleWalk-IsDone⁻ p (λ {()}) in + let w∈adj = paths-throughAll (proj₁ nodes) w in + ⊥-elim (noCycles (lose (nodes-complete n) (lose w∈adj ¬IsDone-w))) + }) + + NoCycles⇒adj-complete : NoCycles → ∀ {n₁ n₂} {p : Path n₁ n₂} → p ∈ˡ adj n₁ n₂ + NoCycles⇒adj-complete noCycles {n₁} {n₂} {p} + with findCycle p + ... | inj₁ (w , w≡p) rewrite sym w≡p = paths-throughAll (proj₁ nodes) w + ... | inj₂ (nᶜ , (wᶜ , wᶜ≢done)) = ⊥-elim (wᶜ≢done (noCycles (proj₁ wᶜ))) + Is-⊤ : Node → Set Is-⊤ n = All (PathExists n) (proj₁ nodes) diff --git a/Utils.agda b/Utils.agda index e8cde8e..49b8ec1 100644 --- a/Utils.agda +++ b/Utils.agda @@ -16,12 +16,16 @@ open import Function.Definitions using (Injective) open import Relation.Binary using (Antisymmetric) renaming (Decidable to Decidable²) open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl; cong) open import Relation.Nullary using (¬_; yes; no; Dec) +open import Relation.Nullary.Decidable using (¬?) open import Relation.Unary using (Decidable) All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs +Decidable-¬ : ∀ {p c} {C : Set c} {P : C → Set p} → Decidable P → Decidable (λ x → ¬ P x) +Decidable-¬ Decidable-P x = ¬? (Decidable-P x) + data Unique {c} {C : Set c} : List C → Set c where empty : Unique [] push : ∀ {x : C} {xs : List C}