formal-lean-proof-basics

Learning Lean 4 from scratch

Lean 4 Proof Basics

Overview

Fundamental concepts and patterns for writing proofs in Lean 4, covering propositions as types, proof terms, basic tactics, and simple proof structures.

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:

# Install Lean 4 (via elan)
⚠️ **SECURITY**: Piping curl to shell is dangerous. For production:

Download script first

curl -O https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh

Verify checksum

sha256sum elan-init.sh

Review content

less elan-init.sh

Then execute

bash elan-init.sh

For development/learning only:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Create new project

lake new my_project cd my_project

Build project

lake build

Open in VS Code (with Lean 4 extension)

code .


**Dependencies:**
- Lean 4.0.0+ (preferably latest stable)
- VS Code with Lean 4 extension
- mathlib4 (optional, for library access)

## Core Concepts

### 1. Propositions as Types (Curry-Howard)
In Lean, propositions are types, and proofs are terms of those types.

-- Proposition: 2 + 2 = 4 #check (2 + 2 = 4 : Prop)

-- Proof: a term of type "2 + 2 = 4" example : 2 + 2 = 4 := rfl

-- Type of a proof #check (rfl : 2 + 2 = 4)


**Key principle:** To prove proposition P, construct a term of type P.

### 2. Term Mode vs Tactic Mode

**Term mode** (direct proof construction):

-- Prove implication directly example : p → q → p := fun hp hq => hp

-- Prove conjunction example : p ∧ q → q ∧ p := fun ⟨hp, hq⟩ => ⟨hq, hp⟩


**Tactic mode** (interactive proof construction):

example : p → q → p := by intro hp hq exact hp

example : p ∧ q → q ∧ p := by intro ⟨hp, hq⟩ exact ⟨hq, hp⟩


**When to use each:**
- Term mode: Simple proofs, direct constructions, obvious terms
- Tactic mode: Complex proofs, exploratory proving, step-by-step reasoning

### 3. Basic Proof Structure

**Anatomy of a proof:**

-- Theorem statement theorem my_theorem (assumptions : Type) : conclusion := by -- Tactic 1 -- Tactic 2 -- ... -- Tactic N (closes goal)


**Example:**

theorem and_comm (p q : Prop) : p ∧ q → q ∧ p := by intro ⟨hp, hq⟩ -- Introduce hypothesis, destructure exact ⟨hq, hp⟩ -- Provide exact proof term


### 4. Function Types and Implication
Functions and implications are the same (Π-types).

-- These are equivalent example : ∀ (n : Nat), n + 0 = n := fun n => Nat.add_zero n example : ∀ (n : Nat), n + 0 = n := by intro n; exact Nat.add_zero n

-- Implication is a function example : p → q := fun hp => _ -- hp : p, goal: q


## Common Patterns

### Pattern 1: Proving Implications

-- Template theorem impl_proof : P → Q := by intro hP -- Assume P (hypothesis hP) -- Now prove Q using hP sorry

-- Example theorem modus_ponens : p → (p → q) → q := by intro hp hpq apply hpq exact hp


### Pattern 2: Proving Conjunctions

-- Template theorem conj_proof : P ∧ Q := by constructor · -- Prove P sorry · -- Prove Q sorry

-- Example theorem and_intro : p → q → p ∧ q := by intro hp hq constructor · exact hp · exact hq


### Pattern 3: Using Conjunctions

-- Destructuring in intro theorem and_left : p ∧ q → p := by intro ⟨hp, hq⟩ exact hp

-- Using cases theorem and_right : p ∧ q → q := by intro h cases h with | intro hp hq => exact hq


### Pattern 4: Proving Disjunctions

-- Template: prove one side theorem disj_left : P → P ∨ Q := by intro hP left exact hP

theorem disj_right : Q → P ∨ Q := by intro hQ right exact hQ


### Pattern 5: Case Analysis on Disjunctions

-- Template theorem disj_elim : P ∨ Q → (P → R) → (Q → R) → R := by intro hPQ hPR hQR cases hPQ with | inl hP => exact hPR hP | inr hQ => exact hQR hQ

-- Example theorem or_comm : p ∨ q → q ∨ p := by intro h cases h with | inl hp => right; exact hp | inr hq => left; exact hq


### Pattern 6: Negation and Contradiction

-- Negation is implication to False #check (¬p : Prop) -- p → False

