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

Описание тега Вопросы с тегом
Тактики - это программы, написанные на Ltac, нетипизированном языке, который используется в помощнике проверки Coq для преобразования целей и условий. Этот тег следует использовать в вопросах, связанных с проблемами использования тактики Coq для получения доказательств с помощью помощника по доказательствам Coq.
0 ответов

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

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

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

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

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

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

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

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

Я начал изучать Coq и пытаюсь доказать что-то, что кажется довольно простым: если список содержит x, то число экземпляров x в этом списке будет> 0. Я определил функции contains и count следующим образом: Fixpoint contains (n: nat) (l: list nat) : Pr…
17 апр '17 в 13:08
1 ответ

Какую тактику я должен использовать, чтобы вывести противоречие из абсурдного равенства?

Допустим, у меня есть H: 0 = 1 в рамках. Как я могу использовать это, чтобы сделать вывод False?
10 май '17 в 21:59
1 ответ

Примените функцию к обеим сторонам равенства в гипотезе Coq

Вопрос, который у меня есть, очень похож на тот, который представлен в ссылке ниже, но по гипотезе вместо цели. Применить функцию к обеим сторонам равенства в Coq? Скажем, у меня есть следующее определение: Definition make_couple (a:nat) (b:nat) := …
21 июн '18 в 09:33
1 ответ

Coq: Как доказать max a b <= a+b?

Я не могу доказать простую логику max a b &lt;= a+b используя тактику Coq. Как мне решить эту проблему? Ниже приведен код, над которым я работал до сих пор. s_le_n доказано, но не упомянуто здесь для простоты. Theorem s_le_n: forall (a b: nat), a &l…
25 сен '17 в 16:39
1 ответ

Как использовать apply, чтобы "извлечь" подтекст в Coq

Я проиллюстрирую на примере. H : R -&gt; P -&gt; Q H0 : R подцели: (Q -&gt; P) \ / (P -&gt; Q) поэтому мой вопрос, как мне извлечь (P->Q). У меня уже есть R, но когда я "применяю H в H0", он все оценивает и дает мне Q.
08 фев '16 в 04:17
3 ответа

Как выполнить вычисление ровно один раз в Coq?

У меня есть нижеприведенное доказательство с еще тремя подцелями. Доказательство - о правильности оптимизации plus 0 (optimize_0plus) на простом арифметическом языке, продемонстрированном здесь. aexp является "арифметическим выражением" и aeval это …
25 ноя '15 в 04:14
1 ответ

Тактика, чтобы доказать логическое значение

Есть ли тактика, похожая на intros чтобы доказать логическое значение, такое как f : nat -&gt; bool g : nat -&gt; bool Lemma f_implies_g : forall n : nat, eq_true(implb (f n) (g n)). Эта тактика потянет eq_true(f n) в контекст и требуют доказать eq_…
11 июл '18 в 12:46
1 ответ

Противоречивая гипотеза с использованием тактики инверсии кока

Из этого примера: Example foo : forall (X : Type) (x y z : X) (l j : list X), x :: y :: l = z :: j -&gt; y :: l = x :: j -&gt; x = y. Это можно решить, просто сделав inversion по второй гипотезе: Proof. intros X x y z l j eq1 eq2. inversion eq2. ref…
22 май '18 в 16:55
3 ответа

Установить изоморфизм между конечными натуральными числами и сигмой

Я здесь с Coq изучаю отношения между двумя типами, которые я определил. Первый является чем-то вроде конечного подмножества natвсего тремя элементами: Inductive N3 := zero | one | two. Второй тип сигма с элементами, удовлетворяющими предложению {x: …
04 авг '17 в 08:09
1 ответ

Почему Coq не может сам определить симметрию равенства?

Предположим, мы пытаемся формализовать некоторые (полу) теоретико-групповые свойства, например: Section Group. Variable A: Type. Variable op: A -&gt; A -&gt; A. Definition is_left_neutral (e: A) := forall x: A, (op e x) = x. Definition is_right_neut…
21 сен '17 в 23:01
2 ответа

Может ли сочинение попробовать и повторить привести к бесконечному циклу в Coq?

Я знаю, что повторение применяется тактически несколько раз, пока не сработает. Повторная тактика принимает другую тактику и продолжает применять эту тактику, пока не потерпит неудачу. и тактика попытки ничего не делает, когда она "терпит неудачу": …
12 дек '18 в 20:23
2 ответа

Как можно шаг за шагом проверить, что делает более сложная тактика в Coq?

Я пытался пройти через знаменитую и замечательную книгу об основах программного обеспечения, но попал в пример, где simpl. а также reflexivity. просто делайте многое под одеялом и мешаете мне учиться и понимать. Я проходил следующую теорему: Theorem…
05 янв '19 в 00:12
1 ответ

Ltac-аргумент для экземпляра

Тактика instantiate может взять и ident или num как: instantiate (ident:= term) instantiate (num := term) Теперь я хочу использовать второй в определении тактики. Например: Ltac my_instantiate n x:= instantiate(n:=x). К сожалению, это дает следующую…
04 дек '18 в 16:12
0 ответов

Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics

Я получаю ошибку "Basics.vo содержит основы библиотеки, а не библиотеку Metalib.Basics" в CoqIDE 4.5. Я следую Основам программного обеспечения и импортирую Основы как "Требуются Основы экспорта". Также я скомпилировал основы, используя тот же CoqID…
13 фев '19 в 07:48
2 ответа

Coq терпит неудачу в применении тактики

Я пытаюсь доказать следующую простую теорему над натуральными числами: ((i + j) = (i + k)) -&gt; (j = k) Вот что я имею в Coq: Theorem cancel : forall (i j k : nat), ((add i j) = (add i k)) -&gt; (j = k). Proof. intros i j k. induction i. simpl. app…
16 янв '19 в 10:32