formal-lean-theorem-proving

Formalizing complex mathematics

Lean 4 Theorem Proving

Overview

Advanced formalization strategies, proof patterns, and architectural techniques for complex mathematical theorem proving and formal verification in Lean 4.

Scope

Included:

Excluded:

When to Use This Skill

Primary use cases:

Indicators you need this:

When to use other skills instead:

Prerequisites

Required knowledge:

Required setup:

# Lean 4 with mathlib4
lake +leanprover/lean4:nightly-2024-01-15 new my_formalization math
cd my_formalization
lake exe cache get
lake build

Core Concepts

1. Inductive Types

Foundation of Lean's logic and data structures.

-- Simple inductive type
inductive MyNat where
  | zero : MyNat
  | succ : MyNat → MyNat

-- Indexed inductive type (dependent)
inductive Vec (α : Type u) : Nat → Type u where
  | nil : Vec α 0
  | cons : α → Vec α n → Vec α (n + 1)

-- Mutually inductive types
mutual
  inductive Even : Nat → Prop where
    | zero : Even 0
    | succ_odd : Odd n → Even (n + 1)

  inductive Odd : Nat → Prop where
    | succ_even : Even n → Odd (n + 1)
end

-- Inductive predicates
inductive Le : Nat → Nat → Prop where
  | refl : Le n n
  | step : Le n m → Le n (m + 1)

2. Well-Founded Recursion

Proving termination for complex recursive functions.

-- Well-founded relation
def sizeOf_list {α : Type} : List α → Nat
  | [] => 0
  | _::xs => 1 + sizeOf_list xs

-- Structural recursion (automatic termination)
def length {α : Type} : List α → Nat
  | [] => 0
  | _::xs => 1 + length xs

-- Well-founded recursion with custom measure
def ackermann (m n : Nat) : Nat :=
  match m, n with
  | 0, n => n + 1
  | m+1, 0 => ackermann m 1
  | m+1, n+1 => ackermann m (ackermann (m+1) n)
termination_by (m, n)  -- Lexicographic ordering

-- Custom well-founded relation
def div2 (n : Nat) : Nat :=
  if h : n < 2 then 0
  else 1 + div2 (n - 2)
termination_by n
decreasing_by simp_wf; omega

3. Quotient Types

Formal quotients by equivalence relations.

-- Define equivalence relation
def IntEqv : (Nat × Nat) → (Nat × Nat) → Prop :=
  fun (a, b) (c, d) => a + d = b + c

-- Prove it's an equivalence
instance : Setoid (Nat × Nat) where
  r := IntEqv
  iseqv := {
    refl := fun (a, b) => rfl
    symm := fun h => h.symm
    trans := fun h1 h2 => by
      simp [IntEqv] at *
      omega
  }

-- Define quotient
def MyInt : Type := Quotient (inferInstanceAs (Setoid (Nat × Nat)))

-- Lift operations
def MyInt.add : MyInt → MyInt → MyInt :=
  Quotient.lift₂
    (fun (a, b) (c, d) => Quotient.mk _ (a + c, b + d))
    (by
      intro (a, b) (a', b') (c, d) (c', d') hab hcd
      apply Quotient.sound
      simp [IntEqv] at *
      omega)

4. Proof by Reflection

Prove properties by computation.

-- Decidable propositions via computation
def isEven (n : Nat) : Bool :=
  n % 2 == 0

-- Reflect to proposition
theorem even_4 : isEven 4 = true := rfl

-- General reflection pattern
theorem even_iff_mod_eq_zero (n : Nat) :
    isEven n = true ↔ n % 2 = 0 := by
  simp [isEven]
  cases Nat.decEq (n % 2) 0 <;> simp [*]

-- Use reflection for automation
theorem even_100 : 100 % 2 = 0 := by
  have : isEven 100 = true := rfl
  exact (even_iff_mod_eq_zero 100).mp this

Advanced Patterns

Pattern 1: Custom Inductive Predicates

-- Define accessibility predicate
inductive Acc {α : Type} (r : α → α → Prop) : α → Prop where
  | intro : (∀ y, r y x → Acc r y) → Acc r x

-- Prove well-foundedness
theorem natLt_wf : WellFounded (· < · : Nat → Nat → Prop) :=
  ⟨fun n => by
    induction n with
    | zero =>
      constructor
      intro y h
      omega
    | succ n ih =>
      constructor
      intro y h
      cases Nat.lt_or_eq_of_le (Nat.le_of_lt_succ h) with
      | inl h' => exact ih.inv y h'
      | inr h' => rw [←h']; exact ih
  ⟩

