Prove walk splitting
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
d1700f23fa
commit
a277c8f969
@ -2,7 +2,7 @@ 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 Utils using (Unique; push; empty; Unique-append; Unique-++⁻ˡ; Unique-++⁻ʳ; 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)
|
||||
@ -12,12 +12,12 @@ 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.Relation.Unary.All using (All; []; _∷_; map; lookup; zipWith)
|
||||
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ʳ)
|
||||
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₂)
|
||||
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.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
|
||||
@ -45,13 +45,25 @@ record Graph : Set where
|
||||
done : ∀ {n : Node} → Path n n
|
||||
step : ∀ {n₁ n₂ n₃ : Node} → (n₁ , n₂) ∈ˡ edges → Path n₂ n₃ → Path n₁ n₃
|
||||
|
||||
data IsDone : ∀ {n₁ n₂} → Path n₁ n₂ → Set where
|
||||
isDone : ∀ {n : Node} → IsDone (done {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
|
||||
++-done : ∀ {n₁ n₂} (p : Path n₁ n₂) → p ++ done ≡ p
|
||||
++-done done = refl
|
||||
++-done (step e∈edges p) rewrite ++-done p = refl
|
||||
|
||||
++-assoc : ∀ {n₁ n₂ n₃ n₄} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) (p₃ : Path n₃ n₄) →
|
||||
(p₁ ++ p₂) ++ p₃ ≡ p₁ ++ (p₂ ++ p₃)
|
||||
++-assoc done p₂ p₃ = refl
|
||||
++-assoc (step n₁,n∈edges p₁) p₂ p₃ rewrite ++-assoc p₁ p₂ p₃ = refl
|
||||
|
||||
IsDone-++ˡ : ∀ {n₁ n₂ n₃} (p₁ : Path n₁ n₂) (p₂ : Path n₂ n₃) →
|
||||
¬ IsDone p₁ → ¬ IsDone (p₁ ++ p₂)
|
||||
IsDone-++ˡ done _ done≢done = ⊥-elim (done≢done isDone)
|
||||
|
||||
interior : ∀ {n₁ n₂} → Path n₁ n₂ → List Node
|
||||
interior done = []
|
||||
@ -70,8 +82,17 @@ record Graph : Set where
|
||||
... | step _ p | inj₁ IH rewrite IH = inj₁ refl
|
||||
... | step _ p | inj₂ IH rewrite IH = inj₂ refl
|
||||
|
||||
interior-++ : ∀ {n₁ n₂ n₃} → (p₁ : Path n₁ n₂) → (p₂ : Path n₂ n₃) →
|
||||
¬ IsDone p₁ → ¬ IsDone p₂ →
|
||||
interior (p₁ ++ p₂) ≡ interior p₁ ++ˡ (n₂ ∷ interior p₂)
|
||||
interior-++ done _ done≢done _ = ⊥-elim (done≢done isDone)
|
||||
interior-++ _ done _ done≢done = ⊥-elim (done≢done isDone)
|
||||
interior-++ (step _ done) (step _ _) _ _ = refl
|
||||
interior-++ (step n₁,n∈edges p@(step n,n'∈edges p')) p₂ _ p₂≢done
|
||||
rewrite interior-++ p p₂ (λ {()}) p₂≢done = refl
|
||||
|
||||
SimpleWalkVia : List Node → Node → Node → Set
|
||||
SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (λ n → n ∈ˡ ns) (interior p))
|
||||
SimpleWalkVia ns n₁ n₂ = Σ (Path n₁ n₂) (λ p → Unique (interior p) × All (_∈ˡ 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
|
||||
@ -81,7 +102,54 @@ record Graph : Set where
|
||||
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)
|
||||
∈ˡ-narrow : ∀ {x y : Node} {ys : List Node} → x ∈ˡ (y ∷ ys) → ¬ y ≡ x → x ∈ˡ ys
|
||||
∈ˡ-narrow (here refl) x≢y = ⊥-elim (x≢y refl)
|
||||
∈ˡ-narrow (there x∈ys) _ = x∈ys
|
||||
|
||||
SplitSimpleWalkViaHelp : ∀ {n n₁ n₂ ns} (nⁱ : Node)
|
||||
(w : SimpleWalkVia (n ∷ ns) n₁ n₂)
|
||||
(p₁ : Path n₁ nⁱ) (p₂ : Path nⁱ n₂) →
|
||||
¬ IsDone p₁ → ¬ IsDone p₂ →
|
||||
All (_∈ˡ ns) (interior p₁) →
|
||||
proj₁ w ≡ p₁ ++ p₂ →
|
||||
(Σ (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)
|
||||
SplitSimpleWalkViaHelp nⁱ w done _ done≢done _ _ _ = ⊥-elim (done≢done isDone)
|
||||
SplitSimpleWalkViaHelp nⁱ w p₁ done _ done≢done _ _ = ⊥-elim (done≢done isDone)
|
||||
SplitSimpleWalkViaHelp {n} {ns = ns} nⁱ w@(p , (Unique-intp , intp⊆ns)) p₁@(step _ _) p₂@(step {n₂ = nⁱ'} nⁱ,nⁱ',∈edges p₂') p₁≢done p₂≢done intp₁⊆ns p≡p₁++p₂
|
||||
with intp≡intp₁++[n]++intp₂ ← trans (cong interior p≡p₁++p₂) (interior-++ p₁ p₂ p₁≢done p₂≢done)
|
||||
with nⁱ∈n∷ns ∷ intp₂⊆n∷ns ← ++ˡ⁻ʳ (interior p₁) (subst (All (_∈ˡ (n ∷ ns))) intp≡intp₁++[n]++intp₂ intp⊆ns)
|
||||
with nⁱ ≟ n
|
||||
... | yes refl
|
||||
with Unique-intp₁ ← Unique-++⁻ˡ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
|
||||
with (push n≢intp₂ Unique-intp₂) ← Unique-++⁻ʳ (interior p₁) (subst Unique intp≡intp₁++[n]++intp₂ Unique-intp)
|
||||
= inj₁ (((p₁ , (Unique-intp₁ , intp₁⊆ns)) , (p₂ , (Unique-intp₂ , zipWith (uncurry ∈ˡ-narrow) (intp₂⊆n∷ns , n≢intp₂)))) , sym p≡p₁++p₂)
|
||||
... | no nⁱ≢n
|
||||
with p₂'
|
||||
... | done
|
||||
= let
|
||||
-- note: copied with below branch. can't use with <- to
|
||||
-- share and re-use because the termination checker loses the thread.
|
||||
p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
|
||||
n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
|
||||
intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
|
||||
intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
|
||||
intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
|
||||
-- end shared with below branch.
|
||||
Unique-intp₁++[nⁱ] = Unique-++⁻ˡ (interior p₁ ++ˡ (nⁱ ∷ [])) (subst Unique (trans intp≡intp₁++[n]++intp₂ (sym (++ˡ-assoc (interior p₁) (nⁱ ∷ []) []))) Unique-intp)
|
||||
in inj₂ ((p₁ ++ (step nⁱ,nⁱ',∈edges done) , (subst Unique (sym intp₁'=intp₁++[nⁱ]) Unique-intp₁++[nⁱ] , intp₁'⊆ns)) , sym p≡p₁++p₂)
|
||||
... | p₂'@(step _ _)
|
||||
= let p₁' = (p₁ ++ (step nⁱ,nⁱ',∈edges done))
|
||||
n≢nⁱ n≡nⁱ = nⁱ≢n (sym n≡nⁱ)
|
||||
intp₁'=intp₁++[nⁱ] = subst (λ xs → interior p₁' ≡ interior p₁ ++ˡ xs) (++ˡ-identityʳ (nⁱ ∷ [])) (interior-++ p₁ (step nⁱ,nⁱ',∈edges done) p₁≢done (λ {()}))
|
||||
intp₁++[nⁱ]⊆ns = ++ˡ⁺ intp₁⊆ns (∈ˡ-narrow nⁱ∈n∷ns n≢nⁱ ∷ [])
|
||||
intp₁'⊆ns = subst (All (_∈ˡ ns)) (sym intp₁'=intp₁++[nⁱ]) intp₁++[nⁱ]⊆ns
|
||||
p≡p₁'++p₂' = trans p≡p₁++p₂ (sym (++-assoc p₁ (step nⁱ,nⁱ',∈edges done) p₂'))
|
||||
in SplitSimpleWalkViaHelp nⁱ' w p₁' p₂' (IsDone-++ˡ _ _ p₁≢done) (λ {()}) intp₁'⊆ns p≡p₁'++p₂'
|
||||
|
||||
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)
|
||||
SplitSimpleWalkVia (done , (_ , _)) = inj₂ ((done , (empty , [])) , refl)
|
||||
SplitSimpleWalkVia (step n₁,n₂∈edges done , (_ , _)) = inj₂ ((step n₁,n₂∈edges done , (empty , [])) , refl)
|
||||
SplitSimpleWalkVia w@(step {n₂ = nⁱ} n₁,nⁱ∈edges p@(step _ _) , (push nⁱ≢intp Unique-intp , nⁱ∈ns ∷ intp⊆ns)) = SplitSimpleWalkViaHelp nⁱ w (step n₁,nⁱ∈edges done) p (λ {()}) (λ {()}) [] refl
|
||||
|
||||
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))
|
||||
|
||||
|
||||
@ -9,6 +9,7 @@ open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr; fil
|
||||
open import Data.List.Membership.Propositional using (_∈_)
|
||||
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
|
||||
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
|
||||
open import Data.List.Relation.Unary.All.Properties using (++⁻ˡ)
|
||||
open import Data.List.Relation.Unary.Any as Any using (Any; here; there) -- TODO: re-export these with nicer names from map
|
||||
open import Data.Sum using (_⊎_)
|
||||
open import Function.Definitions using (Injective)
|
||||
@ -36,6 +37,14 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
|
||||
help {[]} _ = x'≢x ∷ []
|
||||
help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es
|
||||
|
||||
Unique-++⁻ˡ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique xs
|
||||
Unique-++⁻ˡ [] Unique-ys = empty
|
||||
Unique-++⁻ˡ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = push (++⁻ˡ xs {ys = ys} x≢xs++ys) (Unique-++⁻ˡ xs Unique-xs++ys)
|
||||
|
||||
Unique-++⁻ʳ : ∀ {c} {C : Set c} (xs : List C) {ys : List C} → Unique (xs ++ ys) → Unique ys
|
||||
Unique-++⁻ʳ [] Unique-ys = Unique-ys
|
||||
Unique-++⁻ʳ (x ∷ xs) {ys} (push x≢xs++ys Unique-xs++ys) = Unique-++⁻ʳ xs Unique-xs++ys
|
||||
|
||||
All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
|
||||
Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
|
||||
All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user