Library circulant

Print LoadPath.

Require Import ZArith.
Open Local Scope Z_scope.
Require Import Coq.Sets.Ensembles.

Require Import graphs.
Require Import Zmod.

Definition pZmN (N:Z) := ((ZmodN N)*(ZmodN N))%type.
Inductive Circulant (N:Z) (A:Ensemble (Z))

:Graph (ZmodN N) :=
| In_Circulant :forall n a:(Z),
   In (Z) A a ->
   In (pZmN N) (Circulant N A)
      (Zmod N n,Zmod N (n+a)).
Print Circulant_ind.

Theorem In_Circulant_rec : forall (N:Z) (A:Ensemble (Z)),
forall n a:(Z),
   In (pZmN N) (Circulant N A)
      (Zmod N n,Zmod N (n+a))
   ->exists b, Zmod N a=Zmod N b /\In (Z) A b.

Print Circulant.

Theorem Circulant_opp : forall N:Z, forall A:Ensemble Z,
(forall n:Z, In Z A n -> In Z A (-n))
-> Undirected (ZmodN N) (Circulant N A).

Theorem Circulant_vertexsymmetric : forall (N:Z) (A:Ensemble (Z)),
vertexsymmetric (ZmodN N) (Circulant N A).