Lecture 26: Proof Automation

1 Purpose

Learn how to use simp to automate proofs.

2 Outline

Up until now, we’ve used the tactic simp only [function] to run particular functions. But simp is actually a much more general tactic, which we have intentionally avoided using because using too much automation early can make it hard to learn how to actually construct proofs, and there will always be cases where the automation fails, so it is important to understand how to do things "by hand". But, we’re now at the point where doing things step-by-step may be getting tedious, and avoiding some of that is possible with simp.

At it’s core, simp does two things: it rewrites with known equalities, and it also can try to prove hypotheses that arise from using theorems (which are equalities or not). Our simp only [Nat.add] usage makes it rewrite with only the set of equalities that come from Nat.add. It will keep going until it cannot find any matching cases; this is why it corresponds to "running the function until it gets stuck". i.e., Nat.add really is two equations:

a, Nat.zero   = a
a, Nat.succ b = Nat.succ (Nat.add a b)

And simp only [Nat.add] will rewrite, from left to right, those two equations, as many times as it can, matching a and b with whatever it can.

But there are other uses of simp. First, in a limited way, it can handle implications, provided it can find (among other theorems it is given) the hypotheses. For example:

theorem T : forall P Q R : Prop, 
  (P -> Q -> R) -> (P -> Q) -> (Q -> R) -> P -> R :=
 by intros P Q R H1 H2 H3 H4
    simp only [H1, H2, H3, H4]

Here, we are giving it not functions to rewrite with, but theorems (local ones, i.e., hypotheses) that it can use. It ends up applying a combination and using others to complete the goal. Note that if we leave some out, it won’t change the goal: while when rewriting with equations, it will do anything that makes progress, when it is using theorems that are implications, it will only apply them if it can prove the hypotheses. Note that this only works when the implications are of type Prop.

As a shorthand to listing all of the local hypotheses, we can write simp only [*] to mean, all of the local hypotheses.

theorem T1 : forall P Q R : Prop, 
  (P -> Q -> R) -> (P -> Q) -> P -> R :=
 by intros
    simp only [*]

This is convenient not only to save typing on the line with simp, but in the case where we don’t need to refer to the hypotheses elsewhere, we can use intros with no arguments to get anonymous names (which simp can handle just fine).

But here we are still using simp only. Why only? Well, it turns out that many theorems in the standard library have been marked as potential equations that simp could use, and you can mark your own. If you run simp, or simp [*], this will use all of those marked ones as well as any local ones:

example (p q r : Prop) (hp : p)
        : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := by
  simp [*]

In this case, we rely on built-in theorems that deal with conjunctions and disjunctions. If we did this with simp only [*], it would not be able to prove the goal (it would make some progress: since we have a proof of p, it would rewrite p with True, but then it would get stuck on the rest of the proof).

You can add your own theorems (or definitions) to the set that is used globally by simp by writing:

def double : Nat → Nat
| 0 => 0
| (Nat.succ x) => Nat.succ (Nat.succ (double x))

attribute [simp] double

There is also a shorthand to add the attribute when you are defining the theorem (or function):

@[simp] theorem double_succ (x : Nat) : double (Nat.succ x) = double x + 2 :=
 by sorry

For example: now writing simp or simp [*] will rewrite with the double function, and the double_succ theorem. However, adding global definitions can be a bit fragile, and it may be easier to understand proofs if you add them locally, so you can include both all hypotheses and specific additional theorems as follows:

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

theorem even_double: ∀ x : Nat, even (double x) = true := 
 by intros x
    induction x <;> simp [*, double, even]

theorem mult_2_x: ∀ x : Nat, Nat.mul 2 x = Nat.add x x := 
 by intros; simp [*, Nat.succ_mul]

Note, here, how we prove two theorems from HW7 primarily by appeal to simp. Note two limitations: first, it will not introduce hypotheses: but if we are going to do a proof entirely with simp, we don’t need names for the hypotheses, so using intros is fine. Second, and more importantly, simp will never do induction on a hypothesis, and will only do case analysis on certain built-in types (e.g., it will break a conjunction P /\ Q into two): it will not, e.g., do case analysis on any types you have defined, unless you create theorems specifically for that purpose and mark them as simp theorems.

The reason for not automatically trying induction is a bit more fundamental: automatically figuring out what to do induction on is a really hard problem, and while it may be possible in certain cases, it is not in general. It is one of the things that you will need to do manually: indeed, figuring out what to do induction on is often one of the key parts of a proof; after that, the rest is sometimes somewhat mechanical, and reducing the effort of mechanical steps is what simp can help with.

A related thing it won’t do is generalize parts of the goal (since we often do that in order to do case analysis, it’s not clear how invoking generalize would help simp, but it won’t do it).

Now that we have some sense of how it works, let’s practice by redoing two proofs that we did previously in lecture, this time using simp.

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

theorem twice_n_ev' : forall n, ev' (n * 2) :=
 by intros n; induction n <;> simp [*, ev'.O, ev'.SSO, ev'.sum, Nat.succ_mul]

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 (n + m) -> ev n -> ev m :=  
 by intros n m H1 H2
    induction H2 <;> 
    simp [*, Nat.succ_add] at * <;> 
    simp [*]
    cases H1
    simp [*]

-- alternatively:

theorem succ_succ_ev : forall n, ev (Nat.succ (Nat.succ n)) <-> ev n :=
  by intros n; constructor
     . intro H; cases H; assumption
     . intros; constructor; assumption


theorem ev_ev__ev_alt : forall n m, ev (n + m) -> ev n -> ev m :=  
 by intros n m H1 H2
    induction H2 <;> 
    simp [*, Nat.succ_add, succ_succ_ev] at * <;> 
    simp [*]