diff --git a/doc/changelog/11-standard-library/18032-warn_vector.rst b/doc/changelog/11-standard-library/18032-warn_vector.rst new file mode 100644 index 000000000000..77a38eb45349 --- /dev/null +++ b/doc/changelog/11-standard-library/18032-warn_vector.rst @@ -0,0 +1,9 @@ +- **Added:** + A warning on :g:`Vector.t` to make its new users aware that using + this dependently typed representation of fixed-length lists is more + technically difficult, compared to bundling lists with a proof of their + length. This is not a deprecation and there is no intent to remove it + from the standard library. Use option `-w -stdlib-vector` + to silence the warning + (`#18032 `_, + by Pierre Roux, reviewed by Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Hugo Herbelin, Olivier Laurent, Yishuai Li, Pierre-Marie Pédrot and Michael Soegtrop). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0b8006eeeccd..dbcf0ea0e2db 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -2437,7 +2437,7 @@ The following errors apply to both string and number notations: The following example parses and prints natural numbers between :g:`0` and :g:`n-1` as terms of type :g:`Fin.t n`. - .. coqtop:: all reset + .. coqtop:: all reset warn Require Import Vector. Print Fin.t. diff --git a/test-suite/output/NumberNotations.out b/test-suite/output/NumberNotations.out index 0a968fed979d..7c01ba003271 100644 --- a/test-suite/output/NumberNotations.out +++ b/test-suite/output/NumberNotations.out @@ -305,6 +305,10 @@ This might yield ill typed terms when using the notation. File "./output/NumberNotations.v", line 589, characters 0-146: The command has indeed failed with message: 'via' and 'abstract' cannot be used together. +File "./output/NumberNotations.v", line 636, characters 0-15: +Warning: Using Vector.t is known to be technically difficult, see +. +[warn-library-file-stdlib-vector,stdlib-vector,warn-library-file,user-warn,default] File "./output/NumberNotations.v", line 665, characters 21-23: Warning: Type of I1 seems incompatible with the type of Fin.F1. Expected type is: (nat -> I) instead of I. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index d8a8276cb773..8016e9b879db 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -8,9 +8,14 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** N.B.: Using this encoding of bit vectors is discouraged. +See . *) +Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). + (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) Require Export Bool Sumbool. +#[local] Set Warnings "-stdlib-vector". Require Vector. Export Vector.VectorNotations. diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 6a2b78afb308..bdd141f16c0b 100644 --- a/theories/Logic/FinFun.v +++ b/theories/Logic/FinFun.v @@ -13,6 +13,7 @@ (** Main result : for functions [f:A->A] with finite [A], f injective <-> f bijective <-> f surjective. *) +#[local] Set Warnings "-stdlib-vector". Require Import List PeanoNat Compare_dec EqNat Decidable ListDec. Require Fin. Set Implicit Arguments. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 0b310ba9350b..d4dbdb07a17e 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +#[local] Set Warnings "-stdlib-vector". Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat Basics ByteVector. diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v index 8c2bde394b04..e21b9e63d1e2 100644 --- a/theories/Strings/ByteVector.v +++ b/theories/Strings/ByteVector.v @@ -10,6 +10,7 @@ (* This file is deprecated since 8.19, use list Coq.Init.Byte.byte. *) Local Set Warnings "-deprecated". +Local Set Warnings "-stdlib-vector". Require Import Ascii Basics Bvector String Vector. Export VectorNotations. diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index 9f8b00272d15..b485f65b063c 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -11,7 +11,20 @@ Require Import PeanoNat. Require Arith_base. -(** [fin n] is a convenient way to represent \[1 .. n\] +(** N.B.: This file defines a dependently-type programming view of +bounded integers. Another popular approach is to bundle integers with +a proof of boundedness, thus inheriting integer arithmetic rather than +redefining it on the bounded type. See +https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v +for a similar discussion on bounded lists. + +An alternative implementation can be found for instance in +https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v +One can read more about this type in section 7.4 of this book: +https://zenodo.org/record/4282710#.X_q4aGso-yU . *) +Attributes warn(cats="stdlib vector", note="Alternatives to Fin.t are available, see ."). + +(** [fin n] is a way to represent \[1 .. n\] [fin n] can be seen as a n-uplet of unit. [F1] is the first element of the n-uplet. If [f] is the k-th element of the (n-1)-uplet, [FS f] is the diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v index 90d07d2b205b..ca0014181f2d 100644 --- a/theories/Vectors/Vector.v +++ b/theories/Vectors/Vector.v @@ -8,15 +8,79 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** N.B.: Lists inductively defined with a dependency on their length, +here called vectors, are popular in dependent type programming: +programs embed their specification and only programs are +manipulated. However, this currently requires mastering advanced +dependent type programming to simultaneously handle the list +manipulation and the specification of its length. + +We recommend using lists bundled with, when needed, a proof about +their length rather than vectors. (Thanks to the proof irrelevance of +equality on [nat], any two bundlings of a same list are provably +equal.) This decouples the two aspects above, making it easy to write +code in Gallina and develop proofs with tactics. + +Such an implementation can be found for instance in +https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/tuple.v +One can read more about this tuple type in section 7.1 of this book: +https://doi.org/10.5281/zenodo.4282710 . +In particular, this implementation comes with coercion and canonical +structures so that lists and tuples can be transparently mixed most of +the time. For instance, after [From mathcomp Require Import seq tuple.], +in [Context n1 n2 T (v1 : n1.-tuple T) (v2 : n2.-tuple T) (foo : (n1 + n2).-tuple T -> bool).] +one can write [Check foo (v1 ++ v2).], where [++] is the list concatenation, +and Coq will automatically elaborate it, as [Set Printing All.] would show, +to [foo (cat_tuple v1 v2)] where [cat_tuple] is the lifting of [++] on tuples. + +Another representation can be found in +https://github.com/mit-plv/coqutil/blob/master/src/coqutil/Datatypes/HList.v +where tuples can be manipulated through the [of_list] and [to_list] functions. +This has to be done manually though as the library doesn't automate it. + +To give an example of the difficulties faced with [Vector.t], +writing [VectorDef.rev] constitutes a good exercise. This proves +fairly tricky and requires reimplementing dependent type versions +of functions already written on lists (typing [Vector.rev] even +relies on a tail-recursive version of the addition on natural +numbers whose computational content structurally follows the one +of the auxiliary function [Vector.rev_append] from which +[Vector.rev] is defined; additionally, the computational content +is intertwined with some rewriting steps). In contrast, the +dependent pair encoding reuses functions and lemmas already +written on lists and the definition (called [rev_tuple] in +mathcomp's [tuple.v]) only needs the property that [rev] +preserves the length: + +[[ +Require Import List. + +Record tuple_of (n : nat) T := Tuple + { tval :> list T; tsize : length tval = n }. + +Lemma rev_tupleP [T n] (t : tuple_of n T) : length (rev t) = n. +Proof. now rewrite length_rev, tsize. Qed. +Canonical rev_tuple T n (t : tuple_of n T) := Tuple n T (rev t) (rev_tupleP t). + +(* The canonical instance allows to automatically elaborate tuples: *) +Section TestRevTuple. +Variables (T : Type) (n : nat) (t : tuple_of n T). +Check rev t : tuple_of n T. +]] + +Thus lemmas about lists are enough in most cases. *) +Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). + (** Vectors. - Author: Pierre Boutillier + Initial Author: Pierre Boutillier Institution: PPS, INRIA 12/2010 Originally from the contribution bit vector by Jean Duprat (ENS Lyon). Based on contents from Util/VecUtil of the CoLoR contribution *) +#[local] Set Warnings "-stdlib-vector". Require Fin. Require VectorDef. Require VectorSpec. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 2982ffafe1fd..d4e70d7ac506 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -8,9 +8,13 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** N.B.: Using this encoding of vectors is discouraged. +See . *) +Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). + (** Definitions of Vectors and functions to use them - Author: Pierre Boutillier + Initial Author: Pierre Boutillier Institution: PPS, INRIA 12/2010 *) @@ -19,6 +23,7 @@ Names should be "caml name in list.ml" if exists and order of arguments have to be the same. complain if you see mistakes ... *) Require Import Arith_base. +#[local] Set Warnings "-stdlib-vector". Require Vectors.Fin. Import EqNotations. Local Open Scope nat_scope. diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v index c36917aa905a..8c284dce0257 100644 --- a/theories/Vectors/VectorEq.v +++ b/theories/Vectors/VectorEq.v @@ -8,12 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** N.B.: Using this encoding of vectors is discouraged. +See . *) +Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). + (** Equalities and Vector relations - Author: Pierre Boutillier + Initial Author: Pierre Boutillier Institution: PPS, INRIA 07/2012 *) +#[local] Set Warnings "-stdlib-vector". Require Import VectorDef. Require Import VectorSpec. Import VectorNotations. diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v index 6bbc6b97d30c..b061821297d9 100644 --- a/theories/Vectors/VectorSpec.v +++ b/theories/Vectors/VectorSpec.v @@ -8,12 +8,17 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** N.B.: Using this encoding of vectors is discouraged. +See . *) +Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). + (** Proofs of specification for functions defined over Vector - Author: Pierre Boutillier + Initial Author: Pierre Boutillier Institution: PPS, INRIA 12/2010 *) +#[local] Set Warnings "-stdlib-vector". Require Fin List. Require Import VectorDef PeanoNat Eqdep_dec. Import VectorNotations EqNotations.