Lecture 20: Lists

1 Purpose

Practice proofs with lists.

2 Outline

Today, we’ll do a few proofs about lists. This is practice that should be useful for the homework, and should help you get more familiar with the interactive proof environment. While the theorems we will prove today and tomorrow are not particularly interesting, they should be good exercises.

As a warm up, we’ll look at a proof we did last time, but framed slightly differently: this time using the overloaded infix ++ append syntax, rather than the actual List.append function.

theorem list_app_r_nil : ∀ (T : Type) (l : List T), l ++ [] = l :=
  by intros T l
     induction l
     case nil => rfl
     case cons h t ih => 
       -- simp only [HAppend.hAppend, Append.append, List.append]
       have h1 : (h :: t) ++ [] = h :: (t ++ []) := by rfl
       rw [h1]
       rw [ih]

Note that the nil case proceeds as before, but the cons case doesn’t: in particular, while it might look like we could immediately rw with our induction hypothesis, this is actually a misleading consequence of the binding precedence of :: vs ++: since :: binds tighter than ++, what we have is equivalent to (h::t) ++ [], which means that our induction hypothesis, which is an equality about t ++ [], does not directly apply. This was true in our previous proof too, though it was more obvious, since without the infix operator ++, we could see the precedence more clearly.

But there’s more: if we try to do simp only [List.append], as we did before, nothing would change. This is because ++ is not syntax for List.append, but instead, is a generic abstraction for appending, which in the particular case of Lists, will turn out to be List.append.

We can make this go through by simplifying through the abstraction (shown commented out), but this is an opportunity to show a helpful tactic: have, which allows us to define an intermediate result and prove that, which we will then have as a lemma. We can use this to show that h :: t ++ [] is equal to h :: (t ++ []), without having to know what the exact functions are, because rfl will run whicheven side evaluates to the other. Once we have that, we can rewrite using it, and at that point, our induction hypothesis is usable.

While this is, in some sense, a lesson showing why we will usually use List.append instead of ++, this strategy of using have to make fine-grained changes

To go over carefully how this works, its helpful to think a bit about how append works. The actual definition of append is a tiny bit more complicated, but we could define an equivalent function like this:

def my_append {A : Type} : List A → List A → List A
| [], l => l
| (h :: t), l => h :: (my_append t l)

This should be very familiar from Fundies 1: it is a recursive function that treats its second argument as a simple input, adding each element of the first as it recurs until it reaches the end of the first list and returns the second list.

Looking at this definition, it should be clear that doing induction on the first list is the right way to prove this, as the definition does recursion on this list. Induction and recursion are two sides of the same coin, and in particular, the definition requires that we know whether the first list is empty or non-empty to unfold, which are exactly the cases we consider when doing induction.

In the empty case, we need to show that [] ++ [] = []. This follows by reducing the definition of ++. Another way of saying this is that it follows by definitional equality, as by merely unfolding the definition of ++ we can see that these are equal. This means we can use this using the tactic rfl.

In the non-empty case, we need to show that ⊢ h :: t ++ [] = h :: t, where we know, as an inductive hypothesis, that t ++ [] = t. This looks like you could just rewrite with the hypothesis and be done, but operator precedence is a bit tricky here. The :: binds tighter than ++ (you can right click on either and click "Go to Definition" – :: has precedence 67, whereas ++ has precedence 65). That means that, if we had explicit parenthesis, what we are trying to show is:

ih: t ++ [] = t
⊢ (h :: t) ++ [] = h :: t

However, we know from the definition of ++ that if the first argument is a non-empty list, this is equivalent to h :: (t ++ []), at which point we could rewrite using the hypothesis. To make these steps explicit, and as a useful trick when proving particular equivalences, we define this as an intermediate helper with have. This holds by definitional equality — i.e., reduction — which can be done by the tactic rfl.

Now that we have that lemma, we can rewrite using it, and that then gets the goal in a form where rewriting with the induction hypothesis is sufficient to complete the proof. Note that rw, like many tactics, will check if the result is a trivial equality and complete the proof with refl if so.

