Вопросы по теме 'coq'
Как писать определения без аргументов в Coq?
У меня есть следующий индуктивный тип, определенный в Coq .
Inductive natlist : Type :=
| nil : natlist
| cons : nat -> natlist -> natlist.
Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil....
525 просмотров
schedule
03.04.2022
Что означает true = false в Coq?
[Я не уверен, что это подходит для переполнения стека, но здесь есть много других вопросов Coq, так что, возможно, кто-то может помочь.]
Я работаю над следующим из http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28 (чуть ниже, где вводится...
6649 просмотров
schedule
01.04.2023
Несогласованное поведение Coq относительно неявных параметров определений Let
Я обнаружил какое-то непоследовательное поведение Coq в отношении неявных параметров.
Section foo.
Let id1 {t : Set} (x : t) := x.
Let id2 {t : Set} (x : t) : t. assumption. Qed.
Check id2 (1:nat).
Check id1 (1:nat). (* Fails with "The...
233 просмотров
schedule
18.11.2022
Не удалось найти экземпляр для переменной
Контекст: я работаю над упражнениями по Software Foundations .
Theorem neg_move : forall x y : bool,
x = negb y -> negb x = y.
Proof. Admitted.
Theorem evenb_n__oddb_Sn : forall n : nat,
evenb n = negb (evenb (S n)).
Proof.
intros n....
2616 просмотров
schedule
17.02.2023
Ошибка при определении Аккермана в Coq
Я пытаюсь определить функцию Акерманна-Петерса в Coq и получаю сообщение об ошибке, которого я не понимаю. Как видите, я упаковываю аргументы a, b Аккермана в пару ab ; Я предоставляю упорядочение, определяющее функцию упорядочивания аргументов....
1765 просмотров
schedule
01.04.2022
Доказательство - Coq - Нужна ли индукция?
У меня есть сценарий, в котором я хочу доказать лемму, включающую ряд строковых и списковых переменных. Возможно, для этого нужна «индукция», но может ли кто-нибудь помочь мне в доказательстве приведенной ниже леммы. Если нужен остальной код, я могу...
200 просмотров
schedule
08.10.2022
Используя экзистенциальную теорему в Coq
У меня есть следующая теорема в Coq: Theorem T : exists x:A, P x. Я хочу иметь возможность использовать это значение в последующем доказательстве. I.E. Я хочу сказать что-то вроде: «пусть o представляет такое значение, что P o . Я знаю, что o...
521 просмотров
schedule
10.08.2022
Ошибка типа внутри и снаружи раздела
У меня есть функция " HF " с типом внутри раздела S
Open S.
HF: forall f : dup_sig Sig, dup_ar f = ASignature.arity (F f)
End S.
Signature: Type
Sig: Signature
dp_Sig : Signature
dup_sig : Signature -> Signature
F : dup_sig Sig ->...
40 просмотров
schedule
16.05.2024
Как объединить два дерева в coq?
Упомянутые здесь деревья обладают тем свойством, что на всех поддеревьях (включая все дерево) содержимое корня имеет наивысший приоритет; но порядок не указан на родственных узлах. Дерево определяется следующим образом:
Inductive tree : Set :=...
343 просмотров
schedule
03.09.2022
Добавление гипотез, которых нет в текущих гипотезах
У меня есть доказательство, и в моей гипотезе есть:
...
l0 : list
(list (ATrs.rule (Sig a)) * boolean * option (list positiveInteger) *
option cpf.dpProof)
H: forall
x : list (ATrs.rule (Sig a)) * bool * option (list...
220 просмотров
schedule
28.06.2023
Рекомендации по эффективному использованию базы данных подсказок Coq
«Вопрос, который вы задаете, кажется субъективным и, скорее всего, будет закрыт».
Ну, я это знаю, но все же кажется, что стоит спросить здесь.
Мне много раз говорили, что я должен использовать базу данных подсказок и авто, потому что это...
744 просмотров
schedule
17.06.2022
Новый прицел в Coq
Я хотел бы иметь свой собственный объем, чтобы играть с длинными дистрибутивами.
Declare Scope my_scope.
Delimit Scope my_scope with my.
Open Scope my_scope.
Definition f (x y a b : nat) : nat := x+y+a+b.
Notation "x < y * a = b" := (f x y a...
1593 просмотров
schedule
12.08.2022
Доказательство менее чем
Я пытаюсь доказать некоторые теоремы о less_than в Coq. Я использую это индуктивное определение:
Inductive less_than : nat->nat->Prop :=
| lt1 : forall a, less_than O (S a)
| lt2 : forall a b, less_than a b -> less_than a (S b)...
86 просмотров
schedule
17.07.2023
Гипотеза универсальной количественной оценки в Coq
Я хочу изменить гипотезу H из формы ниже
mL : Map
mR : Map
H : forall (k : RecType) (e : String.string),
MapsTo k e (filter (is_vis_cookie l) mL) <->
MapsTo k e (filter (is_vis_cookie l) mR)...
197 просмотров
schedule
21.06.2022
Как сделать нотации видимыми вне подписи модуля в Coq?
Я определил сигнатуру модуля в Coq, которая определяет несколько обозначений. Однако, когда я пытаюсь использовать эти обозначения вне подписи, Coq терпит неудачу. Упрощенная версия моего кода приведена ниже. Любая помощь будет оценена по...
340 просмотров
schedule
12.05.2023
Извлечение в файл OCaml с помощью рекурсивного извлечения в Coq
Я хочу извлечь функцию foo из Coq в файл OCaml . Поскольку моя реальная функция должна использовать Recursive Extraction , когда я запускаю программу, она выводит извлеченный код OCaml в cmd . Но хотелось бы вывести в файл, например: foo.ml...
169 просмотров
schedule
22.04.2023
Concoqtion (Coq + MetaOCaml) — почему отказались?
Прежде чем беспокоить людей в списке рассылки OCaml, я подумал, что могу опубликовать свой вопрос здесь. Я только что обнаружил эту красоту (ссылка на сайт Concoqtion). Concoqtion — это расширение MetaOCaml, которое позволяет использовать...
371 просмотров
schedule
18.12.2022
Понимание семантики кода
У меня есть код OCaml, и мне трудно формализовать функцию mi_pol в Coq, потому что я не совсем понимаю, что именно работает в этом коде, например, на
aux (vec_add add const (vector ci v)) args ps
а также
args.(i-1) <- mat_add add...
99 просмотров
schedule
13.08.2023
Как определить мои собственные (рекурсивные) нотации Coq?
Я начал много работать с Ensemble s, потому что они более гибкие. Чтобы помочь мне в этом, я пытаюсь дать несколько удобных обозначений. Например, относительно легко сделать следующее:
Notation "a ∈ S" := (@In _ S a) (at level 80).
И я...
1202 просмотров
schedule
29.07.2023
Coq: проблемы со списком в индуктивном
Я новичок в Coq, но с некоторыми усилиями мне удалось доказать различные индуктивные леммы. Однако я застреваю на всех упражнениях, в которых используется следующее индуктивное определение:
Inductive In (A:Type) (y:A) : list A -> Prop :=...
1260 просмотров
schedule
30.05.2023
