The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

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