The Coq mailing list

["Luke Palmer" <lrpalmer AT gmail.com>]

Hi, I'm having some trouble doing some simple coinduction.  Here is a
simplified case that I have the same problem with:

CoInductive Seq : Type :=
| cons : nat -> Seq -> Seq.

CoFixpoint mapSeq (f : nat->nat) (seq:Seq) :=
  match seq with
  | cons n s' => cons (f n) (mapSeq f s')
  end.

CoInductive IncreasingFrom : nat -> Seq -> Prop :=
| increasing_next : forall n n' rest, n <= n' -> IncreasingFrom n' rest
         -> IncreasingFrom n (cons n' rest).

Definition monotone f := forall x y, x <= y -> f x <= f y.

Lemma monotone_map : forall f x seq, IncreasingFrom x seq ->
IncreasingFrom (f x) (mapSeq f seq).
  intro f.
  cofix.
  intros.
  destruct H.

And here I get stuck.  The goal is [IncreasingFrom (f n) (mapSeq f
(cons n' rest))].  I would like to change that to [IncreasingFrom (f
x) (cons (f n') (mapSeq f rest))], but coinductive types have this odd
unfolding rule that I can't figure out how to apply.

Thanks,
Luke