The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Luke Palmer wrote:
> [...]
> 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 following works:

Definition hd (seq:Seq) := match seq with cons n s' => n end.
Definition tl (seq:Seq) := match seq with cons n s' => s' end.

Lemma Seq_form : forall seq, seq = cons (hd seq) (tl seq).
Proof.
  intros.
  destruct seq.
  reflexivity.
Qed.

Lemma monotone_map : forall f x seq, monotone f ->
  IncreasingFrom x seq ->
  IncreasingFrom (f x) (mapSeq f seq).
Proof.
  intros f.
  cofix.
  intros x seq Hmonotone H.
  rewrite Seq_form.
  refine
    (match H in IncreasingFrom x' seq' return seq = seq' -> _ with
       increasing_next _ _ _ _ _ => fun Heq => _ end (refl_equal seq)).
  apply increasing_next.
  simpl; auto.
  rewrite (Seq_form seq) in Heq.
  injection Heq.
  simpl; auto.
Qed.


The basic idea is to transform the goal into something that fits
increasing_next's conclusion and then apply this constructor (the aim is
to respect the guard condition), and then use the coinduction
hypothesis. Note that I need "monotone f" as an hypothesis. The refine
call is a slightly more precise version of "destruct H".

> [...] coinductive types have this odd
> unfolding rule that I can't figure out how to apply.

Think of way to force computation in a lazy language. This is what I do
with hd and tl.


Cheers,

-- 
Stéphane Glondu