The Coq mailing list

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

On Thursday 10 July 2008 22:11:07 Vladimir Komendantsky wrote:
> On Thu, Jul 10, 2008 at 03:42:08PM +0100, Sean Wilson wrote:
> > I don't expect to be able to automate everything, as long the heuristic
> > works in most cases, it should be helpful. I could do analysis of
> > definitions first to avoid unfolding such problematic functions.
>
> There can be several relevant methods as long as OCaml is concerned. The
> obvious one is to unfold a construction given that it is an evaluable
> global reference. It's a simple method that works nicely. It involves the
> following functions to do a test and conversion:
...

Hi,

I've written a short OCaml tactic called "unfold_simple" based on your code 
snippets that:

1. finds all subterms in the conclusion that are evaluable global references 
(which I assume means "unfoldable").

2. unfolds one reference at a time but undoes an unfold if unfolding produces 
any "Fix" terms (as I will rely on a call to "simpl" to simplify such terms 
as much possible).

It probably isn't going to work everywhere, but a call to "repeat progress 
(simpl; try unfold_simple)" cleans up my goals in the way I want for now. 
This is really useful when working with goals containing references to 
definitions like these:

Definition empty_queue := (nil, nil).
Definition queue_to_list (q : queue) := (fst q) ++ (rev (snd q)).
Definition queue_eq q1 q2 := (queue_to_list q1) = (queue_to_list q2).
Definition is_empty (q : queue) := (fst q = nil) /\ (snd q = nil).
Definition normal_form (q : queue) := (fst q <> nil) \/ snd q = nil.

Thanks for the feedback everyone!

Regards,

Sean