Stream: math-comp users

Topic: Matrix representation


view this post on Zulip Julin Shaji (Oct 03 2023 at 15:49):

Hi. I was trying to have a representation of matrices using mathcomp and upon searching online, came across:
https://github.com/VeriNum/LAProof/blob/main/floatlib.v

It had this definition for matrix:

Definition matrix t := list (list (ftype t)).

But I wasn't sure I understood it properly.
Doesn't this line mean that matrix t is a list of lists where t is a finite type?
Does that also somehow constraint it to be a proper matrix? As in every row has same number of elements?

view this post on Zulip Julin Shaji (Oct 03 2023 at 15:52):

Oh.. I guess the proof is made from here:
https://github.com/verified-network-toolchain/Verified-FEC/blob/cav22/proofs/Matrix/ListMatrix.v#L392

Definition rect {A} (l: list (list A)) m n : Prop :=
  Zlength l = m /\ 0 <= n /\ Forall (fun x => Zlength x = n) l.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 15:55):

Hi @Julin Shaji , math-comp matrices are defined in https://math-comp.github.io/htmldoc_2_0_0/mathcomp.algebra.matrix.html

view this post on Zulip Emilio Jesús Gallego Arias (Oct 03 2023 at 15:57):

See also the math-comp book , as pointed out in the other thread, section 7.8 explains how matrices are built

view this post on Zulip Julin Shaji (Oct 09 2023 at 05:55):

To get the notations for matrix, do we need to import some module?

I tried:

From mathcomp Require Import all_ssreflect all_algebra.

Compute \matrix_(i<3, j<7) if i==j then 1 else 0.
(*
Unknown interpretation for notation "\matrix_ ( _ < _ , _ < _ ) _".
*)

but that's giving error.

view this post on Zulip Julin Shaji (Oct 09 2023 at 05:56):

Opening ring_scope changes the error to:

Local Open Scope ring_scope.

Compute \matrix_(i<3, j<7) if i==j then 1 else 0.
(*
In environment
i : ordinal_finType 3
j : ordinal_finType 7
The term "j" has type "Finite.sort (ordinal_finType 7)"
while it is expected to have type "Equality.sort (ordinal_finType 3)".
*)

view this post on Zulip Julin Shaji (Oct 09 2023 at 05:59):


Compute \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0). worked though.

view this post on Zulip Julin Shaji (Oct 09 2023 at 06:01):

But that seems to leave holes.

view this post on Zulip Julin Shaji (Oct 09 2023 at 06:15):

Example eg1 := \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0).
(*
The following term contains unresolved implicit arguments:
  (\matrix_(_, _) (fun i0 j0 : ?T =>
                   if i0 == j0 as x return ?t@{i:=i0; j:=j0; b:=x}
                   then 1
                   else 0))
More precisely:
- ?T: Cannot infer the implicit parameter T of eq_op whose type is "eqType".
- ?t: Cannot infer ?t in the partial instance "GRing.Ring.sort ?t" found for
  this placeholder of type "Type" in environment:
  i, j : ?T
  b : bool
*)

view this post on Zulip Quentin VERMANDE (Oct 09 2023 at 07:05):

The notation is indeed in ring_scope, there is nothing more to import. In the second code snippet, the problem is that the types of i and j mismatch (and Coq can't coerce between 'I_3 and 'I_7), "(i : nat) == j" or "(i == j :> nat)" would work (and you need to give the type of 1 and/or 0) . In the last one, I think the underscores mean that the arguments are not used. The error is that, since you re-bind i and j when declaring the function, Coq does not know what type to give them (and it does not know what the return type should be either).

view this post on Zulip Julin Shaji (Oct 09 2023 at 07:33):

I tried this but got error:

Fail Compute \matrix_(i<3, j<7) if (i:nat)==j then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=(i : nat) == j}" (cannot satisfy
constraint "?t0" == "?t@{b:=(i : nat) == j}").
*)
Fail Compute \matrix_(i<3, j<7) if (i==j :> nat) then 1 else 0.
(*
The command has indeed failed with message:
In environment
i : ordinal_finType 3
j : ordinal_finType 7
Unable to unify "?t0" with "?t@{b:=i == j :> nat}" (cannot satisfy constraint
"?t0" == "?t@{b:=i == j :> nat}").
*)

Is this not what was meant?

From the error, I suppose i is of type 'I_3 and j is of type 'I_7. And the type mismatch is what's causing the problem (I guess that's what was mentioned as well). Is it so?

view this post on Zulip Julin Shaji (Oct 09 2023 at 07:34):

Quentin VERMANDE said:

and you need to give the type of 1 and/or 0

You mean that of a ring or is this something different?

view this post on Zulip Pierre Roux (Oct 09 2023 at 07:49):

In ring_scope, 1 and 0 are the units of some ring so you need to precise which one. For instance

Section Mat.
Variable R : ringType.
Check \matrix_(i<3, j<7) if i == j :> nat then 1 : R else 0.

view this post on Zulip Pierre Roux (Oct 09 2023 at 07:50):

(but I agree the error message is not very informative)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 09 2023 at 16:04):

Indeed these kind of problems are really off putting for beginners, I wonder if we could add some custom error rules as to help with the messages?

view this post on Zulip Michael Soegtrop (Oct 10 2023 at 06:26):

