Automation of evidence in Coq, how to decompose evidence

Question

I am following the Software Foundation book and I am in the chapter entitled "Imp".

The authors disclose a small language that looks like this:

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

Here is the function to evaluate these expressions:

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.

The exercise is to create a function that optimizes the score. For example:

APlus a (ANum 0) --> a

Here is my optimization function:

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. 

And now I will prove that the optimization function sounds:

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

This proof is rather complicated. Therefore, I tried to decompose the proof using some lemmas.

Here is one lemma:

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

I have proof, but it's boring. I do induction on a, and then for each case, I destroy b and destroy exp to handle the case where b is 0.

I need to do this because

n+0 = n

is not reduced automatically, we need a theorem that is equal to plus_0_r.

, , Coq, .

:

http://pastebin.com/pB76JFGv

, "Hint Rewrite 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 *)

, .

Answer 2

, , X, .

destruct X; try congruence; auto.

, optimization_a.

Lemma opt1: forall a b, a = ANum 0 -> optimizer_a (APlus a b) = optimizer_a b.
  intros.
  destruct a; try congruence; auto;
  destruct n; try congruence; auto.
Qed.

Lemma opt2: forall a b, b = ANum 0 -> optimizer_a (APlus a b) = optimizer_a a.
  intros;
  destruct a; try congruence; auto;
  destruct b; try congruence; auto;
  destruct n; try congruence; auto;
  destruct n0; try congruence; auto.
Qed.

Lemma opt3:
  forall a b,
    a <> ANum 0 -> b <> ANum 0 ->
    optimizer_a (APlus a b) = APlus (optimizer_a a) (optimizer_a b).
Proof.
  intros.
  destruct a; try congruence; auto;
  destruct b; try congruence; auto;
  destruct n; try congruence; auto;
  destruct n0; try congruence; auto.
Qed.

, Ltac-fu, , .

, , .

, , , (Is a = ANum 0 ? Is b?) . , , , a ANum 0, .

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

ANum0_dec a a = ANum 0 , a <> ANum 0 .

Require Import Arith. (* for "auto with arith" to handle n = n + 0 *)

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);  destruct (ANum0_dec b).
  - rewrite opt1; subst; auto.
  - rewrite opt1; subst; auto.
  - rewrite opt2; subst; simpl; auto with arith.
  - rewrite opt3; subst; auto.
Qed.