The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Here's how to do it with a bit less duplication.  The key is to use a 
[Section] or explicit [fun] to bind each argument that is not supposed 
to vary during recursion, so that expanding out the definitions leads to 
exactly the code you gave at first.

Section frec_grec.
  Variables f g : nat -> nat -> nat.
  Variable a : nat.

  Fixpoint frec b :=
    match a with
      | O => 0
      | S a' => f a' b + g a' b
    end +
    match b with
      | O => 0
      | S b' => frec b' + grec b'
    end
  with grec b :=
    match a with
      | O => 0
      | S a' => f a' b + g a' b
    end +
    match b with
      | O => 0
      | S b' => grec b'
    end.
End frec_grec.

Fixpoint f (a : nat) :=
  frec f g a
with g (a : nat) :=
  grec f g a.


On 07/15/2013 04:18 AM, Jacques-Henri Jourdan wrote:
> Does the following fits your needs ?
>
> Fixpoint f (a:nat) :=
>   (fix frec b :=
>     match a with
>       | O => 0
>       | S a' => f a' b + g a' b
>     end +
>     match b with
>       | O => 0
>       | S b' => frec b' + grec b'
>     end
>    with grec b :=
>    match a with
>      | O => 0
>      | S a' => f a' b + g a' b
>    end +
>    match b with
>      | O => 0
>      | S b' => grec b'
>    end
>    for frec)
> with g (a:nat) :=
> (fix frec b :=
>     match a with
>       | O => 0
>       | S a' => f a' b + g a' b
>     end +
>     match b with
>       | O => 0
>       | S b' => frec b' + grec b'
>     end
>    with grec b :=
>    match a with
>      | O => 0
>      | S a' => f a' b + g a' b
>    end +
>    match b with
>      | O => 0
>      | S b' => grec b'
>    end
>    for grec).
>
> I was searching how to do that without code replication, but I have no 
> Idea for now.