(* week-12_reasoning-about-streams-using-coinduction.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_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.

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

(* Bisimilarity -- the coinductive counterpart of structural equality: *)

CoInductive bisimilar : forall V : Type, (V -> V -> bool) -> stream V -> stream V -> Prop :=
  Bisimilar :
    forall (V : Type)
           (eqb_V : V -> V -> bool)
           (v1 v2 : V),
      eqb_V v1 v2 = true ->                                  (* 1 *)
      forall v1s v2s : stream V,
        bisimilar V eqb_V v1s v2s ->                         (* 2 *)
        bisimilar V eqb_V (SCons V v1 v1s) (SCons V v2 v2s). (* 3 *)

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

(* 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_bisimilarity :
  bisimilar nat Nat.eqb ones_and_zeroes (SCons nat 1 zeroes_and_ones).
Proof.
  cofix coIH.
  (* It seems so easy
     Yeah, so doggone easy
     Oh, it seems so easy
     Yeah, where Coq's concerned
     My brain can learn
     Oh-oh-oh

     -- Linda Ronstadt (nearly) *)
  exact coIH.
(* Qed. *)
(* Not so fast, Louie.

   -- Rick Blaine (exactly) *)
  Show Proof.
Abort.

(* The plausible theorem with a proof by coinduction: *)

Theorem the_same_ones_and_zeroes :
  bisimilar nat Nat.eqb ones_and_zeroes (SCons nat 1 zeroes_and_ones).
Proof. (* with two occurrences of the apply tactic *)
  cofix coIH.
  rewrite -> fold_unfold_ones_and_zeroes.
  rewrite -> fold_unfold_zeroes_and_ones.
  Search (Nat.eqb _ _ = true).
  Check (Bisimilar
           nat
           Nat.eqb
           1
           1
           (Nat.eqb_refl 1)).
  Check (Bisimilar
           nat
           Nat.eqb
           1
           1
           (Nat.eqb_refl 1)
           (SCons nat 0 ones_and_zeroes)
           (SCons nat 0 (SCons nat 1 zeroes_and_ones))).
  apply (Bisimilar
           nat
           Nat.eqb
           1
           1
           (Nat.eqb_refl 1)
           (SCons nat 0 ones_and_zeroes)
           (SCons nat 0 (SCons nat 1 zeroes_and_ones))).
  Check (Bisimilar
           nat
           Nat.eqb
           0
           0
           (Nat.eqb_refl 1)
           ones_and_zeroes
           (SCons nat 1 zeroes_and_ones)).
  apply (Bisimilar
           nat
           Nat.eqb
           0
           0
           (Nat.eqb_refl 1)
           ones_and_zeroes
           (SCons nat 1 zeroes_and_ones)).
  exact coIH.
Qed. (* Yay! *)

(* Another proof of the same theorem: *)

Theorem the_same_ones_and_zeroes' :
  bisimilar nat Nat.eqb ones_and_zeroes (SCons nat 1 zeroes_and_ones).
Proof.
  cofix coIH. (* with one occurrence of the apply tactic *)
  rewrite -> fold_unfold_ones_and_zeroes.
  rewrite -> fold_unfold_zeroes_and_ones.
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (SCons nat 0 ones_and_zeroes) (SCons nat 0 (SCons nat 1 zeroes_and_ones))).
  apply (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (SCons nat 0 ones_and_zeroes) (SCons nat 0 (SCons nat 1 zeroes_and_ones))).
  Check (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones)).
  Check (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones) coIH).
  exact (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones) coIH).
Qed.

(* A third proof of the same theorem: *)

Theorem the_same_ones_and_zeroes'' :
  bisimilar nat Nat.eqb ones_and_zeroes (SCons nat 1 zeroes_and_ones).
