The Coq mailing list

[Jannis Limperg <jannis AT limperg.de>]

Hey Igor,

here's a solution to your puzzle. Hope it helps! For more info, see the
CPDT chapter on coinduction [1]. In general, Coq's coinduction is a bit
annoying, so you may want to consider alternative representations. For
example, streams over T can also be represented as functions [nat -> T].

[1] http://adam.chlipala.net/cpdt/html/Cpdt.Coinductive.html

Cheers,
Jannis


Parameter T: Type.
Parameter R: T -> T -> Prop.

(* [{a' | R a a'}] is like [exists a', R a a'], but the latter only
allows you to extract the witness when you're building something in
Prop. Below, we'll need to build a stream (which lives in Type, not
Prop) using exists_all, so we need to use the 'stronger' existential.*)
Hypothesis exists_all : forall a, {a' | R a a'}.

CoInductive stream : Type :=
| sintro: forall a: T, stream -> stream.

Definition head (s : stream) : T :=
  match s with
  | sintro x xs => x
  end.

Definition tail (s : stream) : stream :=
  match s with
  | sintro x xs => xs
  end.

(* This 'trivial' lemma is a workaround for a limitation of Coq's
coinductive types. See below for a use case. *)
Lemma stream_eta : forall s, s = sintro (head s) (tail s).
Proof.
  intro s. destruct s. reflexivity.
Qed.

CoInductive smatch : stream -> stream -> Prop :=
| smatch_intro:
    forall a1 a2 s1' s2',
    R a1 a2 ->
    smatch s1' s2'  ->
    smatch (sintro a1 s1') (sintro a2 s2').

(* The solution to your original problem is to define the stream and the
proof that it matches separately. This is necessary because while stream
and smatch are coinductive types, [exists s', smatch s s'] is not, and
you can only use corecursion when constructing a coinductive type. *)
CoFixpoint matching_stream (s : stream) : stream :=
  sintro (proj1_sig (exists_all (head s))) (matching_stream (tail s)).

Lemma matching_stream_matches : forall s, smatch s (matching_stream s).
Proof.
  cofix rec.
  intro s.
  destruct s as [hd tl].
  (* At this point, Coq does not reduce [matching_stream (sintro hd tl)]
  (try cbn). This is why we need stream_eta. *)
  rewrite (stream_eta (matching_stream (sintro hd tl))).
  constructor; cbn.
  - exact (proj2_sig (exists_all hd)).
  - exact (rec tl).
Qed.

Theorem stream_ex:
  forall s, exists s', smatch s s'.
Proof.
  intro s. exists (matching_stream s). apply matching_stream_matches.
Defined.