Proof automation in Coq how to factorize a proof

Question

I'm following the book Software Foundation and I'm on the chapter named "Imp".

The authors expose a small language that is the following :

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 optimize the evaluation. For example :

APlus a (ANum 0) --> a

Here there is my optimize 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 would prove that the optimization function is sound :

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

This proof is quite difficult. So 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 the proof, but it is boring. I do an induction on a and then, for every case, I destruct b and destruct the exp to handle the case when b is 0.

I need to do that because

n+0 = n

doesn't reduce automatically, we need a theorem which is plus_0_r.

Now, I wonder, how can I build a better proof with Coq in order to avoid some boring repetitions during the proof.

Here is my proof for this lemma :

http://pastebin.com/pB76JFGv

I think I should use "Hint Rewrite plus_0_r" but I don't know how.

By the way, I'm also interested to know some tips in order to show the initial theorem (the soudness of my optimization function).

Answer 1

If you use the technique above, you can define your own tactical, so you don't have to type as much. And since the proofs are very short, you could do without the lemmas. (I called the tactical dca for destruct-congruence-auto.)

The shorter proof is not that readable, but it is essentially: consider the cases of the variables.

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.

Then use it

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 *)

You could probably also do the full proof in this compact form.