(* week-09_in-the-wake-of-the-midterm-project.v *)
(* was: midterm-project.v *)
(* LPP 2025 - CS3234 2024-2025, Sem2 *)
(* Olivier Danvy <olivier@comp.nus.edu.sg> *)
(* Version of 22 Mar 2025 *)

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

(* A sketchy study of polymorphic lists. *)

(* members of the group:
   date: 
*)

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

(* Paraphernalia: *)

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

Require Import Arith Bool List.

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

(* Task 1 (about eqb_list) is omitted. *)

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

(* Task 2 (about list_length and list_length_alt) is omitted. *)

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

(* Task 3 (about list_copy) is omitted. *)

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

(* Task 4 (about list_append) is omitted. *)

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

(* Task 5 (about list_reverse) is omitted. *)

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

(* Task 6 (about list_map): *)

Definition specification_of_list_map (map : forall V W : Type, (V -> W) -> list V -> list W) :=
  (forall (V W : Type)
          (f : V -> W),
      map V W f nil = nil)
  /\
  (forall (V W : Type)
          (f : V -> W)
          (v : V)
          (vs' : list V),
      map V W f (v :: vs') = f v :: map V W f vs').

(* Exercise 01 *)

(* Prove the following property: *)

Property a_sketchy_characterization_of_list_map :
  forall list_map : forall V W : Type, (V -> W) -> list V -> list W,
    specification_of_list_map list_map ->
    forall (V W : Type)
           (f : V -> W),
      (list_map V W f nil = nil)
      /\
      (forall v3 : V,
          list_map V W f (v3 :: nil) = f v3 :: nil)
      /\
      (forall v2 v3 : V,
          list_map V W f (v2 :: v3 :: nil) = f v2 :: f v3 :: nil)
      /\
      (forall v1 v2 v3 : V,
          list_map V W f (v1 :: v2 :: v3 :: nil) = f v1 :: f v2 :: f v3 :: nil).
Proof.
Admitted.

Fixpoint list_map (V W : Type) (f : V -> W) (vs : list V) : list W :=
  match vs with
    nil =>
    nil
  | v :: vs' =>
    f v :: list_map V W f vs'
  end.

Proposition list_map_satisfies_the_specification_of_list_map :
  specification_of_list_map list_map.
Proof.
Admitted.

(* Exercise 02 *)

(* a. Characterize the following computation: *)

Check (a_sketchy_characterization_of_list_map
         list_map
         list_map_satisfies_the_specification_of_list_map
         nat
         nat
         (fun n : nat => n)).

(* b. Characterize the following computation: *)

Check (a_sketchy_characterization_of_list_map
         list_map
         list_map_satisfies_the_specification_of_list_map
         nat
         nat
         (fun n : nat => S n)).

(* c. Characterize the following computation: *)

Check (fun (V : Type) =>
         a_sketchy_characterization_of_list_map
           list_map
           list_map_satisfies_the_specification_of_list_map
           V
           V
           (fun v : V => v)).

(* d. Characterize the following computation: *)

Check (fun (V : Type) =>
         a_sketchy_characterization_of_list_map
           list_map
           list_map_satisfies_the_specification_of_list_map
           V
           (list V)
           (fun v : V => v :: nil)).

(* e. Characterize the following computation: *)

Check (fun (V : Type) =>
         a_sketchy_characterization_of_list_map
           list_map
           list_map_satisfies_the_specification_of_list_map
           V
           (V * V)
           (fun v : V => (v, v))).

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

(* Task 7 (about list_fold_right and list_fold_left): *)

(* ***** *)

Definition specification_of_list_fold_right (fold_right : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
  (forall (V W : Type)
          (nil_case : W)
          (cons_case : V -> W -> W),
     fold_right V W nil_case cons_case nil =
     nil_case)
  /\
  (forall (V W : Type)
          (nil_case : W)
          (cons_case : V -> W -> W)
          (v : V)
          (vs' : list V),
     fold_right V W nil_case cons_case (v :: vs') =
     cons_case v (fold_right V W nil_case cons_case vs')).

(* Exercise 03 *)

(* Prove the following property: *)

Property a_sketchy_characterization_of_list_fold_right :
  forall list_fold_right : forall V W : Type, W -> (V -> W -> W) -> list V -> W,
    specification_of_list_fold_right list_fold_right ->
    forall (V W : Type)
           (n : W)
           (c : V -> W -> W),
      (list_fold_right V W n c nil = n)
      /\
      (forall v3 : V,
          list_fold_right V W n c (v3 :: nil) = c v3 n)
      /\
      (forall v2 v3 : V,
          list_fold_right V W n c (v2 :: v3 :: nil) = c v2 (c v3 n))
      /\
      (forall v1 v2 v3 : V,
          list_fold_right V W n c (v1 :: v2 :: v3 :: nil) = c v1 (c v2 (c v3 n))).
Proof.
Admitted.

Fixpoint list_fold_right (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
  match vs with
    nil =>
    nil_case
  | v :: vs' =>
    cons_case v (list_fold_right V W nil_case cons_case vs')
  end.

Proposition list_fold_right_satisfies_the_specification_of_list_fold_right :
  specification_of_list_fold_right list_fold_right.
Proof.
Admitted.

(* Exercise 04 *)

(* a. Characterize the following computation: *)

Check (fun (V : Type) =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           nat
           0
           (fun (v : V) (ih : nat) => S ih)).

(* b. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (list V)
           nil
           (fun (v : V) (ih : list V) => v :: ih)).

(* c. Characterize the following computation: *)

Check (fun (V : Type)
           (v2s : list V) =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (list V)
           v2s
           (fun (v : V) (ih : list V) => v :: ih)).

(* d. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (list (list V))
           nil
           (fun (v : V) (ih : list (list V)) => (v :: nil) :: ih)).

(* e. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (list (V * V))
           nil
           (fun (v : V) (ih : list (V * V)) => (v, v) :: ih)).

(* f. Characterize the following computation: *)

Check (fun (V W : Type)
           (cons_case : V -> W -> W) =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (W -> W)
           (fun w : W => w)
           (fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w))).

(* ***** *)

Definition specification_of_list_fold_left (fold_left : forall V W : Type, W -> (V -> W -> W) -> list V -> W) :=
  (forall (V W : Type)
          (nil_case : W)
          (cons_case : V -> W -> W),
     fold_left V W nil_case cons_case nil =
     nil_case)
  /\
  (forall (V W : Type)
          (nil_case : W)
          (cons_case : V -> W -> W)
          (v : V)
          (vs' : list V),
     fold_left V W nil_case cons_case (v :: vs') =
     fold_left V W (cons_case v nil_case) cons_case vs').

(* Exercise 05 *)

(* Prove the following property: *)

Property a_sketchy_characterization_of_list_fold_left :
  forall list_fold_left : forall V W : Type, W -> (V -> W -> W) -> list V -> W,
    specification_of_list_fold_left list_fold_left ->
    forall (V W : Type)
           (n : W)
           (c : V -> W -> W),
      (list_fold_left V W n c nil = n)
      /\
      (forall v3 : V,
          list_fold_left V W n c (v3 :: nil) = c v3 n)
      /\
      (forall v2 v3 : V,
          list_fold_left V W n c (v2 :: v3 :: nil) = c v3 (c v2 n))
      /\
      (forall v1 v2 v3 : V,
          list_fold_left V W n c (v1 :: v2 :: v3 :: nil) = c v3 (c v2 (c v1 n))).
Proof.
Admitted.

(* ***** *)

Fixpoint list_fold_left (V W : Type) (nil_case : W) (cons_case : V -> W -> W) (vs : list V) : W :=
  match vs with
    nil =>
    nil_case
  | v :: vs' =>
    list_fold_left V W (cons_case v nil_case) cons_case vs'
  end.

Proposition list_fold_left_satisfies_the_specification_of_list_fold_left :
  specification_of_list_fold_left list_fold_left.
Proof.
Admitted.

(* Exercise 06 *)

(* a. Characterize the following computation: *)

Check (fun (V : Type) =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           nat
           0
           (fun (v : V) (ih : nat) => S ih)).

(* b. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (list V)
           nil
           (fun (v : V) (ih : list V) => v :: ih)).

(* c. Characterize the following computation: *)

Check (fun (V : Type)
           (v2s : list V) =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (list V)
           v2s
           (fun (v : V) (ih : list V) => v :: ih)).

(* d. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (list (list V))
           nil
           (fun (v : V) (ih : list (list V)) => (v :: nil) :: ih)).

(* e. Characterize the following computation: *)

Check (fun V : Type =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (list (V * V))
           nil
           (fun (v : V) (ih : list (V * V)) => (v, v) :: ih)).

(* f. Characterize the following computation: *)

Check (fun (V W : Type)
           (cons_case : V -> W -> W) =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (W -> W)
           (fun w : W => w)
           (fun (v : V) (ih : W -> W) (w : W) => ih (cons_case v w))).

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

(* Postlude *)

Check (fun (V W : Type)
           (cons_case : V -> W -> W) =>
         a_sketchy_characterization_of_list_fold_right
           list_fold_right
           list_fold_right_satisfies_the_specification_of_list_fold_right
           V
           (W -> W)
           (fun w : W => w)
           (fun (v : V) (ih : W -> W) (w : W) => cons_case v (ih w))).

Check (fun (V W : Type)
           (cons_case : V -> W -> W) =>
         a_sketchy_characterization_of_list_fold_left
           list_fold_left
           list_fold_left_satisfies_the_specification_of_list_fold_left
           V
           (W -> W)
           (fun w : W => w)
           (fun (v : V) (ih : W -> W) (w : W) => cons_case v (ih w))).

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

(* end of week-09_in-the-wake-of-the-midterm-project.v *)