CODEWITHSUNDEEP
logiccoqinductionmutual-recursion
Khan
Khan

Reputation: 303

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

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.

Upvotes: 1

Views: 2498

Answers (2)

ejgallego
ejgallego

Reputation: 6852

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.

Upvotes: 2

Vinz
Vinz

Reputation: 6047

From my experience, it is really hard to define mutual function on a type T and on list T. I recall a post on Coq-club about this subjet, I have to find it again.

The "easy" solution is to define a mutual inductive type where you define event and event_list at the same time. However, you won't be able to use the list library...

Upvotes: 1

Related Questions