some corecursive stuff in coq

corecursion.v

(* A type for infinite streams *)
CoInductive stream (A:Type) :=
  | scons : A -> stream A -> stream A.

Implicit Arguments scons.

Definition stream_hd {A:Type} (s:stream A) :=
  match s with scons x _ => x end.

Definition stream_tl {A:Type} (s:stream A) :=
  match s with scons _ s' => s' end.

(* Getting the Nth element of a stream is a regular fixpoint decreasing on n *)
Fixpoint Nth {A:Type} (n:nat) (s:stream A) : A :=
  match n with
      O => stream_hd s
    | S n' => Nth n' (stream_tl s)
  end.

(* This function is useful to force unfolding a stream one level *)
Definition stream_decompose {A:Type} (s:stream A) :=
  match s with scons x s' => scons x s' end.

(* This lemma tells us that stream_decompose is an identity *)
Lemma stream_dec {A:Type} : forall s:stream A, s = stream_decompose s.
Proof.
  intros s.
  destruct s.
  simpl.
  trivial.
Qed.

(* Instead let's define the predicate as coinductive *)
CoInductive stream_increasing' : stream nat -> Prop :=
  | str_inc' : forall n s, n < stream_hd s -> stream_increasing' s -> stream_increasing' (scons n s).

Inductive stream_increasing_2 : stream nat -> Prop :=
  str_inc_2 : forall s, (forall n, Nth n s < Nth (S n) s) -> stream_increasing_2 s.

Lemma Nth_scons : forall (A:Type) n (x:A) s, Nth (S n) (scons x s) = Nth n s.
  auto.
Qed.

Theorem increasing_equiv : forall s, stream_increasing' s -> stream_increasing_2 s.
Proof.
  intros s H.
  split.
  intros m.
  revert s H.
  induction m.
  intros s H; destruct H; auto.
  intros s H.
  destruct s.
  rewrite !Nth_scons.
  apply IHm.
  inversion H; subst.
  assumption.
Qed.

Lemma inc_2_scons : forall n s, stream_increasing_2 (scons n s) -> stream_increasing_2 s.
Proof.
  intros n s H.
  inversion H; subst.
  apply str_inc_2.
  intros m.
  specialize H0 with (n0:=S m).
  rewrite !Nth_scons in H0.
  assumption.
Qed.

Theorem increasing_equiv' : forall s, stream_increasing_2 s -> stream_increasing' s.
Proof.
  cofix.
  intros s H.
  destruct s.
  split.
  inversion H; subst.
  specialize H0 with (n0:=0).
  simpl in H0.
  assumption.
  apply increasing_equiv'.
  apply (inc_2_scons n).
  assumption.
Qed.