Quelle bibliothèque de vecteurs utiliser dans coq?

Je me demande, y at-il une bibliothèque couramment utilisée pour les vecteurs dans coq, I.e. listes indexées par leur longueur dans leur type.Quelle bibliothèque de vecteurs utiliser dans coq?

Certains tutoriels font référence à Bvector, mais il n'est pas trouvé lorsque j'essaie de l'importer.

Il y a Coq.Vectors.Vectordef, mais le type défini ici est simplement nommé t ce qui me fait penser qu'il est destiné à un usage interne.

Quelle est la pratique la meilleure ou la plus courante pour quelqu'un qui ne veut pas rouler sa propre bibliothèque? Est-ce que je me trompe sur les vecteurs dans la bibliothèque standard? Ou y a-t-il un autre Lib que j'ai manqué? Ou les gens utilisent-ils simplement des listes, jumelées à des preuves de leur longueur?

Source

2017-02-17 jmite

Je pense que @ejgallego répond à cette question dans ce [fil du coq-club] (https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00099.html). Aussi, [cette réponse] (http://stackoverflow.com/a/30159566/2747511) par Arthur Azevedo de Amorim a le même esprit: "Alors que les types dépendants sont intéressants pour certaines choses, on ne sait pas à quel point ils sont utiles en général Mon impression est que certains pensent qu'ils sont très compliqués à utiliser, et que l'avantage d'avoir certaines propriétés exprimées au niveau du type plutôt que de les avoir comme théorèmes séparés ne vaut pas cette complexité supplémentaire. " –

En outre, vous pouvez 'Require Vector' (sans importer) et utiliser le nom qualifié' Vector.t'. –

@AntonTrunov Savez-vous pourquoi il s'appelle t? – jmite

Il y a généralement trois approches de vecteurs en Coq, chacun avec leurs propres compromis:

vecteurs définis inductivement, comme il est prévu par la bibliothèque standard Coq.
Listes associées à une affirmation de leur longueur.
Tuples imbriqués récursivement.

Listes avec longueur sont bien en ce qu'ils sont facilement sous la contrainte à des listes, de sorte que vous pouvez réutiliser un grand nombre de fonctions qui opèrent sur des listes simples. Les vecteurs inductifs ont l'inconvénient d'exiger beaucoup de correspondance de motifs dépendants, en fonction de ce que vous faites avec eux.

Pour la plupart des développements, je préfère la définition de tuple récursive:

Definition Vec : nat -> Type := 
    fix vec n := match n return Type with 
       | O => unit 
       | S n => prod A (vec n) 
       end.

Source

2017-02-22 04:14:52

"Les vecteurs inductifs ont l'inconvénient d'exiger beaucoup de correspondance de motifs typés de manière dépendante". Ouais, cela ressemble à quelque chose que Coq est plus faible par rapport à Agda. – jmite

Je travaille beaucoup avec des vecteurs en Coq et je me sers module standard Coq.Vectors.Vector. Il utilise la définition de vecteur inductive de manuel.

Le problème principal est qu'avec cette approche, il faut un moulage de type fastidieux dans les situations où un vecteur de longueur, disons a+b et b+a ne sont pas du même type. J'ai aussi fini par utiliser la bibliothèque Coq CoLoR (opam instal coq-color) qui inclut le paquet CoLoR.Util.Vector.VecUtil qui contient beaucoup de lemmes et de définitions utiles pour les vecteurs. J'ai fini par écrire encore plus dessus.

Source

2017-10-20 01:25:35 krokodil

Quelle bibliothèque de vecteurs utiliser dans coq?

Répondre

Questions connexes