Library CayleyGraph

Section CayleyGraphs.

Require Import graphs.
Require Import Groups.
Require Import EnsembleFacts.

Require Import Coq.Lists.List.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Classical.
Require Import Coq.Sets.Finite_sets_facts.
Require Import Coq.Arith.Arith.

Inductive CayleyGraph (U:Type) (f:Operation U) (A:Ensemble U)
:Graph U:=
| In_CayleyGraph : forall v a:U,
   In U A a ->
   In (dtype U) (CayleyGraph U f A) (v, f v a).
Check CayleyGraph_ind.

Theorem In_CayleyGraph_rec :
forall (U:Type) (f:Operation U) (A:Ensemble U) (v w:U),
 In (dtype U) (CayleyGraph U f A) (v, w)
 -> exists a:U, w=f v a /\ In U A a.

Theorem In_CayleyGraph_recgroup :
forall (U:Type) (f:Operation U) (A:Ensemble U) (v a:U),
Group U f->
 In (dtype U) (CayleyGraph U f A) (v, f v a)
 -> In U A a.

Theorem CayleyGraph_addleftisiso : forall (U:Type) (f:Operation U)
(A:Ensemble U) (a:U), Group U f->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A)
(fun x:U=> f a x).

Theorem CayleyGraph_vertexsymmetric :
forall (U:Type) (f:Operation U) (A:Ensemble U),
Group U f-> vertexsymmetric U (CayleyGraph U f A).

Theorem CayleyGraph_opp :
forall (U:Type) (f:Operation U) (A:Ensemble U),
Group U f->
(forall a ia:U, In U A a -> Inverse U f a ia -> In U A ia)
-> Undirected U (CayleyGraph U f A).

Theorem CayleyGraph_opp_rec :
forall (U:Type) (f:Operation U) (A:Ensemble U),
Group U f-> Undirected U (CayleyGraph U f A) ->
(forall a ia:U, In U A a -> Inverse U f a ia -> In U A ia).

Theorem CayleyGraph_isoadjacencies :
forall (U1 U2:Type) (f1:Operation U1) (f2:Operation U2)
(A1:Ensemble U1) (A2:Ensemble U2) (i:U1->U2) (zero1:U1) (zero2:U2),
Group U1 f1-> Group U2 f2 ->
Identity U1 f1 zero1 -> Identity U2 f2 zero2 ->
Isomorphism U1 U2 (CayleyGraph U1 f1 A1) (CayleyGraph U2 f2 A2) i->
i zero1 = zero2 -> A2=apply_func U1 U2 i A1.

Lemma CayleyGraph_isoIn :
forall (U1 U2:Type) (f1:Operation U1) (f2:Operation U2)
(A1:Ensemble U1) (A2:Ensemble U2) (i:U1->U2) (zero1:U1) (zero2:U2)
(a:U1),
Group U1 f1-> Group U2 f2 ->
Identity U1 f1 zero1 -> Identity U2 f2 zero2 ->
Isomorphism U1 U2 (CayleyGraph U1 f1 A1) (CayleyGraph U2 f2 A2) i->
i zero1 = zero2 -> In U1 A1 a -> In U2 A2 (i a).

Theorem CayAbel_inversioniso:
forall (U:Type) (f:Operation U) (A:Ensemble U) (s:U->U),
AbelianGroup U f -> Undirected U (CayleyGraph U f A) ->
Group_Inversion U f s ->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A) s.

Lemma CayAbel_addrightisiso : forall (U:Type) (f:Operation U)
(A:Ensemble U) (a:U), AbelianGroup U f->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A)
(fun x:U=> f x a).

Theorem CayleyGraph_StronglyConnected:
forall (U:Type) (f:Operation U) (A:Ensemble U) (zero v:U),
Group U f-> StronglyConnected U (CayleyGraph U f A) ->
Identity U f zero ->
exists l:list U,
(forall a:U, List.In a l -> In U A a) /\
fold_left f l zero =v.


