[stdlib] Warn about Vector.v #18032
[stdlib] Warn about Vector.v #18032
Conversation
coqbot-app
bot
added
the
needs: full CI
|
I am not completely convinced with the idea of deprecating something when there is no immediate substitute already present in stdlib. I understand the purpose of warning users but are the deprecation warnings really appropriate for that? |
|
What else do we have? Note that thanks to the specific |
|
Is it proper to deprecate a standard library in favor of an external project? I see the notes refer to the If tuples are prefered in place of vectors, then at least a copy of the examples should be hosted in the Coq repository? |
|
Using `since="8.19 vector"` means it's not possible to disable the warning using -deprecated-since-8.19, I don't think it's good.
I also don't know that we should deprecate Vector.
Gaëtan Gilbert
…On 11/09/2023 11:18, Pierre Roux wrote:
Following a few discussions on Zulip, it seems nice to warn new users about the fact that this part of the standard library is no longer state of the art.
* Added / updated *test-suite*.
* Added *changelog*.
* Added / updated *documentation*. (vectors are absent from the stdlib part of the refman)
o Documented any new / changed *user messages*.
o Updated *documented syntax* by running |make doc_gram_rsts|.
* Opened *overlay* pull requests.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
You can view, comment on, or merge this pull request online at:
#18032 <#18032>
Commit Summary
* 4042452 <4042452> [stdlib] Warn about Vector.v
File Changes
(8 files <https://github.com/coq/coq/pull/18032/files>)
* *A* doc/changelog/11-standard-library/18032-warn_vector.rst <https://github.com/coq/coq/pull/18032/files#diff-0e99782b073272be3685f9d05bdb295ff403e58d8399dc25fe96823fc7871c7e> (7)
* *M* theories/Bool/Bvector.v <https://github.com/coq/coq/pull/18032/files#diff-09b906c77080ef86361e47b391cdee50d7e9025d1bcdb45125a1c90038bf4acf> (34)
* *M* theories/Logic/FinFun.v <https://github.com/coq/coq/pull/18032/files#diff-f12a3e6f765d90357ab8f8b201ce3be28ad3c1cfc897527976448d1d2ed5a599> (1)
* *M* theories/Vectors/Fin.v <https://github.com/coq/coq/pull/18032/files#diff-726e8123c9e389126bcddceb647b31f6acc0a4e31785ace86bb67dac5f660264> (52)
* *M* theories/Vectors/Vector.v <https://github.com/coq/coq/pull/18032/files#diff-a519ad647cb66a1318a419339d504e9491cfc89a8f9bdcb9d47bfc20f437887d> (8)
* *M* theories/Vectors/VectorDef.v <https://github.com/coq/coq/pull/18032/files#diff-e669433d5ee57a7aaa0d45962468d584e7d964440969dc2a496c593e1aed0539> (57)
* *M* theories/Vectors/VectorEq.v <https://github.com/coq/coq/pull/18032/files#diff-4d2398dca2300950121d4ba53fd1186623503c467d1d5102b1202b30610b9a37> (15)
* *M* theories/Vectors/VectorSpec.v <https://github.com/coq/coq/pull/18032/files#diff-f8b3858c368b739a91a40c8eefc62f152c4a1fe4a34900944ab07238a3425e24> (100)
Patch Links:
* https://github.com/coq/coq/pull/18032.patch <https://github.com/coq/coq/pull/18032.patch>
* https://github.com/coq/coq/pull/18032.diff <https://github.com/coq/coq/pull/18032.diff>
—
Reply to this email directly, view it on GitHub <#18032>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AASZB3DMINBBIM64Z36IURDXZ3JMZANCNFSM6AAAAAA4TACHJ4>.
You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>
|
|
I have been working towards reducing reliance on Unlike other stdlib features whose deprecation I've recently been involved in, Vector is used in inter-project interfaces. Thus recommending users to find their own alternative, especially if the example is as heavy as a commitment as mathcomp, feels a little bit short. This need is roughly why we created mit-plv/coqutil, although length-constrained lists may not have been the first shared definition there. I don't think that pointing to coqutil instead would help much, though it is more stdlib-like than mathcomp. I wonder whether the best solution for the coq ecosystem as a whole would be to have in the standard library a vector-isomorphic definition (that is generally accepted as not too bad)? |
|
Thanks for your comments! We do agree on many points. As you may have noticed, the title of the PR is "Warn about Vector.v", it's not about deprecating it, at least not in the usual meaning: recommendation to no longer use because we plan to remove. It's only about warning new users that The fact that a deprecation warning is used is just a technical choice and maybe the changelog entry should read more "Added warning" than "Deprecated"?
Indeed, it's not a deprecation, maybe this should be made even clearer?
We could point to a stable release. That being said, that wouldn't make much change, tuples have been there forever and are very stable.
Code duplication sounds like a very bad idea, nowadays it's pretty easy to just use the coq-mathcomp-ssreflect package.
Right, maybe the field should just be
I agree, I also think it should be neither removed nor deprecated. But considering the situation (it's a less than ideal choice for most potential users), we should warn about it IMHO.
The point is not to recommend current users to change, rather to warn newcomers.
I'm not sure what you mean by "comitment" but just to be clear, it's perfectly possible to use just mathcomp's tuples without having to use anything else in the library. This just requires the mathcomp-ssreflect subpackage, not the whole library. Sure it's another dependency but experience shows it's at least as stable and well maintained than the stdlib.
Sure we could point to that solution as well (maybe in the header of the file and have the warning message point to that header).
Probably, but meanwhile it seems worth warning about the current state. |
I think using the warning infrastructure may be too heavy for this goal. A comment at the top of the file may be more appropriate. |
|
Possibly be should have a separate level "hints" for such things. |
|
I would be very happy to have the documentation of this module give a down-to-earth overview of the considerations for why one might not want to use it, both based on what it does and how it is implemented (my attempt for Z/nZ). Recommending alternatives seems nice too, and perhaps listing multiple ones is more appropriate given that no one has made it to stdlib. I think proux01 is right to look for some more prominent mechanism for that, as picking up a library after having seen examples (but no documentation) is feasible and probably somewhat common. I also sympathize with the objections to the use of |
theories/Bool/Bvector.v
Outdated
| proof (computable, in bool, to enjoy proof irrelevance) about its | ||
| length, as done for instance in | ||
| https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/tuple.v | ||
| *) |
There was a problem hiding this comment.
Can these lines be completed with a stronger analysis, e.g.:
- Is it about the absence of dependent pattern-matching in Coq? And if yes, how does this interact with Equations or with Pattern-matching with small inversion #16097?
- Is it about the dependency of types in equality proofs? And if yes, doesn't the argument then apply more generally to any kind of (relevant) dependent type?
- Should the argument be applied to Agda?
- In which sense isn't it more about two different styles of representing a given structure, each with different advantages, vs one representation being uniformly better than the other? Shouldn't we better work at being able to mechanically switch transparently between the two different representations?
There was a problem hiding this comment.
Can these lines be completed with a stronger analysis
I gave it an attempt
Is it about the absence of dependent pattern-matching in Coq
Dependent pattern-matching would probably only marginally help as the program and proof would still be mixed
Should the argument be applied to Agda
I guess in Agda, the mixing of program and proof may be less painful since there is anyway no tactic language to handle proofs, but still.
In which sense isn't it more about two different styles of representing a given structure, each with different advantages, vs one representation being uniformly better than the other
That's in part true. However, out of the Zulip discussions I had the feeling that there is an overwhelming preference for the dependent pair encoding. The only advantage I could find to the current stdlib encoding is that it "looks nicer" and it might be somewhat more modular when embeding it in more complex structures such as n-ary trees (although those are still probably easier to handle with dependent pairs).
Shouldn't we better work at being able to mechanically switch transparently between the two different representations
Not sure this is worth the effort.
There was a problem hiding this comment.
Shouldn't we better work at being able to mechanically switch transparently between the two different representations
Not sure this is worth the effort.
I was mentioning it because it is a kind of mechanism I'm interested in anyway in general (though not in a very short term).
Regarding the comment in the file, the ideal would be to give factual data (e.g. examples of what works and of what does not work). Or a pointer to such analysis.
BTW, can you add a link to the Zulip discussion.
Pinging @fblanqui otherwise relatively to CoLoR.
There was a problem hiding this comment.
I guess in Agda, the mixing of program and proof may be less painful since there is anyway no tactic language to handle proofs, but still.
I mentioned Agda because the motivations for users are not necessarily only about relying on tactics, or avoiding dependencies in type. I have a couple of Agda users in my surrounding and they are e.g sensitive to issues such as controlling/understanding the proof terms they are writing. The comment to put in the file should reflect the diversity of motivations among users.
There was a problem hiding this comment.
Another issue, related to my comment about transparently switching between different representations of a same structure, is that Vector.t vs fun n => {l & length l = n} is not only about "formalization techniques" but about logical questions. In the present case, the difference between the two representations is connected to a standard logical equivalence called the fibered/indexed equivalence (aka "Grothendieck for the dummies"). So, there is also a fundamental logical issue around which I think is worth to be mentioned.
There was a problem hiding this comment.
I looked through the Zulip links, and a number of the issues there do not seem to be resolved by the alternative definitions we have discussed here. My takeaway from these links' advice is much closer to "use list", with "use another definition of vectors" being an alternative that may sometimes work but wouldn't be recommended for just anybody. Entirely speculating, perhaps being able to list some pros and cons of vectors constructed as { list | length }, Fixpoint, or Inductive is a good sign that one may be able to use any of these definitions successfully 😸.
There was a problem hiding this comment.
- Is it about the dependency of types in equality proofs? And if yes, doesn't the argument then apply more generally to any kind of (relevant) dependent type?
- Should the argument be applied to Agda?
My understanding is that the issue applies to any indexed inductive type where K applies to the index but not judgmentally. If K does not apply to the index, then index mis-matches can be backed in mathematics. Agda (with K) has pattern matching support for easing the use of K, and, I imagine, Equations probably has similar support. This applies much less to parameterized inductives, where having proofs that cross parameters is much less common, and, I expect, much more coherent.
There was a problem hiding this comment.
the ideal would be to give factual data (e.g. examples of what works and of what does not work). Or a pointer
to such analysis.
Feel free to ad such a pointer if you know a good one
Meanwhile, I've added the examle offered by Emilio in #6459
There was a problem hiding this comment.
I looked through the Zulip links, and a number of the issues there do not seem to be resolved by the alternative definitions we have discussed here.
Sorry, that's not my understanding. It seems to me that the dependent pair encoding ({ list | length list = n }) does help in most cases. Also note that all Coq developers who express a clear opinion in those Zulip streams (and there are quite a few) strongly discourage the use of Vector.t.
There was a problem hiding this comment.
I do see that vector is consistently discouraged, and I agree it should be. Indeed, basically any alternative (list, length-constrained list, fixpoint on nat, function from fin) seems better. I think our different reading of the discussion may very well come down to interpretation and background, for example I recall reading "dependently typed" as referring to all of the solutions except bare list. But as we're not looking to decide the one representation for the entire coq ecosystem here, perhaps let's mention list among the potential alternatives and move on? I imagine something along the lines of "consider ... - list, if enforcing the length by typing is not essential, or when manipulating sequences of variying, non-literal lengths" might be good.
To avoid code duplication, a possibility, in the spirit of the stdlib2 project, would be to move ssr tuples to stdlib. Maybe is this too idealistic, but e.g. developers of mit-plv/coqutil and ssr tuples could then work together at providing a "standard" version of vector-as-subset-of-list about which everyone would (ideally) agree? Or, at least, if too many differences cannot be reconciled, there would be a common place where to collect and centralize the different variants of vectors/tuple and where to emphasize their differences. Actually, it might be useful to get the opinion also of CoLoR, which, iirc, has a large library of vectors-as-indexed-type. |
proux01
force-pushed
the
warn_vector
branch
from
4042452
to
0674b1e
Compare
theories/Logic/FinFun.v
Outdated
| @@ -233,6 +233,7 @@ Qed. | |||
|
|
|||
|
|
|||
| (** An example of finite type : [Fin.t] *) | |||
| #[local] Set Warnings "-deprecated-since-stdlib-vector". | |||
There was a problem hiding this comment.
Wouldn't this suggest that FinFun.v should be split with the second part moved to Vectors? or probably even better Fin_Finite moved and the proof of bSurjective_bBijective rewritten not to depend on Fin?
This would make Fin depend on FinFun rather than the converse.
There was a problem hiding this comment.
Maybe, but that's definitely matter for another PR.
I've tried to make the "no deprecation" intent clearer.
@MSoegtropIMC and @andres-erbsen ideally we would have some kind of docstring mechanism to attach some documentation to definitions. Meanwhile the deprecation warnings is probably the closest we have.
@SkySkimmer I agree, done
@herbelin this would require also adding
That's the process we already use for
Well, as @andres-erbsen mentions above, mathcomp's tuple is imlemented with mathcomp's subtype mechanism and canonical structures whereas coqutil was later developped so as to not use those and uses typeclasses. So I'm not very optimistic here.
Sure, who should we ping? |
|
coqutil tuples do not use typeclasses or any other programmable elaboration. I am not attached to the specific definition in coqutil and would be happy to work on standardization without presuming that design. From my perspective, it seems substantially preferable to have this code in live stdlib rather than coqutil regardless of how it is defined. EDIT: coqutil tuples, fiat-crypto tuples, color prodn. |
proux01
force-pushed
the
warn_vector
branch
from
0674b1e
to
a54712b
Compare
proux01
force-pushed
the
warn_vector
branch
from
a54712b
to
fd9ed31
Compare
|
Thanks @ejgallego I missed that one. (I'm not marking the current PR as fixing the issue though, since it only introduces a warning) You write there
to what precisely are you refering, other than mathcomp tuples? Andres and Hugo already kindly pointed to coqutil, fiat-crypto and color but the last two are the exact same as stdlib's |
|
For the record, bouncing on the
As well known, because it separates computation and logic, the approach à la Curry allows easily to use terms for the computational part and tactics for the logical part. The approach à la Church requires either proficiency in writing programs with tactics, or proficiency in managing equality proofs as programs (or both). The version à la Curry (which reuses the Require Import List Arith.
Import EqNotations.
Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1").
Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )").
Notation "x .1" := (projT1 x) (at level 1, left associativity, format "x .1").
Notation "x .2" := (projT2 x) (at level 1, left associativity, format "x .2").
Notation "(= [ x ] p ; q )" := (eq_sigT x _ p q) (at level 0, format "(= [ x ] p ; '/ ' q )").
Notation "(= p ; q )" := (eq_sigT _ _ p q) (at level 0, format "(= p ; '/ ' q )").
Arguments UIP_nat {x y p1 p2}.
Infix "∘" := eq_trans (at level 45).
Notation "H ⁻¹" := (eq_sym H) (at level 5).
Definition vector A n := {l : list A & length l = n}.
Lemma rew_lift {A n n' } (v : vector A n) (w : vector A n') {H : n' = n} : v.1 = w.1 -> v.1 = (rew H in w).1.
Proof. now destruct H. Defined.
Definition vnil {A} : vector A 0 := (nil; eq_refl).
Definition vcons {A} n a (v : vector A n) : vector A n.+1 := (a :: v.1; f_equal S v.2).
Definition vrev {A n} (v : vector A n) : vector A n := (rev v.1; rev_length v.1 ∘ v.2).
Definition vappend {A n n'} (v : vector A n) (v' : vector A n') : vector A (n + n') :=
(v.1 ++ v'.1; app_length _ _ ∘ f_equal2 Nat.add v.2 v'.2).
Lemma vappend_vnil_r A n (v : vector A n) : vappend v vnil = rew (eq_sym (Nat.add_0_r _)) in v.
Proof (= rew_lift (vappend v vnil) _ (app_nil_r v.1); UIP_nat).
Lemma vappend_assoc A n n' n'' (v : vector A n) (v' : vector A n') (v'' : vector A n'') :
vappend (vappend v v') v'' = rew Nat.add_assoc _ _ _ in vappend v (vappend v' v'').
Proof
(= rew_lift (vappend (vappend v v') v'') (vappend v (vappend v' v'')) (app_assoc v.1 v'.1 v''.1)⁻¹; UIP_nat).
Lemma vappend_vrev A n n' (v : vector A n) (v' : vector A n') :
vrev (vappend v v') = rew Nat.add_comm _ _ in (vappend (vrev v') (vrev v)).
Proof (= rew_lift (vrev (vappend v v')) (vappend (vrev v') (vrev v)) (rev_app_distr v.1 v'.1); UIP_nat).
Lemma vrev_vrev A n (v : vector A n) : vrev (vrev v) = v.
Proof (= [(vrev (vrev v))] rev_involutive v.1; UIP_nat).
The version à la Church (which lifts the Require Import List Vector VectorDef Arith.
Import EqNotations.
Arguments nil {A}.
Arguments cons {A} h n v.
Import VectorNotations.
Fixpoint nat_add_0_r n : n = n + 0 :=
match n with
| 0 => eq_refl
| S n => f_equal S (nat_add_0_r n)
end.
Fixpoint rev {A n} (v : t A n) : t A n :=
match v with
| [] => []
| a :: v => rew (Nat.add_1_r _) in append (rev v) [a]
end.
Theorem rew_shift {A} {P : A -> Type} {x y} {g} {a : P (g y)} {f : forall z, P z -> P (g z)} (H : x = y) (p : P x)
: a = f y (rew H in p) -> a = rew (f_equal g H) in f x p.
Proof. now destruct H. Defined.
Fixpoint append_nil_r {A n} (v : t A n) : v ++ [] = rew nat_add_0_r _ in v :=
match v with
| [] => eq_refl
| a :: v => rew_shift _ _ (f_equal (@cons _ a _) (append_nil_r v))
end. (* mimicking the proof of List.app_nil_r *)
Fixpoint append_assoc A n n' n'' (v : t A n) (v' : t A n') (v'' : t A n'') :
(v ++ v') ++ v'' = rew [t A] Nat.add_assoc n n' n'' in (v ++ (v' ++ v'')).
Admitted. (* one loop + equality reasoning, mimicking the proof of List.app_assoc *)
Fixpoint append_rev {A n n'} (v : t A n) (v' : t A n') :
rev (append v v') = rew (Nat.add_comm n' n) in append (rev v') (rev v).
Admitted. (* one loop + equality reasoning, mimicking the proof of List.rev_app_distr *)
Fixpoint rev_involutive {A n} (v : t A n) : rev (rev v) = v.
Admitted. (* one loop + equality reasoning, mimicking the proof of List.rev_involutive *)Note that even if the final result talks about Note that both could be made "nicer" by using notations, etc., at least in a way which allows to compare them even better (but I'm lacking time for it). |
|
For "vectors" represented as the pair of a list and a proof that the list has some length, what is actually the relevant file to look at in Also, has someone a reference to code which develops the recursive formulation of |
|
I also have questions about
|
@herbelin thanks for the comparison! As a side note, to better emphasize the ability to use Ltac, I'd probably rather write the first one something like: Require Import List Arith.
Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1").
Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ; '/ ' y )").
Definition vector A n := {l : list A & length l = n}.
Coercion vlist {A n} (v : vector A n) : list A := projT1 v.
Lemma vlist_inj {A n} (v w : vector A n) : v = w :> list A -> v = w.
Proof.
destruct v as [v vl]; destruct w as [w wl]; simpl; intro vw.
revert wl; rewrite <-vw; intro wl.
now cut (vl = wl); [intro vwl; rewrite vwl|apply UIP_nat].
Qed.
Lemma vlength {A n} (v : vector A n) : length v = n. Proof. now destruct v. Qed.
Lemma vcast_subproof {A n n'} (eq_nn' : n = n') (v : vector A n) : length v = n'.
Proof. revert v; rewrite eq_nn'; apply vlength. Qed.
Definition vcast {A n n'} (eq_nn' : n = n') (v : vector A n) : vector A n' :=
(v : list A; vcast_subproof eq_nn' v).
Lemma vnil_subproof {A} : @length A nil = 0. Proof. reflexivity. Qed.
Definition vnil {A} : vector A 0 := (nil; vnil_subproof).
Lemma vcons_subproof {A n} a (v : vector A n) : length (a :: v) = n.+1.
Proof. now simpl; rewrite vlength. Qed.
Definition vcons {A} n a (v : vector A n) : vector A n.+1 :=
(a :: v; vcons_subproof a v).
Lemma vrev_subproof {A n} (v : vector A n) : length (rev v) = n.
Proof. now rewrite rev_length, vlength. Qed.
Definition vrev {A n} (v : vector A n) : vector A n := (rev v; vrev_subproof v).
Lemma vappend_subproof {A n n'} (v : vector A n) (v' : vector A n') :
length (v ++ v') = n + n'.
Proof. now rewrite app_length, !vlength. Qed.
Definition vappend {A n n'} (v : vector A n) (v' : vector A n') : vector A (n + n') :=
(v ++ v'; vappend_subproof v v').
Lemma vappend_vnil_r A n (v : vector A n) :
vappend v vnil = vcast (eq_sym (Nat.add_0_r _)) v.
Proof. now apply vlist_inj; simpl; rewrite app_nil_r. Qed.
Lemma vappend_assoc A n n' n'' (v : vector A n) (v' : vector A n') (v'' : vector A n'') :
vappend (vappend v v') v'' = vcast (Nat.add_assoc _ _ _) (vappend v (vappend v' v'')).
Proof. now apply vlist_inj; simpl; rewrite app_assoc. Qed.
Lemma vappend_vrev A n n' (v : vector A n) (v' : vector A n') :
vrev (vappend v v') = vcast (Nat.add_comm _ _) (vappend (vrev v') (vrev v)).
Proof. now apply vlist_inj; simpl; rewrite rev_app_distr. Qed.
Lemma vrev_vrev A n (v : vector A n) : vrev (vrev v) = v.
Proof. now apply vlist_inj; simpl; rewrite rev_involutive. Qed.Just a few questions:
|
coqbot-app
bot
added
the
needs: full CI
|
@proux01 is this PR still relevant? |
ppedrot
removed
the
needs: merge of dependency
|
Yes, I'll complete it once I'm done with #18248 (I'm on it). Sorry for the delay. |
proux01
added
the
request: full CI
coqbot-app
bot
removed
request: full CI
|
@ppedrot this is, finally, ready (the windows failure with GTK is certainly unrelated) |
coqbot-app
bot
added
the
needs: full CI
|
Gentle ping @ppedrot this is still ready |
|
Will merge soon except if people have more comments about the contents of the PR. |
|
I made a (last) suggestion but I'm otherwise impressed by how many interesting discussions and contributions this PR has generated for Coq. |
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
|
@ppedrot CI seems happy |
|
Let's merge, this has waited enough. @coqbot merge now |
|
Thanks |
Requires #18349 (merged)Following a few discussions on Zulip, it seems nice to warn new users about the fact that this part of the standard library is no longer state of the art:
See also #6459
Added / updated documentation.(vectors are absent from the stdlib part of the refman)Documented any new / changed user messages.Updated documented syntax by runningmake doc_gram_rsts.Opened overlay pull requests.