The Coq mailing list

[Guilhem Moulin <guilhem.moulin AT ens-lyon.org>]

I didn't know it, thanks!
As attachment is the hint Yves just gave me

Guilhem.

On Tue, 26 May 2009 at 17:33:57 +0200, Stéphane Lescuyer wrote:
> Nothing's impossible but certainly, it won't happen overnight :) In
> the meanwhile, you might be interested in this work by Arthur
> Charguéraud :
> http://www.chargueraud.org/arthur/research/2009/fixwf/
> In particular, his fixpoint library has some support for
> mutually-recursive functions.
> 
> HTH,
> 
> Stéphane L.

--- Begin Message ---

• From: Yves Bertot <Yves.Bertot AT sophia.inria.fr>
• To: Guilhem Moulin <guilhem.moulin AT ens-lyon.org>
• Subject: Re: [Coq-Club] Mutual definition using a well-founded measure
• Date: Tue, 26 May 2009 17:16:50 +0200
• Authentication-results: mx.google.com; spf=neutral (google.com: 140.77.166.68 is neither permitted nor denied by best guess record for domain of Yves.Bertot AT sophia.inria.fr) smtp.mail=Yves.Bertot AT sophia.inria.fr

You could define a single function using a sum-type as input, with the various alternative in the input
corresponding to the various functions you wish to define recursively. This works well in your case,
because the output of the two mutually recursive functions are in the same type.

Inductive inpt : Type :=
 g_arg (c:nat*list nat) | f_arg (c:nat*list nat).

Function h(x:inpt) : nat :=
 match x with
     f_arg c =>
    match fst c with
    | 0 =>  0
    | S n => h(f_arg (n, snd c)) + h(g_arg(n, snd c))
    end
 | g_arg c =>
    match  snd c with
    | nil => 0
    | a::l => h(f_arg(fst c, l)) + h(g_arg (fst c, l))
    end
 end.

Definition f c = h (f_arg c).
Definition g c = h (g_arg c).

You should be able to prove the expected equations for f and g.

When the output types are different, it becomes slightly more complex,
but it should still be possible, although you will have to come back to
basic well-founded induction.

Here is an example:

f (x:nat) = match x with 0 => 0 | S p => Zabs_nat (2+(g (Z_of_nat p)))
with
g (x:Z) = if Z_le_dec x 0 then 0%Z else Z_of_nat (2 + f (Zabs_nat (x - 1)))

These functions should be definable with:

Inductive inp2 : Type :=
  f2_arg (x:nat) | g2_arg (x:Z).

Definition type_f (x:inp2) := match x with f2_arg _ => nat | g2_arg _ => Z end.

Definition inp2_nat (x:inp2) := match x with f2_arg n => n | g2_arg z => Zabs_nat z end.

Lemma l1 : forall x, (0 < x)%Z -> inp2_nat (f2_arg (Zabs_nat (x-1))) < inp2_nat (g2_arg x).
Admitted.

Lemma l2 : forall x, inp2_nat (g2_arg (Z_of_nat x)) < inp2_nat (f2_arg (S x)).
Admitted.

Now, with these lemmas you should be able to define h2 so that it captures the combined
behavior of f and g. I have to leave now, but I will complete the development later.

Yves



Yves



--- End Message ---

Attachment: signature.asc
Description: Digital signature