The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

Hello 

  I am defining three mutually recursive functions in Coq on list of events (trees), however, I get the termination error. Here is my definition:

Require Import List.

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

Parameter listmax: list nat -> nat.

Parameter eventbool : forall (P:event->Prop) (e:event), {P e} + {~ P e}.

Parameter stronglysee : event -> event -> Prop. 

Fixpoint parentround (e: event) : nat :=

  match e with

 | node l =>  listmax (map round l)

 end

   

 with round e := match (eventbool roundinc e) with 

   | left _ => parentround e + 1

   | right _ => parentround e

   end    

 with roundinc e :=   

  exists S:list event, 

    (forall y, List.In y S /\ round y = parentround e /\ stronglysee e y).

Each call to round inside parentround gets an event which is the sub-term of original event and recursive calls to parentround inside roundinc gets event again a sub-term of original event. The call to round inside roundinc is a bit tricky. According to the definition of stronglysee, if  stronglysee e  y then it means y is a sub-term of e. To ensure, event e is decreasing in each recursive call, a relation can be defined on the function below: 

Fixpoint generation (e: event) : nat := 

 match e with 

 | node l => match l with

     | nil => 0

     | x::xs => 1 + listmax (map generation l)

     end

 end.

Where the generation of event in each call is decreasing. A lemma such as 

 Lemma ordersee: forall x y, stronglysee x y -> generation x > generation y.

 need to be proved. 

QUESTIONS: 

1) Can I instead define parentround as inductive type? Keeping in mind, the function returns a nat value, which will later be used in functions such as max : nat -> nat -> nat. 

2)  Is the approach 'accessibility predicates'  (as mentioned by Chlipala) suitable? The generation function above can be used in the order relation required, however, the reasoning might be very cumbersome as pointed in [https://www.irisa.fr/celtique/pichardie/papers/flops06.pdf]. 

3) Any other easy way to define this function in Coq? 

Thanks, 

Wilayat