Stream: Coq users

Topic: Trouble with reduction


view this post on Zulip 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?

view this post on Zulip Yann Leray (Jun 28 2022 at 16:01):

In this case, you should simplify before starting your induction

view this post on Zulip Callan McGill (Jun 28 2022 at 19:47):

Could you elaborate why?

view this post on Zulip 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

view this post on Zulip 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: Jan 29 2023 at 06:02 UTC