Pattern 2: Sized Types

-- Size-indexed vector operations
def Vec.append {α : Type} : Vec α m → Vec α n → Vec α (m + n)
  | .nil, ys => ys
  | .cons x xs, ys => .cons x (xs.append ys)

-- Type-safe head
def Vec.head {α : Type} : Vec α (n + 1) → α
  | .cons x _ => x

-- Dependent pattern matching
def Vec.tail {α : Type} : Vec α (n + 1) → Vec α n
  | .cons _ xs => xs

Pattern 3: Propositional Truncation

-- Existential without data
structure Nonempty (α : Type u) : Prop where
  intro :: (val : α)

-- Use for proof irrelevance
theorem exists_of_nonempty {α : Type} {p : α → Prop}
    (h : Nonempty α) : (∃ x, True) :=
  ⟨h.val, trivial⟩

-- Squash for propositions
def TruncatedExists (p : α → Prop) : Prop :=
  ∃ x, p x  -- Already in Prop, so truncated

Pattern 4: Proof Automation with Macros

-- Simple tactic macro
macro "solve_nat_eq" : tactic =>
  `(tactic| omega)

example (n : Nat) : n + 0 = n := by solve_nat_eq

-- Macro with arguments
macro "rw_all" t:term : tactic =>
  `(tactic| rw [$t] at *)

-- Custom notation
notation:65 lhs:65 " ≈ " rhs:66 => Equivalence lhs rhs

Pattern 5: Well-Founded Induction Principles

-- Define custom induction principle
theorem nat_strong_induction {p : Nat → Prop}
    (h : ∀ n, (∀ m, m < n → p m) → p n) :
    ∀ n, p n := by
  intro n
  suffices ∀ m, m < n → p m from h n this
  intro m hm
  apply nat_strong_induction h

