The Coq mailing list

[harke AT cs.pdx.edu]

IIUC, you need to force a single unfolding by pattern matching on your
coinductive data.  I've interleaved the specific answer with the code
you've provided.

On Fri, Oct 10, 2008 at 02:46:52PM -0600, Luke Palmer wrote:
] 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.

Definition force s :=
   match s with
   | cons h t => cons h t
   end.

Lemma rw s:
   s = force s.
Proof.
intros [h t].
auto.
Qed.

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

(* here you have: IncreasingFrom (f n) (mapSeq f (cons n' rest)) *)

rewrite rw.
simpl.

(* here you have: IncreasingFrom (f x) (cons (f n') (mapSeq f rest)) *)

-- 
Tom Harke