Library Lists


Lists
Section Lists.

Lists are the ubiqitous datastructure in functional programming, as you should know from Haskell. Given a set A we define list A to be the set of finite sequences of elements of A. E.g. the sequence [1,2,3] is an element of list nat. We can iterate this process and construct lists of lists, e.g. [[1,2],[3]] is an element of list (list nat). However lists are uniform, that is all elements need to have the same type so we cannot form a list like [1,true] or [[1,2],3].

We are going to formally introduce lists using an inductive definition which has a lot in common with the definition of the natural numbers in the previous chapter. And indeed the theory of lists has a lot in common with the theory of the natural number, so we can call this list arithmetic.

Arithmetic for lists


Set Implicit Arguments.
Load Arith.

We define lists inductively. Given a set A a list over A is either the empty list nil or it is the result of putting an element a in fornt of an already constructed list l, we write cons a l. nil and cons are constructors of list A, as 0 and S (successor) were constructors of nat.

Inductive list (A : Set) : Set :=
 | nil : list A
 | cons : A -> list A -> list A.

Implicit Arguments nil [A].

In functional programming cons is usually written as an infix operation. In Haskell this is : but since this symbol is used for member ship in Coq, we use :: instead. Hence the meaning of : and :: in Coq and Haskell are exactly swapped.

Infix "::" := cons (at level 60, right associativity).

As an example we can define the list [2,3]

Definition l23 : list nat
  := 2 :: 3 :: nil.

And by consing another 1 in front we obtain [1,2,3].

Definition l123 : list nat
  := 1 :: l23.

We are going to prove some basic theorems about lists following the development for natural numbers. There we showed that now successor of a natural number is 0 (peano7), here we show that no cons list is equal to the enmpty list.

Theorem nil_cons : forall (A:Set)(x:A) (l:list A),
  nil <> x :: l.
intros.
discriminate.
Qed.

The next peano axiom peano8 expressed the injectivity of the successor. We have a similar statement for lists: if two cons lists are equal then their tail is equal. To prove this we define tail as we had define predecessor for numbers.

Definition tail (A:Set)(l : list A) : list A :=
  match l with
  | nil => nil
  | cons a l => l
  end.

The proof follows exactly the one for peano8.

Theorem cons_injective :
  forall (A : Set)(a b : A)(l m : list A),
    a :: l = b :: m -> l = m.
intros A a b l m h.
fold (tail (cons a l)).
rewrite h.
unfold tail.
reflexivity.
Qed.

However, unlike S, cons has another argument, the head of the list. We can also show that it is injective in this argument, that is if two cons lists are eqaul thenthere head is equal.

There is a slight problem in defining head, we cannot (as in Haskell) define head : list A -> A, because it could be that A is empty but there is still nil : list A and what should the head of this list be?

To overcome this issue we define head : A -> list A -> A where the first argument is a dummy argument which is returned for the empty list.

Definition head (A : Set)(x : A)(l : list A) : A :=
  match l with
  | nil => x
  | a :: m => a
  end.

Once we have defined head the proof of injectivity is rather straightforward.

Theorem cons_injective' :
  forall (A : Set)(a b : A)(l m : list A),
    a :: l = b :: m -> a = b.
intros A a b l m h.
fold (head a (a :: l)).
rewrite h.
unfold head.
reflexivity.
Qed.

As for natural numbers we have also an induction principle for lists: if a property is true for the empty list, and if it holds for a list l then it also holds for cons a l for any a, then it holds for all lists. In Coq we use the same tactic induction to perform list indiuction.

Theorem ind_list : forall (A : Set)(P : list A -> Prop),
  P nil
  -> (forall (a:A)(l : list A), P l -> P (a :: l))
  -> forall l : list A, P l.
intros A P hnil hcons l.
induction l.
exact hnil.
apply hcons.
exact IHl.
Qed.

Lists form a monoid


