Callan McGill (Jun 28 2022 at 15:52): 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