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
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.`
this is not the 100% story, but that's a pattern I often use.
for Fixpoint
, no Arguments
is needed, because simpl
has a rule that automatically unfolds fixpoints when that lets a match reduce — a iota
reduction
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.
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.
(but I doubt it will, so I have this answer memorized instead)
Thanks I will have to comprehend this and I will get back with more questions!
It now makes complete sense to me! thanks alot!
Last updated: Oct 13 2024 at 01:02 UTC