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).
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: Oct 03 2023 at 21:01 UTC