title: How to execute a computation exactly once in Coq?
body: <p>I have  a proof below with three more sub-goals to go. The proof is about the correctness of optimizing away <code>plus 0</code> (<code>optimize_0plus</code>) in a simply arithmetic language demonstrated <a href="https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html" rel="nofollow noreferrer">here</a>. <code>aexp</code> is "arithmetic expression" and <code>aeval</code> is "arithmetic evaluation". </p>
  
  <pre><code>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)
  </code></pre>
  
  <p>, where the <code>optimize_0plus</code> is:</p>
  
  <pre><code>Fixpoint optimize_0plus (a:aexp) : aexp :=
    match a with
    | ANum n =&gt;
        ANum n
    | APlus (ANum 0) e2 =&gt;
        optimize_0plus e2
    | APlus e1 e2 =&gt;
        APlus (optimize_0plus e1) (optimize_0plus e2)
    | AMinus e1 e2 =&gt;
        AMinus (optimize_0plus e1) (optimize_0plus e2)
    | AMult e1 e2 =&gt;
        AMult (optimize_0plus e1) (optimize_0plus e2)
    end.
  </code></pre>
  
  <p>My war plan is to apply <code>optimize_0plus</code> in the LHS of the current sub-goal, and obtain:</p>
  
  <pre><code>aeval (APlus (optimize_0plus a1) (optimize_0plus a2)) = aeval (APlus a1 a2) 
  </code></pre>
  
  <p>(But I can't figure out how to do this in Coq).</p>
  
  <p>Then, through some <code>simpl</code>, obtain:</p>
  
  <pre><code>(aeval (optimize_0plus a1)) + (aeval (optimize_0plus a2)) = (aeval a1) + (aeval a2)
  </code></pre>
  
  <p>and apply the induction hypotheses <code>IHa1</code> and <code>IHa2</code> to complete the proof.</p>
  
  <p>My question is:</p>
  
  <p>How can I tell Coq to apply the definition of <code>optimize_0plus</code> exactly once, and <strong>do no more and no less</strong>?</p>
  
  <p>I have tried <code>simpl optimize_0plus</code>, but it gives something with a long <code>match</code> statement, which seems to be doing too much. And I do not like to use the <code>rewrite</code> tactic every time to establish a lemma because this computation is exactly one step with paper and pencil.</p>
  
  <p>Notes: </p>
  
  <p>1.This is related to my <a href="https://stackoverflow.com/questions/33060802/how-to-apply-a-function-once-during-simplification-in-coq">earlier question here</a>, but the answers there about using <code>simpl XXX</code> does not seem to work here. This seems to be a more complicated case.</p>
  
  <p>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 <code>a1</code> etc. </p>
  
  <pre><code>  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.
  </code></pre>
  
  <p>So, my concern is not really to prove this simple theorem, but on how to prove this intuitively as I would on paper.</p>
  
  <p>-- UPDATE -- </p>
  
  <p>Thanks to @gallais, my original plan is incorrect as one can change </p>
  
  <pre><code>aeval (optimize_0plus (APlus a1 a2))
  </code></pre>
  
  <p>to </p>
  
  <pre><code>aeval (APlus (optimize_0plus a1) (optimize_0plus a2))
  </code></pre>
  
  <p>only for the cases where <code>a1</code> is not <code>ANum 0</code>. The <code>0</code> case has to be dealt with separately by <code>destruct a1.</code> as with the course website quoted in Note 2. </p>
  
  <p>However, I still have the same question for the other cases, listed below, which I think my original plan should work: </p>
  
  <pre><code>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)
  </code></pre>
  
  <p>For each of these 5 cases, it seems that one application (<code>beta</code> reduction??) of <code>optimize_0plus</code> should allow us to change e.g. (for <code>AMinus</code>)</p>
  
  <pre><code>aeval (optimize_0plus (AMinus a1 a2))  
  </code></pre>
  
  <p>to</p>
  
  <pre><code>aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))
  </code></pre>
  
  <p>, right?</p>
  
  <p>If so, how can I do this one-step reduction?</p>
  
  <p>Note:
  I tried </p>
  
  <pre><code>Eval cbv beta in (aeval (optimize_0plus (AMinus a1 a2))).
  </code></pre>
  
  <p>And I couldn't even get <code>aeval (AMinus (optimize_0plus a1) (optimize_0plus a2))</code> as I'd like to using a <code>Eval</code> in the proof. </p>