The Coq mailing list

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

Hi Wilayat,

> 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.

Hence event is a type of finitely branching trees indexed by tuple.

> 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*. 

Well I have an easy definition for you ;-) :

Definition roundinc (_ : event) := true.

Because with this definition

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

you can always choose S as the empty list to fulfil
the exists S condition.

Another problem is that the definition of round e calls
(eventbool roundinc) as well as parentround on the same
argument e, which is not a syntactically well-founded
way of doing recursive calls. So you may need to unfold
those definitions to make them acceptable to Coq.

Dominique


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