The Coq mailing list

[harke AT cs.pdx.edu]

If you wish to do this in a more primitive way you could do the
following:

begin Coq *)

Require Import List.

Definition fg : nat -> list nat -> bool -> nat :=
   fix fg c  : list nat -> bool -> nat := 
   fix fg_c (d:list nat) : bool -> nat := 
   fun b =>
   if b
   then
      match c with
      | 0   => 0
      | S n => fg n d true + fg n d false
      end
   else
      match d with
      | nil  => 0
      | a::l => fg_c l true + fg_c l false
      end
.

(* end Coq

In this
  - I've curried the input
  - the mutual recursion of f and g, each returning a [nat], is
    rolled together into a non-mutual recursive fg which returns a
    [bool -> nat].  [bool] is used as a conveniently predefined
    index type with 2 elements, though any other 2 element type
    would work.
  - the use of nested [fix]es allows you to recurse on either the
    [nat] argument (with no restriction on the [list nat] arg),
    or the [list nat] arg (with the restriction that the [nat]
    arg doesn't change)


On Tue, May 26, 2009 at 04:36:39PM +0200, Guilhem Moulin wrote:
] 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.

-- 
Tom Harke
Portland State University