Formal Lean Tactics

Lean 4 Tactics

Overview

Advanced tactics, tactic combinators, automation strategies, and custom tactic development for efficient proof construction in Lean 4.

Scope

Included:

• Core tactic repertoire (rw, simp, ring, linarith, omega)
• Tactic combinators and control flow
• Simplification and normalization
• Automation tactics (aesop, tauto, decide)
• Conversion mode (conv)
• Structured proofs (calc, have, show)
• Tactic debugging and inspection
• Custom tactic basics

Excluded:

• Basic proof structure (see lean-proof-basics.md)
• mathlib4 library search (see lean-mathlib4.md)
• Advanced metaprogramming (separate skill)
• Complex formalization strategies (see lean-theorem-proving.md)

When to Use This Skill

Primary use cases:

• Optimizing proof efficiency
• Automating repetitive reasoning
• Complex equational reasoning
• Arithmetic and algebraic proofs
• Debugging stuck proofs
• Developing domain-specific tactics

Indicators you need this:

• "How do I simplify this expression?"
• "What tactic should I use for arithmetic?"
• "How do I automate this proof pattern?"
• "My proof is too verbose"
• "How do I use conv mode?"

When to use other skills instead:

• Learning basic proofs → lean-proof-basics.md
• Finding mathlib theorems → lean-mathlib4.md
• Formalization architecture → lean-theorem-proving.md

Prerequisites

Required knowledge:

• Lean 4 basics (see lean-proof-basics.md)
• Tactic mode fundamentals
• Basic mathematical reasoning

Required setup:

# Lean 4 with mathlib4 (for advanced tactics)
lake new my_project math
cd my_project
lake update
lake build

Key dependencies:

• Lean 4.0.0+
• mathlib4 (for tactics like ring, linarith, omega)

Core Concepts

1. Tactic Monad and Goal State

Tactics operate in a monadic context, transforming goal states.

-- Goal state structure
-- ⊢ goal
-- Context:
--   h1 : assumption1
-- h2 : assumption2
-- Goal: conclusion

-- Tactics transform this state
example (h : p) : p ∨ q := by
  -- State: h : p ⊢ p ∨ q
  left
  -- State: h : p ⊢ p
  exact h
  -- State: (no goals)

2. Rewriting and Simplification

The workhorse of equational reasoning.

-- rw: Directed rewriting
example (h : a = b) : f a = f b := by
  rw [h]

-- simp: Simplification with simp set
example : 0 + n = n := by
  simp

-- simp with arguments
example : xs.reverse.reverse = xs := by
  simp [List.reverse_reverse]

3. Unification and Pattern Matching

Tactics use unification to match patterns and apply theorems.

-- apply unifies with goal
example (h : p → q) : p → q := by
  apply h  -- Unifies goal with conclusion of h

-- refine for partial terms with holes
example : ∃ n, n + 0 = n := by
  refine ⟨?_, ?_⟩
  · exact 5
  · simp

4. Simp Lemmas and Normal Forms

The simp tactic uses lemmas marked with @[simp].

-- Declaring simp lemmas
@[simp]
theorem zero_add (n : Nat) : 0 + n = n := by
  induction n <;> simp [*, Nat.add_succ]

-- Using simp
example (n : Nat) : 0 + (0 + n) = n := by
  simp  -- Applies zero_add twice

Advanced Tactics

Tactic 1: rw (Rewrite)

Directed equational reasoning.

-- Basic rewrite
example (h : a = b) : a + c = b + c := by
  rw [h]

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

-- Rewrite backwards
example (h : a = b) : b = a := by
  rw [←h]

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

-- Rewrite everywhere
example (h : a = b) (h1 : f a = c) (h2 : g a = d) : f b = c ∧ g b = d := by
  rw [h] at *
  exact ⟨h1, h2⟩

Tactic 2: simp (Simplification)

Normalize expressions using simp lemmas.

-- Basic simplification
example : [1, 2] ++ [] = [1, 2] := by simp

-- With specific lemmas
example : xs.reverse.reverse = xs := by
  simp only [List.reverse_reverse]

-- With hypotheses
example (h : x = 0) : x + y = y := by
  simp [h]

-- Simplify everywhere
example (h : x = 0) : x + y = y ∧ y + x = y := by
  simp [h] at *
  exact ⟨h, h⟩

-- Simplify with arithmetic
example : (n + 1) * 2 = n * 2 + 2 := by
  simp [Nat.add_mul, Nat.mul_comm]

Key simp variants:

