Is it possible to get a plain `seq`

or `list`

from a mathcomp matrix representation using coqeal? I guess the seqmx part is for that?

How do we use that?

I tried:

```
From mathcomp Require Import all_ssreflect all_algebra.
Definition egmat: 'M[bool]_3 := \matrix_(i<3, j<3) (true).
From CoqEAL Require Import hrel param refinements trivial_seq.
From CoqEAL.refinements Require Import seqmx.
Definition egseq := mkseqmx_ord (fun_of_matrix egmat).
```

but `egseq`

had ssreflect stuff in it when I tried extracting it.

I'm not even sure what you are asking for makes any sense. Mathcomp matrices are abstract matrices. CoqEAL offers a refinement to lists of lists meaning you can use the latter to actually compute programs proved correct with the former. But all actual computation will eventually happen on lists of lists, not on mathcomp matrices. If ever you have some constant at some point in your program, you'll have, as part of the refinement proof of your program, to prove that the precise list of list used in the refined program is indeed a refinement of the mathcomp matrix in the abstract program.

What I wanted to do was to make some proof involving matrices. At first I tried using `Vector.t`

from stdlib, but that got complicated real quick.

Then I discovered mathcomp's matrices and proved some properties involving that.

Now, I wish to make the mathcomp matrix (abstract) into a more concrete (computable?) form (`seq`

).

Basically, I need a way to transport the theorems proven about the mathcomp matrices to the `seq (seq A)`

.

This is what refinement is about, right?

Sorry I'm still a beginner at this.

Then seqmx indeed contains a `seqmx_of_fun : forall n m, ('I_n -> 'I_m -> A) -> seq (seq A)`

(mathcomp matrices are coercible to functions `'I_n -> 'I_m -> A`

) and a proof that this matches its definition of refinement: https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v#L300-L316

My point was that, while this function exist it's inefficient and you probably don't want to really compute it, I see it more as a specification tool.

I got a matrix multiplication (as mathcomp `matrix`

terms) like:

```
Goal
let m1:'M[bool]_(1,2) := \row_i (if i == 0 then 1 else 0) in
let m2 := \col_i (if i == 0 then 1 else 0) in
let res := m1 *m m2 in
res == 1.
Proof.
rewrite //=.
(*
1 subgoal
========================= (1 / 1)
\row_i (if i == 0 then 1 else 0) *m \col_i (if i == 0 then 1 else 0) == 1
*)
```

If this was a computation friendly statement, this is trivially proven.

Can I convert to a computation friendly `seqmx`

representation and then solve the proof?

I mean, I was trying to understand how coqeal is meant to be used.

Coqeal does provide a refinement of matrix multiplication (from mathcomp matrices to lists of lists) but you also need to provide a refinement of your `m1`

and `m2`

to get something practically computable.

Could the refinement type be like this?

```
R: matrix A rows cols -> seq (seq A) -> Type
```

If that would work, how can it be made?

```
Definition matSeqR {A: Type} {rows cols: nat}
: matrix A rows cols -> seq (seq A) -> Type :=
fun mat sq => _.
```

What can be put in place of the hole here?

Is there a function that gives the value at the (i,j)-cell of a `seqmx`

in coqeal?

If there is one like `seq_ij`

, we could've had:

```
Definition matSeqR {A: Type} {rows cols: nat}
: matrix A rows cols -> seq (seq A) -> Type :=
fun mat sq => mat =2 (seq_ij sq).
```

Am I headed in the right direction here?

There is already a refinement in seqmx https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v#L300 you don't need to redefine it, you just need to instanciate it for your precise matrices (take for instance as exemple the 0 matrix: https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v#L357 )

Thanks.

Any idea where `nat_R`

used in that definition (`Rseqmx`

) is defined? It seems to be from CoqEAL but I can't find it.

I guess the purpose of `nat_R`

here is to refine `ordinal`

to `nat`

.

Probably, `About nat_R`

will tell you the file and I let you do a grep to find the precise place.

I had done both. But couldn't find it.

Closest match was `nat_Rxx`

.

At https://github.com/coq-community/coqeal/blob/1.1.3/refinements/param.v

```
Lemma nat_Rxx n : nat_R n n.
Proof.
elim: n=> [|n];
[ exact: nat_R_O_R | exact: nat_R_S_R ].
Qed.
```

And `Print`

shows the definition of `nat_R`

as:

```
Inductive nat_R : nat -> nat -> Set :=
nat_R_O_R : nat_R 0 0
| nat_R_S_R : forall H H0 : nat, nat_R H H0 -> nat_R H.+1 H0.+1.
```

Indeed, it's automatically generated by paramcoq with the command `Parametricity nat`

Ah..

Thanks.

Julin Shaji said:

I guess the purpose of

`nat_R`

here is to refine`ordinal`

to`nat`

.

This doesn't seem to be the case. `nat_R: nat -> nat -> Set`

.

What's the purpose of `nat_R`

here?

It's just a way to record that two nat are equal.

Pierre Roux said:

Indeed, it's automatically generated by paramcoq with the command

`Parametricity nat`

What's the purpose of auto-generating this `nat_R`

definition?

I mean, as you said, `nat_R n m`

seems to be a way of saying that `n = m`

.

Where is does come in useful?

As itself, it may indeed seem a bit dumb, but then it can be used to automatically derive parametricity relations for more complex definitions involving nat.

Found this in the 'refinements for free' paper:

https://inria.hal.science/hal-01113453/document

For now, we can only express and infer parametricity on polymorphic expressions (no dependent types allowed), by putting the polymorphic types outside

the relation. Hence we do not need to introduce a quantification over relations.

Does this mean that the parametricity relation technique will work only if the type is not a dependent type?

As in, this can't be done for a type like `forall ty: type, t ty`

?

Does this mean that the parametricity relation technique will work only if the type is not a dependent type?

CoqEAL offers a refinmement for mathcomp matrices which is a dependent type, so I'd say the answer to your question is no.

Last updated: Jul 25 2024 at 15:02 UTC