(* week-12_reasoning-about-lazy-lists-using-coinduction.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 10 Apr 2025 *)

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

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

Require Import Arith Bool List.

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

CoInductive lazy_list (V : Type) : Type :=
  LNil : lazy_list V
| LCons : V -> lazy_list V -> lazy_list V.

CoInductive bisimilar : forall (V : Type), (V -> V -> bool) -> lazy_list V -> lazy_list V -> Prop :=
| Bisimilar_LNil :
    forall (V : Type)
           (eqb_V : V -> V -> bool),
      bisimilar V eqb_V (LNil V) (LNil V)
| Bisimilar_LCons :
    forall (V : Type)
           (eqb_V : V -> V -> bool)
           (v1 v2 : V),
      eqb_V v1 v2 = true ->
      forall v1s v2s : lazy_list V,
        bisimilar V eqb_V v1s v2s ->
        bisimilar V eqb_V (LCons V v1 v1s) (LCons V v2 v2s).

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

(* Reasoning with lazy lists: *)

Definition lazy_list_decompose (V : Type) (vs : lazy_list V) :=
  match vs with
    LNil _ =>
    LNil V
  | LCons _ v vs' =>
    LCons V v vs'
  end.

Theorem lazy_list_decomposition :
  forall (V : Type)
         (vs : lazy_list V),
    vs = lazy_list_decompose V vs.
