(* week-11_programming-with-streams.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 06 Apr 2025 *)

(* ********** *)

Require Import Arith Bool List.

(* ********** *)

(* Paraphernalia for reasoning equationally: *)

Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.

(* ********** *)

(* Miscellanies: *)

(* ***** *)

Fixpoint eqb_list (V : Type) (eqb_V : V -> V -> bool) (v1s v2s : list V) : bool :=
  match v1s with
    nil =>
    match v2s with
      nil =>
      true
    | v2 :: v2s' =>
      false
    end
  | v1 :: v1s' =>
    match v2s with
      nil =>
      false
    | v2 :: v2s' =>
      eqb_V v1 v2 && eqb_list V eqb_V v1s' v2s'
    end
  end.

(* ********** *)

(* Polymorphic streams: *)

CoInductive stream (V : Type) : Type :=
  SCons : V -> stream V -> stream V.

(* ***** *)

Property a_stream_does_not_end :
  forall (V : Type)
         (vs : stream V),
    exists (v : V) (vs' : stream V),
      vs = SCons V v vs'.
Proof.
  intros V [v vs'].
  exists v, vs'.
  reflexivity.
Qed.

(* ***** *)

Definition stream_head (V : Type) (vs : stream V) : V :=
  match vs with
    SCons _ v _ =>
    v
  end.

Definition stream_tail (V : Type) (vs : stream V) : stream V :=
  match vs with
    SCons _ _ vs' =>
    vs'
  end.

(* ***** *)

(* "stream_index V n vs" maps the stream vs into its element at index n *)

Fixpoint stream_index (V : Type) (vs : stream V) (n : nat) : V :=
  match n with
    0 =>
    match vs with
      SCons _ v _ =>
      v
    end
  | S n' =>
    match vs with
      SCons _ _ vs' =>
      stream_index V vs' n'
    end
  end.

Lemma fold_unfold_stream_index_O :
  forall (V : Type)
         (vs : stream V),
    stream_index V vs 0 =
    match vs with
      SCons _ v _ =>
      v
    end.
Proof.
  fold_unfold_tactic stream_index.
Qed.

Lemma fold_unfold_stream_index_S :
  forall (V : Type)
         (vs : stream V)
         (n' : nat),
    stream_index V vs (S n') =
    match vs with
      SCons _ _ vs' =>
      stream_index V vs' n'
    end.
Proof.
  fold_unfold_tactic stream_index.
Qed.

(* ***** *)

(* "stream_prefix V n vs" maps the stream vs into the list of its n first elements *)

Fixpoint stream_prefix (V : Type) (n : nat) (vs : stream V) : list V :=
  match n with
    0 =>
    nil
  | S n' =>
    match vs with
      SCons _ v vs' =>
      v :: stream_prefix V n' vs'
    end
  end.

Lemma fold_unfold_stream_prefix_0 :
  forall (V : Type)
         (vs : stream V),
    stream_prefix V 0 vs = nil.
Proof.
  fold_unfold_tactic stream_prefix.
Qed.

Lemma fold_unfold_stream_prefix_S :
  forall (V : Type)
         (n' : nat)
         (v : V)
         (vs' : stream V),
    stream_prefix V (S n') (SCons V v vs') =
    v :: stream_prefix V n' vs'.
Proof.
  fold_unfold_tactic stream_prefix.
Qed.

(* ********** *)

(* A sample of simple streams: *)

(* ***** *)

(* The stream of 0's: *)

CoFixpoint zeroes : stream nat :=
  SCons nat 0 zeroes.

Lemma testing_zeroes :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 3 zeroes)
    (0 :: 0 :: 0 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* The stream of 1's: *)

CoFixpoint ones : stream nat :=
  SCons nat 1 ones.

Lemma testing_ones :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 3 ones)
    (1 :: 1 :: 1 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* The stream of consecutive 0's and 1's that starts with 0: *)

CoFixpoint zeroes_and_ones : stream nat :=
  SCons nat 0 (SCons nat 1 zeroes_and_ones).

Lemma testing_zeroes_and_ones :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 5 zeroes_and_ones)
    (0 :: 1 :: 0 :: 1 :: 0 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* The stream of consecutive 1's and 0's that starts with 1: *)

CoFixpoint ones_and_zeroes : stream nat :=
  SCons nat 1 (SCons nat 0 ones_and_zeroes).

Lemma testing_ones_and_zeroes :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 5 ones_and_zeroes)
    (1 :: 0 :: 1 :: 0 :: 1 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ********** *)

(* stream_map is the stream analogue of list_map in the midterm project: *)

CoFixpoint stream_map (V W : Type) (f : V -> W) (vs : stream V) : stream W :=
  match vs with
    SCons _ v vs' =>
    SCons W (f v) (stream_map V W f vs')
  end.

Lemma testing_stream_map_with_the_stream_of_zeroes :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 5 (stream_map nat nat S zeroes))
    (1 :: 1 :: 1 :: 1 :: 1 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* Another stream of 1's: *)

Definition ones' : stream nat :=
  stream_map nat nat S zeroes.

Lemma testing_ones' :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 3 ones')
    (1 :: 1 :: 1 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ********** *)

(* partial_sums maps a stream of natural numbers to the stream of its partial sums *)
(* for example, it maps
     SCons nat n1 (SCons nat n2 (SCons nat n3 (SCons nat n4 ...)))
   to
     SCons nat n1 (SCons nat (n1 + n2) (SCons nat (n1 + n2 + n3) (SCons nat (n1 + n2 + n3 + n4) ...)))
*)

CoFixpoint partial_sums_aux (ns : stream nat) (a : nat) : stream nat :=
  match ns with
    SCons _ n ns' =>
    SCons nat (n + a) (partial_sums_aux ns' (n + a))
  end.

Definition partial_sums ns := partial_sums_aux ns 0.

(* ***** *)

(* An alternative implementation of partial_sums: *)

CoFixpoint partial_sums'_aux (ns : stream nat) (a : nat) : stream nat :=
  match ns with
    SCons _ n ns' =>
    SCons nat a (partial_sums'_aux ns' (n + a))
  end.

Definition partial_sums' ns :=
    match ns with
    SCons _ n ns' =>
      partial_sums'_aux ns' n
    end.

Lemma testing_partial_sums'_using_the_stream_of_ones :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 5 (partial_sums' ones))
    (1 :: 2 :: 3 :: 4 :: 5 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* And a third stream of 1's: *)

Definition ones'' : stream nat :=
  partial_sums (SCons nat 1 zeroes).

Lemma testing_ones'' :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 3 ones'')
    (1 :: 1 :: 1 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ********** *)

(* A simple way to construct the stream of successive positive numbers: *)

CoFixpoint make_stream_of_successive_numbers (i : nat) : stream nat :=
  SCons nat i (make_stream_of_successive_numbers (S i)).

Lemma testing_make_stream_of_successive_numbers :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 4 (make_stream_of_successive_numbers 5))
    (5 :: 6 :: 7 :: 8 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

Definition stream_of_successive_positive_numbers :=
  make_stream_of_successive_numbers 1.

Lemma testing_stream_of_successive_positive_numbers :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 4 stream_of_successive_positive_numbers)
    (1 :: 2 :: 3 :: 4 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

(* An alternative way to construct the stream of successive positive numbers: *)

Definition stream_of_successive_positive_numbers' :=
  partial_sums ones.

Lemma testing_stream_of_successive_positive_numbers' :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 4 stream_of_successive_positive_numbers')
    (1 :: 2 :: 3 :: 4 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ********** *)

CoFixpoint make_stream_of_successive_numbers_2 (i : nat) : stream nat :=
  SCons nat i (make_stream_of_successive_numbers_2 (S (S i))).

Lemma testing_make_stream_of_successive_numbers_2 :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 4 (make_stream_of_successive_numbers_2 5))
    (5 :: 7 :: 9 :: 11 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

Definition stream_of_successive_odd_numbers :=
  make_stream_of_successive_numbers_2 1.

Lemma testing_stream_of_successive_odd_numbers :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 7 stream_of_successive_odd_numbers)
    (1 :: 3 :: 5 :: 7 :: 9 :: 11 :: 13 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

CoFixpoint make_stream_of_successive_odd_numbers (i : nat)  : stream nat :=
  SCons nat (S (2 * i)) (make_stream_of_successive_odd_numbers (S i)).

Lemma testing_make_stream_of_successive_odd_numbers :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 5 (make_stream_of_successive_odd_numbers 10))
    (21 :: 23 :: 25 :: 27 :: 29 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

Definition stream_of_successive_odd_numbers' : stream nat :=
  make_stream_of_successive_odd_numbers 0.

Lemma testing_stream_of_successive_odd_numbers' :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 7 stream_of_successive_odd_numbers')
    (1 :: 3 :: 5 :: 7 :: 9 :: 11 :: 13 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ***** *)

CoFixpoint make_stream_of_successive_squares (i : nat) : stream nat :=
  SCons nat (i * i) (make_stream_of_successive_squares (S i)).

Definition stream_of_successive_positive_squares : stream nat :=
  make_stream_of_successive_squares 1.

Lemma testing_stream_of_successive_positive_squares :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 7 stream_of_successive_positive_squares)
    (1 :: 4 :: 9 :: 16 :: 25 :: 36 :: 49 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

Definition stream_of_successive_positive_squares' : stream nat :=
  partial_sums stream_of_successive_odd_numbers.

Lemma testing_stream_of_successive_positive_squares' :
  eqb_list
    nat
    Nat.eqb
    (stream_prefix nat 7 stream_of_successive_positive_squares')
    (1 :: 4 :: 9 :: 16 :: 25 :: 36 :: 49 :: nil)
  = true.
Proof.
  compute.
  reflexivity.
Qed.

(* ********** *)

(* Transducing a stream into a stream of pairs: *)

CoFixpoint transduce_1_2 (V : Type) (vs : stream V) : stream (V * V) :=
  match vs with
    SCons _ v1 (SCons _ v2 vs') =>
    SCons (V * V) (v1, v2) (transduce_1_2 V vs')
  end.

(* Transducing a stream of pairs into a stream of triples: *)

CoFixpoint transduce_2_3 (V : Type) (ps : stream (V * V)) : stream (V * V * V) :=
  match ps with
    SCons _ (v1, v2) (SCons _ (v3, v4) (SCons _ (v5, v6) ps')) =>
    SCons (V * V * V) (v1, v2, v3) (SCons (V * V * V) (v4, v5, v6) (transduce_2_3 V ps'))
  end.

(* Transducing a stream of triples into a stream of pairs: *)

CoFixpoint transduce_3_2 (V : Type) (ts : stream (V * V * V)) : stream (V * V) :=
  match ts with
    SCons _ (v1, v2, v3) (SCons _ (v4, v5, v6) ts') =>
    SCons (V * V) (v1, v2) (SCons (V * V) (v3, v4) (SCons (V * V) (v5, v6) (transduce_3_2 V ts')))
  end.

(* ********** *)

(* end of week-11_programming-with-streams.v *)