coqで使用するベクターライブラリはどれですか？

Question

私は、coqのベクターによく使用されるライブラリがあるのだろうかと疑問に思っています。型の長さでインデックスされたリスト

一部のチュートリアルではBvectorを参照していますが、インポートしようとすると見つかりません。

Coq.Vectors.Vectordefがありますが、そこに定義されているタイプはちょうどtという名前で、内部使用を意図しています。

自分のライブラリーを転載したくない人にとって、最も優れた、最も一般的な方法は何ですか？私は標準ライブラリのベクターについて間違っていますか？それとも、別のリブがありますか？あるいは、人々は長さの証明と組み合わせたリストを使うだけですか？

Answer 1

Coqの中のベクトルに3つのアプローチは、一般的にありますが、自分のトレードオフを持つ各：Coqの標準ライブラリで提供される

1. 誘導は、ベクトルを定義しました。

2. リストは長さのアサーションとペアになっています。

3. 再帰的にネストされたタプル。

リストの長さは、リストに簡単に強制されている点で優れているため、プレーンリストで動作する多くの関数を再利用できます。誘導ベクトルは、あなたがそれらで何をしているかに依存して、多くの依存型パターンマッチングを必要とするという欠点があります。最も発展のために

、私は再帰的タプルの定義を好む：

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

Answer 2

私はCoqの内のベクトルで広範囲に働いていると私は標準Coq.Vectors.Vectorモジュールを使用しています。これは、教科書誘導ベクトル定義を使用しています。

主な問題は、長さのベクトル、たとえばa+bとb+aが同じタイプではない状況で退屈な型キャストが必要であるということです。

また、ベクトルを含むCoq CoLoRライブラリ（opam instal coq-color）を使用しました。これには、多くの有用な補題とベクトルの定義が含まれています。私はそれの上にさらに書くことに終わった。