lib.graph-walks.Walk.QuasiSimple.md.
Version of Sunday, January 22, 2023, 10:42 PM
Powered by agda version 2.6.2.2-442c76b and pandoc 2.14.0.3
{-# OPTIONS --without-K --exact-split #-}
module lib.graph-walks.Walk.QuasiSimple
where
open import foundations.Core
open import lib.graph-definitions.Graph
open Graph
open import lib.graph-walks.Walk hiding (length)
open import lib.graph-walks.Walk.Composition
module
quasi-simple-walks
{ℓ : Level}{G : Graph ℓ }
where
open ∈-walk G
isQuasi : ∀ {x z : Node G} → Walk G x z → Type ℓ
isQuasi w = ∏[ y ∶ Node G ] (isProp (y ∈w w))
syntax isQuasi w = w is-quasi-simple
being-quasi-simple-is-prop
: ∀ {x y : Node G}
→ (w : Walk G x y)
→ isProp (w is-quasi-simple)
being-quasi-simple-is-prop w = pi-is-prop (λ w → prop-is-prop)
one-point-walk-is-quasi-simple
: ∀ (x : Node G)
→ (⟨ x ⟩ is-quasi-simple)
one-point-walk-is-quasi-simple x _ = ⊥-is-prop
module
WR {ℓ : Level}(G : Graph ℓ)
(_≟Node_ : (x y : Node G) → (x ≡ y) + (x ≠ y))
where
open quasi-simple-walks {ℓ = ℓ}{G}
one-edge-is-quasi-simple
: ∀ {x y} → (e : Edge G x y)
→ (e ⊙ ⟨ y ⟩) is-quasi-simple
one-edge-is-quasi-simple {x = x}{y} e r
= is-prop-A+B (Node-is-set G _ _) ⊥-is-prop (λ {(_ , empty) → empty})
open ∈-walk G
open ∙-walk G
_?∈_ : ∀ {x y} → (z : Node G) → (w : Walk G x y) → Dec ( z ∈w w)
z ?∈ ⟨ _ ⟩ = no id
_?∈_ {x = x} z (e ⊙ w)
with z ≟Node x
... | inl idp = yes (inl idp)
... | inr z≠x
with z ?∈ w
... | yes z∈w = yes (inr z∈w)
... | no w∌z = no λ { (inl z≡x) → z≠x z≡x
; (inr z∈w) → w∌z z∈w}
open import foundations.Nat ℓ
open dec-<
open import lib.graph-walks.Walk.Composition
-- Subwalk relation (subsequence of edges) -------------------------------
data
isSubwalk : ∀ {a b c d} → Walk G a b → Walk G c d → Type ℓ
where
⊂w-right
: ∀ {a b c}
→ (w : Walk G b c) → (p : Walk G a b)
-------------------------------------
→ isSubwalk w (p ·w w)
⊂w-left
: ∀ {a b c}
→ (p : Walk G a b) → (w : Walk G b c)
-------------------------------------
→ isSubwalk p (p ·w w)
⊂w-trans
: ∀ {a1 a2 b1 b2 c1 c2}
→ {p : Walk G a1 a2} {q : Walk G b1 b2} {r : Walk G c1 c2}
→ isSubwalk p q → isSubwalk q r
-------------------------------
→ isSubwalk p r
syntax isSubwalk p q = p ⊂w q
⊂w-refl : ∀ {x y }
→ (w : Walk G x y)
---------------------------
→ isSubwalk w w
⊂w-refl w = ⊂w-right w ⟨ _ ⟩
⊂w-⊙ : ∀ {a b c}
→ {e : Edge G a b}
→ {w : Walk G b c}
→ isSubwalk w (e ⊙ w)
⊂w-⊙ {b = b}{e = e} {⟨ _ ⟩} = ⊂w-right ⟨ b ⟩ (e ⊙ ⟨ b ⟩)
⊂w-⊙ {b = b}{e = e} {x ⊙ w} = ⊂w-right (x ⊙ w) (e ⊙ ⟨ b ⟩)
⊂w-⊙' : ∀ {a b c d z}
→ {w₁ : Walk G a b} {w₂ : Walk G c d}
→ isSubwalk w₁ w₂
→ {e : Edge G z c}
→ isSubwalk w₁ (e ⊙ w₂)
⊂w-⊙' pp = ⊂w-trans pp ⊂w-⊙
∈w-to-⊂w : ∀ {x y z}
→ {w : Walk G y z}
→ x ∈w w
---------------------------
→ isSubwalk ⟨ x ⟩ w
∈w-to-⊂w {w = e ⊙ w} (inl idp) = ⊂w-left ⟨ _ ⟩ (e ⊙ w)
∈w-to-⊂w {x} {w = e ⊙ w} (inr xinw) = ⊂w-⊙' (∈w-to-⊂w xinw)
cong-⊙-⊂w' : ∀ {x y z}
→ {e : Edge G x y} → {w : Walk G y z}
→ isSubwalk (e ⊙ ⟨ y ⟩) (e ⊙ w)
cong-⊙-⊂w' {e = e} {w} = ⊂w-left (e ⊙ ⟨ _ ⟩) w
-- Prefix relation -------------------------------------------------------
data
Prefix : ∀ {a b c} → Walk G a b → Walk G a c → Type ℓ
where
head
: ∀ {a b} → {w : Walk G a b}
----------------------------
→ Prefix ⟨ a ⟩ w
by-edge
: ∀ {a b c d}
→ {e : Edge G a b}
→ {w₁ : Walk G b c}
→ {w₂ : Walk G b d}
→ Prefix w₁ w₂
------------------------------
→ Prefix (e ⊙ w₁) (e ⊙ w₂)
find-suffix
: ∀ {a b c}
→ (w₁ : Walk G a b) (w : Walk G a c)
→ Prefix w₁ w
→ ∑[ w₂ ∶ Walk G b c ] (w ≡ (w₁ ·w w₂))
find-suffix ⟨ _ ⟩ w₂ _ = (w₂ , idp)
find-suffix (e ⊙ w₁) (e ⊙ w) (by-edge p₁) =
( w₂
, (begin
(e ⊙ w) ≡⟨ cong (e ⊙_) (proj₂ IH) ⟩
(e ⊙ (w₁ ·w w₂)) ≡⟨ ! ∙w-assoc _ w₁ w₂ ⟩
((e ⊙ w₁) ·w w₂) ∎))
where
IH : ∑[ w₂ ] (w ≡ (w₁ ·w w₂))
IH = find-suffix w₁ w p₁
w₂ = proj₁ IH
prefix-·w : ∀ {a b c d}
→ {w₁ : Walk G b c} {w₂ : Walk G b d}
→ Prefix w₁ w₂ → {p : Walk G a b}
------------------------------------
→ Prefix (p ·w w₁) (p ·w w₂)
prefix-·w {w₁ = w₁} {w₂} w₁<w₂ {⟨ _ ⟩} = w₁<w₂
prefix-·w {w₁ = w₁} {w₂} w₁<w₂ {x ⊙ p} = by-edge (prefix-·w w₁<w₂)
prefix-preserves-left-∙w : ∀ {a b c d}
→ {w₁ : Walk G b c} {w₂ : Walk G b d}
→ Prefix w₁ w₂ → {p : Walk G a b}
------------------------------------
→ Prefix (p ·w w₁) (p ·w w₂)
prefix-preserves-left-∙w {w₁ = ⟨ _ ⟩} {w₂} w₁<w₂ {⟨ _ ⟩} = head
prefix-preserves-left-∙w {w₁ = ⟨ _ ⟩} {w₂} head {x ⊙ p} =
by-edge (prefix-preserves-left-∙w head)
prefix-preserves-left-∙w {w₁ = x ⊙ w₁} {x ⊙ w₂} (by-edge w₁<w₂) {p}
= tr (λ p → Prefix p _) (change-prefix w₁)
(tr (λ p → Prefix ((newprefix ∙w w₁)) p) (change-prefix w₂) proof)
where
tx = (target G x)
newprefix = (p ·w (x ⊙ ⟨ tx ⟩ ))
change-prefix : ∀ {d} → (w : Walk G tx d)
→ (newprefix ∙w w) ≡ (p ·w (x ⊙ w))
change-prefix w = (∙w-assoc p ((x ⊙ ⟨ (target G x) ⟩ )) w)
proof : Prefix (newprefix ∙w w₁) (newprefix ∙w w₂)
proof = prefix-preserves-left-∙w w₁<w₂
left-part-⊂w : ∀ {a b c}
→ (p : Walk G a b) → {w : Walk G a c}
→ (∑[ q ∶ Walk G b c ] (w ≡ (p ·w q)))
--------------------------------------
→ isSubwalk p w
left-part-⊂w p {w} (q , o) rewrite o = ⊂w-left p q
right-part-⊂w : ∀ {a b c}
→ (q : Walk G b c)
→ {w : Walk G a c}
→ (∑[ p ∶ Walk G a b ] (w ≡ (p ·w q)))
--------------------------------------
→ isSubwalk q w
right-part-⊂w q {w} (p , o) rewrite o = ⊂w-right q p
∈-∙w-right
: ∀ {a b c p}
→ (w : Walk G b c) → (p ∈w w)
→ (q : Walk G a b)
-------------------
→ (p ∈w (q ·w w))
∈-∙w-right {a} (e ⊙ w) (inl idp) ⟨ .a ⟩ = inl idp
∈-∙w-right {a} (e ⊙ w) (inr x) ⟨ .a ⟩ = inr x
∈-∙w-right w'@(e ⊙ w) (inl idp) (e' ⊙ oo)
= inr (∈-∙w-right w' (inl idp) oo)
∈-∙w-right w'@(e ⊙ w) (inr p∈w) (e' ⊙ oo) =
inr (∈-∙w-right w' (∈-∙w-right w p∈w (e ⊙ ⟨ (target G e) ⟩)) oo)
∈-∙w-left
: ∀ {a b c p}
→ (w : Walk G a b)
→ (p ∈w w)
→ (q : Walk G b c)
-------------------
→ (p ∈w (w ·w q))
∈-∙w-left {b = b} (x ⊙ w) (inl idp) ⟨ .b ⟩ = inl idp
∈-∙w-left {a} (e ⊙ w) (inl idp) (x₁ ⊙ q) = inl idp
∈-∙w-left {b = b} (e ⊙ w) (inr p∈w) ⟨ .b ⟩ = inr ((∈-∙w-left w p∈w _))
∈-∙w-left {a} w'@(x ⊙ w) (inr p∈w) (x₂ ⊙ q) = inr (∈-∙w-left w p∈w _)
∈-⊙b
: ∀ {a b c p}
→ (w : Walk G a b)
→ (p ∈w w)
→ (e : Edge G b c)
-------------------
→ (p ∈w (w ⊙b e))
∈-⊙b (x ⊙ w) (inl idp) e = inl idp
∈-⊙b (x ⊙ w) (inr x∈w) e = inr (∈-⊙b w x∈w e)
⊂-smaller : ∀ {a b c d}
→ (w' : Walk G b c) (w : Walk G a d)
→ {e : Edge G a b} → isSubwalk (e ⊙ w') w
-----------------------------------------
→ isSubwalk w' w
⊂-smaller w' w {e} e⊙w'⊂w = ⊂w-trans ⊂w-⊙ e⊙w'⊂w
⊂w-to-∈
: ∀ {a b c d p}
→ (w₁ : Walk G a b) (w₂ : Walk G c d)
→ isSubwalk w₁ w₂ → (p ∈w w₁)
------------------------------------
→ (p ∈w w₂)
⊂w-to-∈ (e ⊙ w₁) _ (⊂w-right .(e ⊙ w₁) p₁) p = ∈-∙w-right (e ⊙ w₁) p p₁
⊂w-to-∈ (e ⊙ w₁) _ (⊂w-left .(e ⊙ w₁) w) p = ∈-∙w-left (e ⊙ w₁) p w
⊂w-to-∈ {p = p} (e ⊙ w₁) w₂ (⊂w-trans w₁<q q<w₂) p₁∈e⊙w₁
= ⊂w-to-∈ _ _ q<w₂ (⊂w-to-∈ (e ⊙ w₁) _ w₁<q p₁∈e⊙w₁)
prefix-is-subwalk
: ∀ {a b c}
→ (w₁ : Walk G a b) (w₂ : Walk G a c)
→ Prefix w₁ w₂
------------------------------------
→ isSubwalk w₁ w₂
prefix-is-subwalk ⟨ _ ⟩ w₂ p₁2 = ⊂w-left ⟨ _ ⟩ w₂
prefix-is-subwalk {b = b} (x ⊙ w₁) w₂ p
= left-part-⊂w (x ⊙ w₁) (proj₁ suffix , proj₂ suffix)
where
suffix : ∑[ rest ] (w₂ ≡ ((x ⊙ w₁) ·w rest))
suffix = find-suffix (x ⊙ w₁) w₂ p
-- Split walks by a given vertex -----------------------------------------
data SplitAt {x z : Node G} (w : Walk G x z) (y : Node G)
: Type ℓ
where
nothing : ¬ (y ∈w w) → SplitAt w y
just : (w₁ : Walk G x y)
→ Prefix w₁ w
→ ¬ (y ∈w w₁)
----------------
→ SplitAt w y
-- The following function splits a walk at some given point.
split_at_
: ∀ {x z : Node G}
→ (w : Walk G x z)
→ (y : Node G)
→ SplitAt w y
-- x-e-b-z
-- y
split ⟨ x ⟩ at y = nothing id
split (e ⊙ w) at y
with y ≟Node source G e
... | inl idp = just ⟨ y ⟩ head id
... | inr y≠x
with split w at y
... | nothing w∌y = nothing (λ {(inl y≡x) → ⊥-elim (y≠x y≡x)
; (inr y∈w) → ⊥-elim (w∌y y∈w)})
... | just w₁ p w₁∌y = just (e ⊙ w₁) (by-edge p)
λ { (inl y≡x) → y≠x y≡x
; (inr y∈w₁) → w₁∌y y∈w₁
}
-- Two handy lemmas on simple walks --------------------------------------
⊙-quasi-simple-is-quasi-simple
: ∀ {x y z : Node G}
→ {e : Edge G x y}
→ {w : Walk G y z}
→ w is-quasi-simple
→ ¬ (x ∈w w)
→ (e ⊙ w) is-quasi-simple
⊙-quasi-simple-is-quasi-simple {x}{e = e}{w} w-is-quasi-simple w∌x
r = is-prop-A+B (Node-is-set G _ _) (w-is-quasi-simple r) helper
where
helper : ∀ {r} → ¬ ((r ≡ x) × (r ∈w w))
helper {r} (idp , x∈w) = w∌x x∈w
?is-quasi-simple : ∀ {x y} → (w : Walk G x y) → Dec (w is-quasi-simple)
?is-quasi-simple {x = x} {.x} ⟨ .x ⟩ = yes (one-point-walk-is-quasi-simple x)
?is-quasi-simple {x = x} {y} (e ⊙ w)
with ?is-quasi-simple w
... | no ¬p = no λ {p → ¬p (λ x x∈1w x∈2w → inr-is-injective (p x (inr x∈1w) (inr x∈2w)))}
... | yes w-is-quasi-simple
with x ?∈ w
... | no w∌x = yes (⊙-quasi-simple-is-quasi-simple {e = e} w-is-quasi-simple w∌x)
... | yes x∈w = no (λ p → get-⊥ (x-in-different-pos p))
where
x-in-different-pos : ((e ⊙ w) is-quasi-simple) → inr x∈w ≡ inl idp
x-in-different-pos w-s = w-s x (inr x∈w) (inl idp)
get-⊥ : inr x∈w ≡ inl idp → ⊥ ℓ
get-⊥ ()
conservation
: ∀ {x y z : Node G}
→ (e : Edge G x y)(p : Walk G y z)
→ (e ⊙ p) is-quasi-simple
→ p is-quasi-simple
conservation {x = x}{y} e p ep-quasi-simple n
= λ m∈₁ m∈₂ → inr-is-injective (ep-quasi-simple n (inr m∈₁) (inr m∈₂))
¬⊂w⟨⟩
: ∀ {a b c} {w : Walk G b c} {e : Edge G a b}
→ ¬ ((e ⊙ w) ⊂w ⟨ a ⟩)
¬⊂w⟨⟩ {a} {e = e} e⊂w⟨a⟩ = a∈⟨a⟩
where
a∈⟨a⟩ : a ∈w ⟨ a ⟩
a∈⟨a⟩ = ⊂w-to-∈ (e ⊙ _) (⟨ a ⟩) e⊂w⟨a⟩ (inl idp)
private
variable
a b c d k k' k1 k2 : Node G
n : ℕ
-- Special cases on walks ------------------------------------------------
data
Loop : ∀ {x y} → Walk G x y → Type ℓ
where
is-loop : ∀ {x y} {w : Walk G x y} → x ≡ y → Loop w
data
NonTrivialLoop
: ∀ {x y} → Walk G x y → Type ℓ
where
is-loop : ∀ {x y z} {e : Edge G x y}
→ (x≡z : x ≡ z)
→ (w : Walk G y z)
→ NonTrivialLoop (e ⊙ w)
data
NonTrivial
: ∀ {x y} → Walk G x y → Type ℓ
where
has-edge : ∀ {x y z} {w : Walk G y z}
→ (e : Edge G x y)
→ NonTrivial (e ⊙ w)
is-concat
: ∀ {x y z : Node G}
→ (u : Walk G x y)
→ (nt : NonTrivial u)
→ {v : Walk G y z}
→ NonTrivial (u ∙w v)
is-concat (e ⊙ u) nt {v} = has-edge {w = u ∙w v} e
data NoReduce : ∀ {x y} → Walk G x y → Type ℓ where
is-dot : ∀ {x} → NoReduce ⟨ x ⟩
is-edge : ∀ {x y} {e : Edge G x y}
→ (≠ : x ≠ y)
→ NoReduce (e ⊙ ⟨ y ⟩)
data Trivial : ∀ {x y} → Walk G x y → Type ℓ
where
is-dot : ∀ {x y} {w : Walk G x y} → 0 ≡ length w → Trivial w
-- Two handy lemmas we need after ----------------------------------------
different-endpoints-is-nontrivial
: ∀ {x y} → (x ≠ y) → (w : Walk G x y) → NonTrivial w
different-endpoints-is-nontrivial x≠y ⟨ _ ⟩ = ⊥-elim (x≠y idp)
different-endpoints-is-nontrivial x≠y (e ⊙ w) = has-edge e
∈-non-trivial : ∀ {x y} → (w : Walk G x y) → NonTrivial w → x ∈w w
∈-non-trivial w (has-edge _) = inl idp
-- A relation for normalisation on walks ---------------------------------
-- One (harder to work with) alternative is to generalize the relation to
-- consider _→r_ between walks with different endpoints.
infix 4 _→r_
data
_→r_ : ∀ {a b : Node G}
→ Walk G a b → Walk G a b
→ Type ℓ
where
ξ₁
: (Ω : Walk G a b) (● : Walk G a b)
→ (is-loop : NonTrivialLoop Ω)
→ (to-dot : Trivial ●)
------------------------
→ Ω →r ●
ξ₂
: (e : Edge G a k) (p q : Walk G k c)
→ ¬ Loop (e ⊙ p)
→ a ≠ k
→ p →r q
--------------------
→ (e ⊙ p) →r (e ⊙ q)
ξ₃
: (e : Edge G a k) (p : Walk G k a) (q : Walk G a b)
→ (¬l : ¬ Loop ((e ⊙ p) ∙w q))
→ (l : Loop (e ⊙ p))
→ (nt : NonTrivial q)
→ (p' : Walk G a b)
→ (un : p' ≡ ((e ⊙ p) ∙w q))
---------------------------------------------
→ p' →r q
-- Point do not reduce.
trivial-walks-do-not-reduce
: ∀ {a x} (m : Edge G a x)(q : Walk G x a)
→ ⟨ a ⟩ →r (m ⊙ q)
→ ⊥ ℓ
trivial-walks-do-not-reduce m q (ξ₁ _ _ _ (is-dot ()))
-- Reduction reasoning ---------------------------------------------------
infix 1 begin→r*_
infixr 2 _→r⟨_⟩_
infixr 2 _→r*⟨_⟩_
infix 2 _→r*_
infix 3 _→r*∎
-- Reflexive and transitive closure for our →r relation on walks ---------
data
_→r*_ : ∀ {a b : Node G}
→ Walk G a b → Walk G a b
→ Type ℓ
where
_→r*∎
: ∀ (p : Walk G a b)
--------------------
→ p →r* p
_→r⟨_⟩_
: ∀ (p : Walk G a b) {q r : Walk G a b}
→ (p →r q) → (q →r* r)
--------------------
→ p →r* r
_→r*⟨_⟩_
: ∀ (p : Walk G a b) {q r : Walk G a b}
→ p →r* q
→ q →r* r
---------
→ p →r* r
_→r*⟨_⟩_ p {.p} (.p →r*∎) qr = qr
_→r*⟨_⟩_ p {q} (.p →r⟨ x ⟩ pq) qr = p →r⟨ x ⟩ (_ →r*⟨ pq ⟩ qr)
one-step
: ∀ {p q : Walk G a b}
→ p →r q
→ p →r* q
one-step {p = p}{q} pq = p →r⟨ pq ⟩ q →r*∎
begin→r*_
: ∀ {M N : Walk G a b}
→ M →r* N
------
→ M →r* N
begin→r* M→r*N = M→r*N
-- Some handy functions to recover walks from the reductions --------------
subs
: ∀ {p q : Walk G a b}
→ p ≡ q → p →r* q
subs {p = p} idp = p →r*∎
get-original-walk
: {p q : Walk G a b}
→ p →r* q
→ Walk G a b
get-original-walk {p = p} _ = p
get-reduced-walk
: {p q : Walk G a b}
→ p →r* q
→ Walk G a b
get-reduced-walk {q = q} _ = q
-- Essential lemmas ------------------------------------------------------
nf-∈
: {x : Node G}
→ (q : Walk G a c) → x ∈w q
→ (p : Walk G a c) → p →r q
------------------------------
→ x ∈w p
nf-∈ (e ⊙ q') (inl idp) ⟨ _ ⟩ (ξ₁ _ _ () _)
nf-∈ (e ⊙ q') (inl idp) (x ⊙ p) pq = inl idp
nf-∈ {x = x} (e ⊙ q') (inr x∈q') p pq
with split q' at x
... | nothing x₁ = ⊥-elim (x₁ x∈q')
... | just w₁ w₁-is-prefix-of-q' w₁∌x
with pq
... | ξ₁ _ _ _ (is-dot ())
... | ξ₂ _ q _ _ _ q→q' = inr x∈q
where
x∈q : x ∈w q
x∈q = nf-∈ _ x∈q' _ q→q'
... | ξ₃ e₁ p₁ .(e ⊙ q') l l₁ nt .(e₁ ⊙ (G ∙-walk.·w p₁) (e ⊙ q')) idp
= inr ((∈-∙w-right ((e ⊙ q')) x∈e⊙q' _))
where
x∈e⊙q' : x ∈w (e ⊙ q')
x∈e⊙q' = ∈-∙w-right q' x∈q' (e ⊙ _)
nf-∈'
: {x : Node G}
→ (q : Walk G a c) → x ∈w q
→ (p : Walk G a c) → p →r* q
-----------------------------
→ x ∈w p
nf-∈' {x = x} q x∈q .q (.q →r*∎) = x∈q
nf-∈' {x = x} q x∈q p (.p →r⟨ x₁ ⟩ pq) = nf-∈ q₁ x∈q₁ p x₁
where
q₁ = get-original-walk pq
x∈q₁ : x ∈w q₁
x∈q₁ = nf-∈' {x = x} q x∈q q₁ pq
-- contrapositive
nf-¬∈
: {x : Node G}
→ (p : Walk G a c) → ¬ (x ∈w p)
→ (q : Walk G a c) → p →r* q
------------------------------
→ ¬ (x ∈w q)
nf-¬∈ p ¬x∈p q p→q = contrapositive (nf-∈' q) (λ o → ¬x∈p (o p p→q))
-- Length evolution through the reductions -------------------------------
length-lem→r
: (p q : Walk G a b)
→ p →r q
-----------------------------------------------
→ (length q < length p)
length-lem→r ⟨ _ ⟩ q (ξ₁ .(⟨ _ ⟩) .q () to-dot)
length-lem→r ⟨ _ ⟩ q (ξ₃ e p .q ¬l (is-loop x) nt .(⟨ _ ⟩) un) = ⊥-elim (¬l (is-loop idp))
length-lem→r (x ⊙ p) q (ξ₁ .(x ⊙ p) .q is-loop₁ (is-dot x₁)) = tr (λ o → o < length (x ⊙ p)) x₁ ∗
length-lem→r (x ⊙ p) .(x ⊙ r) (ξ₂ .x .p r nl x₁ pq) = length-lem→r _ _ pq
length-lem→r (x ⊙ .((G ∙-walk.·w p₁) q)) q (ξ₃ .x p₁ .q ¬l l nt .(x ⊙ (G ∙-walk.·w p₁) q) idp)
= right-part<whole _ p₁ q idp
-- More handy lemmas to shorten the coming proofs ------------------------
ξ₂-⊙
: ∀ {q r : Walk G b c} {a≠b : a ≠ b}{a≠c : a ≠ c}
→ q →r* r → (e : Edge G a b)
------------------------------
→ (e ⊙ q) →r* (e ⊙ r)
ξ₂-⊙ {q = ⟨ _ ⟩} {.(⟨ _ ⟩)} (.(⟨ _ ⟩) →r*∎) e = (e ⊙ ⟨ _ ⟩) →r*∎
ξ₂-⊙ {q = ⟨ _ ⟩} {r}{a≠b}{a≠c} (.(⟨ _ ⟩) →r⟨ x ⟩ qr) e
= (e ⊙ ⟨ _ ⟩) →r⟨ ξ₂ _ _ _ (λ { (is-loop x) → a≠c x}) a≠c x ⟩ ξ₂-⊙ {a≠b = a≠b}{a≠c} qr e
ξ₂-⊙ {q = x ⊙ q} {.(x ⊙ q)} (.(x ⊙ q) →r*∎) e = (e ⊙ (x ⊙ q)) →r*∎
ξ₂-⊙ {q = x ⊙ q} {r}{a≠b}{a≠c} (.(x ⊙ q) →r⟨ x₁ ⟩ qr) e
= (e ⊙ (x ⊙ q)) →r⟨ ξ₂ _ _ _ (λ { (is-loop x) → a≠c x}) a≠b x₁ ⟩ ξ₂-⊙ {a≠b = a≠b}{a≠c} qr e
-- Normal form on walks under the →r relation ----------------------------
data Reduce {x y} (p : Walk G x y) : Type ℓ
where
reduction
: {q : Walk G x y}
→ p →r q
--------
→ Reduce p
data Normal {x y}(p : Walk G x y) : Type ℓ
where
normal
: p is-quasi-simple
→ ¬ Reduce p
→ Normal p
normal-is-quasi-simple : ∀ {x y}{w : Walk G x y} → Normal w → w is-quasi-simple
normal-is-quasi-simple (normal w-is-quasi-simple _) = w-is-quasi-simple
Normal-is-prop : ∀ {x y} {w : Walk G x y} → isProp (Normal w)
Normal-is-prop {w = w} (normal w-s1 ¬r1) (normal w-s2 ¬r2)
= ap² normal (being-quasi-simple-is-prop _ w-s1 w-s2)
(pi-is-prop (λ _ → ⊥-is-prop) ¬r1 ¬r2)
{- A simple walk can be a loop but without inner loops. We have
some examples:
- a dot, and edge, or even edge forming a loop.
- also, a walk with a loop attached at the end.
Simple walks are not the normal forms. One further reduction
step is necessary to get their normal form. In other words,
normal forms on walks are simple walks with no more
reductions.
-}
-- Progress property of the →r relation.
-- A walk reduces or it is in its normal form.
data Progress {x y} (p : Walk G x y) : Type ℓ
where
step : Reduce p → Progress p
done : Normal p → Progress p
-- Dots and nonloop edges do not reduce.
No-reduce-no-step : (p : Walk G a b) → NoReduce p → ¬ Reduce p
No-reduce-no-step ⟨ _ ⟩ is-dot (reduction (ξ₁ .(⟨ _ ⟩) _ () to-dot))
No-reduce-no-step ⟨ _ ⟩ is-dot (reduction (ξ₃ e p _ ¬l l nt .(⟨ _ ⟩) un)) = ⊥-elim (¬l (is-loop idp))
No-reduce-no-step (x ⊙ .(⟨ _ ⟩)) (is-edge ≠) (reduction (ξ₁ .(x ⊙ ⟨ _ ⟩) _ (is-loop x≡z .(⟨ _ ⟩)) to-dot)) = ⊥-elim (≠ x≡z)
No-reduce-no-step (x ⊙ .(⟨ _ ⟩)) (is-edge ≠) (reduction (ξ₂ .x .(⟨ _ ⟩) r nl x₁ (ξ₁ .(⟨ _ ⟩) .r () to-dot)))
No-reduce-no-step (x ⊙ .(⟨ _ ⟩)) (is-edge ≠) (reduction (ξ₂ .x .(⟨ _ ⟩) r nl x₁ (ξ₃ e p .r ¬l l nt .(⟨ _ ⟩) ())))
No-reduce-no-step (x ⊙ .(⟨ _ ⟩)) (is-edge ≠) (reduction (ξ₃ .x ⟨ _ ⟩ _ ¬l l nt .(x ⊙ ⟨ _ ⟩) idp)) = ⊥-elim (≠ idp)
-- Dots and nonloop edges are simple walks.
No-reduce-is-quasi-simple : (p : Walk G a b) → NoReduce p → p is-quasi-simple
No-reduce-is-quasi-simple ⟨ x ⟩ nored = one-point-walk-is-quasi-simple x
No-reduce-is-quasi-simple (e ⊙ ⟨ x ⟩) (is-edge ≠) = ⊙-quasi-simple-is-quasi-simple {e = e} (one-point-walk-is-quasi-simple x) (λ z → z)
-- Dots and nonloop edges are in their normal form.
No-reduce-is-normal : (p : Walk G a b) → NoReduce p → Normal p
No-reduce-is-normal p nored = normal (No-reduce-is-quasi-simple p nored) (No-reduce-no-step p nored)
-- To prove normalisation on walks, we need to establish a
-- well-foundedness relation on walks to prove termination of
-- our algorithm.
module WF {ℓ₁}{ℓ₂} (A : Type ℓ₁)
(_<'_ : A → A → Type ℓ₂)
where
-- Accesible data type.
data
Acc
(n : A)
: Type (ℓ₁ ⊔ ℓ₂)
where
acc
: (∀ m → m <' n → Acc m) -- Strong induction.
→ Acc n
-- Well-founded types: those where all its elements are "accesible".
Well-founded : Type (ℓ₁ ⊔ ℓ₂)
Well-founded = ∀ n → Acc n
-- We show now the well-foundness on natural numbers related with less than
-- relation ("<"). We do this because, the length of our walks is a natural number.
-- We will relate walks by their length.
-- The main complication in the proof above arises from the non-inductive definition
-- of this relation. It's straightforward if one uses an inductive def.
module _ where
open WF ℕ _<_
nat-wf : Well-founded
nat-wf zero = WF.acc λ m p → ⊥-elim (n<0 {ℓ} {n = m} p)
nat-wf (succ n) = WF.acc (go n)
where
accn : Acc n
accn = nat-wf n
go : ∀ n m → m < succ n → Acc m
go zero zero ∗ = nat-wf 0
go zero (succ m) p = tr Acc (! sm≡0) (nat-wf 0)
where
sm≡0 = k<1→k≡0 {k = succ m} p
go (succ n) zero ∗ = nat-wf 0
go (succ n) (succ m) m<sn = WF.acc helper
where
helper : (m₁ : ℕ) → m₁ < succ m → Acc m₁
helper m₁ m₁<sm
with <s-to-<= m₁ m m₁<sm
... | inl idp = go n m₁ m<sn
... | inr m₁<m = go n m₁ (<-trans {x = m₁} m₁<m m<sn)
-- We need a well-founded relation on walks which is the following.
_⊰_ : (∑[ x ] ∑[ y ] Walk G x y) → (∑[ x ] ∑[ y ] Walk G x y) → Type ℓ
(_ , _ , p) ⊰ (_ , (_ , q)) = length p < length q
-- For technical reasons, we pack the endpoints of each walk
∑∑walk : ∀ {x y} → (w : Walk G x y) → ∑[ x ] ∑[ y ] Walk G x y
∑∑walk {x = x}{y} w = (x , y , w)
-- Inverse-image shows WF.
ii-acc'
: ∀ {x y} {w : Walk G x y}
→ WF.Acc ℕ _<_ (length w)
→ WF.Acc (∑[ x ] ∑[ y ] Walk G x y) _⊰_ (x , y , w)
ii-acc' (acc g) = WF.acc (λ {(_ , _ , a) a<w → ii-acc' (g (length a) a<w)})
-- Well-foundedness on walks
∑∑walk-wf : WF.Well-founded (∑[ x ] ∑[ y ] Walk G x y) _⊰_
∑∑walk-wf (_ , _ , a) = ii-acc' (nat-wf (length a))
-- Recursion principle on walks ------------------------------------------
-- Fold.
fold-acc
: ∀ {ℓ₂ : Level}(P : ∀ {x y} → Walk G x y → Type ℓ₂)
→ (∀ {x y} → (b : Walk G x y) → (∀ {x' y'} → (a : Walk G x' y') → ∑∑walk a ⊰ ∑∑walk b → P a) → P b)
------------------------------------------------------------------------------------
→ ∀ {x y} → (w : Walk G x y) → WF.Acc (∑[ x ] ∑[ y ] Walk G x y) _⊰_ (∑∑walk w) → P w
fold-acc P φ w (WF.acc g) = φ w (λ a a<w → fold-acc P φ a (g (∑∑walk a) a<w))
-- Rec.
∑∑walk-rec : {ℓ₂ : Level}(P : ∀ {x y} → Walk G x y → Type ℓ₂)
→ (∀ {x y} → (b : Walk G x y) → (∀ {x' y'} → (a : Walk G x' y') → ∑∑walk a ⊰ ∑∑walk b → P a) → P b)
-----------------------------------------------------------------------------------------------
→ ∀ {x y} → (w : Walk G x y) → P w
∑∑walk-rec P = rec ∑∑walk-wf
where
rec
: WF.Well-founded (∑[ x ] ∑[ y ] Walk G x y) _⊰_
→ (∀ {x y} → (b : Walk G x y) → (∀ {x' y'} → (a : Walk G x' y') → ∑∑walk a ⊰ ∑∑walk b → P a) → P b)
-----------------------------------------------------------------------------------------------
→ ∀ {x y} → (w : Walk G x y) → P w
rec wf φ w = fold-acc P φ w (wf (∑∑walk w))
-- Normalization on walks ------------------------------------------------
module _ where
P : ∀ {x z : Node G}
→ Walk G x z
→ Type ℓ
P {x = x}{z} = λ w → ∑[ v ∶ Walk G x z ] (w →r* v) × Normal v
normalize : ∀ {x z} → (w : Walk G x z) → P w
normalize = ∑∑walk-rec P body
where
body
: ∀ {x z : Node G} (b : Walk G x z)
→ ({x' z' : Node G} (a : Walk G x' z') → ∑∑walk a ⊰ ∑∑walk b → P a) → P b
body ⟨ x ⟩ φ = ⟨ x ⟩ , (⟨ _ ⟩ →r*∎) , (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
body {x = x}{z} (e ⊙ ⟨ _ ⟩) φ
with x ≟Node z
... | inl idp = ⟨ x ⟩
, one-step (ξ₁ _ _ (is-loop idp ⟨ x ⟩) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
... | inr x≠z = (e ⊙ ⟨ _ ⟩)
, ((e ⊙ ⟨ z ⟩) →r*∎)
, (normal (⊙-quasi-simple-is-quasi-simple {e = e} (one-point-walk-is-quasi-simple x) id)
(No-reduce-no-step _ (is-edge x≠z)))
body {x = x}{z} (e ⊙ w@(_ ⊙ _)) φ
with x ≟Node z
... | inl idp
= ⟨ x ⟩ , one-step (ξ₁ _ _ (is-loop idp _) (is-dot idp))
, (normal (one-point-walk-is-quasi-simple x) (No-reduce-no-step ⟨ x ⟩ is-dot))
... | inr x≠z
with x ≟Node (start-of G w)
... | inl idp = helper
where
helper : P (e ⊙ w)
helper with φ w (<-succ (length w))
... | (w' , w→w' , (normal w'-is-quasi-simple no-red))
= w'
, (begin→r*
e ⊙ w →r*⟨ (e ⊙ w) →r*∎ ⟩
(e ⊙ ⟨ x ⟩) ∙w w →r*⟨ one-step (ξ₃ _ ⟨ _ ⟩ _ (λ { (is-loop x) → x≠z x})
(is-loop idp) (has-edge _) _ idp ) ⟩
w →r*⟨ w→w' ⟩
w' →r*∎)
, (normal w'-is-quasi-simple no-red)
... | inr x≠y
with split w at x
... | just w₁ w₁prefix w₁∌x = helper
where
helper : _
helper with find-suffix w₁ w w₁prefix
... | (w₂ , w≡w₁∙w₂) = helper2
where
helper2 : P (e ⊙ w)
helper2 with φ w₂ (right-part<whole w w₁ w₂ w≡w₁∙w₂)
... | (w' , w₂→w' , (normal w'-is-quasi-simple no-red))
= w'
, (begin→r*
e ⊙ w →r*⟨ ξ₂-⊙ {a≠b = x≠y}{x≠z}(subs w≡w₁∙w₂) e ⟩
(e ⊙ w₁) ·w w₂ →r*⟨ one-step (ξ₃ _ _ _ (λ { (is-loop x) → x≠z x}) (is-loop idp)
(different-endpoints-is-nontrivial x≠z w₂) _ idp) ⟩
w₂ →r*⟨ w₂→w' ⟩
w' →r*∎)
, (normal w'-is-quasi-simple no-red)
... | nothing w∌x
with φ w (<-succ (length w))
... | ⟨ _ ⟩ , w→z , (normal pp no-red)
= (e ⊙ ⟨ z ⟩)
, ξ₂-⊙ {a≠b = x≠z}{x≠z} w→z e
, (normal ((⊙-quasi-simple-is-quasi-simple {e = e} (one-point-walk-is-quasi-simple x) id))
(No-reduce-no-step (e ⊙ ⟨ z ⟩) (is-edge x≠z)))
... | w'@(m ⊙ sw) , w→w' , (normal w'-is-quasi-simple no-red)
= (e ⊙ w') , e⊙w-to-e⊙w' , (normal e⊙w'-is-quasi-simple ¬red-e⊙w')
where
e⊙w-to-e⊙w' : (e ⊙ w) →r* (e ⊙ w')
e⊙w-to-e⊙w' = ξ₂-⊙ {a≠b = x≠y}{x≠z} w→w' e
e⊙w'-is-quasi-simple : (e ⊙ w') is-quasi-simple
e⊙w'-is-quasi-simple = ⊙-quasi-simple-is-quasi-simple {e = e} {w'} w'-is-quasi-simple ¬x∈w'
where
¬x∈w' : ¬ (x ∈w w')
¬x∈w' x∈w' = ⊥-elim (w∌x x∈w)
where
x∈w : x ∈w w
x∈w = nf-∈' w' x∈w' w w→w'
¬red-e⊙w' : Reduce (e ⊙ w') → ⊥ ℓ
¬red-e⊙w' (reduction (ξ₁ _ _ (is-loop x≡y _) to-dot)) = ⊥-elim (x≠z x≡y)
¬red-e⊙w' (reduction (ξ₂ _ _ _ _ _ w'→q)) = no-red (reduction w'→q)
¬red-e⊙w' (reduction (ξ₃ e p q ¬l l nt .(_ ⊙ (m ⊙ sw)) w≡)) = get-⊥ x-in-different-pos
where
x∈q : x ∈w (p ∙w q)
x∈q = ∈-∙w-right _ (∈-non-trivial q nt) p
x∈w' : x ∈w w'
x∈w' with ≡-walks-to-∑ w≡
... | idp , m⊙sw≡p∙q = tr (λ o → x ∈w o) (! m⊙sw≡p∙q) x∈q
x-in-different-pos : inr x∈w' ≡ inl idp
x-in-different-pos = e⊙w'-is-quasi-simple x (inr x∈w') (inl idp)
get-⊥ : inr x∈w' ≡ inl idp → ⊥ ℓ
get-⊥ ()
progress
: ∀ {x y} → (p : Walk G x y)
----------------------------
→ Progress p
progress ⟨ _ ⟩ = done (No-reduce-is-normal _ is-dot)
progress {x = x}{y} (e ⊙ ⟨ _ ⟩)
with x ≟Node y
... | inl idp = step (reduction (ξ₁ _ _ (is-loop idp _) (is-dot idp)))
... | inr x≠y = done (No-reduce-is-normal _ (is-edge x≠y))
progress {x = x}{y} w@(e1 ⊙ (e2 ⊙ p))
with normalize w
... | w' , (.w →r⟨ next-step ⟩ w→*w') , (normal w'-is-quasi-simple ¬red-w')
= step (reduction next-step)
... | .w , (.w →r*∎) , (normal w'-is-quasi-simple ¬red-w')
= done (normal w'-is-quasi-simple ¬red-w')
?normal : ∀ {x y} → (w : Walk G x y) → Dec (Normal w)
?normal w with progress w
... | step red = no λ { (normal x ¬red) → ¬red red}
... | done nf = yes nf
?reduce : ∀ {x y} → (w : Walk G x y) → Dec (Reduce w)
?reduce w with progress w
... | step red = yes red
... | done (normal _ ¬red) = no (λ red → ¬red red)
(2022-12-28)(57c278b4) Last updated: 2021-09-16 15:00:00 by jonathan.cubides (2022-07-06)(d3a4a8cf) minors by jonathan.cubides (2022-01-26)(4aef326b) [ reports ] added some revisions by jonathan.cubides (2021-12-20)(049db6a8) Added code of cubical experiments. by jonathan.cubides (2021-12-20)(961730c9) [ html ] regular update by jonathan.cubides (2021-12-20)(e0ef9faa) Fixed compilation and format, remove hidden parts by jonathan.cubides (2021-12-20)(5120e5d1) Added cubical experiment to the master by jonathan.cubides (2021-12-17)(828fdd0a) More revisions added for CPP by jonathan.cubides (2021-12-15)(0d6a99d8) Fixed some broken links and descriptions by jonathan.cubides (2021-12-15)(662a1f2d) [ .gitignore ] add by jonathan.cubides (2021-12-15)(0630ce66) Minor fixes by jonathan.cubides (2021-12-13)(04f10eba) Fixed a lot of details by jonathan.cubides (2021-12-10)(24195c9f) [ .gitignore ] ignore .zip and arxiv related files by jonathan.cubides (2021-12-09)(538d2859) minor fixes before dinner by jonathan.cubides (2021-12-09)(36a1a69f) [ planar.pdf ] w.i.p revisions to share on arxiv first by jonathan.cubides