simp           -- Use full simp set
simp only [...]  -- Use only specified lemmas
simp [h1, h2]  -- Add hypotheses to simp set
simp at h      -- Simplify hypothesis
simp at *      -- Simplify all
simp?          -- Show which lemmas were used (debugging)

Tactic 3: ring (Ring Arithmetic)

Decide equality in commutative (semi)rings.

-- Polynomial equality
example (a b : Nat) : (a + b) * (a + b) = a * a + 2 * a * b + b * b := by
  ring

-- Complex expressions
example (x y z : Int) :
    (x + y) * z - x * z = y * z := by
  ring

-- Works with variables and constants
example (n : Nat) : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by
  ring

Tactic 4: linarith (Linear Arithmetic)

Solve linear arithmetic goals.

-- From linear inequalities
example (h1 : a ≤ b) (h2 : b < c) : a < c := by
  linarith

-- With arithmetic
example (h : x ≤ 3) : 2 * x + 1 ≤ 7 := by
  linarith

-- Complex linear reasoning
example (h1 : x + y ≤ 10) (h2 : x ≥ 3) (h3 : y ≥ 4) : x + y ≤ 10 := by
  linarith

Tactic 5: omega (Integer/Natural Arithmetic)

Decision procedure for Presburger arithmetic (linear integer arithmetic).

-- Natural number arithmetic
example (n m : Nat) (h : n + m = 5) (h2 : n ≥ 3) : m ≤ 2 := by
  omega

-- Integer arithmetic
example (x y : Int) (h1 : x + y = 10) (h2 : x - y = 2) : x = 6 := by
  omega

