Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq


Chronological Thread 
  • From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq
  • Date: Wed, 21 Sep 2016 10:35:55 +0200
  • Organization: LORIA

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




Archive powered by MHonArc 2.6.18.

Top of Page