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

Unset Elimination Schemes.

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

(** Syntactic sugar for creating lists. [ [a1; b2; ...; an] = a1 :: b2 :: ... :: an :: nil ]. *)
Notation "[ x ]" := (x :: nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons 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} (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) (a0 : A) : A :=
  match l with
    | nil => a0
    | cons b l => fold_left f l (f a0 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 *)

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

(** The [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 map2 {A B C} (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) :: (map2 f def_l def_r l1 l2)
  end.

(** ** Reversal *)

(** Tail-recursive list reversal. *)
Fixpoint reverse_acc {A} (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} (l : list A) : list A := reverse_acc nil l.

(** ** Getting Elements *)

(** The head of a list is its first element. If the list is empty, it returns the default value. *)
Definition head {A} (default : A) (l : list A) : A :=
  match l with
  | nil => default
  | a :: _ => a
  end.

(** The tail of a list is the list without its first element. *)
Definition tail {A} (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 the default value. *)
Fixpoint last {A} (default : A) (l : list A) : A :=
  match l with
  | nil => default
  | _ :: l => last default l
  end.

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

(** ** Removing Elements *)

(** Remove the last element of a list and do nothing if it is empty. *)
Fixpoint remove_last {A} (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).

(** ** Membership Predicate *)

(** The "In list" predicate *)
Fixpoint InList {A} (a : A) (l : list A) : Type0 :=
  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 {A} (P : A -> Type) l : Type :=
  match l with
  | nil => Unit
  | x :: l => P x /\ for_all P l
  end.