The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, January 05, 2014 10:30:11 AM Daniel Schepler wrote:
> On Sunday, January 05, 2014 01:01:48 PM Jacques-Henri Jourdan wrote:
> > Hi Coq-Club !
> > 
> > I face a case where the cofixpoint guard condition seems too strong to me.
> > Here is a simplified version:
> > 
> > Require Import Streams.
> > 
> > CoInductive Tr :=
> > 
> > | L : nat -> Tr
> > | N : nat -> Tr -> Tr -> Tr.
> > 
> > CoFixpoint cfp (tr:Tr) (st:Stream nat) :=
> > match tr with
> > 
> > | L n => Cons n st
> > | N n l r =>
> > 
> > Cons n (cfp l (cfp r st))
> > end.
> > 
> > How can I make this definition accepted by Coq?
> 
> How about:
> 
> CoFixpoint cfps (trs:list Tr) (st:Stream nat) :=
>   match trs with
> 
>   | nil => st
>   | cons (L n) trs' => Cons n (cfps trs' st)
>   | cons (N n l r) trs' => Cons n (cfps (cons l (cons r trs')) st)
> 
>   end.
> 
> Definition cfp (tr:Tr) (st:Stream nat) :=
>   cfps (cons tr nil) st.

As a follow-up, here's how you could prove reduction rules for cfp:

Lemma cfps_nil : forall st, EqSt st (cfps nil st).
Proof.
destruct st; constructor; simpl.
reflexivity.
apply EqSt_reflex.
Qed.

Lemma cfps_app : forall trs1 trs2 st,
  EqSt (cfps (trs1 ++ trs2) st)
       (cfps trs1 (cfps trs2 st)).
Proof.
cofix; intros.
destruct trs1; simpl.
apply cfps_nil.

constructor.
destruct t; simpl.
reflexivity.
reflexivity.
destruct t; simpl.
apply cfps_app.
apply cfps_app with (trs1 := (t1 :: t2 :: trs1)%list)
  (trs2 := trs2).
Qed.

Lemma cfp_red1 : forall n st, EqSt (cfp (L n) st) (Cons n st).
Proof.
intros.
constructor; simpl.
reflexivity.
apply sym_EqSt.
apply cfps_nil.
Qed.

Lemma cfp_red2 : forall n l r st,
  EqSt (cfp (N n l r) st)
       (Cons n (cfp l (cfp r st))).
Proof.
intros.
constructor; simpl.
reflexivity.
apply cfps_app with (trs1 := (l :: nil)%list)
  (trs2 := (r :: nil)%list).
Qed.
-- 
Daniel Schepler