Stream: Coq users

Topic: ✔ Is it possible to make simpl automatically unfold defin...


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

view this post on Zulip 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 !_ _ /.

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 13:10):

that means, approximately, "reduce beta_reduce when it is applied to two arguments, and the first argument is a constructor.`

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 13:10):

this is not the 100% story, but that's a pattern I often use.

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

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 13:14):

Using Arguments effectively can benefit from looking at the manual. Two entry pointers are:

https://coq.inria.fr/distrib/current/refman/proofs/writing-proofs/equality.html?highlight=cbn#coq:tacn.simpl

It unfolds constants only if they lead to an ι-reduction, i.e. reducing a match or unfolding a fixpoint.

https://coq.inria.fr/distrib/current/refman/language/extensions/arguments-command.html?highlight=cbn#effects-of-arguments-on-unfolding

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

view this post on Zulip Paolo Giarrusso (Sep 25 2022 at 13:18):

(but I doubt it will, so I have this answer memorized instead)

view this post on Zulip walker (Sep 25 2022 at 13:42):

Thanks I will have to comprehend this and I will get back with more questions!

view this post on Zulip walker (Sep 25 2022 at 14:28):

It now makes complete sense to me! thanks alot!


Last updated: Mar 29 2024 at 12:02 UTC