在研究其他作者的Coq证明时,我经常遇到一种策略,让我们说"inv eq Heq"或"intro_b".我想了解这样的策略.
如何在我当前的项目中找到某个Coq策略或战术符号？
第二,有没有办法找到它的定义？
我使用了SearchAbout,Search,Locate和Print但找不到上述问题的答案.
在coq中,是否有可能将引理或假设应用于当前目标的子表达式？例如,我想应用plus是可交换的事实,以便在此示例中交换3和4.
Require Import Coq.Arith.Plus.
Inductive foobar : nat -> Prop :=
| foob : forall n:nat, foobar n.
Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)
得到:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".
我怎样才能告诉coq在这个目标中究竟应用plus_comm？
我有一个功能PolyInterpretation(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt.html)
Definition PolyInterpretation := forall f : Sig, poly (arity f).
和模块签名TPolyInt(http://color.inria.fr/doc/CoLoR.PolyInt.APolyInt_MA.html)
Module Type TPolyInt.
Parameter sig : Signature.
Parameter trsInt : PolyInterpretation sig.
Parameter trsInt_wm : PolyWeakMonotone trsInt.
End TPolyInt.
Module PolyInt (Export PI : TPolyInt).
然后在我的文件中rainbow.v,我定义了一个TPolyInt_imp使用仿函数的模块目的PolyInt
Module TPolyInt_imp.
Variable arity : symbol -> nat.
Variable l : list {g : symbol & poly (arity f).
Definition sig := Sig arity.
Definition trsInt f := fun_of_pairs_list …在尝试创建循环遍历可变长度参数列表的Ltac定义时,我在Coq 8.4pl2上遇到以下意外行为.有谁可以向我解释一下？
Ltac ltac_loop X :=
match X with
| 0 => idtac "done"
| _ => (fun Y => idtac "hello"; ltac_loop Y)
end.
Goal True.
ltac_loop 0. (* prints "done" as expected *)
ltac_loop 1 0. (* prints "hello" then "done" as expected *)
ltac_loop 1 1 0. (* unexpectedly yields "Error: Illegal tactic application." *)
我设法将目标减少到了
(fun x0 : PSR => me (x x0)) = x
我知道这reflexivity会有效,但出于教学原因,我宁愿继续减少它.
me是一个身份功能,所以unfold me简化它
(fun x0 : PSR => x x0) = x
这只是一个将函数应用于x虚拟变量的匿名函数x0,所以你可以说两边都只是函数x.如果可能的话,我想在双方达成相同的表达方式.
当我试图证明一个关于递归函数的定理时(见下文),我最终得到了一个可简化的表达式
(fix picksome L H := match A with .... end) L1 H1 = RHS
我想扩大match表达,但Coq拒绝.这样做simpl只是扩大了右侧为不可读的混乱.为什么Coq无法完成证明simpl; reflexivity,以及如何指示Coq精确扩展redex,并完成证明？
该函数是一个递归函数pick,它接受list nat并执行第一个nat调用a,a从列表中删除以下项,并在剩余列表上进行递归.即
pick [2;3;4;0;1;3])=[2; 0; 1]
我试图证明的定理是函数'只对包含零的列表无效'.以下是导致问题的发展:
Require Import Arith.
Require Import List.
Import ListNotations.
Fixpoint drop {T} n (l:list T) :=
match n,l with
| S n', cons _ l' => drop n' l'
| O, _ => l
| _, _ => nil
end.
第一个引理: …
我知道Iota减少用于减少/扩展递归函数.例如,给定以下简单递归函数的应用(自然数上的阶乘):
((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2)
Iota缩减扩展了递归调用,有效地迭代递归函数一次:
Eval lazy iota in ((fix fact (n:nat):nat := match n with | O => 1 | S m => n * fact m end) 2).
= (fun n:nat =>
match n with
| 0 => 1
| S m =>
n *
(fix fact (m : nat) : nat :=
match m with
| 0 => …所以这是我在软件基金会工作的一个练习,我必须证明多重是可交换的.这是我的解决方案:
Theorem brack_help : forall n m p: nat,
n + (m + p) = n + m + p.
Proof.
intros n m p.
induction n as [| n'].
Case "n = 0".
simpl.
reflexivity.
Case "n = S n'".
simpl.
rewrite -> IHn'.
reflexivity.
Qed.
Lemma plus_help: forall n m: nat,
S (n + m) = n + S m.
Proof.
intros n m.
induction n as [| n].
Case "n = 0".
simpl.
reflexivity.
Case …鉴于使用;战术的有效Coq证明,是否有通用公式将其转换为有效的等效证明并.替换;？
许多Coq证明使用;或战术排序战术.作为一个初学者,我想看的各个步骤执行,所以我想替换.的;,但让我吃惊,我觉得这可能会破坏证据.
文档;很稀疏,我没有找到.任何地方的明确讨论.我确实看到了纸,上面写着非正式的意义t1; t2就是
适用于在当前证据背景下
t2执行的每个子目标t1,
我想知道是否.只对当前的子目标进行操作并解释了不同的行为？但是,尤其是我想知道如果有修复由替换破损的通用解决方案.的;.
从Coq参考手册（8.5p1）中，我的印象revert是的倒数intro，但generalize在一定程度上也是这样。例如，revert和generalize dependent下面似乎是相同的。
Goal forall x y: nat, 1 + x = 2 + y -> 1 + x + 5 = 7 + y.
intros x y. revert x y.
intros x y. generalize dependent y. generalize dependent x.
仅仅generalize是比它更强大revert吗？
另外，该文档在解释有关以下内容方面有点循环generalize：
此策略适用于任何目标。它概括了有关某个术语的结论。
是generalize类似于演算抽象操作？