-- Use for complex recursion
def fastFib (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n+2 => fastFib (n+1) + fastFib n
termination_by n

Pattern 6: Coinductive Types

-- Infinite streams (coinductive)
coinductive Stream (α : Type u) : Type u where
  | cons : α → Stream α → Stream α

-- Operations on streams
def Stream.head : Stream α → α
  | .cons x _ => x

def Stream.tail : Stream α → Stream α
  | .cons _ xs => xs

-- Bisimulation for equality
def Stream.bisim (R : Stream α → Stream α → Prop) : Prop :=
  ∀ s1 s2, R s1 s2 →
    s1.head = s2.head ∧ R s1.tail s2.tail

Pattern 7: Proof Irrelevance Patterns

-- Use Subtype for computationally relevant data
def Pos : Type := { n : Nat // n > 0 }

def Pos.toNat (p : Pos) : Nat := p.val

-- Proofs are irrelevant
theorem pos_eq_of_val_eq (p q : Pos) (h : p.val = q.val) : p = q := by
  cases p; cases q
  simp at h
  subst h
  rfl

-- Use for predicate subtypes
def Even : Type := { n : Nat // n % 2 = 0 }

Pattern 8: Recursion-Recursion

-- Mutually recursive functions
mutual
  def even : Nat → Bool
    | 0 => true
    | n+1 => odd n

  def odd : Nat → Bool
    | 0 => false
    | n+1 => even n
end

-- Prove properties mutually
mutual
  theorem even_iff : even n = true ↔ n % 2 = 0 := by
    cases n <;> simp [even, odd_iff, *]

  theorem odd_iff : odd n = true ↔ n % 2 = 1 := by
    cases n <;> simp [even, odd, even_iff, *]
end

Pattern 9: Abstract Nonsense (Category Theory Style)

-- Abstract interface
class Functor (F : Type u → Type v) where
  map : (α → β) → F α → F β
  map_id : map (id : α → α) = id
  map_comp : map (g ∘ f) = map g ∘ map f

-- Concrete instances
instance : Functor List where
  map := List.map
  map_id := List.map_id
  map_comp := fun f g => (List.map_comp_map f g).symm

-- Generic theorems
theorem functor_preserves_const {F : Type → Type} [Functor F]
    (x : α) (c : β) :
    Functor.map (fun _ => c) (Functor.map (fun _ => x) fa) =
    Functor.map (fun _ => c) fa := by
  rw [←Functor.map_comp]
  rfl

Pattern 10: Proof Combinators

-- Compose proofs
def proof_comp {p q r : Prop} (h1 : p → q) (h2 : q → r) : p → r :=
  fun hp => h2 (h1 hp)

-- Proof lifting
def lift_iff {p q : Prop} (h : p ↔ q) : (p → r) ↔ (q → r) :=
  ⟨fun hpr hq => hpr (h.mpr hq), fun hqr hp => hqr (h.mp hp)⟩

-- Proof functoriality
theorem map_proof {p q r s : Prop}
    (hpq : p → q) (hrs : r → s)
    (hqr : q → r) : p → s :=
  fun hp => hrs (hqr (hpq hp))

Formalization Architecture

Large-Scale Organization

-- File: MyProject/Basic.lean
-- Foundational definitions

-- File: MyProject/Properties.lean
import MyProject.Basic
-- Basic properties and lemmas

-- File: MyProject/Advanced.lean
import MyProject.Properties
-- Advanced theorems

-- File: MyProject/Automation.lean
import MyProject.Properties
-- Custom tactics and automation

Abstraction Levels

-- Level 1: Raw definition
def raw_gcd (a b : Nat) : Nat := sorry

-- Level 2: Specification
theorem gcd_spec (a b : Nat) :
    (raw_gcd a b ∣ a) ∧
    (raw_gcd a b ∣ b) ∧
    (∀ d, d ∣ a → d ∣ b → d ∣ raw_gcd a b) := sorry

-- Level 3: Interface
class GCD (α : Type) [Dvd α] where
  gcd : α → α → α
  gcd_dvd_left : ∀ a b, gcd a b ∣ a
  gcd_dvd_right : ∀ a b, gcd a b ∣ b
  dvd_gcd : ∀ a b d, d ∣ a → d ∣ b → d ∣ gcd a b

Modular Proofs

-- Separate concerns
namespace IntegerProps
  theorem add_comm : ∀ a b : Int, a + b = b + a := sorry
  theorem mul_comm : ∀ a b : Int, a * b = b * a := sorry
end IntegerProps

namespace RingProps
  variable [Ring R]
  theorem distrib : ∀ a b c : R, a * (b + c) = a * b + a * c := sorry
end RingProps

Quick Reference

Inductive Type Checklist

-- 1. Define constructors
inductive MyType where
  | constructor1 : ...
  | constructor2 : ...

-- 2. Define recursion principle (if needed)
def MyType.rec ...

-- 3. Prove induction principle
theorem MyType.induction ...

-- 4. Define operations
def MyType.operation ...

-- 5. Prove properties
theorem MyType.property ...

Well-Founded Recursion Template

def recursiveFunction (x : α) : β :=
  match ... with
  | base_case => ...
  | recursive_case => ... recursiveFunction ...
termination_by measure_function x
decreasing_by
  -- Prove recursive calls decrease measure
  simp_wf
  -- Additional tactics (omega, etc.)

Quotient Type Template

-- 1. Define relation
def myRel : α → α → Prop := ...

-- 2. Prove equivalence
instance : Setoid α where
  r := myRel
  iseqv := ⟨refl_proof, symm_proof, trans_proof⟩

-- 3. Define quotient
def MyQuotient := Quotient (inferInstanceAs (Setoid α))

-- 4. Lift operations
def MyQuotient.op := Quotient.lift (raw_op) (congruence_proof)

Anti-Patterns

Anti-Pattern 1: Poor Abstraction

-- BAD: Over-concrete definition
def list_sum_nat : List Nat → Nat
  | [] => 0
  | x::xs => x + list_sum_nat xs

-- GOOD: Generic with type classes
def list_sum {α : Type} [Add α] [Zero α] : List α → α
  | [] => 0
  | x::xs => x + list_sum xs

Anti-Pattern 2: Ignoring Automation

-- BAD: Manual proof
theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction a with
  | zero => rfl
  | succ a ih =>
    simp [Nat.add_succ]
    rw [ih]

-- GOOD: Use automation
theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  omega

Anti-Pattern 3: Verbose Proofs

-- BAD: Overly detailed
theorem my_theorem : p ∧ q → q ∧ p := by
  intro h
  have hp := h.left
  have hq := h.right
  have hq_again := hq
  have hp_again := hp
  exact ⟨hq_again, hp_again⟩

-- GOOD: Concise
theorem my_theorem : p ∧ q → q ∧ p := by
  intro ⟨hp, hq⟩
  exact ⟨hq, hp⟩

-- BEST: Term mode
theorem my_theorem : p ∧ q → q ∧ p :=
  fun ⟨hp, hq⟩ => ⟨hq, hp⟩

Anti-Pattern 4: Not Using calc

-- BAD: Manual chaining
theorem transitivity (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by
  rw [h1, h2, h3]

-- GOOD: calc for clarity
theorem transitivity (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d :=
  calc a = b := h1
       _ = c := h2
       _ = d := h3

Anti-Pattern 5: Monolithic Proofs

-- BAD: 100-line proof
theorem huge_theorem : complicated_statement := by
  -- 100 lines of tactics
  sorry

-- GOOD: Modular with lemmas
theorem helper_lemma1 : ... := by ...
theorem helper_lemma2 : ... := by ...
theorem huge_theorem : complicated_statement := by
  have h1 := helper_lemma1
  have h2 := helper_lemma2
  -- Short proof using h1, h2

Anti-Pattern 6: Ignoring Type Universe Issues

-- BAD: Type errors due to universe levels
def bad_list_of_types : List Type := [Nat, String]
-- Error: Type : Type 1, not Type 0

-- GOOD: Explicit universe polymorphism
def good_wrapper {α : Type u} (x : α) : { β : Type u // β = α } :=
  ⟨α, rfl⟩

Related Skills

References

Examples

Example 1: Binary Trees with Proofs

-- Define binary tree
inductive Tree (α : Type) where
  | leaf : Tree α
  | node : α → Tree α → Tree α → Tree α

-- Size function
def Tree.size {α : Type} : Tree α → Nat
  | .leaf => 0
  | .node _ l r => 1 + l.size + r.size

-- Mirror function
def Tree.mirror {α : Type} : Tree α → Tree α
  | .leaf => .leaf
  | .node x l r => .node x r.mirror l.mirror

-- Prove involution
theorem Tree.mirror_involutive {α : Type} (t : Tree α) :
    t.mirror.mirror = t := by
  induction t with
  | leaf => rfl
  | node x l r ihl ihr =>
    simp [mirror, ihl, ihr]

-- Prove size preservation
theorem Tree.size_mirror {α : Type} (t : Tree α) :
    t.mirror.size = t.size := by
  induction t with
  | leaf => rfl
  | node x l r ihl ihr =>
    simp [mirror, size, ihl, ihr]
    omega

Example 2: Ackermann Function with Termination

-- Ackermann function (classic well-founded recursion)
def ackermann : Nat → Nat → Nat
  | 0, n => n + 1
  | m + 1, 0 => ackermann m 1
  | m + 1, n + 1 => ackermann m (ackermann (m + 1) n)
termination_by m n => (m, n)

-- Properties
theorem ackermann_pos (m n : Nat) : 0 < ackermann m n := by
  match m, n with
  | 0, n => omega
  | m + 1, 0 =>
    have : 0 < ackermann m 1 := ackermann_pos m 1
    exact this
  | m + 1, n + 1 =>
    have : 0 < ackermann m (ackermann (m + 1) n) :=
      ackermann_pos m (ackermann (m + 1) n)
    exact this
termination_by m n => (m, n)

Example 3: Quotient for Rational Numbers

-- Rational numbers as quotient
def RatEqv : (Int × Int) → (Int × Int) → Prop :=
  fun (a, b) (c, d) => a * d = b * c

instance : Setoid (Int × Int) where
  r := RatEqv
  iseqv := {
    refl := fun (a, b) => rfl
    symm := fun h => h.symm
    trans := fun {x y z} h1 h2 => by
      obtain ⟨a, b⟩ := x
      obtain ⟨c, d⟩ := y
      obtain ⟨e, f⟩ := z
      simp [RatEqv] at *
      -- Proof by ring manipulation
      have : a * f * (c * d) = b * e * (c * d) := by
        calc a * f * (c * d) = (a * d) * (c * f) := by ring
             _ = (b * c) * (c * f) := by rw [h1]
             _ = b * (c * c * f) := by ring
             _ = b * (c * e * d) := by rw [h2]; ring
             _ = b * e * (c * d) := by ring
      sorry -- Need non-zero denominators
  }

def Rat : Type := Quotient (inferInstanceAs (Setoid (Int × Int)))

Skill Metadata: