How to execute a computation exactly once in Coq?

Question

I have a proof below with three more sub-goals to go. The proof is about the correctness of optimizing away plus 0 (optimize_0plus) in a simply arithmetic language demonstrated here. aexp is "arithmetic expression" and aeval is "arithmetic evaluation".

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)

, where the optimize_0plus is:

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.

My war plan is to apply optimize_0plus in the LHS of the current sub-goal, and obtain:

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

(But I can't figure out how to do this in Coq).

Then, through some simpl, obtain:

(aeval (optimize_0plus a1)) + (aeval (optimize_0plus a2)) = (aeval a1) + (aeval a2)

and apply the induction hypotheses IHa1 and IHa2 to complete the proof.

My question is:

How can I tell Coq to apply the definition of optimize_0plus exactly once, and do no more and no less?

I have tried simpl optimize_0plus, but it gives something with a long match statement, which seems to be doing too much. And I do not like to use the rewrite tactic every time to establish a lemma because this computation is exactly one step with paper and pencil.

Notes:

1.This is related to my earlier question here, but the answers there about using simpl XXX does not seem to work here. This seems to be a more complicated case.

2.The original website offers a proof that works. But the proof there seems to be more complex than necessary as it begins to do case analysis on the terms a1 etc.

  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.

So, my concern is not really to prove this simple theorem, but on how to prove this intuitively as I would on paper.

-- UPDATE --

Thanks to @gallais, my original plan is incorrect as one can change

aeval (optimize_0plus (APlus a1 a2))

to

aeval (APlus (optimize_0plus a1) (optimize_0plus a2))

only for the cases where a1 is not ANum 0. The 0 case has to be dealt with separately by destruct a1. as with the course website quoted in Note 2.

However, I still have the same question for the other cases, listed below, which I think my original plan should work:

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)

For each of these 5 cases, it seems that one application (beta reduction??) of optimize_0plus should allow us to change e.g. (for AMinus)

aeval (optimize_0plus (AMinus a1 a2))  

to

aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))

, right?

If so, how can I do this one-step reduction?

Note: I tried

Eval cbv beta in (aeval (optimize_0plus (AMinus a1 a2))).

And I couldn't even get aeval (AMinus (optimize_0plus a1) (optimize_0plus a2)) as I'd like to using a Eval in the proof.

Answer 1

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.

Answer 2

I see two solutions here:

• state a rewriting lemma with exactly what you want, prove it and then use it. This is the best solution when you need to do a very complex rewriting, but it doesn't scale that nicely since you need to write a lemma for each of your situations. For example here you could state (and trivially prove using simpl):

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

• If I recall correctly, simpl and others don't go under binders. You can use the pattern tactic to "extract" the part you want to simplify, so that simpl or unfold only perform on some sub-term of your expression. You should read the documentation since it is a bit long to explain here.

• EDIT: I forgot to talk about the replace tactics, which act like the rewrite solution but will ask you to prove the lemma right away, as a subgoal.

Answer 3

I agree it is not always easy to make Coq do as much computation as we want. But here, contrary to what you say, the first rewrite is not just a simple computation step. Indeed, optimize_0plus destructs its arguments once, but when it finds something of the form APlus _ _, it needs to destruct the first new argument, so here you need to destruct a1 to compute.

However, your result is still true, and can be considered as a convenient helper lemma to prove the initial theorem.

Lemma optimize_0plus_aux : forall a1 a2,
  aeval (optimize_0plus (APlus a1 a2)) =
  aeval (APlus (optimize_0plus a1) (optimize_0plus a2)).
Proof.
Admitted.

Concerning your initial question about one-step computation, I have two tricks:

• I know you do not want to use rewrite each time, but according to me, having an equation lemma is the best way to apply a fixpoint once. Note that you can generally create this lemma automatically with Functional Scheme. Here,

  Functional Scheme optimize_0plus_ind := Induction for optimize_0plus Sort Prop.
  

• In rare cases, there is a function you never want to unfold during a proof. In such cases, you can temporary make the definition opaque with Opaque <function>. At the end of the proof, make it transparent again with Transparent <function>. However, I do not think it is a good style and do not suggest to use it.