Definition CayAbel_without_nontrivial4cycles
(U:Type) (f:Operation U) (A:Ensemble U)
:= forall (a b c d zero:U),
AbelianGroup U f
-> Identity U f zero ->
In U A a -> In U A b -> In U A c -> In U A d ->
f a (f b (f c d))=zero ->
(f a b=zero \/ f a c=zero \/ f a d=zero).

Lemma CayleyGraph_CommonNeighborhood :
forall (U:Type) (f:Operation U) (A:Ensemble U) (a b x:U),
In U (CommonNeighborhood U (CayleyGraph U f A) a b) x ->
exists v:U, exists w:U, x=f a v /\ x=f b w
/\ In U A v /\ In U A w.

Theorem CayAbel_wont4c_common :
forall (U:Type) (f:Operation U) (A:Ensemble U) (zero:U),
AbelianGroup U f-> Undirected U (CayleyGraph U f A) ->
CayAbel_without_nontrivial4cycles U f A ->
Identity U f zero->
forall a b:U, In U A a -> In U A b -> a<>b ->
 CommonNeighborhood U (CayleyGraph U f A) a b
 = Couple U zero (f a b).

Theorem CayAbel_wont4c_edgecomm_iso :
forall (U1 U2:Type) (f1:Operation U1) (f2:Operation U2)
(A1:Ensemble U1) (A2:Ensemble U2) (i:U1->U2)
(zero1:U1) (zero2:U2) (a b:U1),
AbelianGroup U1 f1-> AbelianGroup U2 f2 ->
Identity U1 f1 zero1 -> Identity U2 f2 zero2 ->
Undirected U1 (CayleyGraph U1 f1 A1) ->
Undirected U2 (CayleyGraph U2 f2 A2) ->
CayAbel_without_nontrivial4cycles U1 f1 A1 ->
CayAbel_without_nontrivial4cycles U2 f2 A2 ->
Isomorphism U1 U2 (CayleyGraph U1 f1 A1) (CayleyGraph U2 f2 A2) i->
i zero1 = zero2 -> In U1 A1 a -> In U1 A1 b -> a<>b ->
i (f1 a b)=f2 (i a) (i b).

Lemma CayAbel_wont4c_ft :
forall (U:Type) (f:Operation U) (A:Ensemble U) (i s:U->U)
(zero:U) (t:U),
AbelianGroup U f-> Identity U f zero ->
Undirected U (CayleyGraph U f A) ->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A) i->
i zero = zero ->
Group_Inversion U f s ->
exists ft,
 (ft=fun v:U=> f (i(f t v)) (s (i t)))/\
 Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A) ft /\
 ft zero=zero.

Lemma CayAbel_wont4c_transcomm :
forall (U:Type) (f:Operation U) (A:Ensemble U) (i:U->U)
(zero:U) (t a b:U),
AbelianGroup U f-> Identity U f zero ->
Undirected U (CayleyGraph U f A) ->
CayAbel_without_nontrivial4cycles U f A ->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A) i->
i zero = zero -> In U A a -> In U A b ->
f (i(f t (f a b))) (i t) =f (i(f t a)) (i(f t b)).

Lemma fold_left_zero: forall (U:Type) (f:Operation U)
(T:list U) (zero a:U), Identity U f zero ->
Associativity U f ->
fold_left f T (f zero a) = f a (fold_left f T zero).

Theorem CayAbel_wont4c_linear :
forall (U:Type) (f:Operation U) (A:Ensemble U) (i:U->U)
(zero:U) (v w:U),
AbelianGroup U f-> Identity U f zero ->
Undirected U (CayleyGraph U f A) ->
CayAbel_without_nontrivial4cycles U f A ->
StronglyConnected U (CayleyGraph U f A) ->
Isomorphism U U (CayleyGraph U f A) (CayleyGraph U f A) i->
i zero = zero ->
i(f v w)=f (i v) (i w).

Print Assumptions CayAbel_wont4c_linear.

End CayleyGraphs.