216 lines
12 KiB
Plaintext
216 lines
12 KiB
Plaintext
open import Graph.Base
|
|
open import Graph.Reasoning
|
|
|
|
module Graph.Properties where
|
|
|
|
+-sym : ∀ { A : Set } { G H : Graph A } → G + H ≡ H + G
|
|
+-sym = record
|
|
{ vₗ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
|
|
; vᵣ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
|
|
; eₗ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
|
|
; eᵣ = λ { (+ₗ x) → +ᵣ x ; (+ᵣ x) → +ₗ x }
|
|
}
|
|
|
|
+-assoc : ∀ { A : Set } { G H I : Graph A } → G + (H + I) ≡ (G + H) + I
|
|
+-assoc = record
|
|
{ vₗ = λ { (+ₗ x) → +ₗ (+ₗ x) ; (+ᵣ (+ₗ x)) → +ₗ (+ᵣ x) ; (+ᵣ (+ᵣ x)) → +ᵣ x }
|
|
; vᵣ = λ { (+ₗ (+ₗ x)) → +ₗ x ; (+ₗ (+ᵣ x)) → +ᵣ (+ₗ x) ; (+ᵣ x) → +ᵣ (+ᵣ x) }
|
|
; eₗ = λ { (+ₗ x) → +ₗ (+ₗ x) ; (+ᵣ (+ₗ x)) → +ₗ (+ᵣ x) ; (+ᵣ (+ᵣ x)) → +ᵣ x }
|
|
; eᵣ = λ { (+ₗ (+ₗ x)) → +ₗ x ; (+ₗ (+ᵣ x)) → +ᵣ (+ₗ x) ; (+ᵣ x) → +ᵣ (+ᵣ x) }
|
|
}
|
|
|
|
+-identityʳ : ∀ { A : Set } { G : Graph A } → G + ε ≡ G
|
|
+-identityʳ = record
|
|
{ vₗ = λ { (+ₗ x) → x }
|
|
; vᵣ = λ x → +ₗ x
|
|
; eₗ = λ { (+ₗ x) → x }
|
|
; eᵣ = +ₗ
|
|
}
|
|
|
|
+-identityˡ : ∀ { A : Set } { G : Graph A } → ε + G ≡ G
|
|
+-identityˡ = record
|
|
{ vₗ = λ { (+ᵣ x) → x }
|
|
; vᵣ = +ᵣ
|
|
; eₗ = λ { (+ᵣ x) → x }
|
|
; eᵣ = +ᵣ
|
|
}
|
|
|
|
+-congˡ : ∀ { A : Set } { G H I : Graph A } → G ≡ H → G + I ≡ H + I
|
|
+-congˡ G≈H = record
|
|
{ vₗ = λ { (+ₗ x) → +ₗ (_≡_.vₗ G≈H x) ; (+ᵣ x) → +ᵣ x }
|
|
; vᵣ = λ { (+ₗ x) → +ₗ (_≡_.vᵣ G≈H x) ; (+ᵣ x) → +ᵣ x }
|
|
; eₗ = λ { (+ₗ x) → +ₗ (_≡_.eₗ G≈H x) ; (+ᵣ x) → +ᵣ x }
|
|
; eᵣ = λ { (+ₗ x) → +ₗ (_≡_.eᵣ G≈H x) ; (+ᵣ x) → +ᵣ x }
|
|
}
|
|
|
|
+-congʳ : ∀ { A : Set } { G H I : Graph A } → H ≡ I → G + H ≡ G + I
|
|
+-congʳ {_} {G} {H} {I} H≡I = begin
|
|
G + H ≡⟨ +-sym ⟩
|
|
H + G ≡⟨ +-congˡ H≡I ⟩
|
|
I + G ≡⟨ +-sym ⟩
|
|
G + I ∎
|
|
where open ≡-Reasoning
|
|
|
|
|
|
⇀-assoc : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H ⇀ I) ≡ (G ⇀ H) ⇀ I
|
|
⇀-assoc = record
|
|
{ vₗ = λ { (⇀ₗ x) → ⇀ₗ (⇀ₗ x) ; (⇀ᵣ (⇀ₗ x)) → ⇀ₗ (⇀ᵣ x) ; (⇀ᵣ (⇀ᵣ x)) → ⇀ᵣ x }
|
|
; vᵣ = λ { (⇀ₗ (⇀ₗ x)) → ⇀ₗ x ; (⇀ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (⇀ᵣ x) → ⇀ᵣ (⇀ᵣ x) }
|
|
; eₗ = λ { (⇀ₗ x) → ⇀ₗ (⇀ₗ x) ; (⇀ᵣ (⇀ₗ x)) → ⇀ₗ (⇀ᵣ x) ; (⇀ᵣ (⇀ᵣ x)) → ⇀ᵣ x ; (⇀ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (⇀ᵣ x) x₁ ; (⇀ₗᵣ x (⇀ₗ x₁)) → ⇀ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (⇀ᵣ x₁)) → ⇀ₗᵣ (⇀ₗ x) x₁ }
|
|
; eᵣ = λ { (⇀ₗ (⇀ₗ x)) → ⇀ₗ x ; (⇀ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (⇀ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (⇀ₗ x₁) ; (⇀ᵣ x) → ⇀ᵣ (⇀ᵣ x) ; (⇀ₗᵣ (⇀ₗ x) x₁) → ⇀ₗᵣ x (⇀ᵣ x₁) ; (⇀ₗᵣ (⇀ᵣ x) x₁) → ⇀ᵣ (⇀ₗᵣ x x₁) }
|
|
}
|
|
|
|
⇀-identˡ : ∀ { A : Set } { G : Graph A } → G ⇀ ε ≡ G
|
|
⇀-identˡ = record
|
|
{ vₗ = λ { (⇀ₗ x) → x }
|
|
; vᵣ = ⇀ₗ
|
|
; eₗ = λ { (⇀ₗ x) → x }
|
|
; eᵣ = ⇀ₗ
|
|
}
|
|
|
|
⇀-identʳ : ∀ { A : Set } { G : Graph A } → ε ⇀ G ≡ G
|
|
⇀-identʳ = record
|
|
{ vₗ = λ { (⇀ᵣ x) → x }
|
|
; vᵣ = ⇀ᵣ
|
|
; eₗ = λ { (⇀ᵣ x) → x }
|
|
; eᵣ = ⇀ᵣ
|
|
}
|
|
|
|
⇀-congˡ : ∀ { A : Set } { G H I : Graph A } → G ≡ H → G ⇀ I ≡ H ⇀ I
|
|
⇀-congˡ G≈H = record
|
|
{ vₗ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.vₗ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x }
|
|
; vᵣ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.vᵣ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x }
|
|
; eₗ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.eₗ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ (_≡_.vₗ G≈H x) x₁ }
|
|
; eᵣ = λ { (⇀ₗ x) → ⇀ₗ (_≡_.eᵣ G≈H x) ; (⇀ᵣ x) → ⇀ᵣ x ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ (_≡_.vᵣ G≈H x) x₁ }
|
|
}
|
|
|
|
⇀-congʳ : ∀ { A : Set } { G H I : Graph A } → H ≡ I → G ⇀ H ≡ G ⇀ I
|
|
⇀-congʳ G≈H = record
|
|
{ vₗ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.vₗ G≈H x) }
|
|
; vᵣ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.vᵣ G≈H x) }
|
|
; eₗ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.eₗ G≈H x) ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ x (_≡_.vₗ G≈H x₁) }
|
|
; eᵣ = λ { (⇀ₗ x) → ⇀ₗ x ; (⇀ᵣ x) → ⇀ᵣ (_≡_.eᵣ G≈H x) ; (⇀ₗᵣ x x₁) → ⇀ₗᵣ x (_≡_.vᵣ G≈H x₁) }
|
|
}
|
|
|
|
⇀-congʳ-≤ : ∀ { A : Set } { G H I : Graph A } → H ≤ I → G ⇀ H ≤ G ⇀ I
|
|
⇀-congʳ-≤ H≤I = record
|
|
{ def = record
|
|
{ vₗ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (_≡_.vₗ (_≤_.def H≤I) (+ₗ x)) ; (+ᵣ x) → x }
|
|
; vᵣ = +ᵣ
|
|
; eₗ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (_≡_.eₗ (_≤_.def H≤I) (+ₗ x)) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (_≡_.vₗ (_≤_.def H≤I) (+ₗ x₁)) ; (+ᵣ x) → x }
|
|
; eᵣ = +ᵣ
|
|
}
|
|
}
|
|
|
|
⇀-distrib-+ : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H + I) ≡ G ⇀ H + G ⇀ I
|
|
⇀-distrib-+ = record
|
|
{ vₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ (+ₗ x)) → +ₗ (⇀ᵣ x) ; (⇀ᵣ (+ᵣ x)) → +ᵣ (⇀ᵣ x) }
|
|
; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (+ₗ x) ; (+ᵣ (⇀ₗ x)) → ⇀ₗ x ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ (+ᵣ x) }
|
|
; eₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ (+ₗ x)) → +ₗ (⇀ᵣ x) ; (⇀ᵣ (+ᵣ x)) → +ᵣ (⇀ᵣ x) ; (⇀ₗᵣ x (+ₗ x₁)) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (+ᵣ x₁)) → +ᵣ (⇀ₗᵣ x x₁) }
|
|
; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (+ₗ x) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (+ₗ x₁) ; (+ᵣ (⇀ₗ x)) → ⇀ₗ x ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ (+ᵣ x) ; (+ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (+ᵣ x₁) }
|
|
}
|
|
|
|
+-distrib-⇀ : ∀ { A : Set } { G H I : Graph A } → (G + H) ⇀ I ≡ G ⇀ I + H ⇀ I
|
|
+-distrib-⇀ = record
|
|
{ vₗ = λ { (⇀ₗ (+ₗ x)) → +ₗ (⇀ₗ x) ; (⇀ₗ (+ᵣ x)) → +ᵣ (⇀ₗ x) ; (⇀ᵣ x) → +ₗ (⇀ᵣ x) }
|
|
; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ (+ₗ x) ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ x ; (+ᵣ (⇀ₗ x)) → ⇀ₗ (+ᵣ x) ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ x }
|
|
; eₗ = λ { (⇀ₗ (+ₗ x)) → +ₗ (⇀ₗ x) ; (⇀ₗ (+ᵣ x)) → +ᵣ (⇀ₗ x) ; (⇀ᵣ x) → +ₗ (⇀ᵣ x) ; (⇀ₗᵣ (+ₗ x) x₁) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ (+ᵣ x) x₁) → +ᵣ (⇀ₗᵣ x x₁) }
|
|
; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ (+ₗ x) ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ x ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (+ₗ x) x₁ ; (+ᵣ (⇀ₗ x)) → ⇀ₗ (+ᵣ x) ; (+ᵣ (⇀ᵣ x)) → ⇀ᵣ x ; (+ᵣ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ (+ᵣ x) x₁ }
|
|
}
|
|
|
|
⇀-decomp : ∀ { A : Set } { G H I : Graph A } → G ⇀ (H ⇀ I) ≡ G ⇀ H + (G ⇀ I + H ⇀ I)
|
|
⇀-decomp = record
|
|
{ vₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ x) → +ᵣ (+ᵣ x) }
|
|
; vᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (+ᵣ (+ₗ (⇀ₗ x))) → ⇀ₗ x ; (+ᵣ (+ₗ (⇀ᵣ x))) → ⇀ᵣ (⇀ᵣ x) ; (+ᵣ (+ᵣ x)) → ⇀ᵣ x }
|
|
; eₗ = λ { (⇀ₗ x) → +ₗ (⇀ₗ x) ; (⇀ᵣ x) → +ᵣ (+ᵣ x) ; (⇀ₗᵣ x (⇀ₗ x₁)) → +ₗ (⇀ₗᵣ x x₁) ; (⇀ₗᵣ x (⇀ᵣ x₁)) → +ᵣ (+ₗ (⇀ₗᵣ x x₁)) }
|
|
; eᵣ = λ { (+ₗ (⇀ₗ x)) → ⇀ₗ x ; (+ₗ (⇀ᵣ x)) → ⇀ᵣ (⇀ₗ x) ; (+ₗ (⇀ₗᵣ x x₁)) → ⇀ₗᵣ x (⇀ₗ x₁) ; (+ᵣ (+ₗ (⇀ₗ x))) → ⇀ₗ x ; (+ᵣ (+ₗ (⇀ᵣ x))) → ⇀ᵣ (⇀ᵣ x) ; (+ᵣ (+ₗ (⇀ₗᵣ x x₁))) → ⇀ₗᵣ x (⇀ᵣ x₁) ; (+ᵣ (+ᵣ x)) → ⇀ᵣ x }
|
|
}
|
|
|
|
+-idem : ∀ { A : Set } { G : Graph A } → G + G ≡ G
|
|
+-idem {_} {G} = begin
|
|
G + G ≡⟨ sym ⇀-identˡ ⟩
|
|
(G + G) ⇀ ε ≡⟨ +-distrib-⇀ ⟩
|
|
(G ⇀ ε) + (G ⇀ ε) ≡⟨ sym +-identityʳ ⟩
|
|
((G ⇀ ε) + (G ⇀ ε)) + ε ≡⟨ sym (+-congʳ ⇀-identˡ) ⟩
|
|
((G ⇀ ε) + (G ⇀ ε)) + (ε ⇀ ε) ≡⟨ sym +-assoc ⟩
|
|
(G ⇀ ε) + ((G ⇀ ε) + (ε ⇀ ε)) ≡⟨ sym ⇀-decomp ⟩
|
|
G ⇀ (ε ⇀ ε) ≡⟨ ⇀-assoc ⟩
|
|
(G ⇀ ε) ⇀ ε ≡⟨ ⇀-identˡ ⟩
|
|
G ⇀ ε ≡⟨ ⇀-identˡ ⟩
|
|
G ∎
|
|
where open ≡-Reasoning
|
|
|
|
+-absorp : ∀ { A : Set } { G H : Graph A } → G ⇀ H + G + H ≡ G ⇀ H
|
|
+-absorp {_} {G} {H} = begin
|
|
G ⇀ H + G + H ≡⟨ +-congˡ (+-congʳ (sym ⇀-identˡ)) ⟩
|
|
G ⇀ H + G ⇀ ε + H ≡⟨ +-congʳ (sym ⇀-identˡ) ⟩
|
|
G ⇀ H + G ⇀ ε + H ⇀ ε ≡⟨ sym +-assoc ⟩
|
|
G ⇀ H + (G ⇀ ε + H ⇀ ε) ≡⟨ sym ⇀-decomp ⟩
|
|
G ⇀ (H ⇀ ε) ≡⟨ ⇀-congʳ ⇀-identˡ ⟩
|
|
G ⇀ H ∎
|
|
where open ≡-Reasoning
|
|
|
|
⇀-sat : ∀ { A : Set } { G : Graph A } → G ⇀ G ⇀ G ≡ G ⇀ G
|
|
⇀-sat {_} {G} = begin
|
|
G ⇀ G ⇀ G ≡⟨ sym ⇀-assoc ⟩
|
|
G ⇀ (G ⇀ G) ≡⟨ ⇀-decomp ⟩
|
|
G ⇀ G + (G ⇀ G + G ⇀ G) ≡⟨ +-congʳ +-idem ⟩
|
|
G ⇀ G + G ⇀ G ≡⟨ +-idem ⟩
|
|
G ⇀ G ∎
|
|
where open ≡-Reasoning
|
|
|
|
≡→≤ : ∀ { A : Set } { G H : Graph A } → G ≡ H → G ≤ H
|
|
≡→≤ {_} {G} {H} G≡H = begin
|
|
G ≡⟨ G≡H ⟩
|
|
H ∎
|
|
where open ≤-Reasoning
|
|
|
|
≲-least : ∀ { A : Set } { G : Graph A } → ε ≤ G
|
|
≲-least {_} {G} = record { def = begin
|
|
ε + G ≡⟨ +-identityˡ ⟩
|
|
G ∎}
|
|
where open ≡-Reasoning
|
|
|
|
+-order : ∀ { A : Set } { G H : Graph A } → G ≤ G + H
|
|
+-order {_} {G} {H} = record { def = begin
|
|
G + (G + H) ≡⟨ +-assoc ⟩
|
|
G + G + H ≡⟨ +-congˡ +-idem ⟩
|
|
G + H ∎}
|
|
where open ≡-Reasoning
|
|
|
|
+⇀-order : ∀ { A : Set } { G H : Graph A } → G + H ≤ G ⇀ H
|
|
+⇀-order {_} {G} {H} = record { def = begin
|
|
G + H + G ⇀ H ≡⟨ +-congˡ +-sym ⟩
|
|
H + G + G ⇀ H ≡⟨ +-sym ⟩
|
|
G ⇀ H + (H + G) ≡⟨ +-congʳ +-sym ⟩
|
|
G ⇀ H + (G + H) ≡⟨ +-assoc ⟩
|
|
G ⇀ H + G + H ≡⟨ +-absorp ⟩
|
|
G ⇀ H ∎}
|
|
where open ≡-Reasoning
|
|
|
|
+-mono : ∀ { A : Set } { G H I : Graph A } → G ≤ H → G + I ≤ H + I
|
|
+-mono {_} {G} {H} {I} G≤H = record { def = begin
|
|
G + I + (H + I) ≡⟨ +-congˡ +-sym ⟩
|
|
I + G + (H + I) ≡⟨ +-assoc ⟩
|
|
I + G + H + I ≡⟨ +-congˡ (sym +-assoc) ⟩
|
|
I + (G + H) + I ≡⟨ +-congˡ (+-congʳ (_≤_.def G≤H)) ⟩
|
|
I + H + I ≡⟨ +-congˡ +-sym ⟩
|
|
H + I + I ≡⟨ sym +-assoc ⟩
|
|
H + (I + I) ≡⟨ +-congʳ +-idem ⟩
|
|
H + I ∎}
|
|
where open ≡-Reasoning
|
|
|
|
⇀-monoˡ : ∀ { A : Set } { G H I : Graph A } → G ≤ H → G ⇀ I ≤ H ⇀ I
|
|
⇀-monoˡ {_} {G} {H} {I} G≤H = record { def = begin
|
|
G ⇀ I + H ⇀ I ≡⟨ sym +-distrib-⇀ ⟩
|
|
(G + H) ⇀ I ≡⟨ ⇀-congˡ (_≤_.def G≤H) ⟩
|
|
H ⇀ I ∎}
|
|
where open ≡-Reasoning
|
|
|
|
⇀-monoʳ : ∀ { A : Set } { G H I : Graph A } → G ≤ H → I ⇀ G ≤ I ⇀ H
|
|
⇀-monoʳ {_} {G} {H} {I} G≤H = record { def = begin
|
|
I ⇀ G + I ⇀ H ≡⟨ sym ⇀-distrib-+ ⟩
|
|
I ⇀ (G + H) ≡⟨ ⇀-congʳ (_≤_.def G≤H) ⟩
|
|
I ⇀ H ∎}
|
|
where open ≡-Reasoning
|