Add decidability proofs for properties
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
927030c337
commit
299938d97e
@ -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)
|
||||
|
||||
|
||||
@ -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}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user