Pacificl L (Apr 04 2022 at 17:58): Pacificl L (Apr 04 2022 at 17:58):Hello, I'm a L3 student and I recently tried to experiment with Coq and especially learn how to deal with math using mathcomp.
Unfortunately, it seems that I'm missing something rudimentary when I try to use it and I am not able to do some simple tasks nor to find resources explaining how to. I searched in the book but if the answer is in there and I missed it or if this question has already be answered elsewhere, sorry.
My problem has to do with opaque definitions : how to use mathcomp without being blocked by them ?
Example :
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype.
From mathcomp Require Import div finfun bigop prime binomial ssralg finset fingroup finalg perm zmodp matrix.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GRing.Theory.
Section Matrix.
Local Open Scope ring_scope.
Local Open Scope nat_scope.
Definition seq_to_matrix n m lrows : 'M[nat]_(n,m) :=
\matrix_(i < n, j < m)
nth 0 (nth [::] lrows i) j.
Definition const_mx m n a : 'M[nat]_(m, n) := \matrix_(i, j) a.
(*Compute \tr (seq_to_matrix 3 3
[:: [:: 1; 2; 3];
[:: 1; 2; 3];
[:: 1; 2; 3]]).*)
Definition diag_mx n : 'M[nat]_n := \matrix_(i, j) if (i==j) then 1 else 0.
Definition f (i:nat) (j:nat) : nat := if (i==j) then 1 else 0.
Example C := const_mx 3 3 1.
Example M := diag_mx 3.
Eval compute in \sum_i M i i.
Example result : \sum_i M i i = 3.
Proof.
unfold M.
unfold diag_mx. simpl. unfold "\sum_".
In this example, the evaluation is not automatically simplified by Coq and when I try to manually prove the result with the sum, I encounter opaque definitions.
Thank you
Paolo Giarrusso (Apr 04 2022 at 19:05):the unlock tactic and rewrite unlock could help, for the Example result… but for proofs in math-comp, you aren’t really supposed to unfold the implementation, but to use the existing theory that is proved in math-comp
Paolo Giarrusso (Apr 04 2022 at 19:06):(AFAICT at least)
Paolo Giarrusso (Apr 04 2022 at 19:07):for your Eval compute example, I’m also curious if there’s a good way to “normalize past opaque definitions”
Pacificl L (Apr 05 2022 at 03:33):Thank you for your answer
In cases like this, with a specific sum for example, how could there be pre-existent theorems in math-comp ? One has to just compute the sum and thus unfold it, right ?
In the same vein, how can we use \tr for specific sizes of matrices ? Here with the same M as before Eval compute in \tr M. raises the error The term "M" has type "'M_3" while it is expected to have type "'M_?n".
Thank you again
Pierre Roux (Apr 05 2022 at 06:27):Indeed unlock sometimes work:
From mathcomp Require Import all_ssreflect.
Goal \sum_(i <- [:: 1; 2; 3]) i^2 = 14.
Proof. by rewrite unlock. Qed.
but note that MathComp types are designed for ease of proofs rather than computations. If you need to perform efficient computations, a good solution is to refine MathComp types towards more computation oriented types with CoqEAL but that's non trivial and I wouldn't recommend it when first discovering MathComp.
Last updated: Oct 13 2024 at 01:02 UTC