The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT inria.fr>]

> hello, i have some problems in building some theory of sequences
>(possibly finite streams).
>
> I cannot prove the theorem :
>
>Theorem I_nth : (s:Sequence)(infinite s)->(n:nat)(nth_defined s n).
>
>telling that if a sequence is infinite, we can define its n-th element
>for each n .

Hello Pierre,

In spite that this theorem talks about infinite sequences, its
proof does not proceed by co-induction but simple by induction 
on the natural number n.

The following script provides a possible proof. It combines the
function nth defined in theories/LISTS/Streams.v (which computes the
nth element of a stream) and the tactic program.

Regards,
Eduardo.


(****************************************************************************)
(*            was "Streams.v"                                               *)
(*                    Modified to allow finite sequences                    *)
(*                     by P. Casteran                                       *)
(****************************************************************************)

Section Sequences. 

Variable A : Set.

(* The set of (possibly finite) streams : definition *)

CoInductive Set Sequence   := Empty : Sequence |
                              Cons : A->Sequence->Sequence.


Definition head : (s:Sequence)(~s=Empty)->A.
Destruct s.
 Intro abs; Absurd Empty=Empty; Trivial.
 Intros; Assumption.
Defined.

Definition tail  := 
  [x:Sequence] Cases x of Empty => Empty | (Cons _ s) => s end.

CoInductive infinite : Sequence -> Prop :=
  Cons_i : (a:A)(s:Sequence)(infinite s) ->(infinite (Cons a s)).


Lemma emptyNoInfinite : (s:Sequence)(infinite s)->~s=Empty.
Intros s H.
Inversion H.
Discriminate.
Qed.

Lemma tailOfInfinite : (s:Sequence)(infinite s)->(infinite (tail s)).
Intros s H.
Inversion H.
Assumption.
Qed.

Fixpoint nth [n:nat] : (s:Sequence)(infinite s)->A := 
  [s:Sequence]
   [H:(infinite s)] 
           Cases n of
                  O    => (head s (emptyNoInfinite s H)) 
                |(S m) => (nth m (tail s) (tailOfInfinite s H))
            end.


(* (is_nth a n s) means  "a is at the n th position in sequence s" *)

Inductive is_nth[a:A]: nat->Sequence->Prop :=
    is_nth_O : (s:Sequence)(is_nth a O (Cons a s))
 |  is_nth_S : (n:nat)(b:A)(s:Sequence)(is_nth a n s)->
                                       (is_nth a (S n) (Cons b s)).

Hint tailOfInfinite is_nth_O is_nth_S.

Inductive nth_defined[s:Sequence;n:nat] : Set :=
    nth_defined_intro : (a:A)(is_nth a n s)->(nth_defined s n).

Theorem I_nth : (n:nat)(s:Sequence)(infinite s)->(nth_defined s n).
Realizer nth.
Program_all.
 Inversion H0.
 Generalize i; Clear i; Simpl;Case s;[Intro i;Inversion i|Auto].
Qed.