Hi everyone,

I have asked this question in Coq Users but now it's getting very specific to math-comp and therefore I am asking here. How can I simplify the right hand side of the expression below to vhd? Few things I learned in the process is that a definition can be `locked`

and I need to unlock it ensure the simplification, but I am not done with the proof (the whole proof on gist). Thank you very much in advance for your help.

```
vhd =
finite_fun_to_vector
(λ y : t n,
matrix_of_fun_def (m:=n) (n:=m.+1)
(λ (i : 'I_n) (j : 'I_m.+1),
vector_to_finite_fun
match fin_inv_S (ord_to_finite j) with
| inl _ => vhd
| inr b => let (x, _) := b in vector_to_finite_fun vtl x
end (ord_to_finite i)) (finite_to_ord y)
(finite_to_ord F1))
Lemma matrix_back_and_forth_same :
forall (n m : nat) (mx : Matrix n m),
mx = matrix_to_Matrix (Matrix_to_matrix mx).
Proof.
unfold matrix_to_Matrix,
Matrix_to_matrix,
matrix_to_Matrix,
matrix_to_finite_fun,
finite_fun_to_matrix,
matrix_of_fun.
unfold locked_with.
destruct matrix_key.
intros ? ?.
revert n.
induction m.
+ intros ? ?.
unfold Matrix in mx.
pose proof (vector_inv_0 mx) as Hn.
subst; reflexivity.
+ intros ? ?.
unfold Matrix in mx.
destruct (vector_inv_S mx) as (vhd & vtl & vp).
subst.
simpl.
f_equal.
```

it is too complicated for me. Maybe you need some kind of extensionnality for Matrix as you have for matrix with `matrixP`

.

For example the companion correctness theorem is easy to prove

```
Lemma ord_to_finite_correctness n (i : 'I_n) :
finite_to_ord (ord_to_finite i) = i.
Admitted.
Lemma Matrix_back_and_forth_same :
forall (n m : nat) (mx : 'M[R]_(n, m)),
mx = Matrix_to_matrix (matrix_to_Matrix mx).
Proof.
move=> n m mx.
apply/matrixP => i j.
rewrite /Matrix_to_matrix mxE.
rewrite /matrix_to_finite_fun /=.
rewrite -!vector_to_finite_fun_correctness.
rewrite -matrix_to_Matrix_correctness.
by rewrite !ord_to_finite_correctness.
Qed.
```

hope this helps.

Thanks @Laurent Théry . I came up with an idea that I can use this `Lemma mxE k F : matrix_of_fun k F =2 F.`

to get rid of the wrapper (Matrix_of_fun k) part and then I was thinking to simplify it, but this rewrite is not working.

Edit: I probably see what you mean by extensionnality.

```
The LHS of mxE
((\matrix[_]_(i, j) _ i j)%R _ _)
does not match any subterm of the goal
Lemma matrix_back_and_forth_same :
forall (n m : nat) (mx : Matrix n m),
mx = matrix_to_Matrix (Matrix_to_matrix mx).
Proof.
unfold matrix_to_Matrix,
Matrix_to_matrix,
matrix_to_Matrix,
matrix_to_finite_fun,
finite_fun_to_matrix.
intros ? ? ?.
rewrite mxE. (* THIS REWRITE IS NOT WORKING *)
```

`mxE`

uses `=2`

, this means that it needs to be apply with 2 arguments. That's why I said you main needs some extensibility. `matrixP`

gives this for the matrix of Mathcomp

Thanks again @Laurent Théry . I was making a stupid mistake and turning a normal value to extentional by applying `f_equal`

. I realised it after looking at your proof. I can't believe myself that I did that :).

```
Lemma finite_to_ord_correctness n (i : Fin.t n) :
ord_to_finite (finite_to_ord i) = i.
Proof.
unfold ord_to_finite, finite_to_ord,
ssr_have.
Search of_nat_lt.
Admitted.
Lemma vector_to_finite_simp :
forall n m (mx : Matrix n m) (i : Fin.t n)
(j : Fin.t m),
vector_to_finite_fun (vector_to_finite_fun mx j) i =
(Matrix_to_matrix mx) (finite_to_ord i) (finite_to_ord j).
Proof.
intros *.
rewrite matrix_to_Matrix_correctness.
repeat rewrite vector_to_finite_fun_correctness.
(* Here I was apply f_equal and turning it into functional *)
rewrite -!vector_to_finite_fun_correctness.
rewrite -matrix_to_Matrix_correctness mxE.
rewrite !finite_to_ord_correctness.
unfold matrix_to_finite_fun.
rewrite !vector_to_finite_fun_correctness.
reflexivity.
Defined.
```

good!

Last updated: Feb 08 2023 at 08:02 UTC