coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Mixing induction and coinduction
- Date: Mon, 22 Apr 2013 10:32:09 +0200
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.
- [Coq-Club] Mixing induction and coinduction, AUGER Cédric, 04/21/2013
- Re: [Coq-Club] Mixing induction and coinduction, Pierre Boutillier, 04/22/2013
- Re: [Coq-Club] Mixing induction and coinduction, AUGER Cédric, 04/22/2013
- Re: [Coq-Club] Mixing induction and coinduction, Andreas Abel, 04/23/2013
- Re: [Coq-Club] Mixing induction and coinduction, AUGER Cédric, 04/22/2013
- Re: [Coq-Club] Mixing induction and coinduction, Pierre Boutillier, 04/22/2013
Archive powered by MHonArc 2.6.18.