Acc is finite

AccFinite.v

CoInductive stream (A : Type) : Type :=
| Cons : A
         -> stream A
         -> stream A.

CoInductive infiniteDecreasingChain A (R : A -> A -> Prop) : stream A -> Prop :=
| ChainCons : forall x y s, infiniteDecreasingChain A R (Cons A y s)
                            -> R y x
                            -> infiniteDecreasingChain A R (Cons A x (Cons A y s)).

Lemma every_Acc_R_is_finite :
  forall A (R : A -> A -> Prop) x,
    Acc R x
    -> forall s, ~ infiniteDecreasingChain A R (Cons A x s).
Proof.
  intros A R x H.
  induction H as [x _ H2].
  intros s H3.
  inversion H3 as [H4 y s' H5 H6]. subst.
  specialize H2 with y s'.
  apply (H2 H6).
  assumption.
Qed.

(* stream A ~=~ nat -> A *)

Definition indexedChain (A : Type) (R : A -> A -> Prop) (s : nat -> A) : Prop :=
  forall n:nat, R (s (S n)) (s n).

Lemma every_Acc_R_is_finite' :
  forall A (R : A -> A -> Prop) x,
    Acc R x
    -> forall s, ~ indexedChain A R (fun n => match n with   (* ~ cons *)
                                              | 0 => x
                                              | S n => s n
                                              end).
Proof.
  intros A R x H.
  induction H as [x _ H2].
  intros s H3; unfold indexedChain in H3.
  assert (H30 := H3 0); simpl in H30.           (* ~ head *)
  specialize H2 with (s 0) (fun n => s (S n)).  (* ~ tail *)
  apply (H2 H30); clear H2 H30.
  intro n.
  assert (H3n := H3 (S n)); simpl in H3n; revert H3n.
  case n; trivial.
Qed.