Mukesh Tiwari (May 08 2022 at 17:15): Mukesh Tiwari (May 08 2022 at 17:15):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.
Mukesh Tiwari (May 09 2022 at 16:52):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
Mukesh Tiwari (May 09 2022 at 17:40):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