Ssreflect Users Discussion List

[Laurent Thery <>]

Hi,

unfortunately most of the operation on matrix does not compute and
indices of matrices are ordinal and not nat that are not so direct to
manipulate.
Finally matrix are easily manipulated when you are working in a ring.
Here I rephrase how I will do your example in an arbitrary field.


====================================================


From mathcomp Require Import all_algebra all_ssreflect.

Section Example.

Local Open Scope ring_scope.
Import GRing.Theory.


Variable R : ringType.

Definition A1 : 'M[R]_(2,2) :=
  \matrix_(i<2,j<2)
    if (i == 0%N :> nat) then
     if (j == 0%N :> nat) then 1%:R else 2%:R
    else
     if (j == 0%N :> nat) then 3%:R else 4%:R.

Lemma A1_00 : A1 0 0 = 1%R.
Proof. by rewrite mxE. Qed.

Lemma trace_is_5: \tr A1 = 5%:R.
Proof.
(* unfold mxtrace *)
rewrite /mxtrace !big_ord_recl big_ord0 /=.
(* unfold index *)
rewrite !mxE /=.
(* compute sum *)
by rewrite addr0 -natrD.
Qed.

End Example.

====================================================

Hope this helps.

--
Laurent