Вопросы по теме 'coq-tactic'
Как применить функцию один раз во время упрощения в Coq?
Насколько я понимаю, вызовы функций в Coq непрозрачны. Иногда мне нужно использовать unfold , чтобы применить его, а затем fold , чтобы вернуть определение / тело функции к ее имени. Это часто бывает утомительно. Мой вопрос: есть ли более простой...
1806 просмотров
schedule
09.07.2023
Есть ли соглашение о порядке применения тактики / подсказок ssreflect?
Я пытаюсь понять, как комбинированные тактики ssreflect должны быть «декомпозированы» (или как они складываются в первую очередь). Одна из моих проблем - понять порядок и ассоциативность татикалов.
Иногда мне кажется, что порядок идет справа...
121 просмотров
schedule
25.09.2022
Как использовать приложение для извлечения импликации в Coq
Я проиллюстрирую это на примере.
H : R -> P -> Q
H0 : R
Подцель:
(Q -> P) \ / (P -> Q)
поэтому мой вопрос в том, как мне извлечь (P-> Q). У меня уже есть R, но когда я «применяю H в H0», он оценивает все и дает мне Q.
93 просмотров
schedule
29.03.2022
Coq - недокументированная ошибка при индукции с eqn:
Используя Coq 8.4pl3, я получаю сообщение об ошибке при индукции с вариантом eqn: , который не указан в разделе индукции в справочном руководстве.
(* Export below requires Software Foundations 4.0. *)
Require Export Logic.
Inductive disjoint (X...
133 просмотров
schedule
20.03.2022
Разделите цель соединения на подцели
Рассмотрим следующее игрушечное упражнение:
Theorem swap_id: forall (m n : nat), m = n -> (m, n) = (n, m).
Proof.
intros m n H.
На данный момент у меня есть следующее:
1 subgoal
m, n : nat
H : m = n...
323 просмотров
schedule
12.01.2022
Как вытащить правую часть из равенства в coq
Если у меня есть следующее:
H : some complicated expression = some other complicated expression
и я хочу схватить
u := some other complicated expression
без жесткого кодирования в моем доказательстве (т. е. с использованием pose )...
88 просмотров
schedule
27.11.2023
Повышение уровня неудач тактики coq
При реализации сложной тактики в Ltac есть некоторые команды Ltac или вызов тактики, которые, как я ожидаю, потерпят неудачу и где это ожидается (например, чтобы завершить repeat или вызвать обратное отслеживание). Эти сбои обычно возникают на...
125 просмотров
schedule
08.10.2022
Упрощение подформул в Coq
Я пытаюсь решить уравнение вида
A * B * C * D * E = F
где * некоторая сложная левая ассоциативная операция.
На данный момент все непрозрачно (включая * и A до F ), и можно сделать прозрачным через autounfold with M_db .
Проблема...
270 просмотров
schedule
31.12.2022
На языке тактики coq в чем разница между интро и интро
На языке тактики Coq, в чем разница между
intro
и
intros ?
483 просмотров
schedule
01.09.2022
Примените функцию к обеим сторонам равенства в гипотезе Coq
Вопрос, который у меня есть, очень похож на вопрос, представленный в приведенной ниже ссылке, но на основе гипотезы, а не цели.
Примените функцию к обеим сторонам равенства в Coq?
Скажем, у меня есть следующее определение:
Definition...
887 просмотров
schedule
28.12.2023
Экзистенциальные цели выполняются слишком рано
У меня есть Class , содержащий как данные, так и аксиомы. Я хочу создать еще один экземпляр в режиме проверки на основе (1) существующего экземпляра и (2) некоторых других входных данных. Я хочу destruct этот второй ввод перед созданием нового...
59 просмотров
schedule
09.03.2023
Ltac: делайте что-то другое в каждой цели
У меня есть сценарий проверки, в котором я исследую несколько случаев, и в настоящее время он довольно медленный, поскольку у меня есть несколько стратегий для решения целей, и я пробую каждую из них в каждом случае.
Я знаю, что мне нужно применять...
217 просмотров
schedule
12.10.2023
Coq: Доказательство связи между ‹и ≤
Я изучаю Coq прямо сейчас, и в более крупном доказательстве меня озадачило следующее подкрепление:
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → n < m.
Или в разложенном виде:
Theorem sub : ∀ n m : nat, n ≤ m → n ≠ m → S n ≤ m....
224 просмотров
schedule
08.04.2024
Coq просто / разворачивается только один раз. (Замените часть цели результатом одной итерации функции.)
Я преподаю в университете на курсе Системы типов языков , и профессор использовал следующий пример для индуктивных доказательств в теории типов на доске на прошлой лекции:
Предположим, что есть натуральные числа, определенные индуктивно (по...
389 просмотров
schedule
02.06.2022
Объединение баз данных подсказок в ядро
Есть ли способ добавить все леммы в базу данных подсказок в ядро, чтобы мне не приходилось писать auto with foo везде в файле?
30 просмотров
schedule
15.11.2023
Вариант индукционной тактики, не требующий использования слова «запомнить» в подтермах
Скажем, у меня есть два отношения R1 и R2 . Если мне нужно решить проблему индукцией по члену R1 A (R2 B C) , мне нужно сначала сделать remember R2 B C , иначе я потеряю информацию о том, что второй аргумент R1 был равен R2 B C . Есть ли...
22 просмотров
schedule
18.05.2023
Применение зависимого типа к аргументу для утверждения цели в Coq?
Если у меня есть такая общая установка, как следующая, как я могу доказать, что утверждаю (f a)?
A : Type
f : A -> Prop
a : A
...
============================
f a
В частности, почему я не могу использовать любую из этих тактик и что...
55 просмотров
schedule
30.04.2023
Дает ли что-нибудь использование тактики разворота с последующим сбросом в Coq?
Добьется ли когда-нибудь unfold def. fold def. чего-нибудь в доказательстве Coq?
Иными словами: будет ли когда-нибудь разница между этими двумя последовательностями применения тактики?:
unfold def. fold def. cbn.
cbn.
107 просмотров
schedule
29.12.2022
Ошибка Coq: невозможно объединить true с is_true (0 ‹a - b - 3)
Не уверен, что делаю неправильно, но я думал, что reflexivity должен работать ниже, но это не так.
a, b : nat
H : (1 <=? a - b - 3) = true
______________________________________(1/7)
is_true (0 < a - b - 3)
Я также пробовал apply...
96 просмотров
schedule
23.02.2023
