coq - Coq 中的证明自动化如何分解证明

Question

我正在关注《软件基础》一书，并且正在阅读名为“Imp”的章节。

作者公开了一种小语言，如下所示:

Inductive aexp : Type :=
  | ANum : nat -> aexp
  | APlus : aexp -> aexp -> aexp
  | AMinus : aexp -> aexp -> aexp
  | AMult : aexp -> aexp -> aexp.

这是计算这些表达式的函数:

Fixpoint aeval (a : aexp) : nat :=
  match a with
  | ANum n ⇒ n
  | APlus a1 a2 ⇒ (aeval a1) + (aeval a2)
  | AMinus a1 a2 ⇒ (aeval a1) - (aeval a2)
  | AMult a1 a2 ⇒ (aeval a1) × (aeval a2)
  end.

练习是创建一个优化评估的函数。例如:

APlus a (ANum 0) --> a

这是我的优化功能:

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

现在，我将证明优化函数是合理的:

Theorem optimizer_a_sound : forall a, aeval (optimizer_a a) = aeval a.

这个证明是相当困难的。所以我尝试使用一些引理来分解证明。

这是一个引理:

Lemma optimizer_a_plus_sound : forall a b, aeval (optimizer_a (APlus a b)) = aeval (APlus (optimizer_a a) (optimizer_a b)).

我有证据，但很无聊。我对 a 进行归纳，然后，对于每种情况，我都会析构 b 并析构 exp 以处理 b 为 0 时的情况。

我需要这样做，因为

n+0 = n

不会自动减少，我们需要一个定理，即plus_0_r。

现在，我想知道如何使用 Coq 构建更好的证明，以避免证明过程中出现一些无聊的重复。

这是我对这个引理的证明:

http://pastebin.com/pB76JFGv

我认为我应该使用“提示重写 plus_0_r”，但我不知道如何使用。

顺便说一句，我也有兴趣了解一些技巧，以展示初始定理(我的优化函数的可靠性)。

Answer 1

如果您使用上述技术，您可以定义自己的战术，因此您不必输入太多内容。由于证明非常短，您可以不用引理。 (我将战术 dca 称为 destruct-congruence-auto。)

较短的证明不太可读，但本质上是:考虑变量的情况。

Lemma ANum0_dec: forall a, {a = ANum 0} + { a <> ANum 0}.
  destruct a; try destruct n; try (right; discriminate); left; auto.
Qed.

Require Import Arith.

Ltac dca v := destruct v; try congruence; auto.

Lemma optimizer_a_plus_sound :
  forall a b,
    aeval (optimizer_a (APlus a b)) = aeval (APlus (optimizer_a a) (optimizer_a b)).
Proof.
  intros a b;
  destruct (ANum0_dec a), (ANum0_dec b).
  - dca a; dca n.
  - dca a; dca n0.
  - dca b; dca n0; dca a; simpl; auto with arith; dca n0.
  - dca a; dca b; dca n1; dca n2.
Qed.

然后使用它

Theorem optimizer_a_sound : forall a, aeval (optimizer_a a) = aeval a.

  induction a.
  * auto.
  * rewrite optimizer_a_plus_sound; simpl; auto.
  *     (* ... and so on for Minus and Mult *)

您或许也可以用这种紧凑的形式进行完整的证明。