Lecture 19: Inductive types & proofs

1 Purpose

Inductive types & inductive proofs

2 Outline

As we’ve learned to program with Lean, we’ve seen several inductive types: not only natural numbers, but lists and various logical connectives and constants.

Today, we’re going to go into more detail about inductive types, and how we can program and prove with them.

Inductive types allow us to define both structures and enumerations: they are the single type definition mechanism that we have, and they are incredibly powerful. Indeed, the theory that underlies Lean is called the Calculus of Inductive Constructions for a reason!

We will show two different ways of defining an arithmetic expression (in the form of a binary tree) in the following:

inductive ArithExp : Type where
  | num : Nat -> ArithExp
  | add : ArithExp -> ArithExp -> ArithExp

This is the first, and the representation that underlies everything else. Since everything has a type, our new inductive type must be given a type: in this case, Type. Then, we have a list of constructors. There can be any (finite) number of constructors, including zero! Each constructor can taken any number of arguments (including zero!) and must return the type being constructed. The only final restriction is called the "positivity" test. That means you cannot define a type like:

inductive MyT : Type where
| C : (MyT -> Prop) -> MyT

Positions in types are called "negative" or "positive", and all occurrences of the type being defined must be positive in its definition. Positive occurrences are the arguments to the constructor, or the return types of function arguments to the constructor. Negative occurrences are arguments to function arguments to the constructor, as above. That means we could define a type like this:

inductive MyT : Type where
  | C : (Prop -> MyT) -> MyT

This requirement is a much more subtle version of the requirement that all functions terminate. If negative occurrences in types were allowed, it would be possible to construct instances of uninhabited types, and in particular prove logical falsehood. This, in turn, would render the logic not useful as a logic, so it is ruled out by the system. We generally won’t run into this, but if you do see that error, you should have some idea of what you should be looking for.

To construct elements of type ArithExp, we use the constructors:

def a1 := ArithExp.num 10
def a2 := ArithExp.add (ArithExp.num 1) (ArithExp.num 2)

To use an ArithExp in code or in a proof, we can use pattern matching, a common feature in typed functional programming, and one we’ve started getting familiar with. This is a more concise form of the pattern of conditionally branching on which case of the data type you are in, and then binding the corresponding elements.

def a3 := ArithExp.add (ArithExp.num 3) (ArithExp.num 4)
def a4 := match a3 with 
          | ArithExp.add e1 _ => e1
          | _ => a3

A match expression takes an expression (here a3), and then a series of clauses. Lean requires that the clauses are exhaustive: they must cover all of the cases of the inductive type, but you can use wildcard (_) patterns to cover multiple cases, or within cases. Note that both in the constructors and pattern matching we are using qualified names: ArithExp.add, not add. When we define a new inductive type, Lean creates what is called a namespace, and puts the constructors inside. This means you can use the same constructor names for different inductive types, which is convenient. You can also define your own namespaces explicitly, which we may do at times.

While that syntax of inductive definition is the core syntax, we will often use the following shorthand, which gives names to the arguments to constructors, writing them a bit more like enumerated struct definitions:

inductive ArithExp : Type where
  | num (n : Nat)
  | add (l : ArithExp) (r : ArithExp)

This is a logically equivalent type, but it comes with convenient field names. In a case where you have multiple cases of the inductive type, this is a little less useful, as until you know which case you are in, you can’t use the fields to access data, though you can use them to construct data without knowing the order:

def a5 := ArithExp.add (r := ArithExp.num 3) (l := ArithExp.num 4)

You can also apply only some of the arguments, and end up with a partially applied function expecting the rest:

#check ArithExp.add (r := ArithExp.num 3) 
-- fun l => ArithExp.add l (ArithExp.num 3) : ArithExp → ArithExp

Let’s practice by writing a function that uses pattern matching to evaluate our arith expressions to a number:

def eval : ArithExp → Nat
  | ArithExp.num n => n
  | ArithExp.add l r => Nat.add (eval l) (eval r)

We’ll come back to using this in a proof in a bit.

Let’s now define a new inductive type, this time for colors. It should be an enumeration of a few constants:

inductive Color : Type where
  | red : Color
  | green : Color
  | blue : Color

Now, let’s define a different representation, where our type has a single constructor that takes three natural numbers as arguments (for red, green, blue light values):

inductive RGB : Type where
  | mk : Nat -> Nat -> Nat -> RGB

We can now define functions that convert between the two representations:

