Ssreflect Users Discussion List

[Georges Gonthier <>]

  The current interface is a compromise:  the weaker interface you propose would be more general , but would support fewer results and constructions (no polynomials!), and having two interfaces as you suggest would complicate the library, and possibly stress the Coq kernel beyond its breaking point (which we are approaching dangerously in the upper tiers of the library). On the longer term, and with a better implementation of Coq, you are most probably right.

  Cheers,

Georges

 

From: Guillaume Cano [mailto:]
Sent: 28 March 2012 17:25
To:
Subject: ring structure and matrices

 

Hi,

In order to instantiate a ringType structure, we have to provide a proof that 0 != 1.
This implies that only square matrices of size n.+1 are a ringType.

So we cannot use the definitions of ssralg for a general matrix.
For example, I want to write :  A ^+ k for a matrix A.

Here A is a block diagonal matrix defined as follows :

Fixpoint diag_block_mx (l : seq {n : nat & 'M[R]_n}) :  'M[R]_(sizemx l) :=
  match l return 'M[R]_(sizemx l) with
  | nil => 0
  | existT p M :: tl => block_mx M 0 0 (diag_block_mx tl)
  end.

where sizemx is a function that returns the dimension of the block diagonal matrices.
sizemx is the sum of all dimensions of the matrices in the sequence l.

It is difficult to express the type of this matrix like sth.+1.
So I cannot write A ^+ k, and in our context using castmx is not simple.


So my question is why don't we have structures like :

ring1Type with a mixin like

Record mixin_of (R : zmodType) : Type := Mixin {
  one : R;
  mul : R -> R -> R;
  _ : associative mul;
  _ : left_id one mul;
  _ : right_id one mul;
  _ : left_distributive mul +%R;
  _ : right_distributive mul +%R;
}.

....

And  an another structure

ring2Type with a mixin like
 
 Definition mixin_of  (R : ring1type) := 0 != 1.
 
....

With such a structure, general square matrices have the structure of ring1type,
and so I can use the operators defined for ring1Type.
and if I can prove that 0 != 1 then I have a ring2Type structure.

I could define a function expmx  for exponentiation of general square matrices and use it,
but the problem remains for other functions defined with ring operators of ssralg.
For example, I can't use horner_mx for the same reason.

Best,
Guillaume.