The Coq mailing list

[Wilayat Khan <wilayatk AT gmail.com>]

Hello Dominique

My type event is actually Inductive event : Type := node: tuple -> list event -> event., where tuple is a record type, and the list of events are parents. The new required type of nat2ev would be, nat2ev: tuple -> nat -> event. But in this case, I fear, we loose information about the tuples of the parents. Regardless of that, I wonder, how to define roundinc (a proposition, with exists inside) as a boolean roundinc: event -> bool. 

An information definition of the of the function parentround (I want to formalize in Coq) is:

   parentround(x) = max({round(y) | y \in parents(x)}, where parents is the list of events inside an event (second argument of node).

   round(x) = if roundinc(x)  then parentround(x) + 1 else parentround(x)

   roundinc(x) = exists S, (forall y \in S, round(y) = parentround(x) /\ stronglysee(x, y)

  

   

Wilayat

--------------------------------------------------------------------------

On Mon, Sep 19, 2016 at 7:51 PM, Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr> wrote:

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