(* week-12_reasoning-about-streams-using-induction.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 10 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.

(* ***** *)

Lemma nat_ind2 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall n : nat, P n -> P (S n) -> P (S (S n))) ->
    forall n : nat, P n.
Proof.
  intros P H_P0 H_P1 H_PSS n.
  assert (H_both : P n /\ P (S n)).
  { induction n as [ | n' [IHn' IHSn']].
    - Check (conj H_P0 H_P1).
      exact (conj H_P0 H_P1).
    - Check (H_PSS n' IHn' IHSn').
      Check (conj IHSn' (H_PSS n' IHn' IHSn')).
      exact (conj IHSn' (H_PSS n' IHn' IHSn')).
  } 
  destruct H_both as [ly _].
  exact ly.
Qed.

Lemma nat_ind2_0 :
  forall P : nat -> Prop,
    P 0 ->
    P 1 ->
    (forall k : nat,
        P k ->
        P (S (S k))) ->
    forall n : nat,
      P n.
Proof.
  intros P H_P0 H_P1 H_PSS n.
  assert (H2 : P n /\ P (S n)).
  { induction n as [ | n' [IHn' IHSn']].
    - exact (conj H_P0 H_P1).
    - split.
      + exact IHSn'.
      + Check (H_PSS n' IHn').
        exact (H_PSS n' IHn'). }
  destruct H2 as [ly _].
  exact ly.
Qed.

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

(* Polymorphic streams: *)

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

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

(* More paraphernalia for reasoning equationally: *)

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

Theorem stream_decomposition :
  forall (V : Type)
         (vs : stream V),
    vs = stream_decompose V vs.
Proof.
  intros V [v vs'].
  unfold stream_decompose.
  reflexivity.
Qed.

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

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

Lemma fold_unfold_zeroes :
  zeroes = SCons nat 0 zeroes.
Proof.
  (* step by step: *)
  rewrite -> (stream_decomposition nat zeroes) at 1.
  unfold stream_decompose.
  unfold zeroes at 1.
  fold zeroes.
  reflexivity.

  Restart.

  (* folding after unfold in one step: *)
  rewrite -> (stream_decomposition nat zeroes) at 1.
  unfold stream_decompose.
  unfold zeroes at 1;
    fold zeroes.
  reflexivity.

  Restart.

  (* all at once (i.e., magical): *)
  rewrite -> (stream_decomposition nat zeroes) at 1.
  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.

Lemma fold_unfold_ones :
  ones = SCons nat 1 ones.
Proof.
  rewrite -> (stream_decomposition nat ones) at 1.
  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.

Lemma fold_unfold_zeroes_and_ones :
  zeroes_and_ones = SCons nat 0 (SCons nat 1 zeroes_and_ones).
Proof.
  rewrite -> (stream_decomposition nat zeroes_and_ones) at 1.
  rewrite -> (stream_decomposition nat zeroes_and_ones) at 1.
  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.

Lemma fold_unfold_ones_and_zeroes :
  ones_and_zeroes = SCons nat 1 (SCons nat 0 ones_and_zeroes).
Proof.
  rewrite -> (stream_decomposition nat ones_and_zeroes) at 1.
  rewrite -> (stream_decomposition nat ones_and_zeroes) at 1.
  reflexivity.
Qed.

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

(* A plausible theorem: *)

Theorem the_same_ones_and_zeroes_using_indexing :
  forall n : nat,
    stream_index nat ones_and_zeroes n = stream_index nat (SCons nat 1 zeroes_and_ones) n.
Proof.
  intro n.
  induction n as [ | | n' IHn'] using nat_ind2_0.
  - rewrite -> fold_unfold_ones_and_zeroes.
    rewrite ->2 fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_ones_and_zeroes.
    rewrite ->2 fold_unfold_stream_index_S.
    rewrite -> fold_unfold_zeroes_and_ones.
    rewrite ->2 fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_ones_and_zeroes.
    rewrite -> fold_unfold_zeroes_and_ones.
    rewrite ->4 fold_unfold_stream_index_S.
    exact IHn'.
Qed.

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

(* A similarly plausible theorem: *)

Theorem the_same_zeroes_and_ones_using_indexing :
  forall n : nat,
    stream_index nat zeroes_and_ones n = stream_index nat (SCons nat 0 ones_and_zeroes) n.

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

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

Lemma fold_unfold_stream_map :
  forall (V W : Type)
         (f : V -> W)
         (v : V)
         (vs' : stream V),
    stream_map V W f (SCons V v vs') = SCons W (f v) (stream_map V W f vs').
Proof.
  intros V W f v vs'.
  rewrite -> (stream_decomposition W (stream_map V W f (SCons V v vs'))).
  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.

Theorem indexing_ones_and_indexing_ones'_give_the_same_result :
  forall n : nat,
    stream_index nat ones n = stream_index nat ones' n.
Proof.
  intro n.
  unfold ones'.
  induction n as [ | n' IHn'].
  - rewrite ->2 fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_ones.
    rewrite -> fold_unfold_stream_index_S.
    rewrite -> fold_unfold_zeroes.
    rewrite -> fold_unfold_stream_map.
    rewrite -> fold_unfold_stream_index_S.
    exact IHn'.
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.

Lemma fold_unfold_partial_sums_aux :
  forall (n : nat)
         (ns' : stream nat)
         (a : nat),
    partial_sums_aux (SCons nat n ns') a =
    SCons nat (n + a) (partial_sums_aux ns' (n + a)).
Proof.
  (* step by step: *)
  intros n ns' a.
  Check (stream_decomposition
           nat
           (partial_sums_aux (SCons nat n ns') a)).
  rewrite -> (stream_decomposition
                nat
                (partial_sums_aux (SCons nat n ns') a)).
  unfold stream_decompose.
  unfold partial_sums_aux at 1.
  fold partial_sums_aux.
  reflexivity.

  Restart.

  (* folding after unfold in one step: *)
  intros n ns' a.
  rewrite -> (stream_decomposition
                nat
                (partial_sums_aux (SCons nat n ns') a)).
  unfold stream_decompose.
  unfold partial_sums_aux at 1;
    fold partial_sums_aux.
  reflexivity.

  Restart.

  (* all at once (i.e., magical): *)
  intros n ns' a.
  rewrite -> (stream_decomposition
                nat
                (partial_sums_aux (SCons nat n ns') a)).
  reflexivity.
Qed.

Definition partial_sums ns := partial_sums_aux ns 0.

(* Revisiting the 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.

Lemma fold_unfold_partial_sums'_aux :
  forall (n : nat)
         (ns' : stream nat)
         (a : nat),
    partial_sums'_aux (SCons nat n ns') a =
    SCons nat a (partial_sums'_aux ns' (n + a)).
Proof.
  intros n ns' a.
  rewrite -> (stream_decomposition
                nat
                (partial_sums'_aux (SCons nat n ns') a)).
  reflexivity.
Qed.

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.

Theorem partial_sum_and_partial_sum'_are_equivalent_using_indexing :
  forall (ns : stream nat)
         (i : nat),
    stream_index nat (partial_sums ns) i = stream_index nat (partial_sums' ns) i.
Proof.
  intros [n ns] i.
  unfold partial_sums, partial_sums'.
  revert n ns.
  induction i as [ | i' IHi']; intros n [n' ns'].
  - rewrite -> fold_unfold_partial_sums_aux.
    rewrite -> Nat.add_0_r.
    rewrite -> fold_unfold_stream_index_O.
    rewrite -> fold_unfold_partial_sums'_aux.
    rewrite -> fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_partial_sums_aux.
    rewrite -> Nat.add_0_r.
    rewrite -> fold_unfold_stream_index_S.
    rewrite -> fold_unfold_partial_sums'_aux.
    rewrite -> fold_unfold_stream_index_S.
Abort.

(* Using the Light of Inductil: *)

Lemma about_indexing_partial_sums_aux_and_partial_sums'_aux :
  forall (n : nat)
         (ns' : stream nat)
         (a : nat)
         (i : nat),
    stream_index nat (partial_sums_aux (SCons nat n ns') a) i
    =
    stream_index nat (partial_sums'_aux ns' (n + a)) i.
Proof.
  intros n ns' a i.
  revert n ns' a.
  induction i as [ | i' IHi']; intros n [n' ns''] a.
  - rewrite -> fold_unfold_partial_sums_aux.
    rewrite -> fold_unfold_partial_sums'_aux.
    rewrite ->2 fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_partial_sums_aux.
    rewrite -> fold_unfold_partial_sums'_aux.
    rewrite ->2 fold_unfold_stream_index_S.
    exact (IHi' n' ns'' (n + a)).
Qed.

Theorem partial_sum_and_partial_sum'_are_equivalent_using_indexing :
  forall (ns : stream nat)
         (i : nat),
    stream_index nat (partial_sums ns) i = stream_index nat (partial_sums' ns) i.
Proof.
  intros [n ns'] i.
  unfold partial_sums, partial_sums'.
  rewrite <- (Nat.add_0_r n) at 2.
  exact (about_indexing_partial_sums_aux_and_partial_sums'_aux n ns' 0 i).
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.

(* ***** *)

Theorem indexing_ones'_and_indexing_ones''_give_the_same_result_by_induction :
  forall n : nat,
    stream_index nat ones' n = stream_index nat ones'' n.
Abort.

Theorem indexing_ones'_and_indexing_ones''_give_the_same_result_because_Leibniz_equality_is_an_equivalence_relation :
  forall n : nat,
    stream_index nat ones' n = stream_index nat ones'' n.
Abort.

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

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

Lemma fold_unfold_make_stream_of_successive_numbers :
  forall i : nat,
    make_stream_of_successive_numbers i =
    SCons nat i (make_stream_of_successive_numbers (S i)).
Proof.
  intro i.
  rewrite -> (stream_decomposition nat (make_stream_of_successive_numbers i)).
  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.

(* ***** *)

Theorem indexing_stream_of_successive_positive_numbers_and_stream_of_successive_positive_numbers'_give_the_same_result :
  forall i : nat,
    stream_index nat stream_of_successive_positive_numbers  i
    =
    stream_index nat stream_of_successive_positive_numbers' i.
Abort.

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

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.

Lemma fold_unfold_make_stream_of_successive_numbers_2 :
  forall i : nat,
    make_stream_of_successive_numbers_2 i =
    SCons nat i (make_stream_of_successive_numbers_2 (S (S i))).
Proof.
  intro i.
  rewrite -> (stream_decomposition nat (make_stream_of_successive_numbers_2 i)).
  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.

Lemma fold_unfold_make_stream_of_successive_odd_numbers :
  forall i : nat,
    make_stream_of_successive_odd_numbers i =
    SCons nat (S (2 * i)) (make_stream_of_successive_odd_numbers (S i)).
Proof.
  intro i.
  rewrite -> (stream_decomposition nat (make_stream_of_successive_odd_numbers i)).
  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.

Theorem indexing_stream_of_successive_odd_numbers_and_stream_of_successive_odd_numbers'_give_the_same_result :
  forall i : nat,
    stream_index nat stream_of_successive_odd_numbers  i
    =
    stream_index nat stream_of_successive_odd_numbers' i.
Abort.

(* ***** *)

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

Lemma fold_unfold_make_stream_of_successive_squares :
  forall i : nat,
    make_stream_of_successive_squares i =
    SCons nat  (i * i) (make_stream_of_successive_squares (S i)).
Proof.
  intro i.
  rewrite -> (stream_decomposition nat (make_stream_of_successive_squares i)).
  reflexivity.
Qed.

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.

Theorem indexing_stream_of_successive_positive_squares_and_stream_of_successive_positive_squares'_give_the_same_result :
  forall i : nat,
    stream_index nat stream_of_successive_positive_squares  i
    =
    stream_index nat stream_of_successive_positive_squares' i.
Proof.
Abort.

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

CoFixpoint stream_append (V : Type) (v1s v2s : stream V) :=
  match v1s with
  | SCons _ v1 v1s' =>
    SCons V v1 (stream_append V v1s' v2s)
  end.

Lemma fold_unfold_stream_append :
  forall (V : Type)
         (v1 : V)
         (v1s' v2s : stream V),
    stream_append V (SCons V v1 v1s') v2s =
    SCons V v1 (stream_append V v1s' v2s).
Proof.
  intros V v1 v1s' v2s.
  rewrite -> (stream_decomposition V (stream_append V (SCons V v1 v1s') v2s)).
  reflexivity.
Qed.

Definition stream_append_simpler (V : Type) (v1s v2s : stream V) :=
  v1s.

Theorem stream_append_and_stream_append_are_equivalent_using_indexing :
  forall (V : Type)
         (eqb_V : V -> V -> bool),
    (forall v : V,
        eqb_V v v = true) ->
    forall (v1s v2s : stream V)
           (i : nat),
      stream_index V (stream_append V v1s v2s) i = stream_index V (stream_append_simpler V v1s v2s) i.
Proof.
  unfold stream_append_simpler.
  intros V eqb_V eqb_V_refl v1s v2s i.
  revert v1s.
  induction i as [ | i' IHi']; intros [v1 v1s'].
  - rewrite -> fold_unfold_stream_append.
    rewrite ->2 fold_unfold_stream_index_O.
    reflexivity.
  - rewrite -> fold_unfold_stream_append.
    rewrite ->2 fold_unfold_stream_index_S.
    exact (IHi' v1s').
Qed.

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

(* Revisiting stream_map: *)

(* ***** *)

(* what about
     map f (map g xs)
   and
     map (f o g) xs
   ?
*)

Theorem about_stream_map_and_compose_using_indexing :
  forall (X : Type)
         (Y : Type)
         (Z : Type)
         (eq_Z : Z -> Z -> Prop),
    (forall z : Z,
        eq_Z z z) ->
    forall (g : X -> Y)
           (f : Y -> Z)
           (xs : stream X)
           (i : nat),
      stream_index Z (stream_map Y Z f (stream_map X Y g xs)) i
      =
      stream_index Z (stream_map X Z (fun x => f (g x)) xs) i.
Proof.
Abort.

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

(* week-12_reasoning-about-streams-using-induction.v *)