def colortoRGB : Color -> RGB
  | Color.red => RGB.mk 255 0 0
  | Color.green => RGB.mk 0 255 0
  | Color.blue => RGB.mk 0 0 255

def RGBtoColor : RGB -> Color
  | RGB.mk 255 0 0 => Color.red
  | RGB.mk 0 255 0 => Color.green
  | RGB.mk 0 0 255 => Color.blue
  | _ => Color.red

What had to happen when we converted from RGB to color? We had to pick a way of handling "all the rest" of the colors. In this case, we just turned everything else into Red. There are other approaches, but the important part is that Lean will always make us handle every case in some way. This is quite different from similar pattern matching in functional languages like Haskell or OCaml, where you can leave out cases and get errors at runtime.

Now, let’s prove that if we convert from Color to RGB and back, we get the same thing:

theorem colorRGB_roundtrip : forall c, RGBtoColor (colortoRGB c) = c :=
 by intros c
    cases c <;> simp only [colortoRGB, RGBtoColor]

Inductive proofs

Our motivation for moving to Lean was to be able to prove properties about unbounded data. Now we know how to define inductive data types, which allow us to describe all sorts of unbounded data: not only numbers, but lists, trees, graphs, etc. Any of the data types that you designed in Fundies 1 are types that you should be able to write down as a suitable inductive definition.

But writing data definitions and defining functions over them was not our goal: we wanted to prove properties. Let’s start to talk about how that works.

We’ve shown how in Lean, logical statements are types, and terms that have the type are proofs of the statement. Just as possibly many terms can have the same type, there are often many ways to prove the same statement. We’ve shown, in detail, how we can apply this to minimal propositional logic – how implication is expressed through function arrows, and application corresponds to modus ponens.

Now we are going to talk about how recursion corresponds to induction.

Inductive types are named that because they can be defined inductively – i.e., the constructors can refer to the type itself. Provided there is at least one base case (i.e., a constructor that does not refer to itself), we can build examples of the data: i.e., it is inhabited.

We will use an inductive type by pattern matching, and often computing recursively.

We’ll start by proving a simple property of lists: that appending an empty list results in the same list. Proving this on the left is trivial (try it!), but on the right requires induction, because of how List.append is defined.

theorem list_app_r_nil : forall (T : Type) (L : List T),
  List.append L List.nil = L :=
 by intros T L
    induction L
    case nil => simp only [List.append]
    case cons x L IH => simp only [List.append]
                        rw [IH]

Here we see a few new tactics. Not only induction, but simp only and rw.

Now, consider our ArithExp inductive type, and eval function. We talked about this as programming: it is a function that takes an expression and returns a number. But we can also think of the type as a logical statement: that given an ArithExp, it is possible to construct a Nat. This isn’t a terribly interesting statement, because we can construct a Nat without anything: we can just use 0, or 1, or any of the infinite other Nats. It thus has lots of proofs, many of which are probably not very useful, at least if we want to treat them also as programs.

Things become much more interesting when we introduce the ability to express equivalence in our logical statements. There are two different ways of doing this in Lean. First, we can express it as two implications: a statement P is equivalent to a statement Q if P -> Q and Q -> P. We can write this compactly as P <-> Q. Constructing a proof for such a theorem involves proving both implications. The other form of equivalence is P = Q, which is an inductive type with a single constructor that takes two identical elements. This means that if you have a proof (i.e., term) of type P = Q, you know that P and Q must actually be the same, as that’s the only way you could have constructed the term. We’ll use both forms of equivalence, though the latter is stronger, since it shows that the two statements must actually be the same, whereas P <-> Q only means that you can prove them each from the other. The other issue is that P <-> Q is only defined for propositions, whereas P = Q is defined for any type.

Let’s use this with our ArithExp definition. Let’s define an optimization, const_fold, that replaces any ArithExp.add of two numbers with the result of the operation.

