## Stream: math-comp users

### Topic: [coqeal] Getting plain `seq` from matrix

#### Julin Shaji (Oct 18 2023 at 05:41):

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.

#### Pierre Roux (Oct 18 2023 at 14:37):

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.

#### Julin Shaji (Oct 19 2023 at 06:27):

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.

#### Pierre Roux (Oct 19 2023 at 09:17):

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.

#### Julin Shaji (Oct 25 2023 at 09:14):

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?

#### Julin Shaji (Oct 25 2023 at 09:14):

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

#### Pierre Roux (Oct 25 2023 at 09:55):

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.

#### Julin Shaji (Oct 25 2023 at 10:24):

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?

#### Pierre Roux (Oct 25 2023 at 10:39):

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 )

#### Julin Shaji (Oct 25 2023 at 11:03):

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.

#### Julin Shaji (Oct 25 2023 at 11:04):

I guess the purpose of `nat_R` here is to refine `ordinal` to `nat`.

#### Pierre Roux (Oct 25 2023 at 11:06):

Probably, `About nat_R` will tell you the file and I let you do a grep to find the precise place.

#### Julin Shaji (Oct 25 2023 at 11:07):

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

#### Julin Shaji (Oct 25 2023 at 11:07):

Closest match was `nat_Rxx`.

#### Julin Shaji (Oct 25 2023 at 11:09):

``````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.
``````

#### Pierre Roux (Oct 25 2023 at 11:10):

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

Ah..

Thanks.

#### Julin Shaji (Oct 25 2023 at 11:45):

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`.

#### Julin Shaji (Oct 25 2023 at 14:27):

What's the purpose of `nat_R` here?

#### Pierre Roux (Oct 25 2023 at 14:55):

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

#### Julin Shaji (Apr 10 2024 at 09:42):

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?

#### Pierre Roux (Apr 10 2024 at 09:45):

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.

#### Julin Shaji (Apr 17 2024 at 10:57):

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`?

#### Pierre Roux (Apr 17 2024 at 11:12):

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