Background Link to heading

Today my colleague Brandon Rozek released a new Lean4 tutorial on his blog. Brandon really likes for people to be able to read his proofs (for some unknown reason). I decided to write this companion piece where I showcase what Lean4 looks like when you don’t care if people can read it. Towards this end I will be golfing Brandon’s tutorial, that is, going for the shortest proofs I can come up with for each provided theorem. Due to this, almost all of my proofs will be done constructively rather than using tactics, as you can often get much shorter proofs outside of tactic mode.

Reading and understanding these is great practice if you ever want to try understanding mathlib, as the developers frequently write completely unreadable non-tactic based proofs.

All examples can be run live on Lean4 Web here

Disjunction and Conjunction Link to heading

None of these rules are particularly interesting or deviate substantially from the proofs presented in Rozek’s tutorial.

Conjunctive Introduction Link to heading

example (H_p : p) (H_q : q) : p ∧ q := 
  And.intro H_p H_q

Conjunctive Elimination Link to heading

example (H_pq : p ∧ q) : p := 
  And.left H_pq

Disjunctive Introduction Link to heading

example (H_p : p) : p ∨ q :=
  Or.intro_left q H_p

Disjunctive Elimination Link to heading

example (H_pr : p → r) (H_qr : q → r) (H_pq : p ∨ q) : r :=
  Or.elim H_pq H_pr H_qr

Negation Link to heading

A bit more interesting, we can use Not.elim for a particularly elegant proof of negation introduction. For double negation elimination we just use Classical.not_not.

Negation Introduction Link to heading

example (H_pq : p → q) (H_pnq : p → ¬q) : ¬p := 
  λH => Not.elim (H_pnq H) (H_pq H)

Double Negation Elimination Link to heading

example {p: Prop} (H_nnp : ¬¬p) : p := 
  Classical.not_not.mp H_nnp

First Order Logic Link to heading

Universal introduction is the only slightly elegant one of these. The rest are already quite simple, even in Rozek’s tutorial.

Universal Elimination Link to heading

example (P : α → Prop) (H : ∀ x, P x) : P y := 
  H y

Universal Introduction Link to heading

example (P Q R : α → Prop) (H_pq : ∀ x : α, P x → Q x)
(H_qr : ∀ x : α, Q x → R x) : ∀ x : α, P x → R x := 
  λx Px => H_qr x (H_pq x Px)

Existential Introduction Link to heading

example (P : α → Prop) (H: P y) : ∃ x: α, P x := 
  Exists.intro y H

Existential Elimination Link to heading

example {p : α → Prop} (H_epx : ∃ x, p x)
(H_pab : ∀ (a : α), p a → b) : b :=
  Exists.elim H_epx H_pab

Induction Link to heading

I use the real list class instead of Rozek’s custom list class.

Append Nil Link to heading

The goal is to prove the List.append_nil theorem that an empty list appended to any list returns the original list. This is a clear usecase for structural induction. In tactic mode we would use the induction tactic, but we can get a much shorter proof using List.recOn.

example (as : List α) : as ++ [] = as :=
  List.recOn as rfl (λh t ih => by simp [ih])

Length Append Link to heading

The goal is to prove the List.length_append theorem, which states that the length of a list formed from appending two lists is the sum of the originals lengths. While Rozek’s tutorial gives this as an example of something you can use double induction to solve, you actually only need single induction to solve it. My proof is just a List.recOn version of the proof given for List.length_append in the source that uses linarith to save characters over Nat.succ_add.

example (as bs : List α) : (as ++ bs).length = as.length + bs.length :=
  List.recOn as (by simp) (λh t ih => by simp [ih]; linarith)