Вопросы по теме 'coq'
Доказательство f (f bool) = bool
Как я могу в coq доказать, что функция f , которая принимает bool true|false и возвращает bool true|false (показано ниже), при двойном применении к одному bool true|false всегда будет возвращать одно и то же значение true|false :
(f:bool...
1396 просмотров
schedule
24.07.2023
Каковы практические ограничения полного языка, отличного от Тьюринга, такого как Coq?
Поскольку существуют не полные по Тьюрингу языки, и, учитывая, что я не изучал Comp Sci в университете, может ли кто-нибудь объяснить что-то, что является неполным по Тьюрингу языком (например, Coq ) не может?
Или полнота / неполнота не...
9161 просмотров
schedule
28.05.2023
Странное поведение точки с запятой в Coq
У меня возникли проблемы с пониманием того, почему мой код Coq не делает того, что я ожидаю в приведенном ниже коде.
Я попытался максимально упростить пример, но проблема больше не проявлялась, когда я сделал его еще проще.
Он использует файлы...
444 просмотров
schedule
29.05.2022
Глифы Unicode для ключевых слов и операторов в Coq / Proof General под Emacs
Этот вопрос связан с настройкой режима Coq в Proof General в Emacs.
Я пытаюсь заставить Emacs автоматически заменять ключевые слова и обозначения в Coq соответствующими глифами Unicode. Мне удалось определить fun как греческую строчную лямбду λ,...
1045 просмотров
schedule
10.02.2023
Используя coq, пытаюсь доказать простую лемму о деревьях
Пытаясь доказать корректность функции вставки элементов в bst, я застрял, пытаясь доказать, казалось бы, тривиальную лемму. Моя попытка до сих пор:
Inductive tree : Set :=
| leaf : tree
| node : tree -> nat -> tree -> tree.
Fixpoint...
576 просмотров
schedule
08.07.2023
Используйте Coq, чтобы доказать разницу между относительными числами
Как вы докажете: forall m n : Z, m < n -> m -n < O в Coq? Огромное спасибо!
103 просмотров
schedule
13.05.2023
Взаиморекурсивная функция и проверка завершения в Coq
ИЗМЕНИТЬ
Require Import Bool List ZArith.
Variable A: Type.
Inductive error :=
| Todo.
Inductive result (A : Type) : Type :=
Ok : A -> result A | Ko : error -> result A.
Variable bool_of_result : result A ->...
966 просмотров
schedule
07.02.2022
Выполнение большого проекта Coq с большим количеством файлов
У меня есть проект Coq с несколькими файлами (скажем, x1.v, x2.v,... xn.v), включая Makefile, хранящийся в папке "C:\Users\WK\Desktop\Personal\coq-project" и установил Coq 8.3 в "C:\Coq" на моем компьютере с Windows 7.
Программы Coq (файлы)...
1456 просмотров
schedule
10.09.2023
Нечетный лямбда-синтаксис в Coq
Я читаю CPDT и есть один пример, который я не понимаю :
Definition plus_rec : nat -> nat -> nat :=
nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)).
Большая часть этого имеет смысл, за исключением...
960 просмотров
schedule
02.06.2023
Рекурсивная функция в Coq
Inductive my_type :=
| Type_pol : Z -> my_type
| Type_matrix : Z -> my_type.
Inductive redPair :=
| RedPair_interpretation : my_type -> redPair.
Inductive orderingProof :=
| OrderingProof_redPair : redPair -> orderingProof....
513 просмотров
schedule
24.11.2022
Как указать уменьшение размера двух индуктивных типов Coq
Я пытаюсь определить индуктивный тип game для комбинаторных игр. Мне нужен метод сравнения, который показывает, являются ли две игры lessOrEq , greatOrEq , lessOrConf или greatOrConf . Затем я могу проверить, равны ли две игры, если они обе...
1708 просмотров
schedule
02.03.2022
Общая рекурсия и индукция в Coq
Предположим, что у меня есть
тип Т
обоснованное отношение R: T-> T-> Prop
функция F1: T-> T, которая делает аргумент «меньше»
условие C: T-> Prop, которое описывает "начальные значения" R
функция F2: T-> T, которая увеличивает аргумент...
535 просмотров
schedule
01.12.2023
Coq, Образец, соответствующий аксиоме с подстановочным знаком
Я работал с Coq и столкнулся с некоторыми проблемами, пытаясь сопоставить объекты, созданные с помощью Axiom, с использованием подстановочного знака. Я создал минимальную программу Coq, которая демонстрирует мою проблему.
Inductive MyType : Set...
258 просмотров
schedule
23.07.2022
coq ошибка при попытке использовать Case. Пример из книги «Основы программного обеспечения»
Я пытаюсь изучить Coq, просматривая онлайн-книгу «Основы программного обеспечения»: http://www.cis.upenn.edu/~bcpierce/sf/
Я использую интерактивный интерпретатор Coq coqtop из командной строки.
В главе, посвященной индукции (...
1470 просмотров
schedule
12.03.2022
Определение COQ Карри Ховарда (A - ›B -› C) - ›(B -› A - ›C) с использованием множеств
Я часами смотрю этому в лицо, не понимая :(
Мне нужно решить некоторые определения с помощью coq, и я должен сделать это с помощью изоморфизма Карри Ховарда. Я прочитал и до сих пор не понимаю, что делаю. Я смотрел другие примеры и пробовал...
457 просмотров
schedule
29.11.2023
Индуктивный предикат для добавления в Coq
Я новичок в индуктивных предикатах в Coq. Я научился определять простые индуктивные предикаты, такие как «даже» (как в adam.chlipala.net/cpdt/html/Predicates.html) или «последний» (как в...
271 просмотров
schedule
04.10.2023
Proof of Paper, Scissor, Rock как экземпляр моноида в Coq
Итак, изучая Coq, я сделал простой пример с игрой бумага, ножницы, камень. Я определил тип данных.
Inductive PSR : Set := paper | scissor | rock.
И три функции:
Definition me (elem: PSR) : PSR := elem.
Definition beats (elem: PSR) : PSR...
169 просмотров
schedule
25.11.2022
Использование запоминания в индукции по высказыванию приводит к некорректной типизации ошибки в Coq.
Вот индуктивные и вычислительные определения четности натуральных чисел.
Inductive ev : nat -> Prop :=
| ev_0 : ev O
| ev_SS : forall n:nat, ev n -> ev (S (S n)).
Definition even (n:nat) : Prop :=
evenb n = true.
И...
436 просмотров
schedule
18.05.2023
В чем разница между Qed и Defined?
В интерактивном средстве доказательства теорем Coq любое интерактивное доказательство или определение может завершаться либо Qed , либо Defined . Есть понятие "непрозрачности", которое Qed обеспечивает выполнение, но Defined нет. Например,...
860 просмотров
schedule
19.11.2022
Преобразовать ~exists в forall в гипотезе
Я застрял в ситуации, когда у меня есть гипотеза ~ (exists k, k <= n+1 /\ f k = f (n+2)) и я хочу преобразовать ее в эквивалентную (надеюсь) гипотезу forall k, k <= n+1 -> f k <> f (n+2) .
Вот небольшой пример:
Require Import...
1374 просмотров
schedule
07.01.2023
