The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT inria.fr>]

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.

--
JH


Le 15/07/2013 00:44, Michiel Helvensteijn a écrit :
> Hi all,
>
> I have two mutually recursive functions with two arguments each
> (simplified example):
>
> Fixpoint f (a: T) (b: U) : V := ...
> with g (a: T) (b: U) : V := ...
>
> I know that they terminate because, as a pair, the arguments are
> structurally decreasing. That is to say, in `f`, `a` decreases and `b`
> is passed unchanged, and in `g`, `a` is passed unchanged and `b`
> decreases.
>
> `Fixpoint` accepts only a single decreasing argument as evidence for
> termination. Apparently the `Function` construct is more flexible
> w.r.t. termination evidence, but not, it seems, for mutual recursion.
>
> Sure, I could add a third argument to decrease on, such as a `c: nat`
> containing the sum of the structural depths of `a` and `b`. But that
> would involve a lot of tedious boilerplate code, not to mention
> preconditions and proofs of the fact that `c` always remains large
> enough.
>
> Is there a technique or construct I'm unaware of? Something that will
> make this easier?
>
> Thanks in advance!
>
> --
> www.mhelvens.net