Let’s now do the other direction:

theorem list_app_l_nil : ∀ {A : Type} (l : List A), [] ++ l = l := 
  by intros A l
     rfl
theorem list_app_l_nil' : ∀ {A : Type} (l : List A), List.append [] l = l := 
  by intros A l
     rfl

Here, the whole proof follows by definitional equality, and so we don’t need induction at all! Why? Well, if we look back at the definition of append, we see that we recur on the first argument, which means that if it is empty, [] ++ l = l by the definition of append!

This asymmetry may seem odd at first, but if you think about the actual program that we are proving facts around, the behavior is very different based on which argument we are talking about! Indeed, the program will never inspect the second argument at all.

Now, let’s practice with some exercises about lists. First, we’ll prove a theorem about length:

theorem list_length_cons : ∀ {A : Type} (h : A) (t : List A), 
  (h :: t).length = t.length + 1 :=
 by intros A h t
     rfl

This, again, followed directly from defintional equality, since length is defined essentially as follows:

def my_length {A : Type} : List A → Nat
| [] => 0
| (_ :: t) => my_length t + 1

Now, let’s prove a simple fact about natural numbers:

theorem nat_zero_add : forall n, Nat.add 0 n = n :=
 by intros n
    induction n
    case zero => rfl
    case succ n IH => 
      simp only [Nat.add]
      rw [IH]

This is a straightforward proof by induction: in the base case, it is trivial (by rfl); in the recursive case, we simplify and use the induction hypothesis.

Let’s prove another fact, this one about successor:

theorem nat_succ_add : forall (n m : Nat), 
  Nat.add (Nat.succ n) m = Nat.succ (Nat.add n m) :=
 by intros n m
    induction m
    case zero => rfl
    case succ m IH => simp only [Nat.add]
                      rw [IH]

This was interesting, as we had two arguments, and we had to decide which to do induction on! In general, if you are proving a fact about a recursive function, you will want to do induction on the argument that the function is structurally recursive on. In this case, that was the second argument. Once we figure that out, the proof ends up being as simple as the previous one.

These lemmas may be useful when we go to prove a more interesting fact about length:

theorem list_length_app : ∀ {A : Type} (l1 l2 : List A), 
 (List.append l1 l2).length = Nat.add l1.length l2.length :=
 by intros A l1 l2
    induction l1
    case nil => 
      rw [list_app_l_nil']
      simp only [List.length]
      rw [nat_zero_add]
    case cons h t ih => 
      simp only [List.length]
      rw [ih]
      rw [nat_succ_add]
      rfl

We’ll proceed by induction on the first list argument.

This is the first proof we’ve done where we’ve had to use previous lemmas: indeed, it would not be possible to do it "all at once", as there are separate inductive arguments that need to be made to carry out individual steps.

In the empty case, we’ll first rewrite using the lemma we just proved, that List.append [] l = l, and then we’ll do definitional simplification using the List.length function to get that List.length [] = 0. Now we are left with a seemingly trivial conundrum: ⊢ List.length l2 = 0 + List.length l2. Now, to understand whether this holds definitionally, we need to know how addition is defined. On natural numbers, addition is defined to recur on the second argument, which means that this is actually not a trivial equality. Fortunately, this is a theorem we just proved!

In the non-empty list case, we first simp only with List.length. At this point, we can use our inductive hypothesis, and we are almost finished: the only issue is a problem of associativity. Our goal is:

⊢ Nat.add (List.length t) (List.length l2) + 1 = Nat.add (List.length t + 1) (List.length l2)

Or, if we abstract out a bit, replacing + 1 with Nat.succ:

⊢ Nat.succ (Nat.add a b) = Nat.add (Nat.succ a) b

This should be true, but it is not true definitionally. Luckily, we had already proved this as a theorem, so we can nearly complete the proof by using it. After rewriting, the goal can be closed with rfl.