website/content/blog/readable-lean3-proofs.md

date	draft	math	medium_enabled	medium_post_id	tags	title
2023-01-27 22:01:54-05:00	false	true	true	5fb876d4d819	Formal Methods	Readable Lean 3 Proofs

Important Note: This blog post uses the Lean 3 syntax

Interactive theorem provers are notorious for showcasing unreadable proofs. Let's illustrate our point with a couple examples and discuss various ways we can make it more readable.

Disjunction Elimination

Disjunction Elimination or proof by cases is a rule of inference that states the following. Consider you have the following three proofs:

1. p \vee q
2. p \rightarrow r
3. q \rightarrow r

Then it doesn't matter if it is p rather than q that holds, in the end r holds. Wikipedia has a nice example of this concept. I numbered the statements to correspond to the above.

1. It is true that either I'm inside or I'm outside.
2. If I'm inside, I have my wallet on me.
3. If I'm outside, I have my wallet on me.

Therefore, I have my wallet on me.

Now let's go over a corresponding proof in Lean.

example (p q r : Prop) : ((p → r) ∧ (q → r) ∧  (p ∨ q)) → r := begin
  intro H,
  cases H,
  cases H_right,
  cases H_right_right,
  case or.inl
  {
    exact H_left H_right_right,
  },
  case or.inr
  {
    exact H_right_left H_right_right,
  },
end

We can see a rough example of proof by cases at work. However, it's extremely hard to follow unless we try to emulate the proof state ourselves. What if I say that it doesn't have to be this way? That in fact, we can have proofs that are more readable. First let's start by replacing intro with assume and add labels to each of our cases.

example (p q r : Prop) : ((p → r) ∧ (q → r) ∧  (p ∨ q)) → r := begin
  assume H : ((p → r) ∧ (q → r) ∧  (p ∨ q)),
  cases H with H_pr H_rest,
  cases H_rest with H_qr H_pq,
  cases H_pq,
  case or.inl : H_p
  {
    exact H_pr H_p,
  },
  case or.inr : H_q
  {
    exact H_qr H_q,
  },
end

Now we know what H is just by looking at the proof. Sadly the cases don't exactly tell us what is contained in each of the hypotheses. But at least they're labeled to give us a clue. We can do better by replacing the initial cases statements with have and exact with show.

example (p q r : Prop) : ((p → r) ∧ (q → r) ∧  (p ∨ q)) → r := begin
  assume H : ((p → r) ∧ (q → r) ∧  (p ∨ q)),
  have H_pr : p → r := and.left H,
  have H_qr : q → r := and.left (and.right H),
  have H_pq : p ∨ q := and.right (and.right H),
  cases H_pq,
  case or.inl : H_p
  {
    show r, from H_pr H_p,
  },
  case or.inr : H_q
  {
    show r, from H_qr H_q,
  },
end

Now we have almost a complete picture of what all of our hypotheses are. The only two that are left unspecified are H_p and H_q. Though we can easily infer what they are by the label. Also by replacing exact with show, we have insight on what is trying to be proved at that given point.

The whole beginning of the proof is setting up the problem. Luckily, Lean provides a more concise syntax that better matches how the problem would be presented.

example {p q r : Prop} (H_pr : p → r) (H_qr : q → r) (H_pq : p ∨ q) : r := begin
  cases H_pq,
  case or.inl : H_p
  {
    show r, from H_pr H_p,
  },
  case or.inr : H_q
  {
    show r, from H_qr H_q,
  },
end

Finally, if we wanted to condense this more, we can make use of the built in or.elim theorem.

example {p q r : Prop} (H_pr : p → r) (H_qr : q → r) (H_pq : p ∨ q) : r := begin
  show r, from or.elim H_pq H_pr H_qr,
end

Negation Introduction

Now let's showcase a more complicated example. Negation introduction or proof by contradiction. Consider that we have the following two proofs:

1. p \rightarrow q
2. p \rightarrow \neg q

Then by negation introduction, we have a proof of \neg p.

The proof is going to rely on the law of excluded middle. That is p \vee \neg p holds.

axiom LEM {p : Prop}: p ∨ ¬ p

The proof also relies on the following property about negation $$ \neg p \iff (p \rightarrow false) $$ Now let's try to prove negation introduction using the cases tactic.

example {p q : Prop} (H_pq : p → q) (H_nq : p → ¬q) : ¬p := begin
  have H_LEM : p ∨ ¬p := LEM,
  cases H_LEM,
  case or.inl : H_p
  {
    have H_nq : ¬q := H_nq H_p,
    have H_qf : q → false := H_nq,
    have H_q : q := H_pq H_p,
    have H_f : false := H_qf H_q,
    -- Can prove anything with a falsity
    -- (Reductio ad absurdum)
    show ¬p, from false.rec (¬p) H_f,
  },
  case or.inr : H_np
  { 
    show ¬p, from H_np,
  },
end

Sadly this proof is too complicated to condense in one line with or.elim. However, we can set it up by creating subproofs with have.

example {p q : Prop} (H_pq : p → q) (H_nq : p → ¬q) : ¬p := begin
  have H_LEM : p ∨ ¬p := LEM,
  have H_npp : ¬p → ¬p := by {
    assume H_np : ¬p,
    show ¬p, from H_np,
  },
  have H_pp : p → ¬p := by {
    assume H_p : p,
    have H_nq : ¬q := H_nq H_p,
    have H_qf : q → false := H_nq,
    have H_q : q := H_pq H_p,
    have H_f : false := H_qf H_q,
    show ¬p, from false.rec (¬p) H_f,
  },
  show ¬p, from or.elim H_LEM H_pp H_npp,
end

Conclusion

When most people are taught how to write proofs in an interactive theorem prover, they are shown tactics such as cases, split, left, right, etc. These tactics manipulate the proof state which is shown to the developer when creating the proof. However, as a line in a proof it provides minimal insight.

We can take the guesswork out of figuring out the proof state by carefully selecting tactics which allow us to explicitely show the object being constructed. In Lean, these are assume, have, and show. Also making use of the inference rules themselves such as or.elim is a great alternative to cases, and and.intro is a great alternative to split.

If you have any other techniques on making ITP proofs more readable, please let me know.