Описание тега coq-plugin
2
ответа
Использование forall в определении рекурсивной функции
Я пытаюсь использовать функцию, чтобы определить рекурсивное определение, используя меру, и я получаю ошибку: Error: find_call_occs : Prod Я публикую весь исходный код внизу, но моя функция Function kripke_sat (M : kripke) (s : U) (p : formula) {mea…
13 дек '10 в 19:37
0
ответов
Coq: перенести тактику Ltac с использованием стиля CPS на тактику ML (плагин OCaml)
Я пытаюсь перенести тактику Coq (в настоящее время написанную на Ltac) на OCaml, чтобы иметь возможность более легко расширять эту тактику (и избежать хаков, которые мне понадобились для эмуляции в Ltac некоторых структур данных, которые в остальном…
04 сен '18 в 18:51
1
ответ
Как настроить цвета для Command и Tactic в ProofGeneral при использовании Coq в Emacs?
Я хочу раскрасить какую-то конкретную команду и тактику в другой цвет, например, я хочу, чтобы команды "Печать" и "Найти" были серыми, а "индукция" - каким-то особым цветом, отличным от других тактик. Возможно ли это в ProofGeneral? Если это не наст…
09 окт '18 в 03:08
1
ответ
Как сделать переписывание терминов высшего порядка в Coq?
Этот вопрос основан на моем вопросе https://cs.stackexchange.com/questions/96533/how-to-transform-lambda-function-to-multi-argument-lambda-function-and-how-to-re Есть две функции и два термина в этом вопросе: Функции: is: (e->t)->(e->t) IS:…
24 авг '18 в 10:38
1
ответ
Переписать работает для целого числа, но не для рациональных для Coq aac_tactics
Я тестировал тактику переписывания Coq по модулю ассоциативности и коммутативности (aac_tactics). Следующий пример работает для целого числа (Z), но выдает ошибку, когда целые числа заменяются рациональными (Q). Require Import ZArith. Import Instanc…
25 июн '16 в 04:32
1
ответ
Каковы стандартные практики для разработки кода Coq в редакторе Atom?
Я хотел разработать некоторый код Coq в Atom. Я хотел иметь возможность проверять мой код построчно, как обычно, как с CoqIDE или emacs proof general. Есть ли что-то подобное для atom или как люди разрабатывают код Coq в редакторе Atom? некоторые сс…
30 ноя '18 в 02:06
1
ответ
OCaml и препроцессор имеют ошибку несовместимых версий при установке tcoq
Я пытался установить tcoq, и у меня была следующая ошибка: "/Users/pinocchio/.opam/4.05.0/bin/ocamlfind" ocamlc -rectypes -w -3-52-56 -c grammar/compat5.ml OCAMLC -c -pp grammar/gramCompat.mlp >> Fatal error: OCaml and preprocessor have incomp…
26 дек '18 в 00:51
1
ответ
Как использовать тактику Coq aac, чтобы доказать равенство в цели?
Я предполагаю, что Coq aac_tactics (8.5p1) должен уметь общаться с асс. и коммутативность. Но я не могу понять, как использовать это доказать простые равенства, такие как 2 + y + 5 = 7 + y Например: Require Import AAC_tactics.AAC. Require Import AAC…
25 июн '16 в 06:06
1
ответ
Где установлен Coq aac_tactics?
Я тестировал библиотеку тактик AAC на предмет переписывания по модулю ассоциативности и коммутативности. Согласно веб-сайту Coq, нужно: В зависимости от вашей установки, измените следующие две строки или добавьте их в файлы.coqrc, заменив "." с путе…
24 июн '16 в 17:26
1
ответ
Paramcoq: свободные теоремы в Coq
Как я могу доказать следующую бесплатную теорему с плагином Paramcoq? Lemma id_free (f : forall A : Type, A -> A) (X : Type) (x : X), f X x = x. Если это невозможно, то какова цель этого плагина?
11 мар '19 в 22:46
0
ответов
Как настроить Coq в качестве средства доказательства теорем для логики первого порядка
Насколько я понимаю, в Coq встроена логика первого порядка https://coq.inria.fr/tutorial/1-basic-predicate-calculus. Но Coq не доказатель теорем, Coq - помощник по проверке, и это означает, что пользователь должен предоставить некоторые подсказки, к…
14 май '19 в 21:14
1
ответ
Как получить имя названной цели в coq api
В настоящее время я работаю над программой ocaml, которая будет использовать coq api для извлечения информации о доказательствах и их целях. Для этого я хочу извлечь имя, данное цели, когда использовалось "уточнение?[Имя]" или какая-то другая тактик…
29 июл '20 в 15:23