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

Question

下面我有一个证据，还有三个子目标。证明了用一种简单的算术语言对plus 0 (optimize_0plus)进行优化是正确的。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.

我的战争计划是将optimize_0plus应用于当前次级目标的LHS中，并获得：

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.这与我的前面的问题有关，但关于使用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所引用的课程网站。

不过，对于其他个案，我仍有同样的问题，如下所列，我认为我原来的计划应能奏效：

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种情况中的每一种，似乎都有一个应用程序(beta还原？)的optimize_0plus应该允许我们改变，例如(对于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)将简化为optimize_0plus a2，而不是APlus-headed项。

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

作为经验法则，每次你想证明一个由模式匹配/递归调用定义的函数的定理时，你都需要经历同样的一系列案例分析/归纳假设。在函数的调用图上，这通常被称为或归纳。

Answer 2

我在这里看到两种解决办法：

• 用你想要的东西来描述一个重写引理，证明它，然后使用它。当您需要进行非常复杂的重写时，这是最好的解决方案，但是它不会很好地扩展，因为您需要为每个情况编写一个引理。例如，您可以在这里声明(并使用simpl进行微小的证明)： a1 a2，optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2)。
• 如果我没记错的话，simpl和其他人不会被绑定。您可以使用pattern策略“提取”要简化的部分，以便simpl或unfold只在表达式的某个子项上执行。您应该阅读文献资料，因为这里的解释有点长。
• 编辑:我忘了讨论replace策略，它的作用类似于rewrite解决方案，但将要求您立即证明引理，作为子目标。

Answer 3

我同意让Coq做我们想做的计算并不总是容易的。但在这里，与您所说的相反，第一次重写并不仅仅是一个简单的计算步骤。实际上，optimize_0plus只解构它的参数一次，但是当它找到某种形式的APlus _ _时，它需要销毁第一个新的参数，所以这里您需要解构a1来计算。

但是，您的结果仍然是正确的，并且可以看作是一个方便的辅助引理来证明初始定理。

Lemma optimize_0plus_aux : forall a1 a2,
  aeval (optimize_0plus (APlus a1 a2)) =
  aeval (APlus (optimize_0plus a1) (optimize_0plus a2)).
Proof.
Admitted.

关于你最初提出的关于一步计算的问题，我有两个技巧：

• 我知道你不想每次都使用rewrite，但是根据我的说法，有一个方程引理是一次应用不动点的最好方法。请注意，通常可以使用Functional Scheme自动创建此引理。这里, 用于optimize_0plus_ind排序支持的功能方案:=归纳。
• 在极少数情况下，有一个函数你永远不想在证明过程中展开。在这种情况下，您可以使用Opaque <function>临时使定义不透明。在证据的末尾，用Transparent <function>使它再次透明。但是，我不认为这是一个好的风格，也不建议使用它。