Julin Shaji (Oct 03 2023 at 15:49): 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?
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.
Hi @Julin Shaji , math-comp matrices are defined in https://math-comp.github.io/htmldoc_2_0_0/mathcomp.algebra.matrix.html
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
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.
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)".
*)
Compute \matrix_(i<3, j<7) (fun i j => if i==j then 1 else 0). worked though.
Julin Shaji (Oct 09 2023 at 06:01):But that seems to leave holes.
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
*)
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).
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?
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?
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.
(but I agree the error message is not very informative)
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?
Michael Soegtrop (Oct 10 2023 at 06:26):Some example files might also help ...
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?
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..
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.
Julin Shaji (Oct 10 2023 at 10:28):How can we get the function used to build the matrix in \matrix?
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
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?
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
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
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:
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_funOkay, so the other way must be
fun_of_matrix. :+1:
Ah sure, I misread your question. This function is actually a coercion btw.
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.
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.
Emilio Jesús Gallego Arias (Oct 12 2023 at 16:28):Hi @Julin Shaji , does rewrite !mxE improve what you see?
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
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.
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?
Julin Shaji (Oct 12 2023 at 16:32):Just for someone who's curious to see an element of the matrix.
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"
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.
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.
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.
Emilio Jesús Gallego Arias (Oct 12 2023 at 16:38):Yup, that's the way
Emilio Jesús Gallego Arias (Oct 12 2023 at 16:39):t
Julin Shaji (Oct 12 2023 at 16:39):Thanks!
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
Most welcome!
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
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?
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.
Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):I got used to write lemmas like that, finish the proofs later on.
Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):as they'll be auto-admitted
Emilio Jesús Gallego Arias (Oct 12 2023 at 18:23):It is a game changer for me.
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.
Florent Becker (Oct 09 2024 at 14:53):In the same vein, is there an ergonomic way to explicitly define the coefficients of a matrix and then query them? I currently have:
Defintion my_mat : 'M_(2,2) := \matrix_(j, i) (tnth (tnth
[tuple
[tuple 17; 93]
; [tuple 18; 71]
] j) i).
Lemma c00: my_mat 0 0 = my_mat 0 0.
rewrite /my_mat !mxE !tnth0.
Then I don’t know how to query the other coefficients of M. For example, I’m stuck in
Lemma c01 p:
let j := Ordinal (m:=1) p in
my_mat ord0 j = my_mat ord0 j.
rewrite /my_mat !mxE. (* then what? *)
Are tuples of tuples the right way to explicitly define a matrix? I need an ergonomic way to input them as well as to query their coefficients (if only to check the input).
Quentin VERMANDE (Oct 09 2024 at 15:00):You can unfold tnth and simplify.
Pierre Roux (Oct 09 2024 at 15:05):Indeed, the following works:
Lemma c01 : my_mat ord0 (inord 1) = 93.
Proof. by rewrite /my_mat mxE /tnth inordK. Qed.
Last updated: Oct 13 2024 at 01:02 UTC