The Coq mailing list

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

Hi,

I'm trying to write some automatic rewriting tactics and was wondering if Coq 
already has a certain feature already.

Given the usual definition of app:

fun A : Type =>
fix app (l m : list A) {struct l} : list A :=
  match l with
  | nil => m
  | a :: l1 => a :: app l1 m
  end

From this definition, we can directly read off two rewrite rules it implies:

forall m, app nil m = m
forall a l1 m, app (a::l1) m = a::app l1 m

With these, we can reduce terms containing app using rewriting without having 
to use the "simpl" tactic. The important points for me is that I want to be 
able to apply reductions one step at a time (in case it is simplified too 
much) and I want access to these rules in both directions. My question is, 
does Coq have a feature that allows me to extract these rewrite rules from 
functions automatically?

Also, is there another (easier) way I can get access to the right-to-left 
versions of these rewrites? I think there's a way using tactics to perform 
only one reduction at a time but I don't know how they could be applied in 
reverse.

By experimenting with tactics, I've found that it's not hard to produce these 
rewrite rules by starting with the lemma "app x y = app x y", unfolding the 
first app, doing case analysis on x and y, then calling various other tactics 
(e.g. to clear up let/in constructs, simplify branches) and folding up app 
definitions to finish up with several (trivial) subgoals, where each goal 
statement is a rewrite rule I need. Doing this, and some hacking in OCaml, I 
can see how one could do it, but I wanted to check if such a feature existed 
already.

Thanks,

Sean