0
ответов
рекурсивно инвертировать гипотезы в coq
У меня возникли проблемы с определением тактики рекурсивного инвертирования гипотез в контексте доказательства. Например, предположим, что у меня есть контекст доказательства, содержащий такую гипотезу: H1: search_tree (node a (node b ...
вопрос задан: 30 December 2011 21:08
0
ответов
Разрушение в результате применения функции предиката
Я новичок в Coq, и у меня есть быстрый вопрос о тактике уничтожения. Предположим, у меня есть функция count, которая подсчитывает количество вхождений данного натурального числа в список натуральных чисел: ...
вопрос задан: 27 December 2011 00:47
0
ответов
Несогласованное поведение Coq в отношении неявных параметров определений Let
Я нашел несколько своего рода противоречивое поведение Coq относительно неявных параметров. Раздел foo. Пусть id1 {t: Set} (x: t): = x. Пусть id2 {t: Set} (x: t): t. предположение. Qed. Проверьте id2 (1: ...
вопрос задан: 15 November 2011 22:03
0
ответов
Построение иерархии классов в Coq?
Я могу наивно построить иерархию алгебраических структур в Coq, используя классы типов. У меня проблемы с поиском ресурсов по синтаксису и семантике Coq для классов типов. Однако я считаю, что ...
вопрос задан: 3 November 2011 04:41
0
ответов
Что означает V в расширении файла Coq?
Является ли .v для проверки? Проверка? ваманос? Почему бы не использовать расширение .coq?
вопрос задан: 1 November 2011 07:18
0
ответов
Как импортировать модули в Coq?
У меня проблемы с импортом определений из модулей в Coq. Я новичок в Coq, но не смог решить проблему с помощью справочного руководства по языку или онлайн-руководства. У меня есть модуль, который определяет ...
вопрос задан: 26 October 2011 23:17
0
ответов
Параметр подмножества
У меня есть набор в качестве параметра: Параметр Q: Установить. Теперь я хочу определить другой параметр, который является подмножеством Q. Что-то вроде: Параметр F: подмножество Q. Как я могу это определить? Думаю, я могу добавить ...
вопрос задан: 4 March 2011 13:09
0
ответов
Сохранение информации при использовании индукции?
Я использую Coq Proof Assistant для реализации модели (небольшого) языка программирования (расширение реализации Featherweight Java Бруно Де Фрейн, Эрик Эрнст, Марио Зюдхольт). Одно дело ...
вопрос задан: 24 December 2010 12:47
0
ответов
Введение в coq?
Я пытаюсь (классически) доказать ~ (forall t: U, phi) -> существует t: U , ~ phi в Coq. Я пытаюсь доказать это противоположным образом: 1. Предположим, что такого t нет (так что ~ (существует t: U, ~ phi)) ...
вопрос задан: 11 December 2010 17:08