coq - 如何在 Coq 中精确执行一次计算？

Question

我在下面有一个证明，还有另外三个子目标。证明是关于用简单算术语言演示的优化 plus 0 (optimize_0plus) 的正确性 here 。 aexp 是“算术表达式”，aeval 是“算术求值”。

3 subgoal
a1 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus a1) = aeval a1
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/3)
aeval (optimize_0plus (APlus a1 a2)) = aeval (APlus a1 a2)

，其中 optimize_0plus 是:

Fixpoint optimize_0plus (a:aexp) : aexp :=
  match a with
  | ANum n =>
      ANum n
  | APlus (ANum 0) e2 =>
      optimize_0plus e2
  | APlus e1 e2 =>
      APlus (optimize_0plus e1) (optimize_0plus e2)
  | AMinus e1 e2 =>
      AMinus (optimize_0plus e1) (optimize_0plus e2)
  | AMult e1 e2 =>
      AMult (optimize_0plus e1) (optimize_0plus e2)
  end.

我的 war 计划是在当前子目标的LHS中应用optimize_0plus，并获得:

aeval (APlus (optimize_0plus a1) (optimize_0plus a2)) = aeval (APlus a1 a2) 

(但我不知道如何在 Coq 中做到这一点)。

然后，通过一些simpl，得到:

(aeval (optimize_0plus a1)) + (aeval (optimize_0plus a2)) = (aeval a1) + (aeval a2)

并应用归纳假设IHa1和IHa2来完成证明。

我的问题是:

如何告诉 Coq 仅应用一次 optimize_0plus 的定义，并且不多也不少？

我尝试过simpl Optimize_0plus，但它给出了一些带有长match语句的内容，这似乎做得太多了。而且我不喜欢每次都使用rewrite策略来建立引理，因为这种计算完全是用纸和笔完成的一步。

注释:

1.这与我的earlier question here有关，但是关于使用 simpl XXX 的答案似乎在这里不起作用。这似乎是一个更复杂的情况。

2.原始网站提供了有效的证明。但那里的证明似乎比必要的更复杂，因为它开始对术语 a1 等进行案例分析。

  Case "APlus". destruct a1.
    SCase "a1 = ANum n". destruct n.
      SSCase "n = 0". simpl. apply IHa2.
      SSCase "n ≠ 0". simpl. rewrite IHa2. reflexivity.
    SCase "a1 = APlus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMinus a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.
    SCase "a1 = AMult a1_1 a1_2".
      simpl. simpl in IHa1. rewrite IHa1.
      rewrite IHa2. reflexivity.

所以，我真正关心的并不是证明这个简单的定理，而是如何像在纸上一样直观地证明这一点。

--更新--

感谢@gallais，我原来的计划是不正确的，因为可以改变

aeval (optimize_0plus (APlus a1 a2))

到

aeval (APlus (optimize_0plus a1) (optimize_0plus a2))

仅适用于a1不是ANum 0的情况。 0 情况必须通过 destruct a1. 单独处理，就像注释 2 中引用的类(class)网站一样。

但是，我对下面列出的其他情况仍然有同样的问题，我认为我原来的计划应该可行:

5 subgoal
SCase := "a1 = APlus a1_1 a1_2" : String.string
Case := "APlus" : String.string
a1_1 : aexp
a1_2 : aexp
a2 : aexp
IHa1 : aeval (optimize_0plus (APlus a1_1 a1_2)) = aeval (APlus a1_1 a1_2)
IHa2 : aeval (optimize_0plus a2) = aeval a2
______________________________________(1/5)
aeval (optimize_0plus (APlus (APlus a1_1 a1_2) a2)) =
aeval (APlus (APlus a1_1 a1_2) a2)
...

______________________________________(5/5)
aeval (optimize_0plus (AMult a1 a2)) = aeval (AMult a1 a2)

对于这 5 种情况中的每一种，似乎 optimize_0plus 的一个应用程序(beta 减少？？)应该允许我们更改，例如(对于AMinus)

aeval (optimize_0plus (AMinus a1 a2))  

至

aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))

，对吗？

如果是这样，我该如何一步步减少？

注意: 我试过了

Eval cbv beta in (aeval (optimize_0plus (AMinus a1 a2))).

我什至无法得到 aeval (AMinus (optimize_0plus a1) (optimize_0plus a2)) 因为我想在证明中使用 Eval 。

Answer 1

这里的问题是你希望依赖的方程根本不正确。不可能出现以下情况:

optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2)

给出您给出的optimize_0plus的定义:如果a1是ANum 0那么optimize_0plus (APlus a1 a2) code> 将简化为单独的 optimize_0plus a2 而不是以 APlus 为标题的术语。

但是，您试图证明的主要定理确实是正确的，并且可以通过检查 a1 来证明:它是 ANum 0 (在这种情况下，第一个分支将是由对 simpl 的调用触发)或者不是(在这种情况下将采用第二个分支)？

根据经验，每次您想要证明有关由模式匹配/递归调用定义的函数的定理时，您都需要经历同一系列的案例分析/归纳假设。这就是通常所说的函数归纳或函数调用图归纳。