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?
In this case, you should simplify before starting your induction
Could you elaborate why?
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
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: Jan 29 2023 at 06:02 UTC