## 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: May 24 2024 at 23:01 UTC