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
>
>
- [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Wilayat Khan, 09/19/2016
- Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Dominique Larchey-Wendling, 09/19/2016
- Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Wilayat Khan, 09/20/2016
- Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Dominique Larchey-Wendling, 09/21/2016
- Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Wilayat Khan, 09/20/2016
- Re: [Coq-Club] Defining three mutually recursive functions on inductive type in Coq, Dominique Larchey-Wendling, 09/19/2016
Archive powered by MHonArc 2.6.18.