Lecture 23: Generalize

1 Purpose

Introduce the generalize tactic, and how it can be used to do case analysis on programs.

2 Outline

Let’s first look at a simple function, that filters lists of numbers, including only numbers greater than or equal to a given number:

def filter_ge : List Nat -> Nat -> List Nat 
| [], _    => []
| x::xs, y => 
  if Nat.ble y x 
  then x :: filter_ge xs y 
  else filter_ge xs y

To warm up, we can prove, as an exercise, the following theorem:

theorem nat_ble_0 : forall n, Nat.ble Nat.zero n = true :=
  by intros n; cases n <;> rfl

theorem filter_ge_zero : forall l, filter_ge l Nat.zero = l :=
 by intros l
    induction l
    case nil => rfl
    case cons x xs IH =>
      simp only [filter_ge]
      rw [nat_ble_0]
      simp only []
      rw [IH]
      rw [ite_true]

Which is that if we filter numbers greater than or equal to 0, we get the whole list.

This requires a helper: knowing that 0 is less than or equal to any number.

The full proof reveals one thing about how if is define in Lean: it is actually shorthand for an operator called ite (if-then-else), and in particular, it takes as an argument a proposition that is decidable. That means it is a proposition that can be computed (proved or disproved). If it is provable, then the if expression evaluates to the first argument, and if it is disprovable, then the if expression evaluates to the second argument. We can see this happening by simplifying, as true = true evaluates to True (the trivial proposition for logical truth), and then we can use one of two rewriting lemmas, ite_true or ite_false to step into the branches.

Now, let’s do another proof: this time showing something "in reverse", more or less: that if the output has a given number, than that number must have been greater or equal to the number we were filtering by.

theorem filter_ge_res : forall x xs l y, filter_ge l y = x :: xs ->
                        Nat.ble y x :=
 by intros x xs l y H
    induction l
    case nil => contradiction
    case cons l ls IH =>
      simp only [filter_ge] at H
      revert H
      generalize H1 : Nat.ble y l = Q
      cases Q
      case false =>
        simp only []
        rw [ite_false]
        intros H1
        apply IH
        assumption
      case true =>
        simp only []
        rw [ite_true]
        intro H1
        cases H1
        assumption

The empty cases is easy: we know the output is non-empty, so the input could not have been empty, so contradiction handles that. The non-empty case is much more interesting. We don’t know what y is, but it seems like we’ll need to do case analysis on whether that boolean test passed (as our inductive hypothesis is about the rest of the list). We could try to do case analysis on y, or on l, but both are numbers: knowing they are 0 or Nat.succ n doesn’t really help us: what we want to know is whether or not they are equal. We want to do case analysis on the result of that boolean test! And this is what generalize allows us to do.

First, though, we need to move H back to the goal, as generalize only operates in the goal. We can do this with revert.

Now, we can use generalize to take an arbitrary expression and give it a name (the boolean value that is the result of Nat.ble y l), extracting all occurrences out of the goal. Now, we can do case analysis on that boolean: whether it is true or false. At this point, the proof is a bit tedious, but relatively straightforward: the key part was using generalize to extract the boolean test out so we could do case analysis on it. This pattern is very common!