The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

On 22.04.13 8:12 PM, AUGER Cédric wrote:
> Well in fact, I just had to change "fix" in "cofix", and it worked.
> cofix is always so hard to understand for me…

Ah, yes, since the "recursive" call "per n" is also under the guard "BF 
b", you can change it into a corecursive call.

You can fuse the nested fixed-points as follows:

Definition periodic (nelb : ne_list_bool) : bool_flow :=
  (cofix periodic nelb_ :=
   match nelb_ with
   NELB b s => BF b match s with
                    | inl _ => periodic nelb
                    | inr n => periodic n
                    end
   end) nelb.

But in general, your suggestion to relax the guard condition would be 
useful.  See also

  Mixed Inductive/Coinductive Types and Strong Normalization
  http://www2.tcs.ifi.lmu.de/~abel/publications.html#aplas07

Cheers,
Andreas

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

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/