Simple proof of stream of ones in Coq

Taking code from CPDT, I'd like to prove a property for the easy stream ones, which always return 1.

CoFixpoint ones : Stream Z := Cons 1 ones.

Also from CPDT, I use this function to retrieve a list from the stream:

Fixpoint approx A (s:Stream A) (n:nat) : list A :=
    match n with
    | O => nil
    | S p => match s with
        | Cons h t => h :: approx A t p
        end
    end.

To get a list of five 1, e.g.:

Eval compute in approx Z ones 5.
= 1 :: 1 :: 1 :: 1 :: 1 :: nil
  : list Z

How do I prove, that for all n given to approx, the list will contain only 1? I'm not even sure how to formulate this. Should I use a help function like nth n list for lists, that return element number n from list? And that

forall (n length : nat), nth n1 (approx Z ones length) = 1

(Or maybe use Zeq instead of =.)

Am I heading the right direction?

Solution

I think having a more general view than the point-wise nth view of lists will be easier to deal with. Here is how I would go (the proof is 0 automation to be sure you see everything) :

Inductive all_ones : list Z -> Prop :=
  | nil_is_ones : all_ones nil (* nil is only made of ones *)
  (* if l is only made of ones, 1 :: l is too *)
  | cons_is_ones : forall l, all_ones l -> all_ones (cons 1%Z l)
  (* and these are the only option to build a list only made of ones
.

CoFixpoint ones : Stream Z := Cons 1%Z ones.

Fixpoint approx A (s:Stream A) (n:nat) : list A :=
    match n with
    | O => nil
    | S p => match s with
        | Cons h t => h :: approx A t p
        end
    end.

Lemma approx_to_ones : forall n, all_ones (approx _ ones n).
Proof.
induction n as [ | n hi]; simpl in *.
- now constructor.
- constructor.
  now apply hi.
Qed.

If you prefer a more functional definition of all_ones, here are some equivalent definitions:

Fixpoint fix_all_ones (l: list Z) : Prop := match l with
  | nil => True
  | 1%Z :: tl => fix_all_ones tl
  | _ => False
end.

Fixpoint fix_bool_all_ones (l: list Z) : bool := match l with
  | nil => true
  | 1%Z :: tl => fix_bool_all_ones tl
  | _ => false
end.

Lemma equiv1 : forall l, all_ones l <-> fix_all_ones l.
Proof.
induction l as [ | hd tl hi]; split; intros h; simpl in *.
- now idtac.
- now constructor.
- destruct hd; simpl in *.
  + now inversion h; subst; clear h.
  + inversion h; subst; clear h. 
    now apply hi.
  + now inversion h; subst; clear h.
- destruct hd; simpl in *.
  + now case h.
  + destruct p; simpl in *.
    * now case h.
    * now case h.
    * constructor; now apply hi.
  + now case h.
Qed.

Lemma equiv2 : forall l, fix_all_ones l <-> fix_bool_all_ones l = true.
Proof.
induction l as [ | hd tl hi]; split; intros h; simpl in *.
- reflexivity.
- now idtac.
- destruct hd; simpl in *.
  + now case h.
  + destruct p; simpl in *.
    * now case h.
    * now case h.
    * now apply hi.
  + now case h.
- destruct hd; simpl in *.
  + discriminate h.
  + destruct p; simpl in *.
    * now case h.
    * now case h.
    * now apply hi.
  + discriminate h. 
Qed.

Best,