def const_fold : ArithExp → ArithExp
  | ArithExp.num n => ArithExp.num n
  | ArithExp.add l r =>
    match l, r with
    | ArithExp.num n, ArithExp.num m => ArithExp.num (Nat.add n m)
    | l', r' => ArithExp.add (const_fold l') 
                             (const_fold r')

We can prove that this is correct, by showing that the result of calling eval on the result of const_fold is the same as calling eval on the original expression, for all expressions.

theorem const_fold_correct1 : 
  forall (e : ArithExp), eval e = eval (const_fold e) :=
  by 
    intro e
    induction e
    case num n => simp only [eval, const_fold]
    case add l r ihl ihr => 
      simp only [eval, const_fold]
      cases l with 
        | num n =>
          cases r with
          | num m =>
            simp only [eval]
          | _ =>
            simp only [eval, const_fold]
            rw [<- ihr]
            simp only [eval]
        | _ =>
          cases r with
          | num m =>
            simp only [eval]
            rw [<- ihl]
            simp only [eval]
          | _ =>
            simp only [eval]
            rw [<- ihr, <- ihl]
            simp only [eval]

First, note that this was what we approximated earlier, using PBT or Rosette. Now we have proved it for all expressions. We did it by induction. What is induction? It’s a strategy for constructing a proof for an arbitrary sized piece of data, in the same way as we write recursive functions over arbitrary sized data.

Let’s look at the proof state after we run the induction tactic. See we have two goals now: one for each case of our data type. This is the same way that a recursive function on ArithExp would have two cases in pattern matching, or two branches in a template. In the base case(s) we have to prove the statement in that case. In the other cases, we have to prove the statement, but we can use (analogously to recursive calls!) the statement on the subparts of the data. i.e., we can assume it already holds on the subparts of the data.

Why does this work? Well, for any example piece of data, it is built out of the constructors, and if we have proved each of these cases, we can build up a proof of the example by starting with the proofs of the base case and then applying the inductive cases over and over. Since we can do that for any data, it works for all!

Now, that was kind of repetitive. If we do a little work, we can make that proof a lot shorter, by relying on some of the tacticals:

theorem const_fold_correct2 : 
  forall (e : ArithExp), eval e = eval (const_fold e) :=
  by 
    intro e
    induction e
    case num n => simp [eval, const_fold]
    case add l r ihl ihr => 
      (simp only [eval, const_fold])
        <;> cases l
        <;> cases r
        <;> simp only [eval]
        <;> (try (rw [<- ihr]))
        <;> (try (rw [<- ihl]))
        <;> simp only [eval]
      

Here, in addition to <;>, which we’ve seen before, we introduce a new one, try, which takes a tactic and even if that tactic fails, still succeeds. This is important because chaining with <;> will only proceed if every tactic along the chain succeeds, so if there are operations that may not succeed, but we want later operations to work, we must wrap them in try. Note that <;> binds tighter than try, so you must wrap try in parentheses!

Now, let’s add, as an exercise, another case to our inductive type: this time for multiplication. Then we’ll update eval, and our constant folding function, and our proof to account for this.

inductive ArithExp : Type where
  | num (n : Nat)
  | add (l r : ArithExp)
  | mul (l r : ArithExp)


def eval : ArithExp → Nat
  | ArithExp.num n => n
  | ArithExp.add l r => Nat.add (eval l) (eval r)
  | ArithExp.mul l r => Nat.mul (eval l) (eval r)

def const_fold : ArithExp → ArithExp
  | ArithExp.num n => ArithExp.num n
  | ArithExp.add l r =>
    match l, r with
    | ArithExp.num n, ArithExp.num m => ArithExp.num (Nat.add n m)
    | l', r' => ArithExp.add (const_fold l') 
                             (const_fold r')
  | ArithExp.mul l r => ArithExp.mul (const_fold l) 
                                     (const_fold r)

theorem const_fold_correct1 : 
  forall (e : ArithExp), eval e = eval (const_fold e) :=
 by intro e
    induction e
    case num n => simp only [eval, const_fold]
    case add l r ihl ihr => 
      simp only [eval, const_fold]
      cases l with 
        | num n =>
          cases r with
          | num m =>
            simp only [eval]
          | add =>
            simp only [eval, const_fold]
            rw [<- ihr]
            simp only [eval]
          | mul =>
            simp only [eval, const_fold]
            simp only [eval, const_fold] at ihr
            rw [<- ihr]
        | add =>
          cases r with
          | num m =>
            simp only [eval, const_fold, eval]
            rw [<- ihl]
            simp only [eval]
          | add =>
            simp only [eval]
            rw [<- ihr, <- ihl]
            simp only [eval]
          | mul => 
            simp only [eval, const_fold]
            rw [<- ihl]
            simp only [eval] at ihr
            rw [ihr]
            simp only [eval]
        | mul => 
          rw [ihl, ihr]
          simp only [eval]
    case mul l r ihl ihr =>
      simp only [const_fold, eval]
      rw [ihr, ihl]