Stream: math-comp users

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


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Julin Shaji (Oct 25 2023 at 09:14):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 )

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:04):

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

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:07):

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

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:07):

Closest match was nat_Rxx.

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:09):

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.

view this post on Zulip Pierre Roux (Oct 25 2023 at 11:10):

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

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:10):

Ah..

view this post on Zulip Julin Shaji (Oct 25 2023 at 11:10):

Thanks.

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Oct 25 2023 at 14:27):

What's the purpose of nat_R here?

view this post on Zulip Pierre Roux (Oct 25 2023 at 14:55):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Julin Shaji (Apr 17 2024 at 10:57):

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?

view this post on Zulip 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