-- With modular arithmetic
example (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 := by
  omega

Tactic 6: conv (Conversion Mode)

Fine-grained rewriting control.

-- Rewrite specific subterm
example : (1 + 2) + 3 = 3 + 3 := by
  conv_lhs =>
    arg 1  -- Select first argument
    rw [Nat.add_comm]
  rfl

-- Navigate expression tree
example : f (g (h a)) = f (g (h b)) := by
  conv_lhs =>
    arg 1    -- Enter f's argument
    arg 1    -- Enter g's argument
    arg 1    -- Enter h's argument
    rw [hab]

-- Using for: target specific occurrences
example : a + (a + b) = (a + a) + b := by
  conv =>
    lhs
    arg 2  -- Second argument of outer +
    rw [Nat.add_comm]

Tactic 7: calc (Calculational Proofs)

Chain equalities and inequalities.

-- Chain equalities
example (h1 : a = b) (h2 : b = c) : a = c := by
  calc a = b := h1
       _ = c := h2

-- Chain inequalities
example (h1 : a ≤ b) (h2 : b < c) : a < c := by
  calc a ≤ b := h1
       _ < c := h2

-- Mixed operations
example (n : Nat) : (n + 1) ^ 2 = n ^ 2 + 2 * n + 1 := by
  calc (n + 1) ^ 2 = (n + 1) * (n + 1) := by rfl
    _ = n * n + n * 1 + 1 * n + 1 * 1 := by ring
    _ = n ^ 2 + 2 * n + 1 := by ring

Tactic 8: aesop (Automated Search)

Automated proof search using a tactic library.

-- Solves goals by searching
example (h : p ∧ q) : q ∧ p := by
  aesop

-- With custom rule sets
example : ∀ x, x ∈ xs → x ∈ xs ++ ys := by
  aesop (add norm simp List.mem_append)

Tactic 9: tauto (Tautology)

Decide propositional tautologies.

-- Propositional logic
example : p ∧ q → q ∧ p := by
  tauto

-- Complex tautologies
example : (p → q) → (q → r) → (p → r) := by
  tauto

Tactic 10: decide (Decision Procedures)

Decide decidable propositions by evaluation.

-- Decidable equality
example : (5 : Nat) ≠ 3 := by
  decide

-- Boolean conditions
example : (10 < 20) = true := by
  decide

-- List membership
example : 3 ∈ [1, 2, 3, 4] := by
  decide

Tactic Combinators

Sequential and Parallel

-- Sequential (;)
example : p → p ∧ p := by
  intro h; constructor; exact h; exact h

-- All goals (<;>)
example : p → p ∧ p := by
  intro h
  constructor <;> exact h  -- Apply to both goals

-- Focus first goal (·)
example : p ∧ q → q ∧ p := by
  intro ⟨hp, hq⟩
  constructor
  · exact hq  -- First goal
  · exact hp  -- Second goal

Control Flow

-- Alternative (first success)
example : p ∨ q := by
  first | left; assumption | right; assumption

-- Try (don't fail)
example : p → p := by
  try rw [some_lemma]  -- Continue even if rw fails
  intro h
  exact h

-- Repeat
example : 0 + (0 + n) = n := by
  repeat rw [Nat.zero_add]
  -- Applies until no longer applicable

Conditional

-- By cases
example : p ∨ ¬p → q → q := by
  intro h hq
  cases h <;> exact hq

-- If-then-else pattern
by
  if h : condition then
    -- Proof with h : condition
    sorry
  else
    -- Proof with h : ¬condition
    sorry

Structured Proof Patterns

Pattern 1: have (Intermediate Results)

-- Name intermediate facts
example (h1 : a = b) (h2 : b = c) : f a = f c := by
  have hab : a = b := h1
  have hbc : b = c := h2
  have hac : a = c := by rw [hab, hbc]
  rw [hac]

-- Anonymous have
example (h : a = b) : f a = f b := by
  have : a = b := h
  rw [this]

Pattern 2: show (Make Goal Explicit)

-- Explicitly show what you're proving
example : p → q → p ∧ q := by
  intro hp hq
  show p ∧ q
  exact ⟨hp, hq⟩

-- Useful for type-directed proof
example : (fun x => x + 0) = (fun x => x) := by
  show (fun x => x + 0) = (fun x => x)
  funext x
  simp

Pattern 3: suffices (Backwards Reasoning)

-- Prove it suffices to show something simpler
example (h : p) : p ∧ p := by
  suffices hp : p from ⟨hp, hp⟩
  exact h

-- Chain backwards
example : a = d := by
  suffices a = c by rw [this, hcd]
  suffices a = b by rw [this, hbc]
  exact hab

Pattern 4: obtain (Destructure Existentials)

-- Clean existential elimination
example (h : ∃ x, P x ∧ Q x) : ∃ x, P x := by
  obtain ⟨x, hPx, hQx⟩ := h
  exact ⟨x, hPx⟩

-- With pattern matching
example (h : ∃ x y, x + y = 10) : ∃ z, z ≤ 10 := by
  obtain ⟨x, y, hsum⟩ := h
  use x
  omega

Debugging Tactics

Inspection

-- Show current goal state
example : p → p := by
  intro h
  trace "{h}"  -- Print hypothesis
  exact h

-- Show term
#check (rfl : a = a)
#print Nat.add  -- Print definition

-- simp? shows which lemmas were used
example : xs.reverse.reverse = xs := by
  simp?
  -- Try this: simp only [List.reverse_reverse]

Common Issues

-- Tactic failed: goal doesn't match
example : p := by
  exact q  -- Error: type mismatch

-- Fix: check types
example : p := by
  have hq : q := sorry
  -- Can't use hq to prove p directly

-- Unknown identifier
example : p := by
  exact h  -- Error: h not found

-- Fix: intro first
example : p → p := by
  intro h
  exact h

Quick Reference

Essential Tactics

-- Equality/Rewriting
rfl            -- Reflexivity
rw [h]         -- Rewrite with h
simp           -- Simplify

-- Arithmetic
ring           -- Ring equality
linarith       -- Linear arithmetic
omega          -- Presburger arithmetic

-- Structure
constructor    -- Build constructor
cases h        -- Case analysis
induction n    -- Induction

-- Automation
aesop          -- Automated search
tauto          -- Propositional tautology
decide         -- Decision procedure

-- Control
exact t        -- Provide exact term
apply t        -- Apply theorem
refine t       -- Partial term with holes

Tactic Combinators

t1; t2         -- Sequential
t1 <;> t2      -- All goals
· t            -- Focus first
first | t1 | t2 -- Alternative
try t          -- Don't fail
repeat t       -- Repeat until failure
all_goals t    -- Apply to all goals

Conversion Mode

conv =>
  lhs          -- Left-hand side
  rhs          -- Right-hand side
  arg n        -- nth argument
  args         -- All arguments
  enter [1, 2] -- Navigate path
  rw [h]       -- Rewrite
  simp         -- Simplify

Anti-Patterns

Anti-Pattern 1: Tactic Soup

-- BAD: Long sequence of low-level tactics
example : complicated_goal := by
  intro h1
  intro h2
  intro h3
  have x := h1
  have y := h2
  rw [x]
  rw [y]
  simp
  ring
  sorry

-- GOOD: Structure and automation
example : complicated_goal := by
  intro h1 h2 h3
  simp [h1, h2]
  ring

Anti-Pattern 2: Ignoring calc

-- BAD: Manual chaining
example (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by
  have hab := h1
  rw [hab]
  have hbc := h2
  rw [hbc]
  exact h3

-- GOOD: Use calc
example (h1 : a = b) (h2 : b = c) (h3 : c = d) : a = d := by
  calc a = b := h1
       _ = c := h2
       _ = d := h3

Anti-Pattern 3: Over-Reliance on sorry

-- BAD: Sorry as crutch
theorem main_result : important_property := by
  have lemma1 := sorry
  have lemma2 := sorry
  sorry

-- GOOD: Explicit admits with tracking
-- In separate file or section
axiom lemma1 : auxiliary_fact_1  -- TODO: issue #123
axiom lemma2 : auxiliary_fact_2  -- TODO: issue #124

theorem main_result : important_property := by
  have h1 := lemma1
  have h2 := lemma2
  -- Actual proof using h1, h2
  sorry  -- Requires h1 and h2, tracked in #125

Anti-Pattern 4: Not Using Automation

-- BAD: Manual propositional reasoning
example : (p ∧ q) ∧ r → r ∧ (q ∧ p) := by
  intro ⟨⟨hp, hq⟩, hr⟩
  constructor
  · exact hr
  · constructor
    · exact hq
    · exact hp

-- GOOD: Let automation handle it
example : (p ∧ q) ∧ r → r ∧ (q ∧ p) := by
  tauto

Anti-Pattern 5: Verbose Rewrites

-- BAD: Rewrite one at a time
example (h1 : a = b) (h2 : b = c) (h3 : c = d) : f a = f d := by
  rw [h1]
  rw [h2]
  rw [h3]

-- GOOD: Batch rewrites
example (h1 : a = b) (h2 : b = c) (h3 : c = d) : f a = f d := by
  rw [h1, h2, h3]

Anti-Pattern 6: Ignoring conv

-- BAD: Rewrite everything (may fail)
example : f (g a + h a) = f (h a + g a) := by
  rw [add_comm]  -- Might rewrite wrong occurrence

-- GOOD: Target specific subterm
example : f (g a + h a) = f (h a + g a) := by
  conv_lhs =>
    arg 1
    rw [add_comm]

Related Skills

• lean-proof-basics.md: Foundational proof techniques
• lean-mathlib4.md: Using mathlib4 library and theorems
• lean-theorem-proving.md: Advanced formalization strategies
• lean-metaprogramming.md: Custom tactic development (advanced)

References

• Lean 4 Tactics Index
• Mathlib4 Tactics Documentation
• Aesop Documentation
• Batteries Tactics

Examples

Example 1: Algebraic Manipulation

-- Expanding and simplifying
example (a b : Nat) : (a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2 := by
  ring

-- Using calc for clarity
example (x y : Int) : (x + y) * (x - y) = x ^ 2 - y ^ 2 := by
  calc (x + y) * (x - y)
      = x * x - x * y + y * x - y * y := by ring
    _ = x ^ 2 - y ^ 2 := by ring

Example 2: Linear Arithmetic

-- Combining linarith with other tactics
example (x y z : Nat) (h1 : x ≤ y) (h2 : y < z) : x < z := by
  linarith

-- Complex linear reasoning
example (a b c : Int)
    (h1 : 2 * a + b ≤ 10)
    (h2 : a + 2 * b ≤ 11)
    (h3 : a ≥ 0)
    (h4 : b ≥ 0) :
    3 * a + 3 * b ≤ 21 := by
  linarith

Example 3: Simplification Strategies

-- Controlled simplification
example (xs ys : List α) :
    (xs ++ ys).reverse = ys.reverse ++ xs.reverse := by
  simp only [List.reverse_append]

-- Simplification with arithmetic
example (n m : Nat) : (n + m) + 0 = n + m := by
  simp

-- Using simp to normalize before other tactics
example (n : Nat) : (n + 1) * 2 = n * 2 + 2 := by
  simp [Nat.add_mul]
  ring

Example 4: Conversion Mode for Precise Rewriting

-- Target specific subexpression
example (h : a = b) : f (g a + c) + d = f (g b + c) + d := by
  conv_lhs =>
    arg 1  -- Enter first argument of +
    arg 1  -- Enter first argument of f
    arg 1  -- Enter first argument of +
    arg 1  -- Enter argument of g
    rw [h]

-- Multiple targeted rewrites
example : (a + b) + (c + d) = (b + a) + (d + c) := by
  conv =>
    lhs
    arg 1
    rw [add_comm]
  conv =>
    lhs
    arg 2
    rw [add_comm]

Skill Metadata:

• Scope: Advanced Lean 4 tactics and automation
• Complexity: Intermediate to advanced
• Prerequisites: lean-proof-basics.md
• Related: lean-mathlib4.md, lean-theorem-proving.md