Proof.
  intros V [ | v vs']; unfold lazy_list_decompose; reflexivity.
Qed.

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

Lemma bisimilar_is_reflexive :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (vs : lazy_list V),
    bisimilar V eqb_V vs vs.
Proof.
Abort.

Lemma bisimilar_is_symmetric :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    bisimilar V eqb_V xs ys ->
    bisimilar V eqb_V ys xs.
Proof.
Abort.

Lemma converse_of_bisimilar_LCons :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (x y : V)
         (xs' ys' : lazy_list V),
    bisimilar V eqb_V (LCons V x xs') (LCons V y ys') ->
    eqb_V x y = true /\ bisimilar V eqb_V xs' ys'.
Proof.
  intros V eqb_V x y xs' ys' BS.
  remember (LCons V x xs') as xs eqn:H_xs.
  remember (LCons V y ys') as ys eqn:H_ys.
  case BS as [V' eqb_V' | V' eqb_V' x' y' H_x'_y' xs'' ys'' H_xs''_ys''].
  - discriminate H_xs.
  - injection H_xs as H_xs''_xs' H_x'_x.
    injection H_ys as H_ys''_ys' H_y'_y.
    rewrite <- H_x'_x.
    rewrite <- H_y'_y.
    rewrite <- H_xs''_xs'.
    rewrite <- H_ys''_ys'.
    split; [exact H_x'_y' | exact H_xs''_ys''].
Qed.

Lemma bisimilar_is_transitive :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys zs : lazy_list V),
    bisimilar V eqb_V xs ys ->
    bisimilar V eqb_V ys zs ->
    bisimilar V eqb_V xs zs.
Proof.
Abort.

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

(* "prefix m ns" maps the stream ns into the list of its m first elements *)

Fixpoint prefix (V : Type) (n : nat) (vs : lazy_list V) : list V :=
  match n with
  | 0 =>
    nil
  | S n' =>
    match vs with
    | LNil _ => 
      nil
    | LCons _ v vs' =>
      v :: (prefix V n' vs')
    end
  end.

Lemma fold_unfold_prefix_0 :
  forall (V : Type)
         (vs : lazy_list V),
    prefix V 0 vs =
    nil.
Proof.
  fold_unfold_tactic prefix.
Qed.

Lemma fold_unfold_prefix_S :
  forall (V : Type)
         (n' : nat)
         (vs : lazy_list V),
    prefix V (S n') vs =
    match vs with
    | LNil _ =>
      nil
    | LCons _ v vs' =>
      v :: (prefix V n' vs')
    end.
Proof.
  fold_unfold_tactic prefix.
Qed.

Lemma fold_unfold_prefix_S_Nil :
  forall (V : Type)
         (n' : nat),
    prefix V (S n') (LNil V) =
    nil.
Proof.
  fold_unfold_tactic prefix.
Qed.

Lemma fold_unfold_prefix_S_Cons :
  forall (V : Type)
         (n' : nat)
         (v : V)
         (vs' : lazy_list V),
    prefix V (S n') (LCons V v vs') =
    v :: (prefix V n' vs').
Proof.
  fold_unfold_tactic prefix.
Qed.

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

(* "partial_sums ns" maps a lazy list of natural numbers to the lazy list of its partial sums *)

CoFixpoint partial_sums_aux (a : nat) (ns : lazy_list nat) : lazy_list nat :=
  match ns with
  | LNil _ =>
    LNil nat
  | LCons _ n ns' =>
    LCons nat (n + a) (partial_sums_aux (n + a) ns')
  end.

Lemma fold_unfold_partial_sums_aux_LNil :
  forall (a : nat),
    partial_sums_aux a (LNil nat) =
    LNil nat.
Proof.
  intro a.
  rewrite -> (lazy_list_decomposition
                nat
                (partial_sums_aux a (LNil nat))).
  reflexivity.
Qed.

Lemma fold_unfold_partial_sums_aux_LCons :
  forall (a n : nat)
         (ns' : lazy_list nat),
    partial_sums_aux a (LCons nat n ns') =
    LCons nat (n + a) (partial_sums_aux (n + a) ns').
Proof.
  intros a n ns'.
  rewrite -> (lazy_list_decomposition
                nat
                (partial_sums_aux a (LCons nat n ns'))).
  reflexivity.
Qed.

Definition partial_sums ns :=
  partial_sums_aux 0 ns.

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

CoFixpoint copy (V : Type) (vs : lazy_list V) :=
  match vs with
  | LNil _ =>
    LNil V
  | LCons _ v vs' =>
    LCons V v (copy V vs')
  end.

Lemma fold_unfold_copy_LNil :
  forall V : Type,
    copy V (LNil V) = LNil V.
Proof.
  intro V.
  rewrite -> (lazy_list_decomposition V (copy V (LNil V))).
  reflexivity.
Qed.

Lemma fold_unfold_copy_LCons :
  forall (V : Type)
         (v : V)
         (vs' : lazy_list V),
    copy V (LCons V v vs') = LCons V v (copy V vs').
Proof.
  intros V v vs'.
  rewrite -> (lazy_list_decomposition V (copy V (LCons V v vs'))).
  reflexivity.
Qed.

Theorem the_thing_about_copy :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (vs : lazy_list V),
    bisimilar V eqb_V vs (copy V vs).
Proof.
Abort.

Theorem copy_preserves_bisimilarity :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    bisimilar V eqb_V xs ys ->
    bisimilar V eqb_V (copy V xs) (copy V ys).
Proof.
Abort.

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

CoFixpoint lazy_list_append (V : Type) (xs ys : lazy_list V) : lazy_list V :=
  match xs with
  | LNil _ =>
    ys
  | LCons _ x xs' =>
    LCons V x (lazy_list_append V xs' ys)
  end.

Lemma fold_unfold_lazy_list_append_LNil :
  forall (V : Type)
         (ys : lazy_list V),
    lazy_list_append V (LNil V) ys =
    ys.
Proof.
  intros V ys.
  rewrite (lazy_list_decomposition V (lazy_list_append V (LNil V) ys)).
  case ys as [ | y ys']; reflexivity.
Qed.

Lemma fold_unfold_lazy_list_append_Cons :
  forall (V : Type)
         (x : V)
         (xs' ys : lazy_list V),
    lazy_list_append V (LCons V x xs') ys =
    LCons V x (lazy_list_append V xs' ys).
Proof.
  intros V x xs' ys.
  rewrite (lazy_list_decomposition V (lazy_list_append V (LCons V x xs') ys)).
  reflexivity.
Qed.

Lemma Nil_is_neutral_for_lazy_list_append_on_the_left :
  forall (V: Type)
         (eqb_V : V -> V -> bool)
         (ys : lazy_list V),
    bisimilar V eqb_V (lazy_list_append V (LNil V) ys) ys.
Proof.
Abort.

Lemma Nil_is_neutral_for_lazy_list_append_on_the_right :
  forall (V: Type)
         (eqb_V : V -> V -> bool)
         (xs : lazy_list V),
    bisimilar V eqb_V (lazy_list_append V xs (LNil V)) xs.
Proof.
Abort.

Lemma lazy_list_append_is_associative :
  forall (V: Type)
         (eqb_V : V -> V -> bool)
         (xs ys zs : lazy_list V),
    bisimilar
      V
      eqb_V
      (lazy_list_append V xs (lazy_list_append V ys zs))
      (lazy_list_append V (lazy_list_append V xs ys) zs).
Proof.
Abort.

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

CoFixpoint lazy_list_map (V W : Type) (f : V -> W) (vs : lazy_list V) : lazy_list W :=
  match vs with
  | LNil _ =>
    LNil W
  | LCons _ v vs' =>
    LCons W (f v) (lazy_list_map V W f vs')
  end.

Lemma fold_unfold_lazy_list_map_LNil :
  forall (V W : Type)
         (f : V -> W),
    lazy_list_map V W f (LNil V) =
    LNil W.
Proof.
  intros V W f.
  rewrite (lazy_list_decomposition W (lazy_list_map V W f (LNil V))).
  reflexivity.
Qed.

Lemma fold_unfold_lazy_list_map_LCons :
  forall (V W : Type)
         (f : V -> W)
         (v : V)
         (vs' : lazy_list V),
    lazy_list_map V W f (LCons V v vs') =
    LCons W (f v) (lazy_list_map V W f vs').
Proof.
  intros V W f v vs'.
  rewrite (lazy_list_decomposition W (lazy_list_map V W f (LCons V v vs'))).
  reflexivity.
Qed.

(* Does lazy_list_map distribute over lazy_list_append? *)

Proposition lazy_list_append_preserves_lazy_list_map :
  forall (V W : Type)
         (eqb_W : W -> W -> bool)
         (f : V -> W)
         (xs ys : lazy_list V),
    bisimilar
      W
      eqb_W
      (lazy_list_map V W f (lazy_list_append V xs ys))
      (lazy_list_append W (lazy_list_map V W f xs) (lazy_list_map V W f ys)).
Proof.
Abort.

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

(* "index_lazy_list n vs" indexes the lazy list vs at index n *)

Fixpoint lazy_list_index (V : Type) (n : nat) (vs : lazy_list V) : option V :=
  match n with
  | 0 =>
    match vs with
    | LNil _ =>
      None
    | LCons _ v vs' =>
      Some v
    end
  | S n' =>
    match vs with
    | LNil _ =>
      None
    | LCons _ v vs' =>
      lazy_list_index V n' vs'
    end
  end.

Lemma fold_unfold_lazy_list_index_O :
  forall (V : Type)
         (vs : lazy_list V),
    lazy_list_index V 0 vs =
    match vs with
      | LNil _ =>
        None
      | LCons _ v vs' =>
        Some v
    end.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

Lemma fold_unfold_lazy_list_index_O_LNil :
  forall (V : Type)
         (vs : lazy_list V),
    lazy_list_index V 0 (LNil V) =
    None.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

Lemma fold_unfold_lazy_list_index_O_LCons :
  forall (V : Type)
         (v : V)
         (vs' : lazy_list V),
    lazy_list_index V 0 (LCons V v vs') =
    Some v.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

Lemma fold_unfold_lazy_list_index_S :
  forall (V : Type)
         (n' : nat)
         (vs : lazy_list V),
    lazy_list_index V (S n') vs =
    match vs with
    | LNil _ =>
      None
    | LCons _ v vs' =>
      lazy_list_index V n' vs'
    end.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

Lemma fold_unfold_lazy_list_index_S_LNil :
  forall (V : Type)
         (n' : nat),
    lazy_list_index V (S n') (LNil V) =
    None.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

Lemma fold_unfold_lazy_list_index_S_LCons :
  forall (V : Type)
         (n' : nat)
         (v : V)
         (vs' : lazy_list V),
    lazy_list_index V (S n') (LCons V v vs') =
    lazy_list_index V n' vs'.
Proof.
  fold_unfold_tactic lazy_list_index.
Qed.

(* ***** *)

(* Reminder: I denotes True in Coq,
   so proving True is achieved by "exact I."
*)

Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
  match ov1 with
  | Some v1 =>
    match ov2 with
    | Some v2 =>
      eqb_V v1 v2
    | None =>
      false
    end
  | None =>
    match ov2 with
    | Some v2 =>
      false
    | None =>
      true
    end
  end.

Theorem same_indexed_elements_implies_bisimilar :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    (forall n : nat,
       eqb_option V eqb_V (lazy_list_index V n xs) (lazy_list_index V n ys) = true) ->
    bisimilar V eqb_V xs ys.
Proof.
Abort.

Theorem bisimilar_implies_same_indexed_elements :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    bisimilar V eqb_V xs ys ->
    forall n : nat,
      eqb_option V eqb_V (lazy_list_index V n xs) (lazy_list_index V n ys) = true.
Proof.
Abort.

(* ***** *)

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.

Theorem bisimilar_implies_same_prefixes :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    bisimilar V eqb_V xs ys ->
    forall n : nat,
      eqb_list V eqb_V (prefix V n xs) (prefix V n ys) = true.
Proof.
Abort.

Theorem same_prefixes_implies_bisimilar :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    (forall n : nat,
       eqb_list V eqb_V (prefix V n xs) (prefix V n ys) = true) ->
    bisimilar V eqb_V xs ys.
Proof.
Abort.

(* ***** *)

Theorem same_prefixes_implies_same_indexed_elements :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    (forall n : nat,
        eqb_list V eqb_V (prefix V n xs) (prefix V n ys) = true) ->
    forall n : nat,
      eqb_option V eqb_V (lazy_list_index V n xs) (lazy_list_index V n ys) = true.
Proof.
Abort.

Theorem same_indexed_elements_implies_same_prefixes :
  forall (V : Type)
         (eqb_V : V -> V -> bool)
         (xs ys : lazy_list V),
    (forall n : nat,
        eqb_option V eqb_V (lazy_list_index V n xs) (lazy_list_index V n ys) = true) ->
    forall n : nat,
      eqb_list V eqb_V (prefix V n xs) (prefix V n ys) = true.
Proof.
Abort.

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

(* end of week-12_reasoning-about-lazy-lists-using-coinduction.v *)