Library graphs
Require Import ssreflect.
Require Import ssrbool.
Require Import ssrfun.
Require Import eqtype.
Require Import seq.
Require Import fintype.
Require Import ssrnat.
Require Import general.
Require Import finfun.
Require Import fingroup.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Opaque fgraph_of_fun cyclicgroup tuplegroup.
Section Graphs.
Record graph : Type := mkGraph {
vertices:> finType;
node_s: vertices;
node_t: vertices;
edgegroup: finGroupType;
eg_order: nat;
eg_orderP: forall d:edgegroup, order eg_order d;
eg_order_positive: 0 < eg_order;
act: groupAction edgegroup vertices;
act_free: free act;
degree: nat;
edges: (ordinal degree) -> edgegroup
}.
Variable G: graph.
Definition mk_ord(n:nat): nat -> option (ordinal n).
move=>n k.
case U: (k < n).
exact (Some (Ordinal U)).
exact None.
Defined.
Definition edge_of_nat(n:nat): edgegroup G :=
match (mk_ord (degree G) n) with
| Some e => edges e
| None =>
match (mk_ord (degree G) (n - (degree G))) with
| Some e => inv (edges e)
| None => unit _
end
end.
End Graphs.
Section CayleyGraph.
Variable G: finGroupType.
Variable m: nat.
Variable m_positive: 0 < m.
Variable order_G: forall g:G, order m g.
Variable gens_G: seq G.
Variable generators_G: generators gens_G.
Definition vertices_CG := G.
Definition node_s_CG := unit G.
Definition node_t_CG := unit G.
Definition edgegroup_CG := G.
Definition eg_order_CG := m.
Definition eg_orderP_CG := order_G.
Definition eg_order_positive_CG := m_positive.
Definition act_CG : groupAction edgegroup_CG vertices_CG.
by apply (@GroupAction edgegroup_CG vertices_CG (fun v x => mul v x));
move=>*; rewrite ?unitrP ?mulP.
Defined.
Lemma act_free_CG: free act_CG.
Proof. by move=>v g H; apply/eqP; apply (cancelr H). Qed.
Definition degree_CG := size gens_G.
Definition edges_CG: (ordinal degree_CG) -> edgegroup_CG :=
fun i => sub (unit G) (gens_G) i.
Definition cayleyGraph: graph :=
(@mkGraph vertices_CG node_s_CG node_t_CG edgegroup_CG
eg_order_CG eg_orderP_CG eg_order_positive_CG
act_CG act_free_CG degree_CG edges_CG).
End CayleyGraph.
Section GraphCR.
The graphs G_{m,d} of Cook & Rackoff, as described in the paper.
Variable d m:nat.
Variable m_greater_one: 1 < m.
Lemma m_positive: 0< m.
Proof. by apply: (leq_trans _ m_greater_one). Qed.
Definition graphCR : graph.
apply (cayleyGraph
(G := tuplegroup d (cyclicgroup m_positive))
(m := m)).
by apply: m_positive.
by apply: order_tuplegroup=>x; apply order_cyclicgroup.
apply (gens_tuplegroup d (gens_cyclicgroup m_positive m_greater_one)).
Defined.
End GraphCR.
Section GraphU.
The graphs H_{m,d} from the paper.
They are called U here, since H is often used for `hypothesis'.
Variable m d:nat.
Variable m_greater_one: 1 < m.
Lemma m_posU: 0< m. Proof. by apply: (leq_trans _ m_greater_one). Qed.
Definition gens_U := gens_wp
(gens_tuplegroup d (gens_cyclicgroup m_posU m_greater_one))
(gens_cyclicgroup m_posU m_greater_one).
Definition graphU : graph.
apply (cayleyGraph (G:= wp (tuplegroup d (cyclicgroup m_posU)) (cyclicgroup m_posU)) (m:=m*m)).
by apply: (leq_trans m_posU _); rewrite -{1}(muln1 m) leq_mul2l; apply/orP; right; apply: m_posU.
apply: order_wp.
apply: order_tuplegroup=>x; apply order_cyclicgroup.
apply: order_cyclicgroup.
apply: comm_cyclicgroup.
apply: gens_U.
Defined.
To show that we haven't cheated in this definition and that this
really is a graph of small degree, we give a proof that the number
of generators is as small as claimed in the paper.
Lemma gensU: size gens_U = d + 1.
Proof. by rewrite /gens_U size_gens_wp size_gens_tuplegroup size_gens_cyclicgroup muln1. Qed.
End GraphU.