Previously, we defined addition and multiplication for numbers. There is a very useful operation resembling addition for lists: append. We define app by structural recursion over lists.

The idea is that to append a list to the empty list is just that list, and to append a list to a cons list has the same head as the list and the tail is obtained by recursively appending the list to the tail.

Fixpoint app (A : Set)(l m:list A) : list A :=
  match l with
  | nil => m
  | a :: l' => a :: (app l' m)
  end.

As in Haskell we use the inifx operation ++ to denote append.

Infix "++" := app (right associativity, at level 60).

As an example we construct the list [2,3,1,2,3] by appending [2,3] and [1,2,3].

Eval compute in (l23 ++ l123).

We show that list A with ++ and nil forms a monoid. Indeed the proofs are basically the same as for (nat,+,0).

Theorem app_nil_l : forall (A : Set)(l : list A),
  nil ++ l = l.
intros A l.
reflexivity.
Qed.

Theorem app_l_nil : forall (A : Set)(l : list A),
  l ++ nil = l.
intros A l.
induction l.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.

Theorem assoc_app : forall (A : Set)(l m n : list A),
  l ++ (m ++ n) = (l ++ m) ++ n.
intros A l m n.
induction l.
reflexivity.
simpl.
rewrite IHl.
reflexivity.
Qed.

Reverse




While there are many similarities between nat and list A there are important differences. Commutativity l ++ m = m ++ l does not hold (what would be a counterexample?). Hence (list A,++,nil) is an example of a non-commutative monoid. Since we commutativity doesn't hold it makes sense to reverse a list (while it didn't make sense to reverse a number).

To define reverse, we first define the operation snoc which adds an element at the end of a given list. This operation again is defined by primitive recursion.

Fixpoint snoc (A:Set)
  (l : list A)(a : A) {struct l} : list A
  := match l with
     | nil => a :: nil
     | b :: m => b :: (snoc m a)
     end.

There is an alternative way to define snoc just by using ++. Can you see how?

As an example we put 1 at the end of [2,3]

Eval compute in (snoc l23 1).

Using snoc it is easy to define rev by primitive recursion. The reverse of an empty list is the empty list. To reverse a cons list, reverse its tail and then snoc the head to the end of the result.

Fixpoint rev
  (A:Set)(l : list A) : list A :=
  match l with
  | nil => nil
  | a :: l' => snoc (rev l') a
  end.

This definition of rev is called naive reverse and it is rather inefficient. Can you see why? How can it be improved?

Some examples.

Eval compute in rev l123.
Eval compute in rev (rev l123).

The 2nd example gives rise to a theorem about rev, namely that to reverse twice is the identity (rev (rev l) = l).

To prove it we first prove a lemma about rev and snoc. How did we discover this lemma?

Lemma revsnoc : forall (A:Set)(l:list A)(a : A),
  rev (snoc l a) = a :: (rev l).
intros A l a.

We proceed by induction over l.

induction l.
simpl.
reflexivity.
simpl.
rewrite IHl.
simpl.
reflexivity.
Qed.

And now we can prove the theorem.

Theorem revrev :
  forall (A:Set)(l:list A),rev (rev l) = l.
intros A l.
induction l.
simpl.
reflexivity.
simpl.

And now it seems that revsnoc is exactly what we need. Lucky that we proved it already.

rewrite revsnoc.
rewrite IHl.
reflexivity.
Qed.

Insertion sort




Our next example is sorting: we want to sort a given lists according to an given order. E.g. the list

4 :: 2 :: 3 :: 1 :: nil

should be sorted into

1 :: 2 :: 3 :: 4 :: nil

We will implement and verify "insertion sort". To keep things simple we will sort lists of natural numbers wrt to the <= order. First we implement a boolean function which compares two numbers:

Fixpoint leqb (m n : nat) {struct m} : bool :=
  match m with
  | 0 => true
  | S m => match n with
           | 0 => false
           | S n => leqb m n
           end
  end.

