Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi,

  Your lemma coucou is an instance of lemma ffunE; lemma beuh is false unless 
s = 1, in which case it can be proved by move=> *; rewrite mxE perm1 eqxx.
  The documentation of a file lists the operations provided by the theory 
(well, for those file for which we've gotten around to write it). It is wise 
to use ONLY the operations that are listed, and not dive into the 
implementation details as you do in coucou: the intended constructor for 
matrices is matrix_of_fun, which locks out conversion simplification to try 
to curtail erratic behavior of the Coq kernel. Due to the poor design of the 
Coq module system we end up exporting the implementaion details, but that 
does not mean you're allowed to use them.
  The documentation doesn't list all the lemmas that are provided, as that 
would be tedious and redundant with the code. If you're going to use a 
theory, you should really browse through the coqdoc to see what's available. 
If you've respected the official interface, then what you need probably 
exists, either directly or as a simple combination (e.g., if coucou used 
\matrix_... then it would just be an instance of mxE).

   Georges

-----Original Message-----
From: Reynald Affeldt [] 
Sent: 17 June 2009 10:42
To: 
Subject: basic facts about matrices


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.