The Coq mailing list

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

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