Ishaan K (Feb 26 2024 at 14:18): Ishaan K (Feb 26 2024 at 14:18):Hello,
I was using matrix and mxalgebra from mathcomp.algebra to create a model for a control system I am building; however, I'm running into an issue with doing operations on the matrices I create that have real constants in them. I tried looking through the documentation of mathcomp.algebra.mxalgebra and mathcomp.algebra.matrix but failed to find any examples or explanation on how I might populate my matrices with constants and variables to do operations on them. I'm fairly new to Coq and would appreciate any suggestions or help.
I've added how I was trying to text it below with constant reals:
(* INR is a functions from reals in the standard library that aids in taking a nat and returning the value as a real (R) *)
(* Setting a constant value to a constant 1 by 1 matrix *)
Let M1 := (const_mx (INR 3)) : 'cV[R]_1.
(* Creating a 2 by 2 matrix of the 1 by 1 matrix M1 *)
Let M2 := (block_mx M1 M1 M1 M1) : 'M[R]_(2,2).
(* Attempts to multiply the matrices to get a result but fails *)
Check (mulmx M2 M2) : 'M[R]_(2,2).
Doesn't fail here. Could you explain what you are expecting?
Ishaan K (Mar 04 2024 at 15:17):Yes, of course @Pierre Roux, I am expecting a 2 by 2 matrix with the constant 18 in each entry of the matrix. However, I receive an error. This might be because of a dependency I might be missing or a different version. I have attached the image below.
coq_math_comp.PNG
One follow-up I have is how would I get the values from each entry from this matrix. Is there some sort of mapping function?
My final goal is to put polynomials in each entry and do matrix multiplication on that. Do you think using math-comp is a viable way of doing this?
Pierre-Yves Strub (Mar 04 2024 at 15:21):Do you want to do actual computations on polynomials/matrices?
Karl Palmskog (Mar 04 2024 at 15:24):standard advice for computing with polynomials/matrices: refine the representation to something that is computation-friendly using CoqEAL (or similar approach): https://github.com/coq-community/coqeal
MathComp is basically constructed/optimized for easy proof and not for big computations
Ishaan K (Mar 04 2024 at 15:44):Eventually, I'd like to preform proofs on my model that I create, but I'd like to use actual computations to test. I will look into CoqEAL. Is there a doc that is associated with the github link of CoqEAL you've sent me @Karl Palmskog?
Karl Palmskog (Mar 04 2024 at 16:16):there are many publications linked here: https://github.com/coq-community/coqeal?tab=readme-ov-file#meta
I recommend https://hal.inria.fr/hal-01113453/document for the refinement part.
You can also look at the source files, like https://github.com/coq-community/coqeal/blob/master/refinements/seqmx.v (refinement of MathComp matrices to lists of lists)
Last updated: Oct 13 2024 at 01:02 UTC