Some example files might also help ...

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

Another doubt.

How can a \matrix be converted to a seq (seq))? Do we have to use coqEAL library for that or is it doable using mathcomp alone?

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

Been trying to read https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v for a while but didn't pull through all of it..

view this post on Zulip Cyril Cohen (Oct 10 2023 at 10:28):

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

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

How can we get the function used to build the matrix in \matrix?

view this post on Zulip Cyril Cohen (Oct 10 2023 at 10:28):

examples of usage are near the end of the file: https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v#L1380-L1472

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

Cyril Cohen said:

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

Concrete as in matrices whose dimensions have been predecided?

view this post on Zulip Cyril Cohen (Oct 10 2023 at 10:29):

Julin Shaji said:

How can we get the function used to build the matrix in \matrix?

It's matrix_of_fun

view this post on Zulip Cyril Cohen (Oct 10 2023 at 10:31):

Julin Shaji said:

Cyril Cohen said:

Indeed for now the only library I know that performs that is CoqEAL but it's limited to computations of concrete matrices.

Concrete as in matrices whose dimensions have been predecided?

Concrete as in a closed term: dimensions are concrete fixed numbers, and the general term is a function that uses no other variable than the two indices

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

Cyril Cohen said:

Julin Shaji [said](https://coq.zulipchat.com/#narrow/stream/237664-math-comp-

It's matrix_of_fun

Okay, so the other way must be fun_of_matrix. :+1:

view this post on Zulip Cyril Cohen (Oct 10 2023 at 10:38):

Julin Shaji said:

Cyril Cohen said:

Julin Shaji [said](https://coq.zulipchat.com/#narrow/stream/237664-math-comp-

It's matrix_of_fun

Okay, so the other way must be fun_of_matrix. :+1:

Ah sure, I misread your question. This function is actually a coercion btw.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 10 2023 at 11:53):

Indeed @Julin Shaji you don't need to use fun_of_matrix usually, Coq should be smart and insert it for you.

The way this works is that when you write

n : nat, A : 'M_n, i j : 'I_n |- A i j

Coq will fail to typecheck the application A i j , however, the coercion mechanism knows that it can insert fun_of_matrix to try to repair the problem, so indeed, Coq will automatically convert A i j to fun_of_matrix A i j.

fun_of_matrix is not displayed by default, but can do so if you wish.

view this post on Zulip Julin Shaji (Oct 12 2023 at 16:26):

Given a 'M[R]_(n,m), is there a way to get the (i, j)-th element of it?

I tried A i j, but that gives a big term. Is there a way to get a 'slim' form with just the element?
Just to see it.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:28):

Hi @Julin Shaji , does rewrite !mxE improve what you see?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:28):

I'm afraid that without a more complete example I'm not sure how to help further

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:29):

In math-comp, A i j will not reduce by default, as to better control some aspects of the proofs, thus you usually need to use rewrite !mxE. as to "normalize" the matrix rep.

view this post on Zulip Julin Shaji (Oct 12 2023 at 16:30):

No, as in how a novice would try first. :halo:

Example eg4 := \matrix_(i<3, j<3)
  (fun i j => i+j%:Z).
(* Example eg4 := \matrix_(i<3, j<3) (i+j).   *)

Compute eg4 0 1.

Would going in to proof mode reduce the term?

view this post on Zulip Julin Shaji (Oct 12 2023 at 16:32):

Just for someone who's curious to see an element of the matrix.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:32):

Indeed that's what we mean when we say "math-comp matrices are not designed for computing"

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:33):

indeed you need to use the proof mode to rewrite the expression symbolically; there are hacks to do so with Compute, but they are hacks so IMHO not worth it.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:38):

Variable (R: ringType).

Example eg4 : 'M[R]_(3,3) :=
  \matrix_(i<3, j<3) (i%:R + j%:R).

Theorem foo : eg4 0 1 = eg4 1 0.
Proof. rewrite /eg4 !mxE /=. Qed.

view this post on Zulip Julin Shaji (Oct 12 2023 at 16:38):

Yeah, I was just curious if there was a way to see a specific element for curiosity's sake. :melting_face:
Definitely not for real usage.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:38):

Yup, that's the way

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

t

view this post on Zulip Julin Shaji (Oct 12 2023 at 16:39):

Thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

The type of mxE is interesting:

mxE : forall [R : Type] [m n : nat] (k : unit) (F : 'I_m -> 'I_n -> R), \matrix[k]_(i, j) F i j =2 F

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

Most welcome!

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):

So as you see, it is just an unwrapping of the \matrix[]_(i,j) notation; this pattern is used along all the math-comp library

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 18:18):

Proof. rewrite /eg4 !mxE /=. Qed. <- that's not meant to work, or do I miss yet more magic?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 18:22):

@Paolo Giarrusso it is indeed missing a last rewrite step, but that's not a problem in my editor.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):

I got used to write lemmas like that, finish the proofs later on.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):

as they'll be auto-admitted

view this post on Zulip Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):

It is a game changer for me.

view this post on Zulip Paolo Giarrusso (Oct 12 2023 at 18:25):

even stating a false goal just to do the computation is reasonable — just always ask if it's 42 :-) Goal eg4 0 1 = 42.


Last updated: Jul 15 2024 at 21:02 UTC