Episode 03: Lists

This command asks Coq to infer ``easy'' type arguments.

As a result of running Set Implicit Arguments, sometimes we will apply functions or constructors to fewer arguments than they are defined to take. When you see that, it simply indicates that Coq was able to automatically infer the missing arguments.

A parameterized, recursive type:

Above we define list to be a type parameterized by some other type T. Furthermore, we say that there are exactly two ways to build a llist: (1) using the lnil constructor or (2) using the lcons constructor. When the lnil constructor is applied to a type T, it yields a value of type llist T:

lnil
     : forall T : Type, llist T

We'll talk a lot more about forall throughout the course, but in this case you can think of it as just a fancy ->. When the lcons constructor is applied to a type T, a value of type T, and a value of type llist T, it yields a value of type llist T:

lcons
     : forall T : Type, T -> llist T -> llist T

Coq will infer the type argument T for lcons, but it will not try to infer the type argument T for lnil, even if it is obvious from context.

So this will break, even though context forces T to be nat:

Check (lcons 1 (lcons 2 (lcons 3 lnil))).

But this works:

However, we can tell Coq to always try to infer the type argument T of lnil from context:

The list type Coq provides is isomorphic to our llist.

Get nifty notations for cons, append, etc.

We'll use countdown to help test our list functions.

For polymorphic functions like length, we must explicitly add a type argument. If we try to define length without the type argument, like so:

Fixpoint length l :=
  match l with
    | nil => 0
    | x::xs => S (length xs)
  end.

we will get an error like:

Error: Cannot infer an internal placeholder of type "Type".

To avoid this problem, just add the type argument and the type for l. Coq can infer the rest:

In lecture, we noticed a simple relationship between length and countdown:

Consider arbitrary n.

We can prove property for arbitrary (S n) if we know property is true for n, so use induction.

Base case: n = O Need to prove length (countdown O) = O, which reflexivity solves by crunching down countdown 0 to nil, then length nil to O, which leaves the goal O = O.

Inductive case: n = S m Need to prove length (countdown (S m)) = S m. First we can cruch countdown (S m) down to S m :: countdown m. Now we crunch length (S m :: countdown m) down to S (length (countdown m)). This leaves us with the goal:

  S (length (countdown m)) = S m

Now if only we happened to know that length (countdown m) = m ... BUT WAIT! That's *exactly* what our induction hypothesis give us! After crunching with simpl, the firstorder tactic is smart enought to figure all this out and use the induction hypothesis to finish the proof.

Append one list to the end of another.

Show that length of two lists appended is just the sum of their lengths.

Consider arbitrary lists l1 and l2.

We can prove for arbitrary l1 = x :: xs if we just know property is true for xs, so use induction.

Base case: l1 = nil. Need to prove length (append nil l2) = length nil + length l2, which reflexivity solves by crunching down to length (l2) = O + length l2 and then to length l2 = length l2.

Inductive case: l1 = x :: xs Need to prove length (append (x :: xs) l2) = length (x :: xs) + length l2. First we can cruch length (append (x :: xs) l2) down to length (x :: append xs l2) and again to S (length (append xs l2)). We can also crunch length (x :: xs) + length l2 down to (S (length xs)) + length l2 which crunches down again to S (length xs + length l2). This leaves us with the goal:

  S (length (append xs l2)) = S (length xs + length l2)

Now if only we happened to know that length (append xs l2) = length xs + length l2 ... BUT WAIT! That's *exactly* what our induction hypothesis give us! After a little crunching from simpl, the firstorder tactic is smart enought to figure all this out and use the induction hypothesis to finish the proof.

Reverse the elements of a list.

Note: ++ is just an infix operator for append, so:

is the same as:

      append (rev xs) (x :: nil)

Note that the above version of rev is not efficient. We can do better using a helper function to collect the reversed version of the list as we recurse:

While rev' is more efficient than rev, it is a bit trickier to reason about. To prove rev and rev' are equivalent, we'll need a fact about append:

It turns out that firstorder already know this one.

Now we need to prove a carefully chosen lemma about rev'_aux.

Now we should be able to prove equivalence.

Note: we have to unfold rev first! This allows us to use rev_rev'_aux.

Question: Why did we need to prove rev_rev'_aux separately from rev_rev'? To prove that rev preserved length, we'll need to know a little more about arithmetic.

We get stuck trying to prove:

  length l + 1 = S (length l)

Question: Why do we get stuck?

Coq has a decision procedure for Pressburger arithmetic. It will make short work of our problem.

upto is another useful function for testing.

We can prove that rev (rev l) = l, but we'll need a lemma about rev and append:

Now for the lemma we really want:

The famous map function provides our first useful example of "higher order functions", which is just a fancy way of saying that map is a function which takes another function as an argument (in this case, the argument is named f).

Question: Are these the same nil?

The also famous fold function.