walker (Sep 25 2022 at 10:31): walker (Sep 25 2022 at 10:31):I have a common pattern where I refine a recursive function.
Fixpoint beta_reduce_rec (y m : Term) (idx: nat): Term.
and then have a thin wrapper like:
Definition beta_reduce (y m : Term) := beta_reduce_rec y m 0.
The problem in in those patterns, is that I always need to do extra unfold before simpl, is there a way to hint simpl to double beta_reduce before attemping simplification.
I am ofcourse assuming that shorter proofs are nicer, and thus wanting to make all my proofs as short as possible
Paolo Giarrusso (Sep 25 2022 at 13:09):Global Arguments beta_reduce /. will make simpl always unfold beta_reduce (applied or not), but you can do even better... say that beta_reduce_rec recurses on the first argument; then you typically want:
Global Arguments beta_reduce !_ _ /.
that means, approximately, "reduce beta_reduce when it is applied to two arguments, and the first argument is a constructor.`
Paolo Giarrusso (Sep 25 2022 at 13:10):this is not the 100% story, but that's a pattern I often use.
Paolo Giarrusso (Sep 25 2022 at 13:11):for Fixpoint, no Arguments is needed, because simpl has a rule that automatically unfolds fixpoints when that lets a match reduce — a iota reduction
Paolo Giarrusso (Sep 25 2022 at 13:14):Using Arguments effectively can benefit from looking at the manual. Two entry pointers are:
It unfolds constants only if they lead to an ι-reduction, i.e. reducing a match or unfolding a fixpoint.
Paolo Giarrusso (Sep 25 2022 at 13:18):I don't know if shorter proofs are always nicer (speed and maintainability also count), but in this case I agree: these Arguments directives automate boring details in a robust way, so they save work for both reader and prover. And this is a common enough issue that (ignoring compatibility questions) I often wish simpl would automate this.
Paolo Giarrusso (Sep 25 2022 at 13:18):(but I doubt it will, so I have this answer memorized instead)
walker (Sep 25 2022 at 13:42):Thanks I will have to comprehend this and I will get back with more questions!
walker (Sep 25 2022 at 14:28):It now makes complete sense to me! thanks alot!
Last updated: Sep 23 2023 at 08:01 UTC