Ssreflect Users Discussion List

[Sidi Ould Biha <>]

Hi,

The standard (and recommended) way of defining a matrix is by using the 
constructor \matrix_(i < n , j < m) f which take a function f of type : 
I_n -> I_m -> R and return a n x m matrix. When you write A i j for a 
matrix A there is a hidden coercion from the matrix type to FunClass. A 
i j mean (fun_of_matrix A) i j. By using the Lemma mxE if A is = 
\matrix_(i, j) f, you will get that (\matrix_(i, j) f) i j = f i j.

So a way to proof the coucou Lemma is the following :
Lemma coucou : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) j,
 Matrix [ffun ij => z ij.1 (s ij.2)] 0 j = z 0 (s j).
Proof.
move=> F n s z j.
set A := (Matrix [ffun ij => z ij.1 (s ij.2)]).
by suff -> : A = \matrix_(i, j) z i (s j); [rewrite mxE | unlock 
matrix_of_fun].
Qed.

But for the beuh Lemma you have to prove the following goal :

Lemma beuh : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) i j,
 (\matrix_(i0, j0) (if s i0 == j0 then 1 else 0)) i j =
 if s i == j then 1 else (1 : F).
Proof.
move=> F n s z i j; rewrite mxE.
----
(if s i == j then 1 else 0) = (if s i == j then 1 else 1)



Reynald Affeldt wrote:
> Hello,
>
> I am afraid it is an easy question that just reveals my lack
> of understanding.
> How am I supposed to prove the following facts?
>
>     Reynald
>
> --
>
> Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq fintype finfun 
> finset prime.
> Require Import groups zmodp ssralg perm matrix bigops.
>
> Open Local Scope ring_scope.
>
> Lemma coucou : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) j,
>   Matrix [ffun ij => z ij.1 (s ij.2)] 0 j = z 0 (s j).
> Proof.
> Abort.
>
> Lemma beuh : forall (F : fieldType) n (s : 'S_n) (z : matrix F 1 n) i j,
>   (\matrix_(i0, j0) (if s i0 == j0 then 1 else 0)) i j = if s i == j then 
> (GRing.one F) else (GRing.one F).
> Proof.
> Abort.
>
>
>   

--
Sidi