Вопросы по теме 'coq-tactic'
Как ввести новую переменную в Coq?
Мне было интересно, есть ли способ ввести совершенно новую переменную во время доказательства теоремы в Coq?
В качестве полного примера рассмотрим следующее свойство отсюда о равномерности длины списка.
Inductive ev_list {X:Type}: list X ->...
4176 просмотров
schedule
18.12.2022
Как выполнить вычисление в Coq ровно один раз?
У меня есть доказательство ниже с еще тремя подцелями. Доказательство касается правильности оптимизации plus 0 ( optimize_0plus ) на простом арифметическом языке, продемонстрированном здесь . aexp - это «арифметическое выражение», а aeval -...
526 просмотров
schedule
11.10.2022
Всегда ли возможен такой переход от квантора существования к квантору всеобщности?
Я читаю/тестирую доказательство в Coq
Theorem ceval_step__ceval: forall c st st',
(exists i, ceval_step st c i = Some st') -> c / st || st'.
Конкретные функции/определения не имеют значения, поскольку они не используются. Через...
454 просмотров
schedule
23.12.2023
Использование тактики "зависимой индукции" для сохранения информации во время индукции
Я только что столкнулся с проблемой, когда Coq induction отбрасывает информацию о сконструированных терминах при чтении доказательства из здесь .
Авторы использовали что-то вроде:
remember (WHILE b DO c END) as cw eqn:Heqcw.
переписать...
580 просмотров
schedule
15.07.2023
Как использовать неравенство для упрощения if-then-else в Coq?
Я нахожусь в середине доказательства, где я сгенерировал два случая
destruct (eq_id_dec Y X)
( eq_id_dec по характеру похож на eq_nat_dec ).
Это дает два случая с добавленными предположениями e: Y = X для равенства и n: Y <> X...
545 просмотров
schedule
28.02.2024
Как доказать (n = n) = (m = m) в Coq?
Я запутался в доказательствах и Prop и т. д. в Coq. Как мы докажем, что (n = n) = (m = m) ?
Я намерен показать, что это как-то True=True . Но это даже правильная формулировка?
Что я пробовал до сих пор:
Theorem test: forall m n:nat, (n...
183 просмотров
schedule
09.05.2023
rewrite работает для =, но не для ‹-› (iff) в Coq
У меня есть следующее во время доказательства, в котором мне нужно заменить normal_form step t на value t , поскольку есть доказанная теорема о том, что есть эквиваленты.
H1 : t1 ==>* t1' /\ normal_form step t1'
t2' : tm
H2 : t2 ==>* t2'...
775 просмотров
schedule
27.04.2023
Как автоматически доказать простое равенство действительных чисел в Coq?
Я ищу auto -подобную тактику, которая может доказать простые равенства, такие как:
1/2 = 2/4
До сих пор я пытался использовать ring_simplify и field_simplify для доказательства равенства. Даже это не срабатывает (Coq 8.5b3). Пример...
252 просмотров
schedule
18.10.2022
Как переключить текущую цель в Coq?
Можно ли переключить текущую цель или подзадачу на подтверждение в Coq?
Например, у меня есть такая цель (из существующего):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
Что я хочу сделать,...
3213 просмотров
schedule
29.12.2022
Разница в исполнении Coq между точкой с запятой; и период.
Учитывая действительное доказательство Coq с использованием тактики ; , существует ли общая формула для преобразования его в действительное эквивалентное доказательство с заменой . на ; ?
Многие доказательства Coq используют ; или тактику...
896 просмотров
schedule
14.08.2022
В чем разница между тактикой возврата и обобщения в Coq?
Из справочного руководства Coq (8.5p1) у меня сложилось впечатление, что revert является обратным intro , но в определенной степени generalize тоже. Например, revert и generalize dependent ниже кажутся одинаковыми.
Goal forall x y: nat,...
1426 просмотров
schedule
23.01.2023
Как правильно использовать локальную тактику Coq?
Я читаю справочное руководство Coq (8.5p1) о
Локальное применение тактики
Разные тактики можно применять к разным целям, используя следующую форму:
[> expr1 | ::: | exprn]
Выражения expri оцениваются как vi для i = 0;...
115 просмотров
schedule
25.06.2022
Coq - disj_conj_intro_patterns для индуктивных предложений
Учитывая произвольное определение индуктивного предложения в Coq, существует ли общая формула для вывода разумного disj_conj_intro_pattern для использования при вызове тактики индукции для индуктивного предложения?
В общем, полный intro_pattern для...
154 просмотров
schedule
07.03.2023
Как работает дискриминационная тактика?
Мне было любопытно, как работает тактика discriminate за кулисами. Поэтому я провел несколько экспериментов.
Сначала простое индуктивное определение:
Inductive AB:=A|B.
Тогда простая лемма, которую можно доказать с помощью тактики...
1065 просмотров
schedule
16.06.2023
Доказательство, включающее развертывание двух рекурсивных функций в COQ
Я начал изучать Coq и пытаюсь доказать то, что кажется довольно простым: если список содержит x, то количество экземпляров x в этом списке будет > 0.
Я определил функции contains и count следующим образом:
Fixpoint contains (n: nat) (l: list...
187 просмотров
schedule
17.04.2023
Доказательство Coq для вычитания не коммутирует
Я хотел бы доказать, что вычитание не работает в Coq, но я застрял. Я считаю, что утверждение, которое я хотел бы доказать в Coq, было бы написано forall a b : nat, a <> b -> a - b <> b - a
Вот что у меня есть для доказательства....
147 просмотров
schedule
13.09.2022
Автоматически выбирать предположение из местного контекста
У меня есть тестовый скрипт с разделом, который выглядит так:
- destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
- destruct (IHx1 _ _ H6). congruence.
- destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
-...
59 просмотров
schedule
06.07.2023
Определение различных типов равенства как индуктивных типов в Coq
Я пытаюсь определить в Coq разные типы равенств. Во время университетского курса мой профессор дал нам правила четырех разных типов, а именно: (я даю только ссылки на правила):
Генцен: https://ibb.co/imQOCF
Лейбниц: https://ibb.co/n0uBzv...
431 просмотров
schedule
08.03.2022
Установить изоморфизм между конечными натуральными числами и сигмой
Я здесь с Coq изучаю отношения между двумя типами, которые я определил. Первый - это что-то вроде конечного подмножества nat , состоящего всего из трех элементов:
Inductive N3 := zero | one | two.
Второй - это сигма-тип с элементами,...
157 просмотров
schedule
17.11.2022
Проверка на evars в тактике, которая возвращает значение
Я пытаюсь написать тактику, которая возвращает значение, и при этом ей нужно проверить, является ли что-то эваром.
К сожалению, я не могу использовать is_evar , потому что тогда считается, что тактика возвращает не значение (а скорее другую...
202 просмотров
schedule
03.06.2023
