Prove that having a top and bottom element is decidable
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
ef3c351bb0
commit
927030c337
@ -2,7 +2,7 @@ module Lattice.Builder where
|
||||
|
||||
open import Lattice
|
||||
open import Equivalence
|
||||
open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; All¬-¬Any; ¬Any-map; fins; fins-complete)
|
||||
open import Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; Unique-narrow; All¬-¬Any; ¬Any-map; fins; fins-complete; findUniversal)
|
||||
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)
|
||||
@ -12,6 +12,7 @@ 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.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.Properties using (¬Any[])
|
||||
open import Data.List.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith; tabulate)
|
||||
open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺; ++⁻ʳ to ++ˡ⁻ʳ)
|
||||
open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
|
||||
@ -22,6 +23,7 @@ open import Data.Empty using (⊥; ⊥-elim)
|
||||
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 Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||||
|
||||
record Graph : Set where
|
||||
@ -154,15 +156,26 @@ record Graph : Set where
|
||||
|
||||
open import Data.List.Membership.DecSetoid (decSetoid {A = Node} _≟_) using () renaming (_∈?_ to _∈ˡ?_)
|
||||
|
||||
splitFromInterior : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
|
||||
Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ interior p'))
|
||||
splitFromInterior done ()
|
||||
splitFromInterior (step _ done) ()
|
||||
splitFromInterior (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , (n' ∷ [] , refl)))
|
||||
splitFromInterior (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
|
||||
with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInterior p' n∈intp'
|
||||
rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
|
||||
splitFromInteriorʳ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
|
||||
Σ (Path n n₂) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ ns ++ˡ n ∷ interior p'))
|
||||
splitFromInteriorʳ done ()
|
||||
splitFromInteriorʳ (step _ done) ()
|
||||
splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (p' , ((λ {()}) , ([] , refl)))
|
||||
splitFromInteriorʳ (step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
|
||||
with (p'' , (¬IsDone-p'' , (ns , intp'≡ns++intp''))) ← splitFromInteriorʳ p' n∈intp'
|
||||
rewrite intp'≡ns++intp'' = (p'' , (¬IsDone-p'' , (n' ∷ ns , refl)))
|
||||
|
||||
splitFromInteriorˡ : ∀ {n₁ n₂ n} (p : Path n₁ n₂) → n ∈ˡ (interior p) →
|
||||
Σ (Path n₁ n) (λ p' → ¬ IsDone p' × (Σ (List Node) λ ns → interior p ≡ interior p' ++ˡ ns))
|
||||
splitFromInteriorˡ done ()
|
||||
splitFromInteriorˡ (step _ done) ()
|
||||
splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (here refl) = (step n₁,n'∈edges done , ((λ {()}) , (interior p , refl)))
|
||||
splitFromInteriorˡ p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) (there n∈intp')
|
||||
with splitFromInteriorˡ p' n∈intp'
|
||||
... | (p''@(step _ _) , (¬IsDone-p'' , (ns , intp'≡intp''++ns)))
|
||||
rewrite intp'≡intp''++ns
|
||||
= (step n₁,n'∈edges p'' , ((λ { () }) , (ns , refl)))
|
||||
... | (done , (¬IsDone-Done , _)) = ⊥-elim (¬IsDone-Done isDone)
|
||||
|
||||
findCycleHelp : ∀ {n₁ nⁱ n₂} (p : Path n₁ n₂) (p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
|
||||
¬ IsDone p₁ → Unique (interior p₁) →
|
||||
@ -176,17 +189,38 @@ record Graph : Set where
|
||||
intp₁'≡intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁ (λ {()}))
|
||||
¬IsDone-p₁' = IsDone-++ˡ p₁ (step nⁱ,nⁱ'∈edges done) ¬IsDone-p₁
|
||||
p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ'∈edges done) p₂'))
|
||||
in findCycleHelp p p₁' p₂' ¬IsDone-p₁' (subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)) p≡p₁'++p₂'
|
||||
Unique-intp₁' = subst Unique (sym intp₁'≡intp₁++[nⁱ]) (Unique-append nⁱ∉intp₁ Unique-intp₁)
|
||||
in findCycleHelp p p₁' p₂' ¬IsDone-p₁' Unique-intp₁' p≡p₁'++p₂'
|
||||
... | yes nⁱ∈intp₁
|
||||
with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInterior p₁ nⁱ∈intp₁ =
|
||||
with (pᶜ , (¬IsDone-pᶜ , (ns , intp₁≡ns++intpᶜ))) ← splitFromInteriorʳ p₁ nⁱ∈intp₁
|
||||
rewrite sym (++ˡ-assoc ns (nⁱ ∷ []) (interior pᶜ)) =
|
||||
let Unique-intp₁' = subst Unique intp₁≡ns++intpᶜ Unique-intp₁
|
||||
in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ ns Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
|
||||
in inj₂ (nⁱ , ((pᶜ , (Unique-++⁻ʳ (ns ++ˡ nⁱ ∷ []) Unique-intp₁' , tabulate (λ {x} _ → nodes-complete x))) , ¬IsDone-pᶜ))
|
||||
|
||||
findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) → (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w → ¬ IsDone (proj₁ w)))
|
||||
findCycle done = inj₁ ((done , (empty , [])) , refl)
|
||||
findCycle (step n₁,n₂∈edges done) = inj₁ ((step n₁,n₂∈edges done , (empty , [])) , refl)
|
||||
findCycle p@(step {n₂ = n'} n₁,n'∈edges p'@(step _ _)) = findCycleHelp p (step n₁,n'∈edges done) p' (λ {()}) empty refl
|
||||
|
||||
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 , []))
|
||||
... | (p''@(step _ _) , (Unique-intp'' , intp''⊆nodes))
|
||||
with nⁱ ∈ˡ? interior p''
|
||||
... | no nⁱ∉intp'' = (step n₁,nⁱ∈edges p'' , (push (tabulate (λ { n∈intp'' refl → nⁱ∉intp'' n∈intp'' })) Unique-intp'' , (nodes-complete nⁱ) ∷ intp''⊆nodes))
|
||||
... | 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
|
||||
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 ))
|
||||
|
||||
Adjacency : Set
|
||||
Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
|
||||
|
||||
@ -280,3 +314,31 @@ record Graph : Set where
|
||||
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₂
|
||||
|
||||
PathExists? : Decidable² PathExists
|
||||
PathExists? n₁ n₂
|
||||
with allSimplePathsNoted ← paths-throughAll {n₁ = n₁} {n₂ = n₂} (proj₁ nodes)
|
||||
with adj n₁ n₂
|
||||
... | [] = no (λ p → let w = toSimpleWalk p in ¬Any[] (allSimplePathsNoted w))
|
||||
... | (p ∷ ps) = yes p
|
||||
|
||||
Is-⊤ : Node → Set
|
||||
Is-⊤ n = All (PathExists n) (proj₁ nodes)
|
||||
|
||||
Is-⊥ : Node → Set
|
||||
Is-⊥ n = All (λ n' → PathExists n' n) (proj₁ nodes)
|
||||
|
||||
Has-⊤ : Set
|
||||
Has-⊤ = Any Is-⊤ (proj₁ nodes)
|
||||
|
||||
Has-T? : Dec Has-⊤
|
||||
Has-T? = findUniversal (proj₁ nodes) PathExists?
|
||||
|
||||
Has-⊥ : Set
|
||||
Has-⊥ = Any Is-⊥ (proj₁ nodes)
|
||||
|
||||
Has-⊥? : Dec Has-⊥
|
||||
Has-⊥? = findUniversal (proj₁ nodes) (λ n₁ n₂ → PathExists? n₂ n₁)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user