lib.graph-classes.ConnectedGraph.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-classes.ConnectedGraph
where
open import foundations.Core
open import lib.graph-definitions.Graph
open import lib.graph-walks.Walk
open import lib.graph-walks.Walk.QuasiSimple
open import lib.graph-walks.Walk.Composition
open Graph
open quasi-simple-walks
variable
ℓ : Level
isConnectedGraph : Graph ℓ → Type ℓ
isConnectedGraph G = (x y : Node G) → ∥ Walk G x y ∥
_is-connected-graph = isConnectedGraph
-- Lemma 5.3
being-connected-is-prop
: {G : Graph ℓ}
→ (isConnectedGraph G) is-prop
being-connected-is-prop = pi-is-prop (λ _ → pi-is-prop (λ _ → truncated-is-prop))
removeNode : ∀ {ℓ : Level} → (G : Graph ℓ) → Node G → Graph ℓ
removeNode {ℓ} G y = graph N' E' N'-is-set E'-forms-sets
where
N' = ∑[ x ∶ Node G ] (x ≡ y → ⊥ ℓ)
E' : N' → N' → Type ℓ
E' (x , _) (y , _) = Edge G x y
N'-is-set : N' is-set
N'-is-set = ∑-set (Node-is-set G) λ _ -> prop-is-set (pi-is-prop (λ _ → ⊥-is-prop))
E'-forms-sets : (x y : N') → (E' x y) is-set
E'-forms-sets (x , _) (y , _) = Edge-is-set G x y
syntax removeNode G x = G ⊝ x
_is-biconnected : {ℓ : Level} → Graph ℓ → Type ℓ
_is-biconnected {ℓ} G = (x : Node G) → (G ⊝ x) is-connected-graph
begin-biconnected-is-prop : {G : Graph ℓ} → (G is-biconnected) is-prop
begin-biconnected-is-prop = pi-is-prop (λ _ → being-connected-is-prop)
module _ {ℓ : Level} (G : Graph ℓ)
(_≟Node_ : (x y : Node G) → (x ≡ y) + (x ≠ y))
where
open import foundations.Fin ℓ
open import foundations.Nat ℓ
{- Given a graph G, two nodes a and b in G, and "a path with n
nodes", we want to construct a graph, denoted by G ⊕ p, formed
by the graph G and connecting the nodes a to b using the path
p.
-}
path-addition : (a b : Node G) → (n : ℕ) → 0 < n → Graph ℓ
path-addition a b n p = graph N' E' N'-is-set E'-forms-sets
where
N' : Type ℓ
N' = Node G + Fin n
E' : N' → N' → Type ℓ
E' (inl x) (inl y) = Edge G x y
E' (inl x) (inr y) = (x ≡ a) × (y ≡ (0 , p))
E' (inr x) (inl y) = (x ≡ fin-pred (0 , p)) × (y ≡ b)
E' (inr x) (inr y) = x ≡ fin-pred y
N'-is-set : N' is-set
N'-is-set = +-set (Node-is-set G) Fin-is-set
E'-forms-sets : (x y : N') → (E' x y) is-set
E'-forms-sets (inl x) (inl y) = Edge-is-set G _ _
E'-forms-sets (inl x) (inr y) = ∑-set (prop-is-set (Node-is-set G _ _)) (λ _ → prop-is-set (Fin-is-set _ _))
E'-forms-sets (inr x) (inl y) = ∑-set (prop-is-set (Fin-is-set _ _)) (λ _ → prop-is-set (Node-is-set G _ _))
E'-forms-sets (inr x) (inr y) = prop-is-set (Fin-is-set _ _)
path-addition-has-original-walks
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x y : Node G) → (Walk G x y)
→ Walk (path-addition a b n p) (inl x) (inl y)
path-addition-has-original-walks a b n p x .x ⟨ .x ⟩ = ⟨ inl x ⟩
path-addition-has-original-walks a b n p x y (_⊙_ {y = y₁} e w) = e ⊙ w'
where
w' : Walk (path-addition a b n p) (inl y₁) (inl y)
w' = path-addition-has-original-walks a b n p _ _ w
path-addition-has-new-walks
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x y : ℕ) → (x< : x < n) → (y< : y < n)
→ ((x ≡ y) + (x < y))
→ Walk (path-addition a b n p) (inr (x , x<)) (inr (y , y<))
path-addition-has-new-walks a b zero ()
path-addition-has-new-walks a b n@(succ n') ∗ zero zero x< y< (inl idp)
rewrite <-prop {n = n}{m = zero} x< y< = ⟨ inr (0 , y<) ⟩
path-addition-has-new-walks a b n@(succ n') ∗ zero (succ y) x< y< (inr *)
with _≟fin_ {n} (0 , x<) (fin-pred (succ y , y<))
... | yes p = p ⊙ ⟨ _ ⟩
... | no ¬p = walk-0-to-y ∙w (pair= (idp , <-prop {succ n'}{y} (<-inj {n}{y} y<) (n⁺<k→n<k {y}{succ n'} y<)) ⊙ ⟨ _ ⟩)
where
open ∙-walk (path-addition a b n *)
walk-0-to-y : Walk (path-addition a b n *) (inr (0 , x<)) (inr (y , <-inj {n}{y} y<))
walk-0-to-y with zero ≟nat y
... | yes idp rewrite <-prop {n = n}{m = zero} (<-inj {n}{y} y<) * = ⟨ inr ((0 , x<)) ⟩
... | no ¬p = path-addition-has-new-walks a b (succ n') ∗ 0 y ∗ ((<-inj {n}{y} y<)) (inr (n≠0 (λ p -> ¬p (sym p))))
path-addition-has-new-walks a b n@(succ n') ∗ (succ x) (succ .x) x< y< (inl idp)
rewrite <-prop {n = n}{m = succ x} x< y< = ⟨ inr (succ x , y<) ⟩
path-addition-has-new-walks a b n@(succ n') ∗ (succ x) (succ y) x< y< (inr x<y)
with _≟fin_ {n} (succ x , x<) (fin-pred (succ y , y<))
... | yes p = p ⊙ ⟨ _ ⟩
... | no ¬p = walk-0-to-y ∙w (pair= (idp , <-prop {succ n'}{y} (<-inj {n}{y} y<) (n⁺<k→n<k {y}{succ n'} y<)) ⊙ ⟨ _ ⟩)
where
open ∙-walk (path-addition a b n ∗)
walk-0-to-y : Walk (path-addition a b n ∗) (inr (succ x , x<)) (inr (y , <-inj {n}{y} y<))
walk-0-to-y with (succ x) ≟nat y
... | yes idp rewrite <-prop {n = n}{m = succ x} (<-inj {n}{y} y<) x< = ⟨ inr (succ x , x<) ⟩
... | no p = path-addition-has-new-walks a b (succ n') ∗ (succ x) y (mono-succ {x}{n'} x<) (<-inj {n}{y} y<)
(inr (<-suc-suc< {ℓ} {x}{y} x<y λ o → ¬p (pair= (sym o , <-prop {succ n'}{y} _ _))))
path-addition-walk-from-the-head
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x : Fin n)
→ Walk (path-addition a b n p) (inr (0 , p)) (inr x)
path-addition-walk-from-the-head a b zero ()
path-addition-walk-from-the-head a b n@(succ n') p x@(natx , x<)
with natx ≟nat 0
... | yes idp = ⟨ inr x ⟩
... | no ¬p = path-addition-has-new-walks a b n p 0 natx p x< (inr (n≠0 {natx} ¬p))
path-addition-walk-to-the-end
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x : Fin n)
→ Walk (path-addition a b n p) (inr x) (inr (fin-pred (0 , p)))
path-addition-walk-to-the-end a b zero ()
path-addition-walk-to-the-end a b n@(succ n') p x@(natx , x<)
with <s-to-<= natx n' x<
... | (inl idp) rewrite <-prop {succ n'}{n'} x< (<-succ n') = ⟨ inr (natx , _) ⟩
... | (inr natx<n') = path-addition-has-new-walks a b n p natx n' x< (<-succ n') (inr natx<n')
path-addition-walk-from-first-endpoint
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x : Fin n)
→ Walk (path-addition a b n p) (inl a) (inr x)
path-addition-walk-from-first-endpoint a b n p x = (idp , idp) ⊙ (path-addition-walk-from-the-head a b n p x)
path-addition-walk-to-last-endpoint
: (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (x : Fin n)
→ Walk (path-addition a b n p) (inr x) (inl b)
path-addition-walk-to-last-endpoint a b n p x
= path-addition-walk-to-the-end a b n p x ∙w (((idp , idp)) ⊙ ⟨ inl b ⟩)
where
open ∙-walk (path-addition a b n p)
path-addition-preserves-connectedness
: G is-connected-graph
→ (a b : Node G) → (n : ℕ) → (p : 0 < n)
→ (path-addition a b n p) is-connected-graph
path-addition-preserves-connectedness G-is-connected a b zero ()
path-addition-preserves-connectedness G-is-connected a b n@(succ n') p
= helper
where
G' : Graph ℓ
G' = path-addition a b n p
N' = Node G + Fin n
open ∙-walk (path-addition a b n p)
helper : (x y : N') → ∥ Walk G' x y ∥
helper (inl x) (inl y)
= trunc-elim trunc-is-prop (λ w → ∣ path-addition-has-original-walks a b n p _ _ w ∣) (G-is-connected x y)
helper (inl x) (inr y@(naty , y<))
with x ≟Node a
... | inl idp = ∣ path-addition-walk-from-first-endpoint a b n p y ∣
... | inr p' = trunc-elim trunc-is-prop (λ w
→ ∣ path-addition-has-original-walks a b n p x a w ∙w walk-a-finy ∣)
(G-is-connected x a)
where
walk-a-finy = path-addition-walk-from-first-endpoint a b n p y
helper (inr x@(natx , x<)) (inl y)
with (x ≟fin fin-pred (0 , p)) | (y ≟Node b)
... | yes idp | inl idp = ∣ (((idp , idp)) ⊙ ⟨ inl b ⟩) ∣
... | yes idp | inr y≠b = trunc-elim trunc-is-prop (λ w
→ ∣ ((((idp , idp)) ⊙ ⟨ inl b ⟩)) ∙w path-addition-has-original-walks a b n p _ _ w ∣
) (G-is-connected b y)
... | no ¬p | inl idp = ∣ walk-fin0-finn-1 ∙w ((idp , idp) ⊙ ⟨ inl b ⟩) ∣
where
walk-fin0-finn-1 : Walk (path-addition a b n p) (inr x) (inr (fin-pred (0 , p)))
walk-fin0-finn-1 = path-addition-walk-to-the-end a b n p x
... | no ¬p | inr y≠b
with (x ≟fin fin-pred (0 , p))
... | yes idp = trunc-elim trunc-is-prop (λ w
→ ∣ ((((idp , idp)) ⊙ ⟨ inl b ⟩)) ∙w path-addition-has-original-walks a b n p _ _ w ∣
) (G-is-connected b y)
... | no ¬p₁ = trunc-elim trunc-is-prop (λ w
→ ∣ walk-finx-b ∙w (((idp , idp)) ⊙ path-addition-has-original-walks a b n p _ _ w) ∣
) (G-is-connected b y)
where
walk-finx-b : Walk (path-addition a b n p) (inr x) (inr (fin-pred (0 , p)))
walk-finx-b = path-addition-walk-to-the-end a b n p x
helper (inr x@(natx , x<)) (inr y@(naty , y<))
with trichotomy natx naty
... | inl (inl idp) = ∣ path-addition-has-new-walks a b n p natx naty x< y< (inl idp) ∣
... | inl (inr natx<naty) = ∣ path-addition-has-new-walks a b n p natx naty x< y< (inr natx<naty) ∣
... | inr naty<natx =
trunc-elim trunc-is-prop (λ w
→ ∣ path-addition-walk-to-last-endpoint a b n p x
∙w path-addition-has-original-walks a b n p _ _ w
·w path-addition-walk-from-first-endpoint a b n p y
∣)
(G-is-connected b a)
(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