181 lines
11 KiB
Agda
181 lines
11 KiB
Agda
module Lattice.Builder where
|
||
|
||
open import Lattice
|
||
open import Equivalence
|
||
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; ¬Any-map; fins; fins-complete)
|
||
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.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.All using (All; []; _∷_; map; lookup)
|
||
open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to ++ˡ⁺)
|
||
open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_)
|
||
open import Data.List.Properties using () renaming (++-conicalʳ to ++ˡ-conicalʳ)
|
||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||
open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂)
|
||
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 Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
|
||
|
||
record Graph : Set where
|
||
constructor mkGraph
|
||
field
|
||
size : ℕ
|
||
|
||
Node : Set
|
||
Node = Fin size
|
||
|
||
nodes = fins size
|
||
|
||
nodes-complete = fins-complete size
|
||
|
||
Edge : Set
|
||
Edge = Node × Node
|
||
|
||
field
|
||
edges : List Edge
|
||
|
||
data Path : Node → Node → Set where
|
||
done : ∀ {n : Node} → Path n n
|
||
step : ∀ {n₁ n₂ n₃ : Node} → (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
|
||
|
||
_++_ : ∀ {n₁ n₂ n₃} → Path n₁ n₂ → Path n₂ n₃ → Path n₁ n₃
|
||
done ++ p = p
|
||
(step e p₁) ++ p₂ = step e (p₁ ++ p₂)
|
||
|
||
++done : ∀ {n₁ n₂} (p : Path n₁ n₂) → p ++ done ≡ p
|
||
++done done = refl
|
||
++done (step e∈edges p) rewrite ++done p = refl
|
||
|
||
interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
|
||
interior done = []
|
||
interior (step _ done) = []
|
||
interior (step {n₂ = n₂} _ p) = n₂ ∷ interior p
|
||
|
||
interior-extend : ∀ {n₁ n₂ n₃} → (p : Path n₁ n₂) → (n₂,n₃∈edges : (n₂ , n₃) ∈ˡ edges) →
|
||
let p' = (p ++ (step n₂,n₃∈edges done))
|
||
in (interior p' ≡ interior p) ⊎ (interior p' ≡ interior p ++ˡ (n₂ ∷ []))
|
||
interior-extend done _ = inj₁ refl
|
||
interior-extend (step n₁,n₂∈edges done) n₂n₃∈edges = inj₂ refl
|
||
interior-extend {n₂ = n₂} (step {n₂ = n} n₁,n∈edges p@(step _ _)) n₂n₃∈edges
|
||
with p ++ (step n₂n₃∈edges done) | interior-extend p n₂n₃∈edges
|
||
... | done | inj₁ []≡intp rewrite sym []≡intp = inj₁ refl
|
||
... | done | inj₂ []=intp++[n₂] with () ← ++ˡ-conicalʳ (interior p) (n₂ ∷ []) (sym []=intp++[n₂])
|
||
... | step _ p | inj₁ IH rewrite IH = inj₁ refl
|
||
... | step _ p | inj₂ IH rewrite IH = inj₂ refl
|
||
|
||
SimpleWalkVia : List Node → Node → Node → Set
|
||
SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (λ n → n ∈ˡ ns) (interior p))
|
||
|
||
SimpleWalk-extend : ∀ {n₁ n₂ n₃ ns} → (w : SimpleWalkVia ns n₁ n₂) → (n₂ , n₃) ∈ˡ edges → All (λ nʷ → ¬ nʷ ≡ n₂) (interior (proj₁ w)) → n₂ ∈ˡ ns → SimpleWalkVia ns n₁ n₃
|
||
SimpleWalk-extend (p , (Unique-intp , intp⊆ns)) n₂,n₃∈edges w≢n₂ n₂∈ns
|
||
with p ++ (step n₂,n₃∈edges done) | interior-extend p n₂,n₃∈edges
|
||
... | p' | inj₁ intp'≡intp rewrite sym intp'≡intp = (p' , Unique-intp , intp⊆ns)
|
||
... | p' | inj₂ intp'≡intp++[n₂]
|
||
with intp++[n₂]⊆ns ← ++ˡ⁺ intp⊆ns (n₂∈ns ∷ [])
|
||
rewrite sym intp'≡intp++[n₂] = (p' , (subst Unique (sym intp'≡intp++[n₂]) (Unique-append (¬Any-map sym (All¬-¬Any w≢n₂)) Unique-intp) , intp++[n₂]⊆ns))
|
||
|
||
postulate SplitSimpleWalkVia : ∀ {n n₁ n₂ ns} (w : SimpleWalkVia (n ∷ ns) n₁ n₂) → (Σ (SimpleWalkVia ns n₁ n × SimpleWalkVia ns n n₂) λ (w₁ , w₂) → proj₁ w₁ ++ proj₁ w₂ ≡ proj₁ w) ⊎ (Σ (SimpleWalkVia ns n₁ n₂) λ w' → proj₁ w' ≡ proj₁ w)
|
||
|
||
postulate findCycle : ∀ {n₁ n₂} (p : Path n₁ n₂) → (Σ (SimpleWalkVia (proj₁ nodes) n₁ n₂) λ w → proj₁ w ≡ p) ⊎ (Σ Node (λ n → Σ (SimpleWalkVia (proj₁ nodes) n n) λ w → ¬ proj₁ w ≡ done))
|
||
|
||
Adjacency : Set
|
||
Adjacency = ∀ (n₁ n₂ : Node) → List (Path n₁ n₂)
|
||
|
||
Adjacency-update : ∀ (n₁ n₂ : Node) → (List (Path n₁ n₂) → List (Path n₁ n₂)) → Adjacency → Adjacency
|
||
Adjacency-update n₁ n₂ f adj n₁' n₂'
|
||
with n₁ ≟ n₁' | n₂ ≟ n₂'
|
||
... | yes refl | yes refl = f (adj n₁ n₂)
|
||
... | _ | _ = adj n₁' n₂'
|
||
|
||
Adjecency-append : ∀ {n₁ n₂ : Node} → List (Path n₁ n₂) → Adjacency → Adjacency
|
||
Adjecency-append {n₁} {n₂} ps = Adjacency-update n₁ n₂ (ps ++ˡ_)
|
||
|
||
Adjacency-append-monotonic : ∀ {adj n₁ n₂ n₁' n₂'} {ps : List (Path n₁ n₂)} {p : Path n₁' n₂'} → p ∈ˡ adj n₁' n₂' → p ∈ˡ Adjecency-append ps adj n₁' n₂'
|
||
Adjacency-append-monotonic {adj} {n₁} {n₂} {n₁'} {n₂'} {ps} p∈adj
|
||
with n₁ ≟ n₁' | n₂ ≟ n₂'
|
||
... | yes refl | yes refl = ∈ˡ-++⁺ʳ ps p∈adj
|
||
... | yes refl | no _ = p∈adj
|
||
... | no _ | no _ = p∈adj
|
||
... | no _ | yes _ = p∈adj
|
||
|
||
adj⁰ : Adjacency
|
||
adj⁰ n₁ n₂
|
||
with n₁ ≟ n₂
|
||
... | yes refl = done ∷ []
|
||
... | no _ = []
|
||
|
||
adj⁰-done : ∀ n → done ∈ˡ adj⁰ n n
|
||
adj⁰-done n
|
||
with n ≟ n
|
||
... | yes refl = here refl
|
||
... | no n≢n = ⊥-elim (n≢n refl)
|
||
|
||
seedWithEdges : ∀ (es : List Edge) → (∀ {e} → e ∈ˡ es → e ∈ˡ edges) → Adjacency → Adjacency
|
||
seedWithEdges es e∈es⇒e∈edges adj = foldr (λ ((n₁ , n₂) , n₁n₂∈edges) → Adjacency-update n₁ n₂ ((step n₁n₂∈edges done) ∷_)) adj (mapWith∈ˡ es (λ {e} e∈es → (e , e∈es⇒e∈edges e∈es)))
|
||
|
||
seedWithEdges-monotonic : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ {p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
|
||
seedWithEdges-monotonic {es = []} e∈es⇒e∈edges p∈adj = p∈adj
|
||
seedWithEdges-monotonic {es = (n₁ , n₂) ∷ es} e∈es⇒e∈edges p∈adj = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (seedWithEdges-monotonic (λ e∈es → e∈es⇒e∈edges (there e∈es)) p∈adj)
|
||
|
||
e∈seedWithEdges : ∀ {n₁ n₂ es adj} → (e∈es⇒e∈edges : ∀ {e} → e ∈ˡ es → e ∈ˡ edges) → ∀ (n₁n₂∈es : (n₁ , n₂) ∈ˡ es) → (step (e∈es⇒e∈edges n₁n₂∈es) done) ∈ˡ seedWithEdges es e∈es⇒e∈edges adj n₁ n₂
|
||
e∈seedWithEdges {es = []} e∈es⇒e∈edges ()
|
||
e∈seedWithEdges {es = (n₁' , n₂') ∷ es} e∈es⇒e∈edges (here refl)
|
||
with n₁' ≟ n₁' | n₂' ≟ n₂'
|
||
... | yes refl | yes refl = here refl
|
||
... | no n₁'≢n₁' | _ = ⊥-elim (n₁'≢n₁' refl)
|
||
... | _ | no n₂'≢n₂' = ⊥-elim (n₂'≢n₂' refl)
|
||
e∈seedWithEdges {n₁} {n₂} {es = (n₁' , n₂') ∷ es} {adj} e∈es⇒e∈edges (there n₁n₂∈es) = Adjacency-append-monotonic {ps = step (e∈es⇒e∈edges (here refl)) done ∷ []} (e∈seedWithEdges (λ e∈es → e∈es⇒e∈edges (there e∈es)) n₁n₂∈es)
|
||
|
||
adj¹ : Adjacency
|
||
adj¹ = seedWithEdges edges (λ x → x) adj⁰
|
||
|
||
adj¹-adj⁰ : ∀ {n₁ n₂ p} → p ∈ˡ adj⁰ n₁ n₂ → p ∈ˡ adj¹ n₁ n₂
|
||
adj¹-adj⁰ p∈adj⁰ = seedWithEdges-monotonic (λ x → x) p∈adj⁰
|
||
|
||
edge∈adj¹ : ∀ {n₁ n₂} (n₁n₂∈edges : (n₁ , n₂) ∈ˡ edges) → (step n₁n₂∈edges done) ∈ˡ adj¹ n₁ n₂
|
||
edge∈adj¹ = e∈seedWithEdges (λ x → x)
|
||
|
||
through : Node → Adjacency → Adjacency
|
||
through n adj n₁ n₂ = cartesianProductWith _++_ (adj n₁ n) (adj n n₂) ++ˡ adj n₁ n₂
|
||
|
||
through-monotonic : ∀ adj n {n₁ n₂ p} → p ∈ˡ adj n₁ n₂ → p ∈ˡ (through n adj) n₁ n₂
|
||
through-monotonic adj n p∈adjn₁n₂ = ∈ˡ-++⁺ʳ _ p∈adjn₁n₂
|
||
|
||
through-++ : ∀ adj n {n₁ n₂} {p₁ : Path n₁ n} {p₂ : Path n n₂} → p₁ ∈ˡ adj n₁ n → p₂ ∈ˡ adj n n₂ → (p₁ ++ p₂) ∈ˡ through n adj n₁ n₂
|
||
through-++ adj n p₁∈adj p₂∈adj = ∈ˡ-++⁺ˡ (∈ˡ-cartesianProductWith⁺ _++_ p₁∈adj p₂∈adj)
|
||
|
||
throughAll : List Node → Adjacency
|
||
throughAll = foldr through adj¹
|
||
|
||
throughAll-adj₁ : ∀ {n₁ n₂ p} ns → p ∈ˡ adj¹ n₁ n₂ → p ∈ˡ throughAll ns n₁ n₂
|
||
throughAll-adj₁ [] p∈adj¹ = p∈adj¹
|
||
throughAll-adj₁ (n ∷ ns) p∈adj¹ = through-monotonic (throughAll ns) n (throughAll-adj₁ ns p∈adj¹)
|
||
|
||
paths-throughAll : ∀ {n₁ n₂ : Node} (ns : List Node) (w : SimpleWalkVia ns n₁ n₂) → proj₁ w ∈ˡ throughAll ns n₁ n₂
|
||
paths-throughAll {n₁} [] (done , (_ , _)) = adj¹-adj⁰ (adj⁰-done n₁)
|
||
paths-throughAll {n₁} [] (step e∈edges done , (_ , _)) = edge∈adj¹ e∈edges
|
||
paths-throughAll {n₁} [] (step _ (step _ _) , (_ , (() ∷ _)))
|
||
paths-throughAll (n ∷ ns) w
|
||
with SplitSimpleWalkVia w
|
||
... | inj₁ ((w₁ , w₂) , w₁++w₂≡w) rewrite sym w₁++w₂≡w = through-++ (throughAll ns) n (paths-throughAll ns w₁) (paths-throughAll ns w₂)
|
||
... | inj₂ (w' , w'≡w) rewrite sym w'≡w = through-monotonic (throughAll ns) n (paths-throughAll ns w')
|
||
|
||
adj : Adjacency
|
||
adj = throughAll (proj₁ nodes)
|
||
|
||
NoCycles : Set
|
||
NoCycles = ∀ (n : Node) → All (_≡ done) (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ᶜ)))
|