The Coq mailing list

[Benoit Razet <benoit.razet AT inria.fr>]

You can use also Fixpoint with the ad-hoc predicate technique and a 
well-founded relation.
The extra argument used for ensuring the termination will be erased at 
extraction.
The following Coq listing may be scary looking compared to the original one...

Require Import List.
Require Import Plus.

Definition pif (c:nat*list nat) := fst c + length (snd c).

(* relation for successor, the well-foundedness of this relation will be 
used. *)
Definition Rnat (n' n : nat) : Prop := n = S n'.

Lemma dom_inv1 : forall c n l n',
  Acc Rnat (pif c) ->
  c = (n, l) ->
  n = S n' -> Acc Rnat (pif (n',l)).
Proof.
intros c n l n' P eq eq1.
rewrite eq in P. rewrite eq1 in P. unfold pif in P. simpl in P.
unfold pif. simpl.
assert (P1 : Rnat (n' + length l) (S (n' + length l))).
  unfold Rnat. reflexivity.
exact (Acc_inv P _ P1).
Defined.

Lemma dom_inv2 : forall c n l a l',
  Acc Rnat (pif c) ->
  c = (n, l) ->
  l = (a :: l') -> Acc Rnat (pif (n,l')).
Proof.
intros c n l a l' P eq eq1.
rewrite eq in P. rewrite eq1 in P. unfold pif in P. simpl in P.
unfold pif. simpl.
generalize (plus_Snm_nSm n (length l')).
intro L. rewrite <- L in P.
assert (P1 : Rnat (n + length l') (S (n + length l'))).
  unfold Rnat. reflexivity.
exact (Acc_inv P _ P1).
Defined.


Fixpoint f (c:nat*list nat) (h : Acc Rnat (pif c)) {struct h} : nat :=
  match c as c1 return c = c1 -> nat with
  | (n,l) => fun eq =>
    match n as n1 return n = n1 -> nat with
    | 0 => fun eq1 => 0
    | S n' => fun eq1 =>
      f (n', l) (dom_inv1 c n l n' h eq eq1)  + g (n', l)  (dom_inv1 c n l n' 
h eq eq1)
    end (refl_equal n)
  end (refl_equal c)

with g (c:nat*list nat) (h : Acc Rnat (pif c)) {struct h} : nat :=
  match c as c1 return c = c1 -> nat with
  | (n,l) => fun eq =>
    match l as l1 return l = l1 -> nat with
    | nil => fun eq1 => 0
    | a :: l' => fun eq1 =>
      f (n, l') (dom_inv2 c n l a l' h eq eq1)  + g (n, l')  (dom_inv2 c n l 
a l' h eq eq1)
    end (refl_equal l)
  end (refl_equal c).


Guilhem Moulin wrote:
> 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.
> >
> > ------------------------------------------------------------------------
> >
> > Subject:
> > Re: [Coq-Club] Mutual definition using a well-founded measure
> > From:
> > Yves Bertot 
> > <Yves.Bertot AT sophia.inria.fr>
> > Date:
> > Tue, 26 May 2009 17:16:50 +0200
> > To:
> > Guilhem Moulin 
> > <guilhem.moulin AT ens-lyon.org>
> >
> > To:
> > Guilhem Moulin 
> > <guilhem.moulin AT ens-lyon.org>
> >
> >
> > 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