-- Proof by contradiction theorem not_not_intro : p → ¬¬p := by intro hp hnp exact hnp hp

-- Using contradiction theorem contradiction : p → ¬p → q := by intro hp hnp exfalso exact hnp hp


### Pattern 7: Universal Quantification

-- Template theorem forall_intro : ∀ (x : α), P x := by intro x -- Prove P x for arbitrary x sorry

-- Example theorem forall_impl : (∀ x, P x → Q x) → (∀ x, P x) → (∀ x, Q x) := by intro hPQ hP x apply hPQ exact hP x


### Pattern 8: Existential Quantification

-- Proving existence theorem exists_intro : P a → ∃ x, P x := by intro hPa use a exact hPa

-- Using existential hypothesis theorem exists_elim : (∃ x, P x) → (∀ x, P x → Q) → Q := by intro ⟨x, hPx⟩ hPQ exact hPQ x hPx


### Pattern 9: Equality and Rewriting

-- Reflexivity example : a = a := rfl

-- Symmetry example (h : a = b) : b = a := h.symm

-- Transitivity example (h1 : a = b) (h2 : b = c) : a = c := by rw [h1, h2]

-- Rewriting in goal example (h : a = b) : f a = f b := by rw [h]

-- Rewriting in hypothesis example (h1 : a = b) (h2 : f a = c) : f b = c := by rw [h1] at h2 exact h2


### Pattern 10: Simple Induction

-- Template theorem nat_induction (P : Nat → Prop) (base : P 0) (step : ∀ n, P n → P (n + 1)) : ∀ n, P n := by intro n induction n with | zero => exact base | succ n ih => exact step n ih

-- Example theorem zero_add (n : Nat) : 0 + n = n := by induction n with | zero => rfl | succ n ih => rw [Nat.add_succ, ih]


## Basic Tactics Reference

### Core Tactics

-- intro: Introduce hypothesis or variable intro h -- Name hypothesis h intro -- Auto-generate name intro ⟨h1, h2⟩ -- Destructure simultaneously

-- exact: Provide exact proof term exact h -- Use hypothesis h exact rfl -- Reflexivity for equality

-- apply: Apply function/theorem (backward reasoning) apply f -- If goal is Q and f : P → Q, new goal is P

-- constructor: Build constructors (and, exists, etc.) constructor -- For ∧, split into two goals

-- left/right: Choose disjunction branch left -- Prove P for goal P ∨ Q right -- Prove Q for goal P ∨ Q

-- cases: Case analysis cases h -- Split on hypothesis h

-- exfalso: Proof by contradiction exfalso -- Change goal to False

-- rfl: Reflexivity rfl -- Prove a = a

-- rw: Rewrite using equality rw [h] -- Rewrite goal using h : a = b rw [h] at h2 -- Rewrite in hypothesis h2 rw [←h] -- Rewrite backwards (b to a)


### Tactic Combinators

-- Sequential execution tac1; tac2 -- Do tac1 then tac2

-- All goals all_goals tac -- Apply tac to all goals

-- Focus on goals · tac -- Focus on first goal next => tac -- Focus on next goal

-- Repetition repeat tac -- Repeat until failure


## Quick Reference

### Logical Connectives

-- Implication P → Q -- Function type fun h => ... -- Proof (term mode) intro h -- Proof (tactic mode)

-- Conjunction P ∧ Q -- And.intro : P → Q → P ∧ Q ⟨hp, hq⟩ -- Construct (term mode) constructor -- Construct (tactic mode)

-- Disjunction P ∨ Q -- Or.inl : P → P ∨ Q, Or.inr : Q → P ∨ Q Or.inl hp -- Construct left (term mode) left; exact hp -- Construct left (tactic mode)

-- Negation ¬P -- P → False fun h => ... -- Prove negation

-- Universal ∀ x, P x -- (x : α) → P x fun x => ... -- Proof (term mode) intro x -- Proof (tactic mode)

-- Existential ∃ x, P x -- Exists.intro : ∀ (a : α), P a → ∃ x, P x ⟨a, ha⟩ -- Construct (term mode) use a; exact ha -- Construct (tactic mode)


### Equality

rfl -- a = a h.symm -- a = b → b = a rw [h] -- Rewrite using h : a = b rw [←h] -- Rewrite backwards calc -- Chain equalities a = b := h1 _ = c := h2


### Common Proof Structures

-- By cases cases h with | case1 => ... | case2 => ...

