The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

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.

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.