The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Wilatyat Khan,

Your definition of roundinc certainly has a problem.
Since event is a infinite type, it is possible to show
that "roundinc e" implies False. Indeed, no list can contain
every element of an infinite type. Maybe it should be replaced
by

with roundinc e :=
 exists S:list event,
     (forall y, List.In y S ->
        round y*=* parentround e /\ stronglysee e y)

but I am not sure this is the intended meaning.

Then assuming that there exists a universal decider for
the Type event is really a strong assumption:

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

You can easily deduce than any predicate over nat is decidable by
injection nat into event

Fixpoint nat2ev n := match n with 0 => node nil | S n => node (nat2ev
n::nil) end.


Then I suggest that roundinc should be constructed as a map
event -> bool which would avoid the use of eventbool.

Having said that, building your mutually inductive functions
should be possible with the Fix operator (Require Import Wf)
which I suppose is the same as "accessibility predicates",
but it is not an easy exercice in my opinion.

Regards,

Dominique