Proof. (* with zero occurrences of the apply tactic *)
  cofix coIH.
  rewrite -> fold_unfold_ones_and_zeroes.
  rewrite -> fold_unfold_zeroes_and_ones.
  Check (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones)).
  Check (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones) coIH).
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (SCons nat 0 ones_and_zeroes) (SCons nat 0 (SCons nat 1 zeroes_and_ones))).
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (SCons nat 0 ones_and_zeroes) (SCons nat 0 (SCons nat 1 zeroes_and_ones)) (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones) coIH)).
  exact (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (SCons nat 0 ones_and_zeroes) (SCons nat 0 (SCons nat 1 zeroes_and_ones)) (Bisimilar nat Nat.eqb 0 0 (Nat.eqb_refl 0) ones_and_zeroes (SCons nat 1 zeroes_and_ones) coIH)).
Qed.

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

(* A similarly plausible theorem: *)

Theorem the_same_zeroes_and_ones_using_bisimilarity :
  bisimilar nat Nat.eqb zeroes_and_ones (SCons nat 0 ones_and_zeroes).
Abort.

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

(* 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 ones_and_ones'_are_bisimilar :
  bisimilar nat Nat.eqb ones ones'.
Proof.
  unfold ones'.
  cofix coIH.
  rewrite -> fold_unfold_zeroes.
  rewrite -> fold_unfold_ones.
  rewrite -> fold_unfold_stream_map.
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) ones (stream_map nat nat S zeroes)).
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) ones (stream_map nat nat S zeroes) coIH).
  exact (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) ones (stream_map nat nat S zeroes) coIH).
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_bisimilarity :
  forall ns : stream nat,
    bisimilar nat Nat.eqb (partial_sums ns) (partial_sums' ns).
Proof.
Abort.

(* Using the Light of co-Inductil: *)

Lemma about_partial_sums_aux_and_partial_sums'_aux :
  forall (n : nat)
         (ns' : stream nat)
         (a : nat),
  bisimilar
    nat
    Nat.eqb
    (partial_sums_aux (SCons nat n ns') a)
    (partial_sums'_aux ns' (n + a)).
Proof.
  cofix coIH.
  intros n [n' ns''] a.
  rewrite -> fold_unfold_partial_sums_aux.
  rewrite -> fold_unfold_partial_sums'_aux.
  Check (Bisimilar nat Nat.eqb (n + a) (n + a) (Nat.eqb_refl (n + a))).
  Check (Bisimilar nat Nat.eqb (n + a) (n + a) (Nat.eqb_refl (n + a)) (partial_sums_aux (SCons nat n' ns'') (n + a)) (partial_sums'_aux ns'' (n' + (n + a)))).
  apply (Bisimilar nat Nat.eqb (n + a) (n + a) (Nat.eqb_refl (n + a)) (partial_sums_aux (SCons nat n' ns'') (n + a)) (partial_sums'_aux ns'' (n' + (n + a)))).
  Check (coIH n' ns'' (n + a)).
  exact (coIH n' ns'' (n + a)).
Qed.

Lemma about_partial_sums_aux_and_partial_sums'_aux_alt :
  forall (n : nat)
         (ns' : stream nat)
         (a : nat),
  bisimilar
    nat
    Nat.eqb
    (partial_sums_aux (SCons nat n ns') a)
    (partial_sums'_aux ns' (n + a)).
Proof.
  cofix coIH.
  intros n [n' ns''] a.
  rewrite -> fold_unfold_partial_sums_aux.
  rewrite -> fold_unfold_partial_sums'_aux.
  Check (Bisimilar
           nat
           Nat.eqb
           (n + a)
           (n + a)
           (Nat.eqb_refl (n + a))
           (partial_sums_aux (SCons nat n' ns'') (n + a))
           (partial_sums'_aux ns'' (n' + (n + a)))).
  Check (Bisimilar
           nat
           Nat.eqb
           (n + a)
           (n + a)
           (Nat.eqb_refl (n + a))
           (partial_sums_aux (SCons nat n' ns'') (n + a))
           (partial_sums'_aux ns'' (n' + (n + a)))
           (coIH n' ns'' (n + a))).
  exact (Bisimilar
           nat
           Nat.eqb
           (n + a)
           (n + a)
           (Nat.eqb_refl (n + a))
           (partial_sums_aux (SCons nat n' ns'') (n + a))
           (partial_sums'_aux ns'' (n' + (n + a)))
           (coIH n' ns'' (n + a))).
Qed.

Theorem partial_sum_and_partial_sum'_are_equivalent_using_bisimilarity :
  forall ns : stream nat,
    bisimilar nat Nat.eqb (partial_sums ns) (partial_sums' ns).
Proof.
  intros [n ns'].
  unfold partial_sums, partial_sums'.
  rewrite <- (Nat.add_0_r n) at 2.
  exact (about_partial_sums_aux_and_partial_sums'_aux n ns' 0).
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 ones_and_ones''_are_bisimilar :
  bisimilar nat Nat.eqb ones ones''.
Proof.
  unfold ones''.
  unfold partial_sums.
  rewrite -> fold_unfold_partial_sums_aux.
  simpl (1 + 0).
  cofix coIH.
  rewrite -> fold_unfold_ones.
  rewrite -> fold_unfold_zeroes.
  rewrite -> fold_unfold_partial_sums_aux.
  simpl (0 + 1).
  Check (Bisimilar
           nat
           Nat.eqb).
  Check (Bisimilar
           nat
           Nat.eqb
           1
           1
           (Nat.eqb_refl 1)).
    Check (Bisimilar
             nat
             Nat.eqb
             1
             1
             (Nat.eqb_refl 1)
             ones
             (SCons nat 1 (partial_sums_aux zeroes 1))
             coIH).
    exact (Bisimilar
             nat
             Nat.eqb
             1
             1
             (Nat.eqb_refl 1)
             ones
             (SCons nat 1 (partial_sums_aux zeroes 1))
             coIH).
Qed.

(* ***** *)

Theorem ones'_and_ones''_are_bisimilar_by_coinduction :
  bisimilar nat Nat.eqb ones' ones''.
Abort.

Theorem ones'_and_ones''_are_bisimilar_by_coinduction_because_bisimilarity_is_an_equivalence_relation :
  bisimilar nat Nat.eqb ones' ones''.
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 stream_of_successive_positive_numbers_and_stream_of_successive_positive_numbers'_are_bisimilar :
  bisimilar
    nat
    Nat.eqb
    stream_of_successive_positive_numbers
    stream_of_successive_positive_numbers'.
Proof.
  unfold stream_of_successive_positive_numbers, stream_of_successive_positive_numbers'.
  unfold partial_sums.
  cofix coIH.
  rewrite -> fold_unfold_make_stream_of_successive_numbers.
  rewrite -> fold_unfold_ones.
  rewrite -> fold_unfold_partial_sums_aux.
  simpl (1 + 0).
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (make_stream_of_successive_numbers 2) (partial_sums_aux ones 1)).
  apply (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (make_stream_of_successive_numbers 2) (partial_sums_aux ones 1)).
Abort.

(* Using the Light of co-Inductil: *)

Lemma the_same_stream_of_successive_positive_numbers_aux :
  forall a : nat,
    bisimilar nat Nat.eqb (make_stream_of_successive_numbers (S a)) (partial_sums_aux ones a).
Proof.
  Compute (let f a :=
             (stream_prefix nat 5 (make_stream_of_successive_numbers (S a)),
              stream_prefix nat 5 (partial_sums_aux ones a))
           in (f 0, f 1, f 2, f 3)).
  cofix coIH.
  intro a.
  rewrite -> fold_unfold_make_stream_of_successive_numbers.
  rewrite -> fold_unfold_ones.
  rewrite -> fold_unfold_partial_sums_aux.
  rewrite -> (Nat.add_1_l a).
  Check (Bisimilar nat Nat.eqb (S a) (S a) (Nat.eqb_refl (S a)) (make_stream_of_successive_numbers (S (S a))) (partial_sums_aux ones (S a))).
  Check (Bisimilar nat Nat.eqb (S a) (S a) (Nat.eqb_refl (S a)) (make_stream_of_successive_numbers (S (S a))) (partial_sums_aux ones (S a)) (coIH (S a))).
  exact (Bisimilar nat Nat.eqb (S a) (S a) (Nat.eqb_refl (S a)) (make_stream_of_successive_numbers (S (S a))) (partial_sums_aux ones (S a)) (coIH (S a))).
Qed.

Theorem the_same_successive_positive_numbers :
  bisimilar
    nat
    Nat.eqb
    stream_of_successive_positive_numbers
    stream_of_successive_positive_numbers'.
Proof.
  unfold stream_of_successive_positive_numbers, stream_of_successive_positive_numbers'.
  unfold partial_sums.
  exact (the_same_stream_of_successive_positive_numbers_aux 0).
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.

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 stream_of_successive_odd_numbers_and_stream_of_successive_odd_numbers'_are_bisimilar :
  bisimilar nat Nat.eqb stream_of_successive_odd_numbers stream_of_successive_odd_numbers'.
Proof.
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 stream_of_successive_positive_squares_and_stream_of_successive_positive_squares'_are_bisimilar :
  bisimilar
    nat
    Nat.eqb
    stream_of_successive_positive_squares
    stream_of_successive_positive_squares'.
Proof.
  unfold stream_of_successive_positive_squares, stream_of_successive_positive_squares'.
  unfold partial_sums.
  unfold stream_of_successive_odd_numbers.
  cofix coIH.
  rewrite -> fold_unfold_make_stream_of_successive_squares.
  rewrite -> fold_unfold_make_stream_of_successive_numbers_2.
  rewrite -> fold_unfold_partial_sums_aux.
  simpl (1 * 1).
  simpl (1 + 0).
  Check (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (make_stream_of_successive_squares 2) (partial_sums_aux (make_stream_of_successive_numbers_2 3) 1)).
  apply (Bisimilar nat Nat.eqb 1 1 (Nat.eqb_refl 1) (make_stream_of_successive_squares 2) (partial_sums_aux (make_stream_of_successive_numbers_2 3) 1)).
(*  coIH : bisimilar nat Nat.eq (make_stream_of_successive_squares 1)
           (partial_sums_aux (make_stream_of_successive_numbers_2 1) 0)
  ============================
  bisimilar nat Nat.eq (make_stream_of_successive_squares 2)
    (partial_sums_aux (make_stream_of_successive_numbers_2 3) 1)
*)
  rewrite -> fold_unfold_make_stream_of_successive_squares.
  rewrite -> fold_unfold_make_stream_of_successive_numbers_2.
  rewrite -> fold_unfold_partial_sums_aux.
  simpl (2 * 2).
  simpl (3 + 1).
  apply (Bisimilar nat Nat.eqb 4 4 (Nat.eqb_refl 4) (make_stream_of_successive_squares 3) (partial_sums_aux (make_stream_of_successive_numbers_2 5) 4)).
Abort.

Theorem the_same_successive_squares_aux_using_bisimilarity :
  forall n : nat,
    bisimilar
      nat
      Nat.eqb
      (make_stream_of_successive_squares (S n))
      (partial_sums_aux (make_stream_of_successive_odd_numbers n) (n * n)).
Proof.
  Compute (let f n :=
             (stream_prefix nat 5 (make_stream_of_successive_squares (S n)),
              stream_prefix nat 5 (partial_sums_aux (make_stream_of_successive_odd_numbers n) (n * n)))
           in (f 0, f 1, f 2)).
  cofix coIH.
  intro n.
  rewrite -> fold_unfold_make_stream_of_successive_squares.
  rewrite -> fold_unfold_make_stream_of_successive_odd_numbers.
  rewrite -> fold_unfold_partial_sums_aux.
  rewrite <- binomial_expansion_Sn.
  Check (Bisimilar
           nat
           Nat.eqb
           (S n * S n)
           (S n * S n)
           (Nat.eqb_refl (S n * S n))
           (make_stream_of_successive_squares (S (S n)))
           (partial_sums_aux (make_stream_of_successive_odd_numbers (S n)) (S n * S n))).
  Check (Bisimilar
           nat
           Nat.eqb
           (S n * S n)
           (S n * S n)
           (Nat.eqb_refl (S n * S n))
           (make_stream_of_successive_squares (S (S n)))
           (partial_sums_aux (make_stream_of_successive_odd_numbers (S n)) (S n * S n))
           (coIH (S n))).
  exact (Bisimilar
           nat
           Nat.eqb
           (S n * S n)
           (S n * S n)
           (Nat.eqb_refl (S n * S n))
           (make_stream_of_successive_squares (S (S n)))
           (partial_sums_aux (make_stream_of_successive_odd_numbers (S n)) (S n * S n))
           (coIH (S n))).
Qed.

Theorem stream_of_successive_positive_squares_and_stream_of_successive_positive_squares'_are_bisimilar :
  bisimilar
    nat
    Nat.eqb
    stream_of_successive_positive_squares
    stream_of_successive_positive_squares'.
Proof.
  unfold stream_of_successive_positive_squares, stream_of_successive_positive_squares'.
  unfold partial_sums.
  Check (the_same_successive_squares_aux_using_bisimilarity 0).
Abort.
(*
  unfold 
  rewrite <- (Nat.add_0_l 0) at 2.
  
  exact (the_same_successive_squares_aux_using_bisimilarity 0).
Qed.
*)
(* ********** *)

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_bisimilarity :
  forall (V : Type)
         (eqb_V : V -> V -> bool),
    (forall v : V,
        eqb_V v v = true) ->
    forall v1s v2s : stream V,
      bisimilar V eqb_V (stream_append V v1s v2s) (stream_append_simpler V v1s v2s).
Proof.
  unfold stream_append_simpler.
  intros V eqb_V eqb_V_refl v1s v2s.
  revert v1s.
  cofix coIH.
  intros [v1 v1s'].
  rewrite -> fold_unfold_stream_append.
  Check (Bisimilar V eqb_V v1 v1 (eqb_V_refl v1) (stream_append V v1s' v2s) v1s').
  Check (Bisimilar V eqb_V v1 v1 (eqb_V_refl v1) (stream_append V v1s' v2s) v1s' (coIH v1s')).
  exact (Bisimilar V eqb_V v1 v1 (eqb_V_refl v1) (stream_append V v1s' v2s) v1s' (coIH 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_bisimilarity :
  forall (X : Type)
         (Y : Type)
         (Z : Type)
         (eqb_Z : Z -> Z -> bool),
    (forall z : Z,
        eqb_Z z z = true) ->
    forall (g : X -> Y)
           (f : Y -> Z)
           (xs : stream X),
      bisimilar Z
                eqb_Z
                (stream_map Y Z f (stream_map X Y g xs))
                (stream_map X Z (fun x => f (g x)) xs).
Proof.
  Compute (let X := nat in
           let Y := nat in
           let Z := nat in
           let eqb_Z := Nat.eqb in
           let g x := 2 * x in
           let f y := S y in
           let xs := make_stream_of_successive_numbers 0 in
           (stream_prefix nat 5 (stream_map Y Z f (stream_map X Y g xs)),
            stream_prefix nat 5 (stream_map X Z (fun x => f (g x)) xs))).
Proof.
Abort.

(* ***** *)

(* does stream_map preserve bisimilarity? *)

Theorem stream_map_preserves_bisimilarity :
  forall (X : Type)
         (eqb_X : X -> X -> bool)
         (Y : Type)
         (eqb_Y : Y -> Y -> bool),
    (forall y : Y,
        eqb_Y y y = true) ->
    forall f : X -> Y,
      (forall x1 x2 : X,
          eqb_X x1 x2 = true ->
          eqb_Y (f x1) (f x2) = true) ->
      forall x1s x2s : stream X,
        bisimilar X eq_X x1s x2s ->
        bisimilar Y eq_Y (stream_map X Y f x1s) (stream_map X Y f x2s).
Proof.
Abort.

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

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