Lecture 37: Inductive types/proofs, Proof automation

1 Purpose

Inductive types & inductive proofs, show proof automation

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!

Automation

But as it turns out, we can do a whole lot better by turning to proof automation. If we step back and think about what we are doing in a proof like this, once we realized we needed to do induction on e, the rest was essentially a matter of case analysis, running eval or const_fold, or rewriting with hypotheses we had.

All of that is tedious but not necessarily fundamentally difficult. There weren’t a lot of choices; we could go down some wrong paths, but likely would figure it out pretty quickly. Instead of doing that, by hand, it turns out we can leverage tools to support proof automation, or proof search, that essentially do exactly that.

For Lean, the best one is a library called Aesop, which you can download and install. Once you do so, you annotate inductive types and definitions to tell the proof search engine if (and to what extent) it should try to use these definitions as it searches for a proof. It essentially does a weighted depth-first-search: each thing it will try has an (annotated) probability of success, and it always tries higher probability techniques that match first, and at some point it either proves the goal, gets stuck and backtracks, or runs out of "depth" that it is allowed and backtracks.

Using Aesop, the above proof becomes just the choice of induction hypothesis: everything else can be figured out by the automation, once we have annotated:

3 More Proof Practice

Let’s do a few proofs about numbers. Here we are going to represent "evenness" as an inductive type, rather than a boolean predicate.

def double : Nat -> Nat
| 0 => 0
| Nat.succ n => Nat.succ (Nat.succ (double n))

theorem double_succ : forall n, double (Nat.succ n) = Nat.succ (Nat.succ (double n)) :=
 by intro n
    simp only [double]

inductive ev : Nat → Prop where
  | O : ev 0
  | SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))

theorem ev_4 : ev 4 :=
 by apply ev.SS; apply ev.SS; apply ev.O

theorem ev_plus4 : forall n, ev n → ev (Nat.add n 4) :=
 by intros n H
    apply ev.SS
    apply ev.SS
    assumption

theorem ev_double : forall n, ev (double n) :=
 by intro n
    induction n <;> simp only [double]
    . constructor
    . apply ev.SS
      assumption

Here, we show a new syntax for proof organization: .. This focuses on the goal at hand, and hides the rest of the proof. This is useful when you have a long proof, and you want to focus on a particular part of it. It can make reading the proof scripts easier later, as you can more easily see where each goal is being proved.

Now, we’ll try to show that our definition of even is equivalent to a more typical boolean predicate definition:

def even : Nat -> Bool
  | 0 => true
  | 1 => false
  | Nat.succ (Nat.succ n) => even n

theorem ev_eq : forall n, ev n ↔ even n :=
 by intro n
    constructor
    case mp =>
      intro H
      induction H
      case O => rfl
      case SS => simp only [even]; assumption
    case mpr =>
      intro H
      sorry

def even_ev : forall n, even n = true -> ev n
| 0 => fun _ => ev.O
| 1 => fun H => by contradiction
| Nat.succ (Nat.succ n) => fun H => ev.SS n (even_ev n H)

Initially, this seems to go well: but we need to do induction on the structure of our relational definition of even, rather than the structure of the natural numbers. Going in the other direction, from the even predicate to the even relation, just doesn’t work. The reason is that natural number induction goes up one number at a time. To prove that Nat.succ n is even, we can assume that n is even. But this is never going to be true! Either n isn’t even, or Nat.succ n isn’t even!

While we could try to define a different induction principle on natural numbers, that goes up two at a time, an easier way to do this is actually go back to our intuition from recursive definitions. Remember: proofs are just functional programs. In this case, what we do is match on 0, 1, and then Nat.succ (Nat.succ n). In the 0 case, it’s trivial. In the 1 case there is an easy contradiction, and in the Nat.succ (Nat.succ n) case, we can use call our function recursively two levels down, exactly as we’d like.

This uses a new tactic: contradiction. This is used whenever we have an absurd statement: usually, a hypothesis that is a constructor for an inductive type that cannot be. In this case, even 1 evaluates to false, and so that hypothesis evaluates to false = true, which is contradictory. More generally, if a hypothesis is an inductive type that is impossible (e.g., if we had H : ev 1, or H : False), as there are no constructor that have that type, then contradiction will prove the goal. Generally, cases H will also do the same, as it will realize there are no possible cases and so the goal is proved.

4 Relations vs. Functions

You’ve written many functions in your programming career, and a bunch in this class. You’ve also now seen a few "relations" in this class, which often capture similar ideas. e.g., we just saw an even function:

