Lecture 21: Proof Practice

1 Purpose

More practice proving.

2 Outline

Today, we are just gonig to practice with some small proofs.

First, we’ll do a few proofs about numbers, using a different representation of even from how we do it in HW. This time, even is represented 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 the one we used in HW.

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.