CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Leo Ducas, 2007-08-06
Describe the morphism between graph restricted to [0,n-1] and the corresponding boolean adjacency matrix of size n*n.

Set Implicit Arguments.

Module Export BMatrix := Matrix BOrdSemiRingT.

Definition of the graph of a boolean matrix

Section GoM.

Variable dim : nat.

Definition mat_unbound (M : matrix dim dim) i j :=
match le_gt_dec dim i with
| left _ => false
| right hi =>
match le_gt_dec dim j with
| left _ => false
| right hj => Vnth (Vnth M hi) hj
end
end.

Notation "z [[ x , y ]]" := (@mat_unbound z x y) (at level 30).

Definition GoM M x y := M[[x,y]] = true.

Basic properties

Section basic.

Variable M : matrix dim dim.

Lemma GoM_true_bounds : forall x y, GoM M x y -> x < dim /\ y < dim.

Lemma GoM_dec : forall x y, {GoM M x y} + {~GoM M x y}.

Lemma GoM_restricted : is_restricted (GoM M) (nats_decr_lt dim).

End basic.

Addition of matrix is union of relation

Section GoM_union.

Variables M N : matrix dim dim.

Lemma orb_matadd : forall x y, (M <+> N)[[x, y]] = M[[x, y]] || N[[x, y]].

Lemma Gmorph_plus : forall x y,
GoM (M <+> N) x y <-> ((GoM M) U (GoM N)) x y.

End GoM_union.

Product of matrix is composition of relation

Section GoM_Compose.

Variables M N : matrix dim dim.

Lemma existandb_dotprod : forall n (v w : vec n),
dot_product v w = true
<-> exists z, exists hz : z<n, Is_true (andb (Vnth v hz) (Vnth w hz)).

Lemma existandb_matmult : forall x y,
(M <*> N)[[x, y]] = true <-> exists z, M[[x,z]] && N[[z,y]] = true.

Lemma Gmorph_mult : forall x y,
GoM (M <*> N) x y <-> (GoM M @ GoM N) x y.

End GoM_Compose.

Exponentiation of matrix is iteration of relation

Section GoM_Iter_le.

Variable M : matrix dim dim.

Fixpoint mat_exp_fast (M : matrix dim dim) n :=
match n with
| O => M
| S i => let N := @mat_exp_fast M i in (N <+> id_matrix dim) <*> N
end.

Lemma mat_id_spec : forall x y,
(id_matrix dim)[[x,y]] = true <-> x=y /\ x<dim /\ y<dim.

Lemma G_morph_id : forall x y,
GoM (id_matrix dim) x y <-> x=y /\ x<dim /\ y<dim.

Lemma Gmorph_iter_le_fast : forall n x y,
GoM (mat_exp_fast M n) x y <-> iter_le_fast (GoM M) n x y.

High enough exponentiation is transitive closure

Lemma Gmorph_clos_trans : forall x y,
GoM (mat_exp_fast M (S (log2 dim))) x y <-> GoM M! x y.

End GoM_Iter_le.

Tranposition of matrix is transposition of relation

Section GoM_transpose.

Variable M : matrix dim dim.

Lemma transp_mat_unbound : forall x y, M[[x,y]] = (mat_transpose M)[[y,x]].

Lemma Gmorph_transpose : forall x y,
GoM (mat_transpose M) x y <-> transp (GoM M) x y.

End GoM_transpose.

The "and" of matrix (element by element) is intersection of relation

Section GoM_intersection.

Variable M N : matrix dim dim.

Definition mat_andb := Vmap2 (Vmap2 andb (n := dim)) (n := dim).

Lemma andb_mat_unbound : forall x y,
(mat_andb M N)[[x,y]] = M[[x,y]] && N[[x,y]].

Lemma Gmorph_intersect : forall x y,
GoM (mat_andb M N) x y <-> GoM M x y /\ GoM N x y.

End GoM_intersection.

Exponentation, transposition, AND of the matrix, gives the SCC of the relation

Section GoM_SCC.

Definition SCC_mat M :=
let N := mat_exp_fast M (S(log2 dim)) in
mat_andb N (@mat_transpose dim dim N).

Variable M : matrix dim dim.

Lemma GoM_SCC : forall x y, GoM (SCC_mat M) x y <-> SCC (GoM M) x y.

End GoM_SCC.

End GoM.

Notation "z [[ x , y ]] " := (@mat_unbound _ z x y) (at level 30).

Section MoG.

Variable dim : nat.
Variable R : relation nat.
Variable R_dec : forall x y, {R x y} + {~R x y}.

Definition MoG := @mat_build dim dim
(fun x y _ _ =>
match R_dec x y with
| left _ => true
| right _ => false
end).

Variable hyp : forall x y, R x y -> x < dim /\ y < dim.

Lemma GoM_MoG : forall x y, GoM MoG x y <-> R x y.

End MoG.