The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

Well, you must have tried simpl, right?

Other than that: you can use Notation instead of Definition; then the
defined term will be unfolded at parse time automatically. However,
Notations have a different scoping behavior.

You can also specify what *not* to unfold, instead of what to unfold,
using compute, if that helps.

-- 
Robin

On Thu, 10 Jul 2008 15:11:56 +0100
Sean Wilson 
<sean.wilson AT ed.ac.uk>
 wrote:

> Hi,
> 
> I'm writing some automated tactics and want to check if there is a
> reduction tactic that can simplify the current goal in a certain way.
> It's sometimes useful to use definitions as shorthands for common
> expressions e.g.
> 
> Definition permutation x y := forall n, count n x = count n y.
> 
> In my domain, it is normally required that all 'simple' definitions
> like this (i.e. non-recursive functions) be unfolded first for my
> automation to work. As a simple example of what I need, given this
> definition:
> 
> Definition f x y := plus x y.
> 
> The following is true:
> 
> Goal forall x y, f x y = f y x.
> 
> My proof automation can prove this goal but only if "f" is unfolded
> first. I've tried various combinations to have this done
> automatically (i.e. I don't want to have to tell it what to unfold
> explicitly) but I cannot find a suitable reduction tactic. The
> closest I've found is compute which gives this:
> 
> forall x y : nat,
> (fix plus (n m : nat) : nat := match n with
>                                | 0 => m
>                                | S p => S (p + m)
>                                end) x y =
> (fix plus (n m : nat) : nat := match n with
>                                | 0 => m
>                                | S p => S (p + m)
>                                end) y x
> 
> I can then "fold plus" to get the simplification I want:
> 
> forall x y : nat, x + y = y + x
> 
> However, I'd like a tactic that does this automatically. Is there a
> tactic that can do unfolding like this without me having explicitly
> name definitions? Perhaps there is a way to automatically fold up
> goals containing "fix plus" like terms? Even a function only
> available in OCaml would be suitable.
> 
> Thanks,
> 
> Sean
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>