The Coq mailing list

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

Hi list

I wish to do some mutual definition using a well-founded measure, like
its cousin using structural induction.


Here is some (stupid) code which does not compile using Coq 8.2, even if
the mathematical definitions seem to terminate:

(***)
Require Import List Recdef.

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

Function f (c:nat*list nat) {measure pif} : nat :=
  match fst c with
    | 0   => 0
    | S n => f (n,snd c) + g (n,snd c)
  end

with g (c:nat*list nat) {measure pif} : nat :=
  match snd c with
    | nil  => 0
    | a::l => f (fst c,l) + g (fst c,l)
  end.
(***)


Do you know if there is any hint or something to solve my problem?

Thanks in advance,
cheers,
Guilhem.

Attachment: signature.asc
Description: Digital signature