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

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

(AFAICT at least)

for your `Eval compute`

example, I’m also curious if there’s a good way to “normalize past opaque definitions”

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

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: Feb 08 2023 at 04:04 UTC