Simplifying your goal should evaluate the hidden fun_of_matrix coercion and expose the fun_of_ffun coercion, which can be expanded with the ffunE lemma:
rewrite /=. (* (t \in [ffun=> [::]] (i, j)) = false *)
rewrite ffunE. (* (t \in [::]) = false *)
by []. (* or by rewrite inE *)
However, the lemma for evaluating matrix expressions is mxE, and it expects the matrix_of_fun derived constructor, not the primitive Coq Matrix one. The normal
syntax for matrix_of_fun is \matrix_(i < m, j < m) [::] (this will not display correctly because of a design flaw in the Coq term display procedure), though here you could simply write const_mx [::].
Although they are in principle effective, the matrix_of_fun and ffun constructors are “locked” to stop the Coq kernel from crashing (this fix is, unfortunately,
only partly effective, and I’m constantly fighting off divergence). Thus, evaluation/simplification will do nothing.
I strongly suggest you read through the internal documentation of the libraries you’re trying to use, as this will tell you what the proper interfaces are.
Trying to bypass them by using directly Coq primitives will make it difficult to use the rest of the library, and could expose you to some of the nasty performance problems that the library implementation tries to solve or mitigate.
Cheers,
Georges
From: Vladimir Komendantsky [mailto:]
Sent: 17 February 2011 12:21
To: ssreflect
Subject: Re: matrix to seq
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
