Описание тега coq

Описание тега Вопросы с тегом
Coq - это формальная система управления доказательствами, полуинтерактивный инструмент доказательства теорем и язык функционального программирования. Coq используется для проверки программного обеспечения, формализации языков программирования, формализации математических теорем, обучения и многого другого. В связи с интерактивным характером Coq, мы рекомендуем задать вопросы для ссылки на исполняемые примеры на https://x80.org/collacoq/, если это будет сочтено целесообразным.
2 ответа

Как мне прочитать определение ex_intro?

Я читаю вводный урок Майка Нахаса по Coq, в котором говорится: Аргументы для ex_intro: предикат свидетель доказательство предиката, вызванного со свидетелем Я посмотрел на определение: Inductive ex (A:Type) (P:A -> Prop) : Prop := ex_intro : fora…
04 авг '16 в 21:32
1 ответ

Используйте False_rec для создания псевдонима типа списка в Coq

Я хотел бы создать зависимую функцию, но я сталкиваюсь с ошибкой несоответствия типов на False_rec срок. Я пытаюсь сделать что-то похожее на следующее: Definition env A := list A. Fixpoint zip (xs ys : env nat) (H : length xs = length ys) : env (nat…
24 авг '18 в 16:21
0 ответов

Восстановление лямбд в Coq без равенства экстенсиональных функций?

Я перейду к основам программного обеспечения. Есть два определения данной функции обратного списка. Fixpoint rev (l:natlist) : natlist := match l with | nil => nil | h :: t => rev t ++ [h] end. и хвост-рекурсивный: Fixpoint rev_append {X} (l1 …
07 окт '16 в 08:15
1 ответ

Рекурсивное использование методов класса типов в Coq

Есть ли способ использовать рекурсию с классами типов Coq? Как, например, при определении шоу для списков, если вы хотите вызвать show функция для списков рекурсивно, тогда вам придется использовать точку фиксирования следующим образом: Require Impo…
15 сен '18 в 20:36
0 ответов

Докажите теорему об остатках в Китае, используя Coq

Я пытаюсь доказать китайскую теорему об остатках, используя Coq. Я уже доказал следующие леммы: Lemma modulo_tran : forall a b c n : Z, (a == b [ n ]) -> (b == c [ n ]) -> (a == c [ n ]) . Lemma modulo_plus_subst : forall a b c n : Z, (a == b …
27 ноя '18 в 12:21
1 ответ

Используйте Coq, чтобы доказать разницу между относительными числами

Как вы докажете: forall m n : Z, m < n -> m -n < O в Coq? Большое спасибо!
01 ноя '12 в 05:04
1 ответ

Канонические структуры в ssreflect

Я пытаюсь разобраться с каноническими структурами в ssreflect. Есть 2 фрагмента кода, которые я взял отсюда. Я принесу кусочки для bool и варианты типов. Section BoolFinType. Lemma bool_enumP : Finite.axiom [:: true; false]. Proof. by case. Qed. Def…
23 авг '17 в 13:55
2 ответа

Представление функций как типов

Функция может быть сильно вложенной структурой: function a(x) { return b(c(x), d(e(f(x), g()))) } Во-первых, интересно, есть ли у функции экземпляр. То есть оценка функции является экземпляром функции. В этом смысле тип - это функция, а экземпляр - …
08 июл '18 в 13:04
0 ответов

Генерал доказательства не может найти библиотеку или ее исходный файл даже с coq-load-path-include-current и coq-compile-before-require

Я на Windows 8.1 с доказательством общего 4.2 и Emacs 24.2.1. Я поставил coq-compile-before-require а также coq-load-path-include-current на, но когда я пытаюсь потребовать библиотеку, исходный файл которой находится в той же папке, я все еще получа…
10 авг '15 в 22:26
1 ответ

Почему Coq.Init.Logic определяет обозначение "A -> B"?

Файл Coq Standard Library Coq.Init.Logic, который можно найти здесь, содержит оператор Notation "A -> B" := (forall (_ : A), B) : type_scope. Я не понимаю, как это возможно, учитывая, что символ -> уже имеет встроенное значение. Является ->…
09 сен '18 в 18:27
0 ответов

Coq учебник по evars, e* тактика, контексты?

Я пытался найти хорошее руководство / чтение / набор упражнений по контекстам Coq, evars, e* тактике и т. Д. В идеале я хочу создать контекст Coq с некоторыми абстрагированными переменными, которые я заполню позже при извлечении OCaml или Haskell. В…
13 фев '18 в 16:14
1 ответ

Ltac: необязательные аргументы тактики

Я хочу сделать тактику Ltac в coq, которая будет принимать 1 или 3 аргумента. Я читал о ltac_No_arg в LibTactics модуль, но если я правильно понял, мне пришлось бы использовать мою тактику с помощью: Coq < mytactic arg_1 ltac_no_arg ltac_no_arg. …
30 июн '17 в 07:10
2 ответа

erewrite, который сначала просит гипотезу?

Я хочу вариант erewrite который сначала запрашивает гипотезу, а затем переходит к переписанной цели, а не наоборот. Вот небольшой пример: Variable P : Prop. Variable SomeProp: Prop -> Prop. Lemma rewriter: forall (R: Prop), SomeProp R -> P = R…
27 июн '18 в 10:41
2 ответа

Почему нельзя сделать вывод, что 0+n=n в этой зависимо типизированной программе?

Я начинаю использовать Coq, и я хотел бы определить некоторые типизированные программы. Учтите следующее: Inductive natlist : nat -> Type := | natnil : natlist 0 | natcons : forall k, nat -> natlist k -> natlist (S k). Fixpoint natappend (n…
14 мар '16 в 13:40
0 ответов

Как развернуть Coq Fixpoint буквально

Я пытался раскрыть Fixpoint определение и получить тело определения. Но Coq не дал бы буквально основную часть определения. Вместо этого он дает мне что-то, начиная с (fix ...), который я не могу использовать. Например, при доказательстве следующего…
27 июл '16 в 04:03
2 ответа

Использование forall в определении рекурсивной функции

Я пытаюсь использовать функцию, чтобы определить рекурсивное определение, используя меру, и я получаю ошибку: Error: find_call_occs : Prod Я публикую весь исходный код внизу, но моя функция Function kripke_sat (M : kripke) (s : U) (p : formula) {mea…
13 дек '10 в 19:37
1 ответ

Как использовать тактику с гипотезой в Coq?

Я новичок в Coq, и я зашел в тупик. У меня есть индуктивное определение, которое выглядит примерно так (я определил принять индуктивно раньше): Inductive fun : accepts -> Prop := | fn1 : fun True | fn2 : forall (n : nat )(A : accepts), fun A -&gt…
10 мар '16 в 17:47
1 ответ

Elim гипотеза двойного отрицания в Coq Proof Assistant?

Может ли кто-нибудь объяснить мне, почему мы должны доказать ~A после elim Ha.? Перед "элим ха" 1 subgoals A : Prop Ha : ~ ~ A ______________________________________(1/1) A После 1 subgoals A : Prop Ha : ~ ~ A ______________________________________(…
02 июн '14 в 13:44
1 ответ

Есть ли какая-то тактика для работы с предусловиями с "и"?

Моя цель как ниже. Есть ли какая-то тактика для решения этих тривиальных задач? Goal forall A (x : A) P Q, (forall y, P y /\ Q y) -> Q x. Proof. intros. intuition. auto. Abort. (* a more complex version *) Goal forall A (x : A) P Q R, (forall y, …
09 янв '19 в 00:27
2 ответа

Как переключиться на конкретную версию Coq?

В настоящее время я использую стандартный, который я установил стандартным способом (вероятно, через веб-сайт). Но я хочу использовать tcoq. Я полагаю, что установил его правильно, потому что у меня есть файл bin и все обычные вещи Coq, кажется, там…
28 янв '19 в 01:33