我发现自己被Coq证明卡住了。
初步定义：
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Export Coq.Strings.String.
Import ListNotations.
Definition total_map (A:Type) := string -> A.
Definition state := total_map nat.
Inductive sinstr : Type :=
| SPush : nat -> sinstr
| SLoad : string -> sinstr
| SPlus : sinstr
| SMinus : sinstr
| SMult : sinstr.
Definition s_execute_instr (st : state) (stack : list nat)
(instr : sinstr)
: option (list nat) :=
match instr with
| SPush n => Some (n :: stack)
| SLoad x => Some (st x :: stack)
| SPlus => match stack with
| x :: y :: stack' => Some (x+y :: stack')
| _ => None
end
| SMinus => match stack with
| x :: y :: stack' => Some (y-x :: stack')
| _ => None
end
| SMult => match stack with
| x :: y :: stack' => Some (x*y::stack')
| _ => None
end
end.
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list sinstr)
: option (list nat) :=
match prog with
| [] => Some (stack)
| instr::prog' => match (s_execute_instr st stack instr) with
| Some stack' => s_execute st stack' prog'
| None => None
end
end.
我尝试了一个定理证明：
Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
s_execute st sk l1 = Some sk' ->
s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st H.
induction l1 as [|l1' l1].
- inversion H. reflexivity.
-
当前状态为：
l1' : sinstr
l1, l2 : list sinstr
sk, sk' : list nat
st : state
H : s_execute st sk (l1' :: l1) = Some sk'
IHl1 : s_execute st sk l1 = Some sk' -> s_execute st sk (l1 ++ l2) = s_execute st sk' l2
============================
s_execute st sk ((l1' :: l1) ++ l2) = s_execute st sk' l2
我走这条路是因为我认为我需要以某种方式使用归纳法，但在这一点上，我不确定如何继续。
我也试过在l2上进行归纳，但这似乎也没有让我取得任何进展；
Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
s_execute st sk l1 = Some sk' ->
s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st H.
induction l2 as [|l2' l2].
- simpl. rewrite <- H. replace (l1 ++ []) with l1.
+ reflexivity.
+ symmetry. apply app_nil_r.
-
l1 : list sinstr
l2' : sinstr
l2 : list sinstr
sk, sk' : list nat
st : state
H : s_execute st sk l1 = Some sk'
IHl2 : s_execute st sk (l1 ++ l2) = s_execute st sk' l2
============================
s_execute st sk (l1 ++ l2' :: l2) =
s_execute st sk' (l2' :: l2)
在SO上问这种问题很奇怪，因为它不是。。。一个可重复使用的问题/标题确实很糟糕，但也不确定如何在这方面改进。
您不应该像在第一行中那样引入所有变量。你应该先看看你的递归函数，然后问自己两个问题：
-
什么是递归函数及其"；结构递归自变量"；在这里您可能已经注意到，当Coq接受递归定义时，它会告诉您它在结构上是递归的。
-
函数中结构上不是递归的参数会发生什么：它们在递归调用之间是否发生变化？
问题1的答案：
在您的例子中，我们有两个主要的递归函数List.app和s_execute。s_execute的递归自变量是含义左侧的l1。s_execute的递归自变量是最后等式左侧的l1 ++ l2，而s_execute的递归自变量仅是右侧的l2。因为l1 ++ l2位于递归自变量的位置，所以我们现在可以通过查看其代码来查看app的递归自变量，并且我们可以看到在递归调用时结构上减少的自变量再次是l1。这给人一种强烈的感觉，即应该对l1进行诱导。
问题2的答案：s_execute包含三个参数。状态在执行过程中不会改变，但堆栈会改变。因此，您可以为整个证明修复st，但不应修复堆栈参数。app也出现了类似的观察结果：第二个参数在递归调用期间不会更改。
实际上，你可以从开始你的证明
intros l1 l2.
induction l1 ....
在引言中不要再多说了，因为堆栈应该保持灵活性，在使用归纳假设时，你需要这种灵活性。
为了好玩，你可以尝试引入更多的论点，但你必须使用revert策略来释放灵活的论点。就像这样：
intros l1 l2 sk sk' st; revert sk.
induction l1 as ....
在这里，只有sk必须被释放(或未固定，或恢复(。
这实际上是一个很好的问题，在形式证明中经常会出现避免固定论点的需要，这些论点需要在归纳假设的使用中改变。
后期编辑
以下是我如何开始你的证明：
Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
s_execute st sk l1 = Some sk' ->
s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1 l2 sk sk' st; revert sk.
induction l1 as [ | n l1 Ih].
simpl; intros sk [= skk']; rewrite skk'; easy.
现在我们在归纳步骤的情况下。在目标的结论中，堆栈仍然是普遍量化的。因此，归纳假说和目标实际上是在谈论两个潜在的不同堆栈。下一步是修复任意堆栈以推断结论。
intros sk.
然后我们计算，
simpl.
我们正在推理代码的符号执行，但我们不知道(s_execute_instr st sk n)将如何产生，所以我们需要涵盖这两种情况，这就是destruct步骤所做的。
destruct (s_execute_instr st sk n) as [sk1 | ].
在第一种情况下(对于(s_execute_instr st sk n)的执行(，会出现一个新的状态sk1，执行将在该状态下进行，我们知道从该状态执行CCD_ 23精确地导致CCD_。让我们把这个新状态命名为complete_l1。现在恰好可以通过实例化这个新状态的归纳假设来完成证明。
intros complete_l1.
now rewrite (Ih sk1).
仍然存在由destruct步骤产生的另一种情况，但这种情况包含形式为None = Some sk'的自不一致假设。easy策略知道如何消除这种情况(实际上easy依赖于discriminate，它实现了我喜欢称之为数据类型的非混淆属性(。
easy.
Qed.
请告诉我你的尝试中遗漏了什么？是destruct步骤吗？
最终，我明白了。
Theorem s_execute_relational : forall (l1 l2: list sinstr) (sk sk': list nat) (st : state),
s_execute st sk l1 = Some sk' ->
s_execute st sk (l1 ++ l2) = s_execute st sk' l2.
Proof.
intros l1.
induction l1 as [| l1' l1].
- intros l2 sk sk' st H. simpl.
inversion H. reflexivity.
- intros l2 sk sk' st H.
assert (forall (x:sinstr) (xs ys: list sinstr), (x::xs) ++ys = x::(xs++ys)) as app_comm_cons.
{
auto.
}
rewrite app_comm_cons.
unfold s_execute in *. destruct (s_execute_instr st sk l1').
+ eapply IHl1. apply H.
+ inversion H.
Qed.