The Coq mailing list

[Pierre CASTERAN <Pierre.Casteran AT labri.u-bordeaux.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 .


 I assume that the problem  comes from the guarding conditions,
(only constructors above the recursive call) but is there some
classical solution ?

Thank you in advance,

Pierre


(****************************************************************************)
(*            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.


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


(* (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)).
       
Inductive nth_defined[s:Sequence;n:nat] : Prop :=
    nth_defined_intro : (a:A)(is_nth a n s)->(nth_defined s n).

Theorem I_nth : (s:Sequence)(infinite s)->(n:nat)(nth_defined s n).
 (* Cofix  naturally doesn't work ! *)

 (* may be use an auxiliary predicate? *)
                                       
    CoInductive AUX : Sequence ->Prop :=
        AUX_i : (a:A)(s:Sequence )
         (AUX s) ->
         ((n:nat)(nth_defined  s n)) ->
         (AUX (Cons a s)).

  Remark triv: (s:Sequence)(AUX s)->(n:nat)(nth_defined  s n).
 Intros s H.
  Inversion H.
  Induction n.
  Exists a;Auto.
  Constructor 1.
 
  Intros.
  Case (H1 n0).
  Intros.
   Exists a0.
  Constructor 2.
  Auto.
  Qed.

  Remark DontWork : (s:Sequence)(infinite s) -> (AUX s).
  Cofix.
  Destruct s.
  Intro.
 Inversion H.

 Intros. 
 Split.
 Apply DontWork.
 Inversion H.
 Auto.

 Intro;Apply triv.
 Guarded.
 Apply DontWork.
 Guarded. (* NO !!!! *)