是否可以切换当前目标或子目标以在Coq中证明？
例如,我有一个这样的目标(来自eexists):
______________________________________(1/1)
?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
我想要做的是首先split证明合适的合并.我认为这将给出存在变量的值?s,而左合并应该只是一个简化.
但split默认情况下,将左合并设置?s > 0为当前目标.
______________________________________(1/2)
?s > 0
______________________________________(2/2)
r1 * (r1 + s1) + ?s = r3 * (r3 + s2)
我知道我可以在战术2:上加上第二个子目标的操作,但这很尴尬因为
1)我看不到目标#2和.的假设
2)如果它处于不同的上下文中,目标#2可能是第三个或第k个目标.证明不可移植.
这就是为什么我想把第二个目标设定为当前目标.
顺便说一下,我正在使用CoqIDE(8.5).
我试图在Coq中证明以下引理:
Require Import Lists.List.
Import ListNotations.
Lemma not_empty : forall (A : Type) (a b : list A),
(a <> [] \/ b <> []) -> a ++ b <> [].
现在我当前的策略是破坏一个,在打破分离之后,理想情况下我可以说,如果一个<> []那么a ++ b也必须<> [] ......这就是计划,但我似乎无法通过类似于第一个"a ++ b <> []"的子目标,即使我的上下文明确指出"b <> []".有什么建议？
我还查看了很多已有的列表定理,并没有找到任何特别有用的东西(减去app_nil_l和app_nil_r,对于某些子目标).
我看到很多Coq战术在功能上相互重叠.
例如,当你在设定确切的结论,您可以使用assumption,apply,exact,trivial,或者其他人.其他例子包括destruct和induction非感应类型(??).
我的问题是:
是否有一个最小的一套基本的策略(即不包括auto,其类似物)完成后,在这个意义上,这一套可以用来证明关于自然数的功能,任何勒柯克,可证明的定理？
这个最小完整集中的策略理想情况下是基本的,因此每个都只执行一个(或两个)函数,并且可以很容易地理解它的作用.
我试图从一个排除中间的在线课程中证明以下简单定理是无可辩驳的,但在第1步被卡住了:
Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P).
Proof.
intros P. unfold not. intros H.
现在我得到:
1 subgoals
P : Prop
H : P \/ (P -> False) -> False
______________________________________(1/1)
False
如果我apply H,那么目标就是P \/ ~P,中间被排除在外,无法建设性地证明.但除此之外apply,我不知道可以对假设做些什么P \/ (P -> False) -> False:暗示->是原始的,我不知道如何destruct分解它.这是唯一的假设.
我的问题是,如何使用原始策略(如此处所表征,即没有神秘auto的策略)来证明这一点？
谢谢.
在Coq(CPDT样式)证明中编写高度自动化的证明时,在广泛使用的基础上eauto N,我必须经常修改我的引理语句以便eauto容易地使用它们.特别是,我必须用形式(2)替换形式(1)forall vars, P (f args)...(在P论文或假设中出现)的陈述forall x args, x = f args -> P x -> ....使用表单(2),eauto可以x根据需要实例化适当的表达式e(通过统一找到),并e = f args通过其通常的证明搜索单独证明.相反,由于形式(1)有必要重写与e = f args证明,一些IIUC期间eauto不会做(除非使用专用Hint Extern).
是否有更好的现有策略来实现相同的结果,这种风格可能是自动化的？我所看到的最接近的是applys_eq软件基础的LibTactics中的策略,它允许在形式(1)中应用引理,但e = f args作为单独的目标; 但是,这种策略需要完全手动规范.
我明白我的要求可能太难或太慢; 知道这是一种合理的方法将有助于停止寻找并继续下去.我听说至少有一位经验丰富的Coq用户描述了同样的问题和相同的方法.
我一直致力于 Coq 中流程演算的形式化（此处为存储库），并且不断发现自己尝试应用一个因等效但语法不同的子术语而失败的函数。这种情况经常是由于de Bruijn 变量的操纵而发生的。当统一失败时，我通常会事先明确替换行为不当的子项，然后应用我需要的函数。一个简单的代码作为我的意思的例子：
Require Import Lia.
Goal
forall P: nat -> Prop,
(forall a b c, P (a + (b + c))) ->
forall a b c, P (b + c + a).
Proof.
intros.
(* Unification fails here. *)
Fail apply H.
(* Replace misbehaving subterms explictly. *)
replace (b + c + a) with (a + (b + c)).
- (* Now application succeeds. *)
apply H.
- (* Show now they …从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类似于演算抽象操作？
我很好奇discriminate战术背后的策略是如何运作的.因此我做了一些实验.
首先是一个简单的归纳定义:
Inductive AB:=A|B.
然后是一个简单的引理,可以通过discriminate策略证明:
Lemma l1: A=B -> False.
intro.
discriminate.
Defined.
让我们看看证明的样子:
Print l1.
l1 =
fun H : A = B =>
(fun H0 : False => False_ind False H0)
(eq_ind A
(fun e : AB => match e with
| A => True
| B => False
end) I B H)
: A = B -> False
这看起来相当复杂,我不明白这里发生了什么.因此,我试图更明确地证明相同的引理:
Lemma l2: A=B -> False.
apply (fun e:(A=B) => match e with end).
Defined. …考虑以下发展:
Require Import Relation RelationClasses.
Set Implicit Arguments.
CoInductive stream (A : Type) : Type :=
| scons : A -> stream A -> stream A.
CoInductive stream_le (A : Type) {eqA R : relation A}
`{PO : PartialOrder A eqA R} :
stream A -> stream A -> Prop :=
| le_step : forall h1 h2 t1 t2, R h1 h2 ->
(eqA h1 h2 -> stream_le t1 t2) ->
stream_le (scons h1 t1) (scons h2 t2).
如果我有一个假设stream_le …
我试图去通过著名的和精彩的软件基础的书,但我到这里的例子simpl.和reflexivity.刚做多在幕后,并阻碍了我的学习和理解.
我正在经历以下定理:
Theorem plus_1_neq_0 : forall n : nat,
beq_nat (n + 1) 0 = false. (* n+1 != 0 *)
Proof.
intros n.
destruct n as [| n'].
-simpl. reflexivity.
-simpl. reflexivity.
Qed.
我真正想要的是什么,让我一步该怎么走至步骤simpl.和reflexivity.所做.有什么东西可以让我这样做吗？
Destruct可以解决以下问题:
因为第一个参数beq_nat(这只是
not equal如!=)不匹配,但第一输入取决于未知的变量n和同样的事情,+这样的匹配不能做任何事情,这样做simpl.会让我们卡住了(出于某种原因).
它显然必须解决它,因为Coq后来接受了证据.但如果仔细观察第二个目标是什么,似乎重新引入了与上述相同的问题:
2 subgoals
______________________________________(1/2)
beq_nat (0 + 1) 0 = false
______________________________________(2/2)
beq_nat (S n' + 1) 0 = false
现在我们已经n' 为双方的第一个参数beq_nat …