The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Sean Wilson wrote:
> 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
>
> ...
Not exactly what you describe, but you can also have directly the single 
fix-point equation:

forall A l, app l m = match l with nil => m | a :: ll => a :: app ll m end.

Here is how:
Welcome to Coq 8.1 (Feb. 2007)

Coq < Require Import List.

Coq < Functional Scheme app_ind := Induction for app Sort Prop.
app_equation is defined
app_ind is defined

Coq < Check app_equation.
app_equation
    : forall (A : Type) (l m : list A),
      l ++ m = match l with
               | nil => m
               | a :: l1 => a :: l1 ++ m
               end
Coq < Lemma example : (1::2::nil)++(3::nil) = (1::2::3::nil).
1 subgoal

 ============================
  (1 :: 2 :: nil) ++ 3 :: nil = 1 :: 2 :: 3 :: nil

example < rewrite app_equation.
1 subgoal

 ============================
  1 :: (2 :: nil) ++ 3 :: nil = 1 :: 2 :: 3 :: nil

example < rewrite app_equation.
1 subgoal

 ============================
  1 :: 2 :: nil ++ 3 :: nil = 1 :: 2 :: 3 :: nil

example < rewrite app_equation.
1 subgoal

 ============================
  1 :: 2 :: 3 :: nil = 1 :: 2 :: 3 :: nil

As you see the single equation app_equation behaves like your collection 
of equations when any of
them would apply...

Note that the fix-point equation is generated automatically when you use 
Function instead of
Fixpoint to define your recursive function (Function does a few more 
things, though, please refer
to the documentation).

Yves