Built with Alectryon, running Coq+SerAPI v8.18.0+0.18.3. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On Mac, use ⌘ instead of Ctrl.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Unset Elimination Schemes.(** * Lists *)(** ** Definition *)Declare Scope list_scope.LocalOpen 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. *)Inductivelist@{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.Schemelist_rect := Induction for list SortType.Schemelist_ind := Induction for list SortType.Schemelist_rec := Minimality for list SortType.(** 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. *)Fixpointlength {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] ]. *)Definitionapp {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]]. *)Fixpointfold_left {AB} (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]]. *)Fixpointfold_right {AB} (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] ]. *)Fixpointmap {AB} (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. *)Fixpointmap2 {ABC} (f : A -> B -> C)
(def_l : list A -> list C) (def_r : list B -> list C)
l1l2 :=
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. *)Fixpointreverse_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] ]. *)Definitionreverse {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. *)Definitionhead {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. *)Definitiontail {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. *)Fixpointlast {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. *)Fixpointnth {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. *)Fixpointremove_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]. *)Fixpointseq_rev (n : nat) : list nat :=
match n with
| O => nil
| S n => n :: seq_rev n
end.(** Ascending sequence of natural numbers [< n]. *)Definitionseq (n : nat) : list nat := reverse (seq_rev n).(** ** Membership Predicate *)(** The "In list" predicate *)FixpointInList {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. *)Fixpointfor_all {A} (P : A -> Type) l : Type :=
match l with
| nil => Unit
| x :: l => P x /\ for_all P l
end.