Library graphs

Section graphs.

Require Import Coq.Lists.List.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.

Require Import EnsembleFacts.

Require Import Setoid.


Definition dtype (U:Type) := (U*U)%type.

Definition Graph (U:Type):Type := Ensemble (dtype U).

Definition Undirected (U:Type) (G:Graph U):Prop :=
forall a b:U, In (dtype U) G (a,b)
-> In (dtype U) G (b,a).

Inductive Neighborhood (U:Type) (G:Graph U) (a:U): Ensemble U :=
|In_Neighborhood : forall b:U,
  In (dtype U) G (a,b) -> In U (Neighborhood U G a) b.

Theorem undirected_neighbor_sym : forall (U:Type) (G:Graph U),
(Undirected U G)-> forall a b:U,
In U (Neighborhood U G a) b->In U (Neighborhood U G b) a.

Definition Isomorphism (U1:Type) (U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2):Prop :=
(Bijective U1 U2 f)/\
forall (a b:U1), In (dtype U1) G1 (a,b) <-> In (dtype U2) G2 (f a, f b).

Definition Isomorph (U1:Type) (U2:Type) (G1:Graph U1) (G2:Graph U2)
:Prop := exists f:U1->U2, Isomorphism U1 U2 G1 G2 f.

Lemma Isomorphism_In : forall (U1 U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2) (a b:U1), Isomorphism U1 U2 G1 G2 f ->
In (dtype U1) G1 (a,b) -> In (dtype U2) G2 (f a,f b).

Lemma Isomorphism_In_rec : forall (U1 U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2) (a b:U1), Isomorphism U1 U2 G1 G2 f ->
In (dtype U2) G2 (f a,f b) -> In (dtype U1) G1 (a,b) .

Theorem isom_neighbor : forall (U1 U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2), Isomorphism U1 U2 G1 G2 f->
forall a:U1, Neighborhood U2 G2 (f a)=
  apply_func U1 U2 f (Neighborhood U1 G1 a).

Inductive outdegree (U:Type) (G:Graph U) (v:U)
:nat -> Prop :=
|neighbor_cardinal : forall n:nat,
  cardinal U (Neighborhood U G v) n ->
    (outdegree U G v n).

Definition outregular (U:Type) (G:Graph U):Prop :=
forall (a b:U) (n:nat),
 (outdegree U G a n)->(outdegree U G b n).

Theorem isom_outdegree : forall (U1 U2:Type)
 (G1:Graph U1) (G2:Graph U2) (f:U1->U2),
 Isomorphism U1 U2 G1 G2 f->
forall (a:U1) (n:nat), (outdegree U1 G1 a n)->
 (outdegree U2 G2 (f a) n).

Definition vertexsymmetric (U:Type) (G:Graph U):Prop :=
forall (a b:U), exists f:U->U,
 (Isomorphism U U G G f) /\ f a=b.

Theorem vertexsymmetric_outregular : forall (U:Type) (G:Graph U),
vertexsymmetric U G -> outregular U G.

Definition CommonNeighborhood (U:Type) (G:Graph U)
(a b:U): Ensemble U := Intersection U
 (Neighborhood U G a) (Neighborhood U G b).

Theorem isom_commonneighbor :
forall (U1 U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2), Isomorphism U1 U2 G1 G2 f->
forall a b:U1, CommonNeighborhood U2 G2 (f a) (f b)=
  apply_func U1 U2 f (CommonNeighborhood U1 G1 a b).

Theorem Graph_isominverse :
forall (U1 U2:Type) (G1:Graph U1) (G2:Graph U2)
(f:U1->U2) (g:U2->U1), Isomorphism U1 U2 G1 G2 f->
InverseFunction U1 U2 f g ->
Isomorphism U2 U1 G2 G1 g.

Theorem Graph_isocomposition :
forall (U1 U2 U3:Type)
(G1:Graph U1) (G2:Graph U2) (G3:Graph U3)
(f:U2->U3) (g:U1->U2),
Isomorphism U2 U3 G2 G3 f -> Isomorphism U1 U2 G1 G2 g ->
Isomorphism U1 U3 G1 G3 (Compose U1 U2 U3 f g).

Inductive Path (U:Type) (G:Graph U) : list U -> Prop:=
|Path_empty: Path U G nil
|Path_single: forall a:U, Path U G (a::nil)
|Path_nonempty: forall (a b:U) (t:list U),
 In (dtype U) G (a,b) -> Path U G (b::t) -> Path U G (a::b::t)
.

Definition StronglyConnected (U:Type) (G:Graph U):Prop:=
forall a b:U, exists P:list U, Path U G P /\
hd b P=a /\ last P a=b.

Lemma list_zerolength: forall (U:Type) (l:list U),
length l=0 -> l=nil.

Lemma list_nonzerolength: forall (U:Type) (l:list U) (n:nat),
length l=S n ->
 exists a:U, exists l':list U, l=a::l'/\length l'=n.

Fixpoint list_pushback
 (U:Type) (l:list U) (a:U) {struct l} : list U :=
match l with
| nil => a::nil
| h :: t => h :: (list_pushback U t a)
end.

Lemma list_nonzerolengthback: forall (U:Type) (l:list U) (n:nat),
length l=S n ->
 exists a:U, exists l':list U,
  l=list_pushback U l' a/\length l'=n.

Lemma SubPath : forall (U:Type) (G:Graph U) (P:list U) (a:U),
Path U G (a::P) -> Path U G P.

Theorem Path_nonemptyback:
forall (U:Type) (G:Graph U) (a b:U) (P:list U),
 In (dtype U) G (a,b) -> Path U G (list_pushback U P a) ->
 Path U G (list_pushback U (list_pushback U P a) b).

Lemma SubPathBack : forall (U:Type) (G:Graph U) (P:list U) (a:U),
Path U G (list_pushback U P a) -> Path U G P.

Lemma list_pushbacknotnil : forall (U:Type) (t:list U) (a:U),
list_pushback U t a<>nil.

Lemma PathExtractBack: forall (U:Type) (G:Graph U)
(P:list U) (a b:U),
Path U G (list_pushback U (list_pushback U P a) b)
-> In (dtype U) G (a,b).

Lemma list_hdpushback : forall (U:Type) (t:list U) (x y h a:U),
t<>nil -> hd x t=h -> hd y (list_pushback U t a) = h.

Lemma list_hdpushbackrev : forall (U:Type) (t:list U) (x h a:U),
hd x (list_pushback U t a)=h -> hd a t=h.

Lemma list_hdchangebase : forall (U:Type) (t:list U) (x y:U),
t<>nil -> hd x t=hd y t.

Lemma list_lastelim : forall (U:Type) (t:list U) (x a b:U),
last (a::b::t) x = last (b::t) x.

Lemma list_lastpushback : forall (U:Type) (t:list U) (x a:U),
last (list_pushback U t a) x = a.

Lemma list_lengthpushback : forall (U:Type) (t:list U) (a:U),
length (list_pushback U t a)=S (length t).

Lemma list_inpushback : forall (U:Type) (t:list U) (x a:U),
List.In x (list_pushback U t a)->
List.In x t \/ x=a.

Lemma list_inpushbackrev : forall (U:Type) (t:list U) (x a:U),
List.In x t -> List.In x (list_pushback U t a).

Lemma list_inpushbacknew : forall (U:Type) (t:list U) (a:U),
List.In a (list_pushback U t a).

Lemma list_foldleft_pushback : forall (U:Type) (f:Operation U)
(t:list U) (z a v:U),
fold_left f (list_pushback U t a) z = f (fold_left f t z) a.


End graphs.