Lecture 24: Standard Libraries

1 Purpose

Learn a little more about how to use standard libraries.

2 Outline

Today, we’re going to practice more with representing properties as inductive relations. We’ll see two different representations of evenness (one we’ve seen before), both of which come up on the HW. We’ll also spend a little time learning how to use the standard library: some tricks for finding definitions, existing theorems, and a few particularly helpful ones you should know about.

First, a new representation of evenness:

inductive ev' : Nat → Prop :=
  | O : ev' 0
  | SSO : ev' 2
  | sum n m (Hn : ev' n) (Hm : ev' m) : ev' (Nat.add n m)

It’s often a good idea to test out a new definition by writing down some examples. So, we should be able to show that 0 & 6 are even:

example : ev' 0 := ev'.O
example : ev' 6 := 
 by have H : 6 = Nat.add (Nat.add 2 2) 2 := rfl
    rw [H]
    -- exact (ev'.sum (Nat.add 2 2) 2 (ev'.sum 2 2 ev'.SSO ev'.SSO) ev'.SSO)
    constructor -- apply ev'.sum
    constructor -- apply ev'.sum
    constructor -- apply ev'.SSO
    constructor -- apply ev'.SSO
    constructor -- apply ev'.SSO

Note that we’ve given several different potential proofs fon 6 being even; they all rely on first decomposing 6 into (2 + 2) + 2, but we can then do it all at once (with exact) or much more easily, we can use either apply with a constructor or, the helper constructor that figures out which constructor to apply.

To get started proving with this definition, let’s show that ev' (Nat.mul n m) = ev' (Nat.mul m n):

theorem comm_ev' : forall n m, ev' (Nat.mul n m) -> ev' (Nat.mul m n) :=
 by intros n m H
    rw [Nat.mul_eq, Nat.mul_comm, <- Nat.mul_eq]
    assumption

Note that to do this, we relied upon standard library theorems, and in particular, helper lemmas that move between the n * m and Nat.mul n m syntax. These are defined for a lot of operators, and are generally called Nat.op_eq where the operator is called op. This is necessary because the standard library theorems are usually defined on the infix syntax, not on the actual function, so if we use the actual underlying functions, we have to move between to use the standard library theorems.

Now, let’s try proving a different theorem: that twice any number is even:

theorem twice_n_ev' : forall n, ev' (Nat.mul n 2) :=
 by intros n
    induction n
    case zero =>
      simp only [Nat.mul]; constructor
    case succ n IH =>
      simp only [Nat.mul]
      rw [(@Nat.add_eq 0), Nat.zero_add]
      rw [Nat.add_eq, Nat.succ_add, Nat.add_comm, Nat.succ_add, Nat.succ_eq_add_one, Nat.succ_eq_add_one, Nat.add_assoc]
      constructor
      have H : n + n = Nat.mul n 2 := by simp only [Nat.mul, Nat.add_eq, Nat.zero_add]
      rw [H]
      assumption
      have H : 1 + 1 = 2 := by rfl
      rw [H]
      constructor

theorem twice_n_ev_better' : forall n, ev' (Nat.mul n 2) :=
 by intros n
    induction n
    case zero =>
      simp only [Nat.mul]; constructor
    case succ n IH =>
      rw [Nat.mul_eq, Nat.succ_mul]
      constructor
      assumption
      constructor


theorem twice_n_ev_alt' : forall n, ev' (Nat.mul n 2) :=
 by intros n
    apply comm_ev'
    induction n
    case a.zero => 
      simp only [Nat.mul]; constructor
    case a.succ n IH => 
      simp only [Nat.mul]
      constructor
      assumption
      constructor

Note something really interesting: we first proved this "directly": it worked, but it involved a lot of manipulation of addition, some multiplication, commutativity, etc. You might end up doing this, but it’s often worth first trying to understand why a proof should go through (in this case, the inductive argument should work since if you know n * 2 is even, then (n + 1)*2 = n*2 + 2 is even, with the latter being straightforward to prove using your ev'.sum constructor). Once you know that, looking for appropriate theorems (in this case, Nat.succ_mul), or proving them first, may significantly cut down the effort.

Another option, of course, is to restate what we are going to prove: in this case, by first using the commutativity theorem we proved. Once we did that, even without Nat.succ_mul our proof was much easier, as the way Nat.mul is defined, the simplification we get after induction was much easier (essentially, the number we were doing induction on corresponded to how Nat.mul is defined recursively). You don’t necessarily have to realize that is going to happen, but if you have multiple different equivalent representations, it’s often worth starting a proof with each one to see which one seems like it’ll worth more easily.

Now, we’ll prove a more interesting (and challenging) theorem, that if the sum of two numbers is even, and one of the numbers is even, the other must be:

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

theorem ev_ev__ev : forall n m, ev (Nat.add n m) -> ev n -> ev m :=  
 by intros n m H1 H2
    induction H2
    case O =>
      rw [Nat.add_eq, Nat.zero_add] at H1
      assumption
    case SS o Ho IH =>
      rw [Nat.add_eq, Nat.succ_add, Nat.succ_add] at H1
      cases H1
      case SS H1 => 
        rw [<- Nat.add_eq] at H1
        apply IH
        assumption

One interesting question, when approaching a proof like this, is what to do induction on (assuming you need to do induction). There are two numbers, and an inductive relation (evenness) on the sum, plus another on the first number. When you are first starting, you may not know which one will be the most useful: and there isn’t necessarily only one answer, but even if multiple are possibilities, one may be much easier than the others!

You can certainly try one approach, but be sure to stop and try others if it doesn’t seem to be going somewhere! And one general intuition is that if the structure of the goal matches the structure of the data you are doing induction on, likely the proof will be much easier. Since we are proving ev m, it’s a good bet that we should do induction on either ev n or ev (Nat.add n m), as they both share the same evenness structure. Between those two, it’s more of a guess, but my guess was that ev n would give me more concrete information to work with, which I could then use with the other hypothesis (that ev (Nat.add n m)), so I tried that first.

Note that I used a few different theorems defined on natural numbers. They are all defined on the n + m syntax, but you can move between that and Nat.add n m using the Nat.add_eq theorem (so you first rewrite with that, then use the built in theorems, and then move back with Nat.add_eq if you need to).