title: Coq: defining more than two mutually recursive functions on inductive type
body: <p>I am defining three mutually recursive functions on inductive type <strong>event</strong>, using two different ways: using <strong>with</strong>  and <strong>fix</strong> keywords, however, Coq complains about <strong>principal argument</strong> and <strong>The reference ... was not found in ...</strong>, respectively.
  Two implementations of the functions are the following: </p>
  
  <pre><code>Require Import List.
  
  Parameter max: list nat -&gt; nat.
  Inductive event : Type := node: list event -&gt; event. 
  Parameter eventbool : forall (P:event-&gt;Prop) (e:event), {P e} + {~ P e}.
  Definition event_sumbool_b (e: event) (p: event -&gt; Prop) : bool :=
    if eventbool p e then true else false.
  
  Fixpoint parentround (e: event) : nat :=
    match e with
   | node l =&gt;  max (rounds l)
   end
  
   with rounds l := 
     match l with 
     | nil =&gt; 0::nil 
     | h::tl =&gt; round h:: rounds tl
     end 
  
   with round e := 
     if event_sumbool_b e roundinc then parentround e + 1 else parentround e
  
   with roundinc e :=
    exists S:list event, (forall y, List.In y S /\ round y = parentround e). 
  </code></pre>
  
  <p>Coq complains <strong>Recursive call to round has principal argument equal to "h" instead of "tl".</strong> Even though, <strong>h</strong> in calling <strong>round</strong> is a sub-term of <strong>e</strong>. Following the idea in <a href="https://cs.stackexchange.com/questions/104/recursive-definitions-over-an-inductive-type-with-nested-components">Recursive definitions over an inductive type</a>, I replaced <strong>parentround</strong> with the following: </p>
  
  <pre><code>Fixpoint parentround (e: event) : nat :=
  
   let round := 
     ( fix round (e: event) : nat := 
        if event_sumbool_b e roundinc then parentround e + 1 else parentround e
     ) in
  
   let roundinc := 
     ( fix roundinc (e: event) : Prop :=
       exists S:list event, (forall y, List.In y S /\ round y = parentround e)
     ) in
  
   match e with
   | node l =&gt;  max (rounds l)
   end
  
   with rounds l :=
     match l with 
     | nil =&gt; 0::nil 
     | h::tl =&gt; round h:: rounds tl
     end. 
  </code></pre>
  
  <p>It now complains about missing definition of <strong>roundinc</strong>. </p>
  
  <p>Please help me defining these three mutually recursive functions <strong>parentround</strong>, <strong>round</strong> and <strong>roundinc</strong>. </p>
  
  <p><strong>EDIT</strong> There is a fourth function <strong>rounds</strong> in the definition, however, it is not problematic so far. </p>