Eval compute in leqb 3 4.
Eval compute in leqb 4 3.

Notation "m <= n" := (leq m n).

We just assume that leq decided <=. I leave it as an exercise to formally prove this, i.e. to replace the axioms by lemmas or theorems.

Axiom leq1 : forall m n : nat, leqb m n = true -> m <= n.
Axiom leq2 : forall m n : nat, m <= n -> leqb m n = true.

The main function of insertion sort is the function insert which inserts a new element into an already sorted list:

Fixpoint insert (n:nat)(ms : list nat) {struct ms} : list nat :=
  match ms with
  | nil => n::nil
  | m::ms' => if leqb n m
              then n::ms
              else m::(insert n ms')
  end.

Eval compute in insert 3 (1::2::4::nil).

Now sort builds a sorted list from any list by inserting each element into the empty list.

Fixpoint sort (ms : list nat) : list nat :=
  match ms with
  | nil => nil
  | m::ms' => insert m (sort ms')
  end.

Eval compute in sort (4::2::3::1::nil).


Fixpoint Sorted (l : list nat) : Prop :=
  match l with
  | nil => True
  | a :: m => Sorted m /\ a <= head a m
  end.

Here is another assumption about <= I am not going to prove but leave as an exercise.

Axiom total : forall m n : nat, m <= n \/ n <= m.

Our goal is to show that insert preserves sortedness, i.e. Sorted l -> Sorted (insert n l). To prove this we need to lemmas.

The first one is useful in the case when the new element is not smaller than the current head. In this case we need to know that the head is smaller than the new element so that we can insert it later.

Lemma leqFalse : forall m n : nat, leqb m n = false -> n <= m.
intros m n h.
destruct (total m n) as [mn | nm].
assert (mnt : leqb m n = true).
apply leq2.
exact mn.
rewrite h in mnt.
discriminate mnt.
exact nm.
Qed.

The other lemma is a little case analysis: the head of the result of insert is either the inserted element or the previous head.

Lemma insertSortCase : forall (n a : nat)(l : list nat),
  head a (insert n l) = n \/ head a (insert n l) = head a l.
intros n a l.

While we say induction we are not going to use the induction hypothesis here. So we could have used destruct on lists here.

induction l.
left.
simpl.
reflexivity.
simpl.
destruct (leqb n a0).
left.
simpl.
reflexivity.
right.
simpl.
reflexivity.
Qed.

We are now able to prove the main lemma on insert.

Lemma insertSorted : forall (n : nat)(l : list nat),
  Sorted l -> Sorted (insert n l).
intros n l.

We prove the implication by induction. Why did we not do another intro?

induction l.

The case for the empty list is easy.

intro h.
simpl.
split.
split.
apply le_refl.

Now the cons case

intro h.
simpl.
simpl in h.
destruct h as [sl al].

We now analyze the result of the comparison.

case_eq (leqb n a).

First case leqb n a = true, that is the element is put in front.

intro na.
simpl.
split.
split.
exact sl.
exact al.

Here we need the correctness of leq wrt <=.

apply leq1.
exact na.

Second case leqb n a = false so we insert a in the tail Here we need our lemmas.

intro na.
simpl.
split.
apply IHl.
exact sl.

Here we have to reason about the head of insert n l, so we use our lemma.

destruct (insertSortCase n a l) as [H1 | H2].

First case: it is the new element.

rewrite H1.
apply leqFalse.
exact na.

Second case: it is the old head.

rewrite H2.
exact al.
Qed.

using the previous lemma it is easy to prove our main theorem.

Theorem sortSorted : forall ms:list nat,Sorted (sort ms).
induction ms.

case ms=nil:

  simpl.
  split.

case a::ms

  simpl.
  apply insertSorted.
  exact IHms.
Qed.

Is this enough? No, we could have implemented a function with the property sort_ok by always returning the empty list. Another important property of a sorting function is that it returns a permutation of the input. I leave this as an exercise.

End Lists.