Require Import Basics.Overture.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Local Unset Elimination Schemes.
Local Set Universe Minimization ToSet.
Local Set Polymorphic Inductive Cumulativity.

(** * Lists *)

(** ** Definition *)

Declare Scope list_scope.
Local Open Scope list_scope.

(** A list is a sequence of elements from a type [A]. This is a very useful datatype and has many applications ranging from programming to algebra. It can be thought of a free monoid. *)
Inductive list@{i|} (A : Type@{i}) : Type@{i} :=
| nil : list A
| cons : A -> list A -> list A.

Arguments nil {A}.
Arguments cons {A} _ _.

Delimit Scope list_scope with list.
Bind Scope list_scope with list.

(** This messes with Coq's parsing of [] in Ltac. Therefore we keep it commented out. It's not difficult to write [nil] instead. *)
(* Notation "[]" := nil : list_scope. *)
Infix "::" := cons : list_scope.

Scheme list_rect := Induction for list Sort Type.
Scheme list_ind := Induction for list Sort Type.
Scheme list_rec := Minimality for list Sort Type.

(** A tactic for doing induction over a list that avoids spurious universes. *)
Ltac simple_list_induction l h t IH :=
  try generalize dependent l;
  fix IH 1;
  intros [| h t];
  [ clear IH | specialize (IH t) ].

(** Syntactic sugar for creating lists. [ [a1, b2, ..., an] = a1 :: b2 :: ... :: an :: nil ]. *)
Notation "[ x ]" := (x :: nil) : list_scope.
Notation "[ x , y , .. , z ]" := (x :: (y :: .. (z :: nil) ..)) : list_scope.

(** ** Length *)

(** Notice that the definition of a list looks very similar to the definition of [nat]. It is as if each [S] constructor from [nat] has an element of [A] attached to it. We can discard this extra element and get a list invariant that we call [length]. *)

(** The length (number of elements) of a list. *)
Fixpoint length {A : Type} (l : list A) :=
  match l with
  | nil => O
  | _ :: l => S (length l)
  end.

(** ** Concatenation *)

(** Given two lists [ [a1; a2; ...; an] ] and [ [b1; b2; ...; bm] ], we can concatenate them to get [ [a1; a2; ...; an; b1; b2; ...; bm] ]. *)
Definition app {A : Type} : list A -> list A -> list A :=
  fix app l m :=
  match l with
   | nil => m
   | a :: l1 => a :: app l1 m
  end.

Infix "++" := app : list_scope.

(** ** Folding *)

(** Folding is a very important operation on lists. It is a way to reduce a list to a single value. The [fold_left] function starts from the left and the [fold_right] function starts from the right. *)

(** [fold_left f l a0] computes [f (... (f (f a0 x1) x2) ...) xn] where [l = [x1; x2; ...; xn]]. *)
Fixpoint fold_left {A B} (f : A -> B -> A) (l : list B) (default : A) : A :=
  match l with
    | nil => default
    | cons b l => fold_left f l (f default b)
  end.

(** [fold_right f a0 l] computes [f x1 (f x2 ... (f xn a0) ...)] where [l = [x1; x2; ...; xn]]. *)
Fixpoint fold_right {A B} (f : B -> A -> A) (default : A) (l : list B) : A :=
  match l with
    | nil => default
    | cons b l => f b (fold_right f default l)
  end.

(** ** Maps - Functoriality of Lists *)

(** The [list_map] function applies a function to each element of a list. In other words [ list_map f [a1; a2; ...; an] = [f a1; f a2; ...; f an] ]. *)
Fixpoint list_map {A B : Type} (f : A -> B) (l : list A) :=
  match l with
  | nil => nil
  | x :: l => (f x) :: (list_map f l)
  end.

(** The [list_map2] function applies a binary function to corresponding elements of two lists. When one of the lists run out, it uses one of the default functions to fill in the rest. *)
Fixpoint list_map2 {A B C : Type} (f : A -> B -> C)
  (def_l : list A -> list C) (def_r : list B -> list C) l1 l2 :=
  match l1, l2 with
  | nil, nil => nil
  | nil, _ => def_r l2
  | _, nil => def_l l1
  | x :: l1, y :: l2 => (f x y) :: (list_map2 f def_l def_r l1 l2)
  end.

(** ** Reversal *)

(** Tail-recursive list reversal. *)
Fixpoint reverse_acc {A : Type} (acc : list A) (l : list A) : list A :=
  match l with
  | nil => acc
  | x :: l => reverse_acc (x :: acc) l
  end.

(** Reversing the order of a list. The list [ [a1; a2; ...; an] ] becomes [ [an; ...; a2; a1] ]. *)
Definition reverse {A : Type} (l : list A) : list A := reverse_acc nil l.

(** ** Getting Elements *)

(** The head of a list is its first element. Returns [None] If the list is empty. *)
Definition head {A : Type} (l : list A) : option A :=
  match l with
  | nil => None
  | a :: _ => Some a
  end.

(** The tail of a list is the list without its first element. *)
Definition tail {A : Type} (l : list A) : list A :=
  match l with
    | nil => nil
    | a :: m => m
  end.

(** The last element of a list. If the list is empty, it returns [None]. *)
Fixpoint last {A : Type} (l : list A) : option A :=
  match l with
  | nil => None
  | a :: nil => Some a
  | _ :: l => last l
  end.

(** The [n]-th element of a list. If the list is too short, it returns [None]. *)
Fixpoint nth {A : Type} (l : list A) (n : nat) : option A :=
  match n, l with
  | O, x :: _ => Some x
  | S n, _ :: l => nth l n
  | _, _ => None
  end.

(** ** Removing Elements *)

(** Remove the last element of a list and do nothing if it is empty. *)
Fixpoint remove_last {A : Type} (l : list A) : list A :=
  match l with
  | nil => nil
  | _ :: nil => nil
  | x :: l => x :: remove_last l
  end.

(** ** Sequences *)

(** Descending sequence of natural numbers starting from [n.-1] to [0]. *)
Fixpoint seq_rev (n : nat) : list nat :=
    match n with
    | O => nil
    | S n => n :: seq_rev n
    end.

(** Ascending sequence of natural numbers [< n]. *)
Definition seq (n : nat) : list nat := reverse (seq_rev n).

(** ** Repeat *)

(** Repeat an element [n] times. *)
Fixpoint repeat {A : Type} (x : A) (n : nat) : list A :=
  match n with
  | O => nil
  | S n => x :: repeat x n
  end.

(** ** Membership Predicate *)

(** The "In list" predicate *)
Fixpoint InList@{i|} {A : Type@{i}} (a : A) (l : list A) : Type@{i} :=
  match l with
    | nil => Empty
    | b :: m => (b = a) + InList a m
  end.

(** ** Forall *)

(** Apply a predicate to all elements of a list and take their conjunction. *)
Fixpoint for_all@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
  match l with
  | nil => Unit
  | x :: l => P x /\ for_all P l
  end.

(** ** Exists *)

(** Apply a predicate to all elements of a list and take their disjunction. *)
Fixpoint list_exists@{i j|} {A : Type@{i}} (P : A -> Type@{j}) l : Type@{j} :=
  match l with
  | nil => Empty
  | x :: l => P x + list_exists P l
  end.