Какую векторную библиотеку использовать в coq?

Мне интересно, существует ли обычно используемая библиотека для векторов в coq, I.e. списки, индексированные по их длине в их типе.Какую векторную библиотеку использовать в coq?

Некоторые учебные пособия ссылаются на Bvector, но его не обнаруживают, когда я пытаюсь импортировать его.

Существует Coq.Vectors.Vectordef, но тип, определенный здесь, называется только t, что заставляет меня думать, что он предназначен для внутреннего использования.

Что является лучшей или наиболее распространенной практикой для тех, кто не хочет катить свою собственную библиотеку? Я ошибаюсь в отношении векторов в стандартной библиотеке? Или есть еще один Либ, которого я не хватает? Или люди просто используют списки, в сочетании с доказательствами их длины?

источник

2017-02-17 jmite

Я думаю, что @ejgallego отвечает на этот вопрос в этой [coq-club thread] (https://sympa.inria.fr/sympa/arc/coq-club/2017-01/msg00099.html). Кроме того, [этот ответ] (http://stackoverflow.com/a/30159566/2747511) Артура Азеведо де Аморима имеет тот же дух: «Хотя некоторые из них интересны для некоторых вещей, неясно, насколько полезны они вообще У меня сложилось впечатление, что некоторые считают, что они очень сложны в использовании, и что преимущество наличия определенных свойств, выраженных на уровне типа, в сравнении с их как отдельными теоремами, не стоит этой дополнительной сложности ». –

Кроме того, вы можете «потребовать вектор» (без импорта) и использовать квалифицированное имя 'Vector.t'. –

@ Антон Трунов, ты знаешь, почему это называется т? – jmite

Есть три общих подхода к векторам в Coq, каждый со своими компромиссами:

индуктивно определенные векторы, как это предусмотрено в стандартной библиотеке Coq.
Списки в паре с утверждением их длины.
Рекурсивно-вложенные кортежи.

Списки-с длиной хороши тем, что они легко принуждены к спискам, так что вы можете использовать множество функций, которые работают на простых списках. Индуктивные векторы имеют недостаток, требующий много зависимого от шаблона сопоставления шаблонов, в зависимости от того, что вы делаете с ними.

Для большинства событий, я предпочитаю рекурсивное определение кортежа:

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

источник

2017-02-22 04:14:52

«Индуктивные векторы имеют недостаток, требуя много зависимого от шаблона соответствия шаблону». Да, это похоже на то, что Coq слабее по сравнению с Agda. – jmite

Я активно работаю с векторами в Coq, и я использую стандартный Coq.Vectors.Vector модуль. Он использует определение индуктивного вектора учебника.

Основная проблема заключается в том, что для этого подхода требуется утомительный тип литья в ситуациях, когда вектор длины, например a+b и b+a, относится не к одному типу.

Я также закончил использование библиотеки Coq CoLoR (opam instal coq-color), которая включает в себя пакет CoLoR.Util.Vector.VecUtil, который содержит множество полезных лемм и определений для векторов. В конце концов я написал еще больше.

источник

2017-10-20 01:25:35 krokodil

Какую векторную библиотеку использовать в coq?

ответ

Смежные вопросы