## Stream: Coq users

### Topic: Trouble with reduction

#### Callan McGill (Jun 28 2022 at 15:52):

I have a basic question that I am confused about. Suppose I have the following type:

``````Inductive aexp : Type :=
| ANum (n : nat)
| APlus (a1 a2 : aexp)
| AMinus (a1 a2 : aexp)
| AMult (a1 a2 : aexp).
``````

with function:

``````Fixpoint opt_a (a:aexp) : aexp :=
match a with
| ANum n => ANum n
| APlus (ANum n) (ANum m) => ANum (n + m)
| APlus (ANum 0) e2 => opt_a e2
| APlus  e1 e2 => APlus  (opt_a e1) (opt_a e2)
| AMinus e1 e2 => AMinus (opt_a e1) (opt_a e2)
| AMult  e1 e2 => AMult  (opt_a e1) (opt_a e2)
end.
``````

I then want to prove this theorem:

``````Lemma opt_a_0 : forall a,
aeval (opt_a (APlus (ANum 0) a)) = aeval a.
Proof.
intros a. induction a.
- simpl. reflexivity.
-
``````

At this point I am supposed to prove: `aeval (opt_a (APlus (ANum 0) (APlus a1 a2))) = aeval (APlus a1 a2)`. I would expect the proof to follow by applying the definition of `opt_a` followed by induction but whenever I run `simpl` it does too much unfolding. Any ideas of how best to approach it?

#### Yann Leray (Jun 28 2022 at 16:01):

In this case, you should simplify before starting your induction

#### Callan McGill (Jun 28 2022 at 19:47):

Could you elaborate why?

#### Yann Leray (Jun 28 2022 at 19:50):

The way you defined `opt_a`, it will already reduce when passed `APlus (ANum 0) a` (whatever the value of `a`) so you if you want to eventually simplify, doing it once as soon as possible is usually a good idea

#### Michael Soegtrop (Jun 29 2022 at 07:28):

There is also an alternative simplification tactic `cbn` which allows a reduction specification as argument, notably you can restrict the symbols you want to expand e.g. with `cbn [aeval opt_a]`. The proof will likely still require quite a bit of case analysis with destruct.

Last updated: Oct 03 2023 at 21:01 UTC