2

我在下面有一个证明，还有三个子目标要做。证明是关于用这里演示的简单算术语言优化 away plus 0( ) 的正确性。是“算术表达式”并且是“算术评估”。optimize_0plusaexpaeval

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 中做到这一点）。

然后，通过 some 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))

仅适用于a1is not的情况ANum 0。案件须按注 2 所引之课程网站0另行处理。destruct a1.

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

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应该允许我们改变例如（for 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在证明中使用的。

4

3 回答 3

3

The problem here is that the equation you're hopping to rely on is simply not true. It cannot be the case that:

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

given the definition of optimize_0plus you have given: if a1 is ANum 0 then optimize_0plus (APlus a1 a2) will reduce to optimize_0plus a2 alone and not an APlus-headed term.

However the main theorem you are trying to prove is indeed correct and can be proven by inspecting a1: is it ANum 0 (in which case the first branch will be fired by a call to simpl) or is it not (in which case the second branch will be taken)?

As a rule of thumb, every time you want to prove a theorem about a function defined by pattern-matching / recursive calls, you need to go through the same series of case-analysis / induction hypothesis. This is what is usually referred to as functional induction or induction on the call graph of the function.

于 2015-11-25T12:50:12.113 回答
1

我在这里看到两个解决方案：

  • 用你想要的东西陈述一个重写引理，证明它然后使用它。当您需要进行非常复杂的重写时，这是最好的解决方案，但是由于您需要为每种情况编写引理，因此它的扩展性并不好。例如，您可以在这里声明（并简单地证明 using simpl）：

      forall a1 a2, optimize_0plus (APlus a1 a2) = APlus (optimize_0plus a1) (optimize_0plus a2).

  • 如果我没记错的话，simpl其他人不会下活页夹。您可以使用该pattern策略“提取”您想要简化的部分，以便simpl或unfold仅在表达式的某些子项上执行。您应该阅读文档，因为在这里解释有点长。

  • 编辑：我忘了谈论replace策略，它的作用类似于rewrite解决方案，但会要求您立即证明引理，作为子目标。

于 2015-11-25T08:26:46.667 回答
1

我同意让 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。这里，

    Functional Scheme optimize_0plus_ind := Induction for optimize_0plus Sort Prop.

  • 在极少数情况下，您永远不想在证明期间展开某个功能。在这种情况下，您可以使用 临时使定义不透明Opaque <function>。在证明的最后，用 使其再次透明Transparent <function>。但是，我认为它不是一个好样式，也不建议使用它。

于 2015-11-25T13:47:20.830 回答