def even : Nat -> Bool
| 0 =>  true
| 1 => false
| Nat.succ (Nat.succ n) => even n

And an even relation:

inductive ev : Nat -> Prop where
| O : ev 0
| SS (n : Nat) (H : ev n) : ev (Nat.succ (Nat.succ n))

We talked (and proved) that the two were equivalent by showing that if you had one you could get the other, e.g., proved the following theorem:

theorem even_ev : forall n, even n = true <-> ev n := by sorry

But how are they different, and how are they the same? That is the purpose of the rest of this lecture.

5 Functions

First, we need to be more formal about what a function is. Mathematically (and the functions in Lean are mathematical functions, i.e., given the same input, they always return the same output), a function is a mapping from inputs to outputs. Another way of stating that is that it is a (potentially infinite) set of input-output pairs, with the restriction that for any input, there is only one output (as calling a function on a particular input can only give you one output).

e.g., we could characterize even as:

Where we would have to give infinite pairs.

We can do this for any function. For example, the factorial function:

def factorial : Nat -> Nat
| 0 => 1
| Nat.succ n => (Nat.succ n) * factorial n

Could also be defined as:

6 Relations

So what is a relation? A relation is a generalization of a function, in that it does not have the restriction that there is only a single output for a given input. Instead, it is a set of niput-output pairs, where there can be multiple outputs for a given input. So any function is as relation, but some relations are not functions. More concisely, you can think of a relation as a connection between inputs and outputs. One way you might get to a relation is by defining a function, and then making the function nondeterministic, i.e., allow it to potentially return different outputs for the same input.

How can we represent relations? Well, in any language we can represent a relation as a predicate (boolean returning function) on pairs (of input-output). e.g., a relation for even could be:

def even_rel : Nat × Bool -> Bool
| (n, true) => n % 2 == 0
| (n, false) => n % 2 == 1

Or we could represent the factorial relation as:

def factorial_rel : Nat × Nat -> Bool
| (n, m) => factorial n == m

The latter being a bit circular, but a valid definition.

But in Lean, we have another way of representing relation that turns out to be really useful when we are writing proofs. Rather than writing them as functions that take pairs and return booleans, we can define them as inductive types.

This is useful because if we are trying to prove something about, e.g., the factorial function, if we have the function, all we know is the input and output: the structure of the code is opaque. But if we represent it as an relation, and encode that as an inductive type, then the structure of the computation corresponds to the constructors of the indpuctive type. We can do case analysis, induction, etc. We’ve seen the ev relation many times, so let’s do one for factorial instead:

inductive fact : Nat -> Nat -> Prop where
| O : fact 0 1
| S (n m : Nat) (H : fact n m) : fact (Nat.succ n) ((Nat.succ n) * m)

Now, why does that relation mean the same thing? And in general, why does this approach work? Rather than proving it (which we’ll do later), let’s look at how the factorial function evaluates. e.g., factorial 4:

block{ factorial 4 = 4 * factorial 3 = 4 * (3 * factorial 2) = 4 * (3 * (2 * factorial 1)) = 4 * (3 * (2 * 1 * factorial 0)) = 4 * (3 * (2 * 1 * 1)) = 24 }

Now, we know this, and we can confirm that we got from the beginning to the end by running #eval factorial 4, but if we are trying to prove something about the factorial function, e.g., we have a hypotheses factorial n = m, there is no way to extract that structure from the hypothesis.

Now, let’s look at the same thing, but with the relation. In this case, we want to see how a value of type fact 4 24 is constructured: i.e., how we construct a proof that the pair (4, 24) is in the factorial relation.

#check (fact.S 3 _ (fact.S 2 _ (fact.S 1 _ (fact.S 0 _ fact.O))) : fact 4 24)

We can see that the term is a sequence of constructors, each of which is a step in the computation: the same steps as we see above when we wrote out how factorial evaluated, but unlike something on paper, this is an actual value we can use in our proofs.

To see this, and to see how this structure can be useful in our proofs, lets show that the two representations are equivalent. One direction (going from the inductive) ends up being easier, because the inductive relation contains so much more structure we can make use of in our proof:

theorem fact_factorial : forall n m, fact n m <-> factorial n = m :=
 by intros n m
    apply Iff.intro
    case mp =>
      intros H
      induction H <;> simp only [factorial, *]
    case mpr =>
      intros H
      revert m
      induction n <;> intros m H
      case zero =>
        simp only [factorial] at H
        rw [<- H]
        constructor
      case succ n IH =>
        simp only [factorial] at H
        rw [<- H]
        constructor
        apply IH
        rfl