Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finset zmodp matrix bigop ssralg.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.
Open Local Scope ring_scope.

Section Exercise.

(*********************************************************************)
(* Define the following matrices over an arbitrary ring R            *)
(* - A row matrice Rn of length n that has a 1 as its last element   *)
(*   all the other being 0s, for n = 4 this gives [0 0 0 1]          *)
(* - A column matrice Cn of length n that has a 1 as its last element*)
(*   all the other being 0s, for n = 4 this gives [0                 *)
(*                                                 0                 *)
(*                                                 0                 *)
(*                                                 1]                *)
(*                                                                   *)
(* - A square matrice Xn of length n that has 1s on the main diagonal*)
(*   and the right and bottom borders all the others being 0s,       *)
(*   for n = 4 this gives                         [1 0 0 1           *)
(*                                                 0 1 0 1           *)
(*                                                 0 0 1 1           *)
(*                                                 1 1 1 1]          *)
(*                                                                   *)
(* Hints : use the \row_ (_ < _) _, \col_ (_ < _) _,                 *)
(*                 \matrix_ (_ < _) (_ < _)                          *)
(* For Xn, give a direct definition and a recursive one using blocks *)
(* (for advanced users prove the equality of the two definitions)    *)
(* Hints : use block_mx the for definition                           *)
(*         and the theorems mxE split1 unliftP for the proof         *)
(*********************************************************************)

Variable R : ringType.

Definition Rn (n: nat) : 'rV[R]_n := \row_(i < n) (n.-1 == i)%:R.

Definition Cn (n: nat) : 'cV[R]_n := \col_(j < n) (n.-1 == j)%:R.

Definition Xn (n: nat) : 'M[R]_n := 
  \matrix_ (i < n, j < n) ((i == j) || (n.-1 == i) || (n.-1 == j))%:R.

Fixpoint XnR (n : nat) : 'M[R]_n :=
  if n is n1.+1 then block_mx 1 (Rn n1) (Cn n1) (XnR n1) else 0.

Lemma XnEXnR n : Xn n = XnR n.
Proof.
elim: n => [| n IH /=]; first by rewrite !thinmx0.
rewrite -{}IH; case: n => [|n]; apply/matrixP=> i j;
    rewrite ?mxE split1; case: unliftP => [i1 ->|->] /=;
    rewrite ?mxE split1; case: unliftP => [j1 ->|->] /=;
    rewrite -?IH ?mxE ?orbF //; try by case: i1=> [] [].
by case: j1=> [] [] //.
Qed.

(*********************************************************************)
(*                                                                   *)
(* Given an arbitrary matrix A, write a function msum that sums of   *)
(* elements of A,  show that                                         *)
(* - the msum of the sum of two matrices A B is the sum of msum of A *)
(*    and the msum of B                                              *)
(* - the msums of a matrix and of its  transpose are equal           *)
(*                                                                   *)
(* Hints use the bigop operation \sum_(_ < _) _ for the definition   *)
(*       use the theorems for the proof mxE big_split eq_bigr        *)
(*********************************************************************)


Definition msum m n (A : 'M[R]_(m,n)) := \sum_(i < m) \sum_(j < n) A i j.

Lemma add_msum m n (A B : 'M_(m, n)) : msum (A + B) = msum A + msum B.
Proof.
rewrite -big_split; apply: eq_bigr => i _ /=.
rewrite -big_split; apply: eq_bigr => j _ /=.
by rewrite mxE.
Qed.

Lemma transpose_msum m n (A : 'M_(m, n)) : msum A^T = msum A.
Proof.
rewrite /msum exchange_big /=.
by apply: eq_bigr => i _; apply: eq_bigr => j _; rewrite !mxE.
Qed.

End Exercise.