348 lines
14 KiB
Text
348 lines
14 KiB
Text
/-
|
||
Copyright (c) 2016 Floris van Doorn. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
||
Authors: Floris van Doorn
|
||
|
||
Graphs and operations on graphs
|
||
|
||
Currently we only define the notion of a path in a graph, and prove properties and operations on
|
||
paths.
|
||
-/
|
||
|
||
open eq sigma nat
|
||
|
||
/-
|
||
A path is a list of vertexes which are adjacent. We maybe use a weird ordering of cons, because
|
||
the major example where we use this is a category where this ordering makes more sense.
|
||
For the operations on paths we use the names from the corresponding operations on lists. Opening
|
||
both the list and the paths namespace will lead to many name clashes, so that is not advised.
|
||
-/
|
||
|
||
inductive paths {A : Type} (R : A → A → Type) : A → A → Type :=
|
||
| nil {} : Π{a : A}, paths R a a
|
||
| cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃), paths R a₁ a₂ → paths R a₁ a₃
|
||
|
||
namespace paths
|
||
|
||
notation h :: t := cons h t
|
||
notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
|
||
|
||
variables {A : Type} {R : A → A → Type} {a a' a₁ a₂ a₃ a₄ : A}
|
||
|
||
definition concat (r : R a₁ a₂) (l : paths R a₂ a₃) : paths R a₁ a₃ :=
|
||
begin
|
||
induction l with a a₂ a₃ a₄ r' l IH,
|
||
{ exact [r]},
|
||
{ exact r' :: IH r}
|
||
end
|
||
|
||
theorem concat_nil (r : R a₁ a₂) : concat r (@nil A R a₂) = [r] := idp
|
||
|
||
theorem concat_cons (r : R a₁ a₂) (r' : R a₃ a₄) (l : paths R a₂ a₃)
|
||
: concat r (r'::l) = r'::(concat r l) := idp
|
||
|
||
definition append (l₂ : paths R a₂ a₃) (l₁ : paths R a₁ a₂) :
|
||
paths R a₁ a₃ :=
|
||
begin
|
||
induction l₂,
|
||
{ exact l₁},
|
||
{ exact cons r (v_0 l₁)}
|
||
end
|
||
|
||
infix ` ++ ` := append
|
||
|
||
definition nil_append (l : paths R a₁ a₂) : nil ++ l = l := idp
|
||
definition cons_append (r : R a₃ a₄) (l₂ : paths R a₂ a₃) (l₁ : paths R a₁ a₂) :
|
||
(r :: l₂) ++ l₁ = r :: (l₂ ++ l₁) := idp
|
||
|
||
definition singleton_append (r : R a₂ a₃) (l : paths R a₁ a₂) : [r] ++ l = r :: l := idp
|
||
definition append_singleton (l : paths R a₂ a₃) (r : R a₁ a₂) : l ++ [r] = concat r l :=
|
||
begin
|
||
induction l,
|
||
{ reflexivity},
|
||
{ exact ap (cons r) !v_0}
|
||
end
|
||
|
||
definition append_nil (l : paths R a₁ a₂) : l ++ nil = l :=
|
||
begin
|
||
induction l,
|
||
{ reflexivity},
|
||
{ exact ap (cons r) v_0}
|
||
end
|
||
|
||
definition append_assoc (l₃ : paths R a₃ a₄) (l₂ : paths R a₂ a₃)
|
||
(l₁ : paths R a₁ a₂) : (l₃ ++ l₂) ++ l₁ = l₃ ++ (l₂ ++ l₁) :=
|
||
begin
|
||
induction l₃,
|
||
{ reflexivity},
|
||
{ refine ap (cons r) !v_0}
|
||
end
|
||
|
||
theorem append_concat (l₂ : paths R a₃ a₄) (l₁ : paths R a₂ a₃) (r : R a₁ a₂) :
|
||
l₂ ++ concat r l₁ = concat r (l₂ ++ l₁) :=
|
||
begin
|
||
induction l₂,
|
||
{ reflexivity},
|
||
{ exact ap (cons r_1) !v_0}
|
||
end
|
||
|
||
theorem concat_append (l₂ : paths R a₃ a₄) (r : R a₂ a₃) (l₁ : paths R a₁ a₂) :
|
||
concat r l₂ ++ l₁ = l₂ ++ r :: l₁ :=
|
||
begin
|
||
induction l₂,
|
||
{ reflexivity},
|
||
{ exact ap (cons r) !v_0}
|
||
end
|
||
|
||
definition paths.rec_tail {C : Π⦃a a' : A⦄, paths R a a' → Type}
|
||
(H0 : Π {a : A}, @C a a nil)
|
||
(H1 : Π {a₁ a₂ a₃ : A} (r : R a₁ a₂) (l : paths R a₂ a₃), C l → C (concat r l)) :
|
||
Π{a a' : A} (l : paths R a a'), C l :=
|
||
begin
|
||
have Π{a₁ a₂ a₃ : A} (l₂ : paths R a₂ a₃) (l₁ : paths R a₁ a₂) (c : C l₂),
|
||
C (l₂ ++ l₁),
|
||
begin
|
||
intros, revert a₃ l₂ c, induction l₁: intros a₃ l₂ c,
|
||
{ rewrite append_nil, exact c},
|
||
{ rewrite [-concat_append], apply v_0, apply H1, exact c}
|
||
end,
|
||
intros, rewrite [-nil_append], apply this, apply H0
|
||
end
|
||
|
||
definition cons_eq_concat (r : R a₂ a₃) (l : paths R a₁ a₂) :
|
||
Σa (r' : R a₁ a) (l' : paths R a a₃), r :: l = concat r' l' :=
|
||
begin
|
||
revert a₃ r, induction l: intros a₃' r',
|
||
{ exact ⟨a₃', r', nil, idp⟩},
|
||
{ cases (v_0 a₃ r) with a₄ w, cases w with r₂ w, cases w with l p, clear v_0,
|
||
exact ⟨a₄, r₂, r' :: l, ap (cons r') p⟩}
|
||
end
|
||
|
||
definition length (l : paths R a₁ a₂) : ℕ :=
|
||
begin
|
||
induction l,
|
||
{ exact 0},
|
||
{ exact succ v_0}
|
||
end
|
||
|
||
/- If we can reverse edges in the graph we can reverse paths -/
|
||
|
||
definition reverse (rev : Π⦃a a'⦄, R a a' → R a' a) (l : paths R a₁ a₂) :
|
||
paths R a₂ a₁ :=
|
||
begin
|
||
induction l,
|
||
{ exact nil},
|
||
{ exact concat (rev r) v_0}
|
||
end
|
||
|
||
theorem reverse_nil (rev : Π⦃a a'⦄, R a a' → R a' a) : reverse rev (@nil A R a₁) = [] := idp
|
||
|
||
theorem reverse_cons (rev : Π⦃a a'⦄, R a a' → R a' a) (r : R a₂ a₃) (l : paths R a₁ a₂) :
|
||
reverse rev (r::l) = concat (rev r) (reverse rev l) := idp
|
||
|
||
theorem reverse_singleton (rev : Π⦃a a'⦄, R a a' → R a' a) (r : R a₁ a₂) :
|
||
reverse rev [r] = [rev r] := idp
|
||
|
||
theorem reverse_pair (rev : Π⦃a a'⦄, R a a' → R a' a) (r₂ : R a₂ a₃) (r₁ : R a₁ a₂) :
|
||
reverse rev [r₂, r₁] = [rev r₁, rev r₂] := idp
|
||
|
||
theorem reverse_concat (rev : Π⦃a a'⦄, R a a' → R a' a) (r : R a₁ a₂) (l : paths R a₂ a₃) :
|
||
reverse rev (concat r l) = rev r :: (reverse rev l) :=
|
||
begin
|
||
induction l,
|
||
{ reflexivity},
|
||
{ rewrite [concat_cons, reverse_cons, v_0]}
|
||
end
|
||
|
||
theorem reverse_append (rev : Π⦃a a'⦄, R a a' → R a' a) (l₂ : paths R a₂ a₃)
|
||
(l₁ : paths R a₁ a₂) : reverse rev (l₂ ++ l₁) = reverse rev l₁ ++ reverse rev l₂ :=
|
||
begin
|
||
induction l₂,
|
||
{ exact !append_nil⁻¹},
|
||
{ rewrite [cons_append, +reverse_cons, append_concat, v_0]}
|
||
end
|
||
|
||
definition realize (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
|
||
(c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃)
|
||
⦃a a' : A⦄ (l : paths R a a') : P a a' :=
|
||
begin
|
||
induction l,
|
||
{ exact ρ a},
|
||
{ exact c v_0 (f r)}
|
||
end
|
||
|
||
definition realize_nil (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
|
||
(c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃) (a : A) :
|
||
realize P f ρ c nil = ρ a :=
|
||
idp
|
||
|
||
definition realize_cons (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
|
||
(c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃)
|
||
⦃a₁ a₂ a₃ : A⦄ (r : R a₂ a₃) (l : paths R a₁ a₂) :
|
||
realize P f ρ c (r :: l) = c (realize P f ρ c l) (f r) :=
|
||
idp
|
||
|
||
theorem realize_singleton {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
|
||
{c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
|
||
(id_left : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c (ρ a₁) p = p)
|
||
⦃a₁ a₂ : A⦄ (r : R a₁ a₂) :
|
||
realize P f ρ c [r] = f r :=
|
||
id_left (f r)
|
||
|
||
theorem realize_pair {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
|
||
{c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
|
||
(id_left : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c (ρ a₁) p = p)
|
||
⦃a₁ a₂ a₃ : A⦄ (r₂ : R a₂ a₃) (r₁ : R a₁ a₂) :
|
||
realize P f ρ c [r₂, r₁] = c (f r₁) (f r₂) :=
|
||
ap (λx, c x (f r₂)) (realize_singleton id_left r₁)
|
||
|
||
theorem realize_append {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
|
||
{c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
|
||
(assoc : Π⦃a₁ a₂ a₃ a₄⦄ (p : P a₁ a₂) (q : P a₂ a₃) (r : P a₃ a₄), c (c p q) r = c p (c q r))
|
||
(id_right : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c p (ρ a₂) = p)
|
||
⦃a₁ a₂ a₃ : A⦄ (l₂ : paths R a₂ a₃) (l₁ : paths R a₁ a₂) :
|
||
realize P f ρ c (l₂ ++ l₁) = c (realize P f ρ c l₁) (realize P f ρ c l₂) :=
|
||
begin
|
||
induction l₂,
|
||
{ exact !id_right⁻¹},
|
||
{ rewrite [cons_append, +realize_cons, v_0, assoc]}
|
||
end
|
||
|
||
/-
|
||
We sometimes want to take quotients of paths (this library was developed to define the pushout of
|
||
categories). The definition paths_rel will - given some basic reduction rules codified by Q -
|
||
extend the reduction to a reflexive transitive relation respecting concatenation of paths.
|
||
-/
|
||
|
||
inductive paths_rel {A : Type} {R : A → A → Type}
|
||
(Q : Π⦃a a' : A⦄, paths R a a' → paths R a a' → Type)
|
||
: Π⦃a a' : A⦄, paths R a a' → paths R a a' → Type :=
|
||
| rrefl : Π{a a' : A} (l : paths R a a'), paths_rel Q l l
|
||
| rel : Π{a₁ a₂ a₃ : A} {l₂ l₃ : paths R a₂ a₃} (l : paths R a₁ a₂) (q : Q l₂ l₃),
|
||
paths_rel Q (l₂ ++ l) (l₃ ++ l)
|
||
| rcons : Π{a₁ a₂ a₃ : A} {l₁ l₂ : paths R a₁ a₂} (r : R a₂ a₃),
|
||
paths_rel Q l₁ l₂ → paths_rel Q (cons r l₁) (cons r l₂)
|
||
| rtrans : Π{a₁ a₂ : A} {l₁ l₂ l₃ : paths R a₁ a₂},
|
||
paths_rel Q l₁ l₂ → paths_rel Q l₂ l₃ → paths_rel Q l₁ l₃
|
||
|
||
open paths_rel
|
||
attribute rrefl [refl]
|
||
attribute rtrans [trans]
|
||
variables {Q : Π⦃a a' : A⦄, paths R a a' → paths R a a' → Type}
|
||
|
||
definition paths_rel_of_Q {l₁ l₂ : paths R a₁ a₂} (q : Q l₁ l₂) :
|
||
paths_rel Q l₁ l₂ :=
|
||
begin
|
||
rewrite [-append_nil l₁, -append_nil l₂], exact rel nil q,
|
||
end
|
||
|
||
theorem rel_respect_append_left (l : paths R a₂ a₃) {l₃ l₄ : paths R a₁ a₂}
|
||
(H : paths_rel Q l₃ l₄) : paths_rel Q (l ++ l₃) (l ++ l₄) :=
|
||
begin
|
||
induction l,
|
||
{ exact H},
|
||
{ exact rcons r (v_0 _ _ H)}
|
||
end
|
||
|
||
theorem rel_respect_append_right {l₁ l₂ : paths R a₂ a₃} (l : paths R a₁ a₂)
|
||
(H₁ : paths_rel Q l₁ l₂) : paths_rel Q (l₁ ++ l) (l₂ ++ l) :=
|
||
begin
|
||
induction H₁ with a₁ a₂ l₁
|
||
a₂ a₃ a₄ l₂ l₂' l₁ q
|
||
a₂ a₃ a₄ l₁ l₂ r H₁ IH
|
||
a₂ a₃ l₁ l₂ l₂' H₁ H₁' IH IH',
|
||
{ reflexivity},
|
||
{ rewrite [+ append_assoc], exact rel _ q},
|
||
{ exact rcons r (IH l) },
|
||
{ exact rtrans (IH l) (IH' l)}
|
||
end
|
||
|
||
theorem rel_respect_append {l₁ l₂ : paths R a₂ a₃} {l₃ l₄ : paths R a₁ a₂}
|
||
(H₁ : paths_rel Q l₁ l₂) (H₂ : paths_rel Q l₃ l₄) :
|
||
paths_rel Q (l₁ ++ l₃) (l₂ ++ l₄) :=
|
||
begin
|
||
induction H₁ with a₁ a₂ l
|
||
a₂ a₃ a₄ l₂ l₂' l q
|
||
a₂ a₃ a₄ l₁ l₂ r H₁ IH
|
||
a₂ a₃ l₁ l₂ l₂' H₁ H₁' IH IH',
|
||
{ exact rel_respect_append_left _ H₂},
|
||
{ rewrite [+ append_assoc], transitivity _, exact rel _ q,
|
||
apply rel_respect_append_left, apply rel_respect_append_left, exact H₂},
|
||
{ exact rcons r (IH _ _ H₂) },
|
||
{ refine rtrans (IH _ _ H₂) _, apply rel_respect_append_right, exact H₁'}
|
||
end
|
||
|
||
/- assuming some extra properties the relation respects reversing -/
|
||
|
||
theorem rel_respect_reverse (rev : Π⦃a a'⦄, R a a' → R a' a) {l₁ l₂ : paths R a₁ a₂}
|
||
(H : paths_rel Q l₁ l₂)
|
||
(rev_rel : Π⦃a a' : A⦄ {l l' : paths R a a'},
|
||
Q l l' → paths_rel Q (reverse rev l) (reverse rev l')) :
|
||
paths_rel Q (reverse rev l₁) (reverse rev l₂) :=
|
||
begin
|
||
induction H,
|
||
{ reflexivity},
|
||
{ rewrite [+ reverse_append], apply rel_respect_append_left, apply rev_rel q},
|
||
{ rewrite [+reverse_cons,-+append_singleton], apply rel_respect_append_right, exact v_0},
|
||
{ exact rtrans v_0 v_1}
|
||
end
|
||
|
||
theorem rel_left_inv (rev : Π⦃a a'⦄, R a a' → R a' a) (l : paths R a₁ a₂)
|
||
(li : Π⦃a a' : A⦄ (r : R a a'), paths_rel Q [rev r, r] nil) :
|
||
paths_rel Q (reverse rev l ++ l) nil :=
|
||
begin
|
||
induction l,
|
||
{ reflexivity},
|
||
{ rewrite [reverse_cons, concat_append],
|
||
refine rtrans _ v_0, apply rel_respect_append_left,
|
||
exact rel_respect_append_right _ (li r)}
|
||
end
|
||
|
||
theorem rel_right_inv (rev : Π⦃a a'⦄, R a a' → R a' a) (l : paths R a₁ a₂)
|
||
(ri : Π⦃a a' : A⦄ (r : R a a'), paths_rel Q [r, rev r] nil) :
|
||
paths_rel Q (l ++ reverse rev l) nil :=
|
||
begin
|
||
induction l using paths.rec_tail,
|
||
{ reflexivity},
|
||
{ rewrite [reverse_concat, concat_append],
|
||
refine rtrans _ a, apply rel_respect_append_left,
|
||
exact rel_respect_append_right _ (ri r)}
|
||
end
|
||
|
||
definition realize_eq {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
|
||
{c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
|
||
(assoc : Π⦃a₁ a₂ a₃ a₄⦄ (p : P a₁ a₂) (q : P a₂ a₃) (r : P a₃ a₄), c (c p q) r = c p (c q r))
|
||
(id_right : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c p (ρ a₂) = p)
|
||
(resp_rel : Π⦃a₁ a₂⦄ {l₁ l₂ : paths R a₁ a₂}, Q l₁ l₂ →
|
||
realize P f ρ c l₁ = realize P f ρ c l₂)
|
||
⦃a a' : A⦄ {l l' : paths R a a'} (H : paths_rel Q l l') :
|
||
realize P f ρ c l = realize P f ρ c l' :=
|
||
begin
|
||
induction H,
|
||
{ reflexivity},
|
||
{ rewrite [+realize_append assoc id_right], apply ap (c _), exact resp_rel q},
|
||
{ exact ap (λx, c x (f r)) v_0},
|
||
{ exact v_0 ⬝ v_1}
|
||
end
|
||
|
||
inductive all (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type :=
|
||
| nil {} : Π{a : A}, all T (@nil A R a)
|
||
| cons : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} {p : paths R a₁ a₂}, T r → all T p → all T (cons r p)
|
||
|
||
inductive Exists (T : Π⦃a₁ a₂ : A⦄, R a₁ a₂ → Type) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type :=
|
||
| base : Π{a₁ a₂ a₃ : A} {r : R a₂ a₃} (p : paths R a₁ a₂), T r → Exists T (cons r p)
|
||
| cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, Exists T p → Exists T (cons r p)
|
||
|
||
inductive mem (l : R a₃ a₄) : Π⦃a₁ a₂ : A⦄, paths R a₁ a₂ → Type :=
|
||
| base : Π{a₂ : A} (p : paths R a₂ a₃), mem l (cons l p)
|
||
| cons : Π{a₁ a₂ a₃ : A} (r : R a₂ a₃) {p : paths R a₁ a₂}, mem l p → mem l (cons r p)
|
||
|
||
definition len (p : paths R a₁ a₂) : ℕ :=
|
||
begin
|
||
induction p with a a₁ a₂ a₃ r p IH,
|
||
{ exact 0 },
|
||
{ exact nat.succ IH }
|
||
end
|
||
|
||
end paths
|