-- By induction induction n with | zero => ... | succ n ih => ...

-- Let binding let x := value show goal


## Anti-Patterns

### Anti-Pattern 1: Over-Complicating Simple Proofs

-- BAD: Verbose tactic proof example : p → p := by intro h have h2 : p := h exact h2

-- GOOD: Direct term example : p → p := fun h => h

-- GOOD: Minimal tactics example : p → p := by intro h; exact h


### Anti-Pattern 2: Ignoring Type Inference

-- BAD: Explicit types everywhere example : (fun (x : Nat) => (x : Nat) + (0 : Nat)) = (fun (x : Nat) => x) := by funext (x : Nat) simp

-- GOOD: Let Lean infer example : (fun x => x + 0) = (fun x => x) := by funext x simp


### Anti-Pattern 3: Manual Term Construction

-- BAD: Building complex terms manually example : p ∧ q → q ∧ p := fun h => And.intro (And.right h) (And.left h)

-- GOOD: Use tactics for clarity example : p ∧ q → q ∧ p := by intro ⟨hp, hq⟩ exact ⟨hq, hp⟩


### Anti-Pattern 4: Not Using Structured Proofs

-- BAD: All tactics at same level example : p ∨ q → q ∨ p := by intro h cases h right assumption left assumption

-- GOOD: Use bullets for structure example : p ∨ q → q ∨ p := by intro h cases h with | inl hp => right exact hp | inr hq => left exact hq


### Anti-Pattern 5: Overuse of sorry

-- BAD: Leaving sorries theorem important_theorem : P := by sorry -- TODO: prove this later

-- GOOD: Use admit only for exploration, remove before committing -- GOOD: Break into lemmas with clear sorry locations lemma helper_lemma : Q := by sorry -- Needs complex proof, tracked in issue #123

theorem important_theorem : P := by have hq := helper_lemma -- ... rest of proof


## Related Skills
- **lean-tactics.md**: Advanced tactics, tactic combinators, automation
- **lean-mathlib4.md**: Using mathlib4 library, finding theorems
- **lean-theorem-proving.md**: Advanced formalization strategies
- **smt-theory-applications.md**: Automated theorem proving with SMT solvers

## References
- [Lean 4 Manual](https://lean-lang.org/lean4/doc/)
- [Theorem Proving in Lean 4](https://lean-lang.org/theorem_proving_in_lean4/)
- [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
- [Natural Number Game (Lean 4 version)](https://adam.math.hhu.de/#/g/leanprover-community/nng4)

## Examples

### Example 1: Classical Logic Theorems

-- Modus tollens theorem modus_tollens : (p → q) → ¬q → ¬p := by intro hpq hnq hp exact hnq (hpq hp)

-- Hypothetical syllogism theorem hyp_syllogism : (p → q) → (q → r) → (p → r) := by intro hpq hqr hp exact hqr (hpq hp)

-- De Morgan's laws (one direction) theorem not_and_of_not_or_not : ¬p ∨ ¬q → ¬(p ∧ q) := by intro h ⟨hp, hq⟩ cases h with | inl hnp => exact hnp hp | inr hnq => exact hnq hq


### Example 2: Quantifier Manipulation

-- Swap quantifiers theorem forall_swap : (∀ x y, P x y) → (∀ y x, P x y) := by intro h y x exact h x y

-- Distribute quantifier over conjunction theorem forall_and : (∀ x, P x ∧ Q x) → (∀ x, P x) ∧ (∀ x, Q x) := by intro h constructor · intro x; exact (h x).left · intro x; exact (h x).right


### Example 3: Simple Arithmetic

-- Addition is commutative (using built-in) example (m n : Nat) : m + n = n + m := Nat.add_comm m n

-- Zero is right identity theorem add_zero (n : Nat) : n + 0 = n := by induction n with | zero => rfl | succ n ih => rw [Nat.add_succ, ih]

-- Successor relationship theorem succ_add (m n : Nat) : (m + 1) + n = (m + n) + 1 := by induction n with | zero => rfl | succ n ih => rw [Nat.add_succ, Nat.add_succ, ih, Nat.add_succ]


---

**Skill Metadata:**
- Scope: Lean 4 proof fundamentals
- Complexity: Beginner to intermediate
- Prerequisites: Basic logic and functional programming
- Related: lean-tactics.md, lean-mathlib4.md, lean-theorem-proving.md