The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Mon, 22 Apr 2013 10:32:09 +0200,
Pierre Boutillier 
<pierre.boutillier AT pps.univ-paris-diderot.fr>
 a
écrit :

> Hi,
> 
> On the one hand, yes it is easy, you just have to change line 933 of
> file kernel/inductive.ml
>     | _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
> by
>    | Fix (rec_args,(names,types,bodies) -> something_smart
> 
> On the other hand, something_smart has to be correct because you are
> in the kernel :-)
> 
> Cheers,
> Pierre B.

Well in fact, I just had to change "fix" in "cofix", and it worked.
cofix is always so hard to understand for me…

> 
> On 21/04/2013 22:11, AUGER Cédric wrote:
> > =============================================================
> > Inductive ne_list_bool :=
> >  NELB : bool -> (unit + ne_list_bool) -> ne_list_bool.
> > CoInductive bool_flow := BF : bool -> bool_flow -> bool_flow.
> >
> > Definition periodic (nelb : ne_list_bool) : bool_flow :=
> >   cofix periodic :=
> >   (fix per nelb_ :=
> >    match nelb_ with
> >    NELB b s => BF b match s with
> >                     | inl _ => periodic
> >                     | inr n => per n
> >                     end
> >    end) nelb.
> > =============================================================
> >
> > Hi all, I wanted the previous code to work.
> > I think I understand why it does not work, and I think I know at
> > trick to do what I want (the trick is simply to unroll the first
> > recursive call to have directly a match). But this trick is not
> > very convenient as I will have to do a first proof with a first
> > unrolling and then the recursive call.
> >
> > So I am asking if it would be easy to have in the next version of
> > Coq an allowance of this term or the following equivalent one
> > (which may be easier to have):
> > =================================================================
> > Definition periodic (nelb : ne_list_bool) : bool_flow :=
> >   cofix periodic :=
> >   (fix per nelb_ :=
> >    BF (match nelb_ with NELB b _ => b end)
> >       (match match nelb_ with NELB _ s => s end with
> >        | inl _ => periodic
> >        | inr n => per n end))
> >   nelb.
> > =================================================================
> > In which it is even more obvious that a call to BF will occur before
> > any call to periodic.
>