Ssreflect Users Discussion List

[Vladimir Komendantsky <>]

On 15 February 2011 15:34, Georges Gonthier <> wrote:

  The new library has functions mxvec and vec_mx that convert ‘M_(m, n) to ‘rV(m * n) and back. If you absolutely want a list you could also cross abstraction layers, since matrices are represented as finfuns themselves represented as tuples which in turn are represented as lists. So, if A : ‘M_(m, n), then val (val (val A)) is the seq that lists the actual contents of A.

   Note that the new library also has functions that convert row vectors to polynomials and conversely (rVpoly and poly_rV).

Thanks for this. It's not clear whether sequences are better for my purposes than vectors. In fact the cells of the matrix also contain sequences at the moment. It's not as easy as it first appears to evaluate the contents of a matrix cell! For example:

Lemma mx_nils : forall (T : eqType) m n (i : 'I_m) (j : 'I_n) (t : T),
  t \in Matrix [ffun=> [::]] i j = false.

(* The rewrite fails! Error: no valid match of RHS of fgraph_map *)
move=> T m n i j t. rewrite -fgraph_map.

I tried to evaluate under the coinductive constructor Matrix but this doesn't help since forcing evaluation and simplifying seems to end up with the term we started from.

Can there be a solution?

Many thanks,
Vladimir