我正在编程语言基础中研究编译器的正确性证明，在屈服并应用我在网上找到的这个解决方案之前，我挠了几个小时(https://github.com/haklabbeograd/software-foundations-coq-workshop/blob/master/Imp.v(。 我尝试调整我的函数(第一个s_execute(，但它仍然无法证明下面的引理(只有后一种实现有效(。 此外，我只能在他的文件中运行在线解决方案时使其工作，而不是我的(除了 instr 与 sinstr 之外，所有定义都相同，变量的定义略有不同(。 为什么会这样(具体来说，为什么统一错误只发生在前一个解决方案中(？ 此外，在书中它说：
请记住，如果堆栈包含的元素少于 tw 个，规范未指定在遇到 [SPlus]、[SMinus] 或 [SMult] 指令时该怎么做。 (为了使您的正确性证明更容易，您可能会发现返回并更改您的实现会有所帮助！
作者希望我们更改哪个定义以使其正确？
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list instr)
: list nat :=
match prog with
| [] => stack
| x :: xs => match x, stack with
| (SPush n), ys => s_execute st (n :: ys) xs
| (SLoad x), ys => s_execute st ((st x) :: ys) xs
| SPlus, y1 :: y2 :: ys => s_execute st ((y1 + y2) :: ys) xs
| SMinus, y1 :: y2 :: ys => s_execute st ((y2 - y1) :: ys) xs
| SMult, y1 :: y2 :: ys => s_execute st ((y2 * y1) :: ys) xs
| _, _ => stack
end
end.
Fixpoint s_execute (st : state) (stack : list nat)
(prog : list instr)
: list nat :=
let newstack :=
match prog with
| [] => stack
| (SPush n)::_ => n::stack
| (SLoad id)::_ => (st id)::stack
| SPlus::_ => match stack with
| n::(m::rest) => (m+n)::rest
| _ => stack
end
| SMinus::_ => match stack with
| n::m::rest => (m-n)::rest
| _ => stack
end
| SMult::_ => match stack with
| n::m::rest => (m*n)::rest
| _ => stack
end
end in
match prog with
| [] => stack
| instr::rest => s_execute st newstack rest
end.
下面的引理仅适用于第二个实现，即使两者都与 s_execute(1|2( 给出的示例匹配。
Lemma s_execute_app : forall st p1 p2 stack,
s_execute st stack (p1 ++ p2) = s_execute st (s_execute st stack p1) p2.
intros st p1.
induction p1.
intros; reflexivity.
intros.
apply IHp1.
Qed.
这两个s_execute定义并不等价：当遇到无效指令时，第一个立即停止(_, _ => stack(，而第二个跳过它，但仍计算程序的其余部分(s_execute ... rest(。
由于这种差异，第一个版本不满足s_execute_app引理。但是，该引理不是练习的一部分，它只是您找到的解决方案的作者的补充，这可能会使最终证明更容易，但不是严格要求的。
所以这就是证明没有通过的主要原因：它不能。
然而，由于语法的差异，证明确实比它可能要早一些：第一个定义在公开递归调用之前做了更多的matchess_execute，而第二个定义在开始时只做一个match，并将其余部分隐藏在本地定义newstack中。
let newstack := ... in
match prog with (* One match... *)
| [] => stack
| instr::rest => s_execute st newstack rest (* ... and the recursive call is revealed *)
end.
如果你看看你用你的s_execute版本在证明中卡在哪里，目标是一大堆看起来不像归纳假设的match，这就是为什么最后一个apply没有通过。当目标中存在match时，通常要尝试的是destruct匹配的任何内容。其中两个情况很容易用apply IHp1调度，所以我们可以像这样链接这些策略，只剩下三个算术运算，其中归纳假设仍然不适用。
destruct a eqn:Ea; try apply IHp1.
再次在目标中更加matches。
destruct stack.
现在我们到达了一个无法解决的目标：
--------------------------------------
[ ] = s_execute st [ ] p2
试着理解为什么这是不正确的，然后通过一步一步地回过头来，你可以重建一个反例来描述最初的命题。
作者希望我们更改哪个定义以使其正确？
这两个定义看起来都是正确的(我还没有验证你的(，但是由于我上面解释的原因，第二个定义很可能会带来一些更简洁的证据。