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

我正在关注软件基金会这本书,我在名为"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

我想我应该使用"Hint Rewrite plus_0_r",但我不知道怎么做.

顺便说一句,我也有兴趣知道一些提示,以显示初始定理(我的优化函数的响度).

如果你使用上面的技术,你可以定义自己的战术,所以你不必输入那么多.由于证据很短,你可以没有引理.(我称之为dcadestruct-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 *)

你也可以用这种紧凑的形式做完整的证明.