Hi everyone, I have this goal and when I am using
simpl, it not simplifying. How can I simplify this expression to apply induction hypothesis?
Edit (new goal:) with the help of @Karl Palmskog , I manage to move one step further. Now, I believe it's
\matrix_(i, j) is somehow blocking the simplification because I have another lemma
matrix_to_finite_back_forth, very similar to
matrix_back_and_forth_same except it does not use ssreflect matrix, which I was able to prove without any problem. Any idea or suggestion would be an excellent help.
vhd = finite_fun_to_vector (λ y : t n, (\matrix_(i, j) matrix_to_finite_fun (cons (Vector.t R n) vhd m vtl) (ord_to_finite i) (ord_to_finite j))%R (finite_to_ord y) (Ordinal (n:=m.+1) (m:=0) (erefl true))) 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. 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. cbn. f_equal. cbn. (* how to simplify \matrix_ ?*) Lemma matrix_to_finite_back_forth : forall n m (mx : Matrix n m), mx = finite_fun_to_matrix (matrix_to_finite_fun mx). Proof (* terms omitted *). Qed.
Complete Source Code (slightly modified) on gist.
the standard answer is to try other evaluation approaches, like
Thanks @Karl Palmskog . cbn worked but it's not simplifying the terms to the point that I can apply reflexivity or induction hypothesis. compute ran for 8 minutes and did nothing before I killed it. For example, the right hand side of the below expression should reduct to
vhd but apparently, it's not happening.
vhd = finite_fun_to_vector (λ y : t n, (\matrix_(i, j) matrix_to_finite_fun (cons (Vector.t R n) vhd m vtl) (ord_to_finite i) (ord_to_finite j))%R (finite_to_ord y) (Ordinal (n:=m.+1) (m:=0) (erefl true)))
if it's slow, you can try
vm_compute, or even
native_compute if you have
coq-native in opam (recommend different opam switch)
some definitions will not reduce because they are "locked" (by library maintainers), not sure if this is happening here
I figured out that
introT, and similarly elimT, are opaque so I wrote one that reduces, using Defined (I also feel something like this happening, and hopefully I will figure it out).
An orthogonal question: is there any rationale behind using
Qed in proofs?
Qed is used for several reasons, not least:
Qed, but only written to disk - this saves a lot of resources
Qedis an abstraction barrier that guarantees that other constants can't depend on the body of the defined constant, only its type. This makes it possible to prove theorems asynchronously, and also to skip doing
Qed-proofs when convenient (
Do you think it's a good idea to have same theorem with two versions: one with Qed and one with Defined?
if you know you need to access (compute with) the body of the constant somewhere else, go with
Defined. Otherwise, I'd go with
Qed until you find out you need something different
even though it's a classic problem in Coq that some constants won't unfold, I think the problem of over-unfolding can be a serious issue (proof context becomes a mess).
Qed can be a way to manage over-unfolding (but for more advanced unfold mitigation, locking is probably the way to go)
Is this what you meant by
locked @Karl Palmskog ?
mx = finite_fun_to_vector (λ x : t m, finite_fun_to_vector (λ y : t n, locked_with matrix_key (* SEE HERE *) (matrix_of_fun_def (m:=n) (n:=m)) (λ (i : ordinal_finType n) (j : ordinal_finType m), vector_to_finite_fun (vector_to_finite_fun mx (ord_to_finite j)) (ord_to_finite i)) (finite_to_ord y) (finite_to_ord x)))
right, yes, that looks like a library locking. This was a library designer choice so that one can't unfold, only use lemmas
you could search for "locked definition" or similar in this stream or the MathComp stream, I know people talk about it form time to time. I don't know the technicalities
https://github.com/math-comp/hierarchy-builder/wiki/Locking says you can try
Thanks @Li-yao and @Karl Palmskog .
rewrite unlock did not work, and these are the relevant definitions in matrix. However, I could not find any lemma but I am not expert in math-comp so I might be missing something obvious.
Definition matrix_of_fun k := locked_with k matrix_of_fun_def. Canonical matrix_unlockable k := [unlockable fun matrix_of_fun k].
Nevermind, I just unfolded the locked definition and get rid of it by destructing it.
∀ (n m : nat) (mx : Matrix n m), mx = finite_fun_to_vector (λ x : t m, finite_fun_to_vector (λ y : t n, (let 'tt := matrix_key in λ (T : Type) (x0 : T), x0) ((ordinal_finType n → ordinal_finType m → R) → 'M_(n, m)) (matrix_of_fun_def (m:=n) (n:=m)) (λ (i : ordinal_finType n) (j : ordinal_finType m), vector_to_finite_fun (vector_to_finite_fun mx (ord_to_finite j)) (ord_to_finite i)) (finite_to_ord y) (finite_to_ord x)))
Very interesting way to not let definition unfold.
Karl Palmskog said:
Qedis used for several reasons, not least:
- proof terms are not persisted in memory after
Qed, but only written to disk - this saves a lot of resources
Is that actually true? I thought it was only that the ones from other files don't get loaded from disk
I've heard it was true at some point in Coq history, but you may be right that nowadays it only affects other files
hence you get these absurdly huge files which take 10GB memory to run
coqc on, but then you don't care once they are compiled
I don't think that Qed proofs were ever removed from the memory of a coqc process. But you're right that their loading is deferred when requiring a vo, which is an important feature.
but you could theoretically make the proof term inaccessible (and thus marked for GC) as soon as Qed is reached, right?
unfortunately the STM is a mess beyond repair
Its not entirely correct that Qed can be GCed safely tho right? For example, extraction is able to peek behind Qed's (which is another design issue in itself). https://github.com/coq/coq/issues/15874
the idea is that it can be swapped to disk (but not by the OS which doesn't have the info)
not gc'd completely away
Last updated: Sep 23 2023 at 14:01 UTC