Coq: defining more than two mutually recursive functions on inductive type

Question

I am defining three mutually recursive functions on inductive type event, using two different ways: using with and fix keywords, however, Coq complains about principal argument and The reference ... was not found in ..., respectively. Two implementations of the functions are the following:

Require Import List.

Parameter max: list nat -> nat.
Inductive event : Type := node: list event -> event. 
Parameter eventbool : forall (P:event->Prop) (e:event), {P e} + {~ P e}.
Definition event_sumbool_b (e: event) (p: event -> Prop) : bool :=
  if eventbool p e then true else false.

Fixpoint parentround (e: event) : nat :=
  match e with
 | node l =>  max (rounds l)
 end

 with rounds l := 
   match l with 
   | nil => 0::nil 
   | h::tl => 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).

Coq complains Recursive call to round has principal argument equal to "h" instead of "tl". Even though, h in calling round is a sub-term of e. Following the idea in Recursive definitions over an inductive type, I replaced parentround with the following:

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 =>  max (rounds l)
 end

 with rounds l :=
   match l with 
   | nil => 0::nil 
   | h::tl => round h:: rounds tl
   end.

It now complains about missing definition of roundinc.

Please help me defining these three mutually recursive functions parentround, round and roundinc.

EDIT There is a fourth function rounds in the definition, however, it is not problematic so far.

Btw, there is an issue with your round function: it doesn't call parentround on a sub-term of e, but directly on e. I don't think this is allowed. — Vinz
Also, in roundinc, the call to round y is not decreasing, it should be something like round l where e = node l — Vinz
@Vinz The function round is called from within rounds where the sub-term of e (which is h) is passed (renaming e in round makes no difference). When it is called from within roundinc, as you pointed it out, y is not decreasing. Actually, the real function is using a complex predicate stronglysee on y and e, which include that y is a sub-event of e. The problem now, in addition, is: even if we include that predicate in roundinc, Coq does not understand automatically, that y is indeed a sub-term of e. — Khan

ejgallego ejgallego · Accepted Answer · 2016-09-07T18:34:35

It was a bit difficult for me to figure out what you would like to compute, I'd start with something like:

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import bigop.

Definition max_seq l := \max_(x <- l) x.

Inductive event : Type :=
  node : seq event -> event.

Fixpoint round_lvl (e : event) : nat :=
  (* XXX: Missing condition *)
  let cond_inc x := round_lvl x in
  match e with
  | node l => max_seq (map cond_inc l)
  end.

But I had trouble parsing what the existence condition means. I suggest you try to express the problem without Coq code first, and maybe from that a solution pops.

Coq: defining more than two mutually recursive functions on inductive type

2 Answers