Описание тега ltac
The Ltac language, Coq's domain-specific language for proof search procedures. Use this tag on questions about the language and questions about proof automation using Ltac.
1
ответ
Ltac: необязательные аргументы тактики
Я хочу сделать тактику Ltac в coq, которая будет принимать 1 или 3 аргумента. Я читал о ltac_No_arg в LibTactics модуль, но если я правильно понял, мне пришлось бы использовать мою тактику с помощью: Coq < mytactic arg_1 ltac_no_arg ltac_no_arg. …
30 июн '17 в 07:10
1
ответ
Ltac не работает после обновления до Coq 8.5
У меня есть следующий Ltac ( отсюда), который работал на Coq 8.4pl6, но он не работает на Coq 8.5 beta 3: Ltac maybe_intro_sym A B := match goal with |[H:B=A|-_] => fail 1 |[H:A=B|-_] => assert (B=A) by auto end. Ltac maybe_intro_sym_neg A B :…
02 дек '15 в 00:25
1
ответ
Как сделать "отрицательный" матч в Ltac?
Я хочу применить правило в случае, когда одна гипотеза присутствует, а другая нет. Как я могу проверить это условие? Например: Variable X Y : Prop. Axiom A: X -> Y. Axiom B: X -> Z. Ltac more_detail := match goal with |[H1:X,<not H2:Y>|-…
09 фев '15 в 15:05
1
ответ
Как мне написать тактику, которая ведет себя как "уничтожить... как"?
В coq, destruct у тактики есть вариант, принимающий "конъюнктивную дизъюнктивную модель введения", которая позволяет пользователю присваивать имена вводимым переменным даже при распаковке сложных индуктивных типов. Язык Ltac в coq позволяет пользова…
09 май '15 в 00:38
1
ответ
Разъединение Commutavity в Coq
Я хотел бы иметь тактику Ltac, которая выполняет работу Disjunction Commutavity. Главным образом, если у меня есть подтермы P \/ Q где-то в гипотезе H, Ltac Com H добавлю Q \/ Pкак еще одна гипотеза для контекста. Я попытался поставить правило комму…
23 окт '18 в 23:46
3
ответа
Переписать единственный случай в ltac
Как я могу призвать rewrite в ltac переписать только одно вхождение? Я думаю, что документация Coq упоминает что-то о rewrite at но я не смог использовать его на практике, и нет примеров. Это пример того, что я пытаюсь сделать: Definition f (a b: na…
01 авг '17 в 02:08
1
ответ
Могу ли я определить тактику в разделе "coqtop - nois"?
$ coqtop -nois Welcome to Coq 8.7.0 (October 2017) Coq < Ltac i := idtac. Toplevel input, characters 0-4: > Ltac i := idtac. > ^^^^ Error: Syntax error: illegal begin of vernac. Я перерабатываю "Coq.Init.Prelude" и "HoTT.Basics.Overture" по…
17 фев '18 в 02:36
1
ответ
Может ли тактика инъекций изменить конечную цель или добавить посторонние предположения?
Рассмотрим следующую разработку, изолированную часть Адама Члипалы simplHyp: (** Fail if H is in context *) Ltac notInCtx H := assert H; [ assumption | fail 1 ] || idtac. Ltac injectionInCtx := match goal with (* Is matching on G strictly necessary?…
14 окт '18 в 14:09
1
ответ
Удалить все двойные отрицания в Coq
Я хотел бы систематически убрать все двойные отрицания, которые могут появиться в моих гипотезах и целях. я знаю это ~~A -> Aэто не часть интуиционистской логики, но курс, который я выбираю, классический, поэтому я не против. Я знаю, что упомянут…
29 окт '18 в 18:13
2
ответа
Расширяемая тактика в Coq
Допустим, у меня есть причудливая тактика, которая решает леммы определенного вида: Ltac solveFancy := some_preparation; repeat (first [important_step1 | important_step2]; some_cleanup); solve_basecase. Теперь я использую эту тактику для доказательс…
19 фев '18 в 14:21
2
ответа
Как написать Ltac, чтобы умножить обе части уравнения на элемент группы в Coq
Используя это определение группы: Structure group := { G :> Set; id : G; op : G -> G -> G; inv : G -> G; op_assoc_def : forall (x y z : G), op x (op y z) = op (op x y) z; op_inv_l : forall (x : G), id = op (inv x) x; op_id_l : forall (x …
28 янв '18 в 21:34
1
ответ
Обобщающие выражения под связывателями
Мне нужно обобщить выражение под связующим. Например, в моей цели есть два выражения: (fun a b => g a b c) а также (fun a b => f (g a b c)) И я хочу обобщить g _ _ c часть: Один из способов сделать это - сначала переписать их в: (fun a b =>…
27 сен '17 в 23:28
0
ответов
Coq: перенести тактику Ltac с использованием стиля CPS на тактику ML (плагин OCaml)
Я пытаюсь перенести тактику Coq (в настоящее время написанную на Ltac) на OCaml, чтобы иметь возможность более легко расширять эту тактику (и избежать хаков, которые мне понадобились для эмуляции в Ltac некоторых структур данных, которые в остальном…
04 сен '18 в 18:51
0
ответов
setoid_rewrite с impl не работает с леммами типа `A -> B`
Пример: Require Import Basics. Require Export Setoid. Require Export Relation_Definitions. Set Implicit Arguments. Lemma simple1 (A B : Prop) (f : A -> B) (x : A) : B. Proof. assert (f2: impl A B) by exact f. setoid_rewrite <- f2. exact x. Qed…
19 окт '18 в 01:28
3
ответа
Coq: просмотр контрольного термина во время написания контрольного сценария
Итак, у меня есть доказательство, которое выглядит так: induction t; intros; inversion H ; crush. Это решает все мои цели, но когда я делаю QedЯ получаю следующую ошибку: Cannot guess decreasing argument of fix. Так что где-то в сгенерированном терм…
19 фев '18 в 23:59
1
ответ
Coq: локальное определение ltac
Если есть способ определить "локальное" выражение Ltac, которое я могу использовать для доказательства леммы, но не видимый снаружи? Lemma Foo ... Proof. Ltac ll := ... destrict t. - reflexivity. - ll. - ll. Qed. (* ll should not be visible here *)
22 авг '18 в 06:52
2
ответа
Создание экзистенциального с конкретным доказательством
В настоящее время я пытаюсь написать тактику, которая создает экземпляр экзистенциального квантификатора, используя термин, который может быть сгенерирован легко (в этом конкретном примере, из tauto). Моя первая попытка: Ltac mytac := match goal wit…
17 окт '17 в 13:41
1
ответ
Как смотреть на несколько целей одновременно?
Я обдумываю тактику написания, которая будет учитывать несколько целей и принимать решения на основе этого. Тем не менее, когда я использую match goal with и смотреть на цель, как мне сказать "пожалуйста, найдите другую цель, которая выглядит следую…
08 апр '18 в 00:42
1
ответ
Как инициализировать пустую базу данных подсказок
У меня есть несколько доказательств, которые придерживаются идентичной структуры. Первый из них может быть закончен с trivialвсе остальные с auto with foo_db, где foo_db база данных подсказок, заполненная подсказками после завершения первого доказат…
13 сен '17 в 11:12
1
ответ
Coq: Ltac определений над списками переменных аргументов?
При попытке создать определение Ltac, которое зацикливается на списке аргументов переменной длины, я столкнулся со следующим неожиданным поведением на Coq 8.4pl2. Кто-нибудь может мне это объяснить? Ltac ltac_loop X := match X with | 0 => idtac "…
29 мар '14 в 05:18