proof-assistant

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.5 Directed Rewriting with `rw`

4.5 Directed Rewriting with rw Rewriting is the primary way to apply propositional equalities in Lean. The tactic rw performs a single, directed replacement using a proof of equality. It is precise, local, and predictable. This section focuses on controlling direction, location, and sequencing. The basic form is: rw [h] where h : a = b . This replaces occurrences of a with b in the goal. The replacement is...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.2 Propositional Equality

4.2 Propositional Equality Propositional equality is the explicit notion of equality in Lean. It is written as a = b and represents a type whose values are proofs that a and b are equal. Unlike definitional equality, it does not rely on computation alone. You construct it, pass it around, and consume it in proofs. The canonical constructor is reflexivity. The term rfl has type a = a . Every...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.16 Rewriting with Equivalences

4.16 Rewriting with Equivalences Equalities are often too strict. In many developments you work with equivalences rather than literal equality. In Lean, these appear as logical equivalence ↔ , isomorphisms ≃ , or other structure-preserving relations. Rewriting with them requires conversion to equality or use of specialized lemmas. Logical equivalence ↔ For propositions, P ↔ Q states that P and Q are interchangeable. You cannot directly use rw with ↔...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.15 Avoiding Rewrite Loops and Nontermination

4.15 Avoiding Rewrite Loops and Nontermination Rewriting systems can diverge if rules are poorly oriented or interact cyclically. In Lean, this risk appears most often with simp , but it can also affect repeated uses of rw . The goal is to design and apply rewrite rules so that every step decreases a clear measure and reaches a stable normal form. A rewrite loop occurs when two or more lemmas...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.6 Simplification with `simp`

4.6 Simplification with simp The tactic simp performs normalization by repeated rewriting using a curated set of lemmas. In Lean, it serves as the primary automation for routine equalities. Unlike rw , which applies a single directed step, simp applies many rules until no further change occurs. At a high level, simp transforms an expression into a canonical form. It uses lemmas marked with the @[simp] attribute, along with a...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.11 Chained Rewriting and `calc`

4.11 Chained Rewriting and calc Complex equalities are rarely achieved in a single step. Instead, you move through a sequence of intermediate forms. Chained rewriting makes this sequence explicit and stable. In Lean, the preferred structure for such chains is the calc block. A calc block expresses equality as a sequence of justified steps: example (a b c : Nat) (h₁ : a = b) (h₂ : b = c)...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.13 Substitution and `subst`

4.13 Substitution and subst Substitution is the direct elimination of equalities from the context. Given a hypothesis h : x = t , the tactic subst h replaces every occurrence of x with t in the goal and in all hypotheses, and then removes h . In Lean, this is a structured form of rewriting that updates the entire context in one step. The basic pattern: example (x y :...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.7 Controlling the `simp` Set

4.7 Controlling the simp Set The behavior of simp depends entirely on the set of rewrite rules it uses. This set is composed of built-in lemmas, imported library lemmas, and user-declared rules marked with @[simp] . Effective use of Lean requires precise control over this set so that normalization remains predictable, terminating, and efficient. By default, simp uses the global simp set. This includes standard arithmetic identities, logical simplifications, and...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.18 Rewriting of Functions and Extensionality

4.18 Rewriting of Functions and Extensionality Equality between functions requires a different treatment than equality between values. In Lean, two functions are equal when they produce equal outputs for all inputs. This principle is formalized by function extensionality . Function extensionality The core lemma is: funext : (∀ x, f x = g x) → f = g It reduces function equality to pointwise equality. To prove f = g...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.10 Rewriting with Lemmas

4.10 Rewriting with Lemmas Lemmas provide reusable equalities that drive most rewriting. In Lean, a well-shaped lemma doubles as a rewrite rule. The focus here is on selecting, orienting, and instantiating lemmas so that rw and simp behave deterministically. A lemma has a type that ends in an equality, possibly with parameters: Nat.add_comm : ∀ a b : Nat, a + b = b + a Using such a lemma...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.3 Reflexivity, Symmetry, and Transitivity

4.3 Reflexivity, Symmetry, and Transitivity Propositional equality in Lean is generated from a small set of core operations. These operations form the algebra of equality: reflexivity introduces equality, symmetry reverses it, and transitivity composes it. Every equality proof is built from these primitives, either directly or through derived tactics. Reflexivity is the base constructor. The term rfl has type a = a . It succeeds when both sides of the...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.4 Congruence and Contextual Rewriting

4.4 Congruence and Contextual Rewriting Equality becomes useful when it propagates through larger expressions. Congruence provides this propagation. It lifts an equality a = b into equalities of the form f a = f b , and more generally into equalities inside structured contexts. In Lean, congruence is the bridge between local equalities and global goals. The basic combinator is congrArg . Given a function f and a proof h...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.14 Dependent Rewriting and Transport

4.14 Dependent Rewriting and Transport When types depend on values, rewriting affects both terms and their types. In Lean, this is handled by transport : moving a term across an equality in an indexed family. Ordinary rw works when the dependency is shallow; deeper dependencies require explicit alignment of indices or use of transport-oriented combinators. Consider a dependent predicate P : Nat -> Prop . Given h : a =...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.9 Rewriting with Hypotheses

4.9 Rewriting with Hypotheses In most proofs, equalities come from the local context. A hypothesis h : a = b is a rewrite rule that you control. The tactic rw applies it directly; simp can use it as part of normalization. This section focuses on disciplined use of hypotheses to keep proofs local and predictable. The basic use is direct replacement in the goal: example (a b : Nat) (h...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.17 Rewriting in Structures and Records

4.17 Rewriting in Structures and Records Structures package multiple fields into a single value. Rewriting with them requires attention to projections, constructors, and extensionality. In Lean, most equalities between structures reduce to equalities between their fields. Projection-based rewriting Given a structure: structure Point where x : Nat y : Nat and a hypothesis h : p = q , rewriting propagates through projections: example (p q : Point) (h :...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.12 Rewriting Under Binders

4.12 Rewriting Under Binders Rewriting becomes more subtle when the target term appears inside a binder such as a lambda, a universal quantifier, or an existential. In these cases, the occurrence is not directly accessible to rw because the term is abstracted over a variable. In Lean, the standard approach is to expose the body of the binder before rewriting. The simplest example is function equality. Suppose you want to...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.8 Case Analysis and Rewriting

4.8 Case Analysis and Rewriting Case analysis splits a goal according to the structure of a value. In Lean, it is performed with cases or pattern matching. Rewriting then proceeds independently in each branch. The combination is common: expose structure first, then normalize each case. The basic pattern: example (n : Nat) : n = 0 ∨ n ≠ 0 := by cases n with | zero => left rfl...

Programming › Lean ›

Chapter 4. Equality and Rewriting

Chapter 4. Equality and Rewriting This chapter isolates the operational core of reasoning in Type Theory as implemented by Lean: equality and its use as a transport mechanism. Most nontrivial proofs in Lean reduce to a controlled sequence of rewrites. The objective here is to make rewriting predictable, terminating, and compositional. Lean exposes two layers of equality. Definitional equality is handled by the kernel through computation. Expressions that reduce to...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.1 Definitional Equality

4.1 Definitional Equality Definitional equality is the built-in notion of equality used by the kernel of Lean. Two expressions are definitionally equal when they reduce to the same normal form by computation. This reduction is automatic and does not require a proof term. In practice, this is the mechanism that allows many goals to close with rfl . The reduction system includes several standard rules. Beta reduction applies when a...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.20 Decidable Equality and Boolean Bridges

4.20 Decidable Equality and Boolean Bridges Reasoning often alternates between propositional equality a = b and boolean equality a == b . In Lean, this bridge is mediated by decidable equality . It allows you to move between computation and proof. Decidable equality A type has decidable equality if for any a b : α , you can decide whether a = b or a ≠ b . This is...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.24 Rewriting Strategies and Heuristics

4.24 Rewriting Strategies and Heuristics Rewriting is most effective when guided by a small set of consistent strategies. In Lean, uncontrolled rewriting leads to fragile proofs and poor performance. This section consolidates practical heuristics for predictable, scalable use. Normalize to canonical forms Choose a canonical representation and drive all expressions toward it. Examples: Eliminate neutral elements: a + 0 → a Normalize constructors: prefer Nat.succ at the outermost level Fix...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.21 Rewriting in Pattern Matching

4.21 Rewriting in Pattern Matching Pattern matching performs case analysis by selecting a branch based on the shape of a value. Rewriting interacts with pattern matching in two ways: it can simplify the scrutinee so that a branch is selected, and it can normalize expressions inside branches after the match is exposed. In Lean, effective use of rewriting around matches reduces many goals to definitional equality. Simplifying the scrutinee When...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.23 Rewriting in Goals vs Hypotheses

4.23 Rewriting in Goals vs Hypotheses Rewriting can target either the goal or the local context. The choice affects proof shape, automation, and stability. In Lean, both are first-class operations; disciplined use keeps proofs linear and predictable. Rewriting the goal Rewriting the goal transforms the target statement directly: example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by rw [h]...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.22 Rewriting with `conv`

4.22 Rewriting with conv The conv tactic provides fine-grained control over rewriting by allowing you to navigate inside an expression and apply transformations at a precise location. In Lean, conv is used when rw or simp either affect too much or fail to reach the intended subterm. Basic structure A conv block focuses on a specific part of the goal: conv => lhs rw [h] This restricts rewriting to the...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.19 Proof Irrelevance and Equality of Proofs

4.19 Proof Irrelevance and Equality of Proofs In Lean, propositions live in Prop , a universe where proof irrelevance holds. This means that any two proofs of the same proposition are considered equal. The identity of a proof object does not matter; only its existence matters. This property simplifies reasoning about equalities that involve proofs. Proof irrelevance principle The core idea is: h₁ h₂ : P ⟹ h₁ = h₂...

Programming › Lean › Chapter 4. Equality and Rewriting ›

4.25 Common Pitfalls and Debugging

4.25 Common Pitfalls and Debugging Rewriting failures in Lean usually come from a small set of recurring issues. This section lists the typical failure modes and the corresponding fixes, with a bias toward fast diagnosis. Pattern mismatch rw [h] does nothing when the left-hand side of h does not match any subterm. -- h : a = b -- goal contains f a, but rewrite expects a Fix by matching...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.24 Simplification and Automation

Lean provides automation to reduce routine proof steps. The goal is to remove mechanical transformations while preserving the logical structure of the argument. The main tool is simp , supported by targeted tactics such as dsimp , simp_all , and lightweight automation like aesop . Problem Manual rewriting becomes repetitive: rw [Nat.add_zero] rw [Nat.zero_add] rw [Nat.add_comm] This obscures the intent. You want Lean to perform standard reductions automatically while keeping...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.25 Common Proof Mistakes and Debugging

Lean proofs fail in predictable ways. The error messages often indicate a mismatch between the goal and the available assumptions, or a misuse of tactics. Effective debugging is a disciplined process: inspect the goal, inspect the context, and identify the exact mismatch. Problem A proof does not compile. Typical symptoms: tactic failed, no goals solved type mismatch unknown identifier failed to unify You need a systematic way to locate and...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.22 Backward Reasoning

Backward reasoning starts from the goal and reduces it to simpler subgoals. Instead of building forward from assumptions, you ask: what must be true for this goal to hold? Lean supports this style through tactics like apply , refine , and introduction rules. Problem You have a goal that is not directly provable from the current context, but there exists a hypothesis or theorem whose conclusion matches the goal. P...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.23 Rewriting Strategies

Rewriting with equality is one of the most frequent operations in Lean. At scale, the challenge is not knowing that rw exists, but deciding what to rewrite, where, and in which direction so the proof remains stable and readable. Problem You have equalities available, but naive rewriting: fails because the shape does not match succeeds but makes the goal harder applies too broadly and breaks later steps You need a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.21 Forward Reasoning

Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate. This style is useful when the proof has a natural data flow: one hypothesis produces an intermediate result, another hypothesis consumes it, and the final result follows. Problem You have assumptions that can be composed, but the goal is not directly available. P Q R : Prop hp : P hPQ...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.20 Using Assumptions Effectively

An assumption is a local term that Lean may use to solve the current goal or produce another proof. In simple proofs, assumptions are often the whole proof. In larger proofs, the main work is to recognize which assumption should be applied, destructured, rewritten, or contradicted. Problem You have several hypotheses in the local context, and you need to decide how to use them. A typical context may look like...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.19 Local Context Management

The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof. Most Lean proofs are won or lost by keeping this context small enough to read and rich enough to solve the current goal. Problem You want to control which assumptions are available, how they are named, and when they should be introduced, removed, or generalized. A typical proof state looks...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.17 Proof Structuring Patterns

A Lean proof should expose the shape of the argument. The goal is not merely to make the theorem compile. The goal is to make the proof local, stable, and readable when the surrounding file changes. Problem You have a theorem that can be proved in several ways, but the proof becomes hard to read because assumptions, intermediate facts, and final construction steps are mixed together. Solution Use a simple...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.16 Introduction and Elimination Rules

Every logical connective in Lean has two sides. An introduction rule explains how to prove the connective. An elimination rule explains how to use a proof of the connective. Most beginner proof failures come from applying the wrong side of this distinction. Problem You want a mechanical method for deciding what to do next from the shape of the goal or the shape of a hypothesis. If the connective appears...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.18 Naming Conventions

Names in Lean carry meaning. They determine how easily a proof can be read, refactored, and extended. Good naming makes the structure of the argument visible without inspecting every term. Problem You want names that reflect the role of each hypothesis and intermediate result, instead of relying on generic placeholders like h , h1 , h2 . Principles Use names that encode: the proposition or structure being described the direction...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.15 Case Analysis

Case analysis is the proof pattern for using data that has more than one possible constructor. In logic, it appears most often with disjunctions, existentials, booleans, natural numbers, and inductive propositions. The basic rule is simple: if a hypothesis could have been built in several ways, prove the goal for each possible way. Problem You have a hypothesis whose type has constructors, and you want to use the information inside...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.12 Universal Quantifiers

A universal statement asserts that a property holds for every element of a type. In Lean, a proof of a universally quantified statement is a function that takes an arbitrary element and returns a proof of the property for that element. The usual notation: ∀ x : α, P x is implemented as a dependent function type. Problem You want to prove or use a statement of the form: ∀...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.14 Proof by Contradiction

Proof by contradiction is a classical proof pattern. To prove a proposition P , assume ¬ P , derive False , and conclude P . In Lean, this is usually written with by_contra . Problem You want to prove: P but the easiest route is to show that assuming ¬ P creates a contradiction. Solution Use by_contra . open Classical theorem by_contra_basic (P : Prop) (h : ¬ P ->...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.13 Classical vs Constructive Logic

Lean is constructive by default. This affects which proofs are available and what information a proof must contain. Classical reasoning can be enabled explicitly when needed. Problem You want to understand why some statements are easy to prove in mathematics but require additional assumptions in Lean, and how to control that boundary. Constructive Logic In constructive logic, a proof must provide explicit evidence. To prove ∃ x, P x ,...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.9 Rewriting with Equality

Rewriting is the main way to use equality in Lean. If you have a proof h : a = b , then rw [h] replaces matching occurrences of a with b . This is the proof assistant version of substitution. Problem You have an equality hypothesis and want to use it to simplify the goal or a hypothesis. h : a = b ⊢ a + 1 = b +...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.11 Existential Quantifiers

An existential statement says that some object exists with a given property. In Lean, a proof of Exists P contains two pieces of data: a witness and a proof that the witness satisfies the predicate. The usual mathematical notation: ∃ x, P x means: Exists (fun x => P x) Problem You want to prove or use a statement of the form: ∃ x : α, P x To prove...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.10 Symmetry and Transitivity

Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity). These operations turn isolated equalities into usable proof pipelines. Problem You have equalities in the wrong direction, or you need to combine several equalities to reach a target. Symmetry If you know: h : a = b then you can reverse it to obtain: b = a Tactic form theorem eq_sym_tactic (a b : Nat) (h : a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.8 Equality Basics

Equality expresses that two terms are identical. In Lean, equality is a proposition. A proof of a = b allows you to replace a with b in other expressions. Problem You want to prove statements involving equality or use equalities to transform goals. Core Idea Equality in Lean is written: a = b A proof of this type shows that a and b are interchangeable. Reflexivity Every term is equal...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.5 Negation

Negation represents "not". In Lean, ¬ P means that a proof of P would lead to False . So a proof of ¬ P is a function from P to False . ¬ P is notation for: P -> False Problem You want to prove or use a statement of the form: ¬ P To prove it, assume P and derive a contradiction. To use it, apply it to a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.6 False and Contradiction

False is the proposition with no constructors. It represents an impossible proof state. If the local context contains a proof of False , Lean can prove any proposition from it. Problem You want to use an impossible hypothesis to finish a proof, or you want to show that a collection of assumptions is contradictory. Solution Use cases on a proof of False . theorem false_elim_example (P : Prop) : False...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.7 True and Trivial Proofs

True is the proposition that always has a proof. It represents a goal with no mathematical content. In Lean, True has one constructor, called True.intro . Problem You want to prove a goal of the form: True or handle a hypothesis of type: h : True A proof of True is immediate. A hypothesis of type True carries no useful information. Solution Use trivial . theorem true_example : True :=...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.4 Disjunction

Disjunction represents "or". A proof of P ∨ Q contains one piece of evidence: either a proof of P or a proof of Q , tagged with the side from which it came. In Lean, disjunction behaves like a sum type for propositions. Problem You want to prove or use a statement of the form: P ∨ Q To prove it, you must choose one side and provide a proof...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.2 Implication and Functions

Implication is the first logical connective to understand in Lean because it is also the ordinary function type. A proof of P -> Q is a function that receives a proof of P and returns a proof of Q . Problem You want to prove a statement of the form: P -> Q In Lean, this means you must write a function from proofs of P to proofs of Q...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.3 Conjunction

Conjunction represents "and". A proof of P ∧ Q contains two pieces of evidence: a proof of P and a proof of Q . In Lean, conjunction behaves like a pair whose fields are logical proofs. Problem You want to prove or use a statement of the form: P ∧ Q To prove it, you must prove both sides. To use it, you may extract either side. Solution Use constructor...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.1 Propositions as Types

Lean identifies propositions with types and proofs with terms. This identification is the foundation of all proof construction in Lean. It is precise and operational. You do not reason about propositions abstractly. You construct inhabitants of types. Problem You want a model where logical statements can be manipulated with the same rules used for programs, so that proofs can be constructed, checked, and composed mechanically. Core Principle A proposition is...

Programming › Lean ›

Chapter 2. Propositions and Proofs

This chapter introduces the proof layer of Lean. The central idea is that a proposition is a type, and a proof is a term of that type. This principle is often called propositions as types. It gives Lean a uniform foundation: definitions, programs, propositions, and proofs are all checked by the same kernel. The chapter begins with implication, conjunction, disjunction, negation, truth, falsehood, equality, and quantifiers. These are the ordinary...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.24 Editor Integration

Lean is normally developed inside an editor with live feedback. The editor displays goals, local hypotheses, inferred types, and errors while the file is being written. This turns Lean from a batch compiler into an interactive proof environment. Problem You want to use the editor effectively: open the correct project, read the goal view, inspect terms, and avoid common tooling mistakes. Solution Use Visual Studio Code with the Lean extension,...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.25 Minimal Working Examples

A minimal working example is the smallest complete Lean fragment that demonstrates a definition, theorem, error, or technique. It should compile by itself inside a project, use only the imports it needs, and contain no unrelated code. Minimal examples are essential for learning, debugging, documentation, and reporting issues. Problem You want to isolate a Lean idea in a short file that another person can run and understand immediately. Solution Start...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.23 Interactive Development Workflow

Lean development is interactive. You usually do not write a complete proof or definition in one pass. You write a statement, inspect the goal, add a small step, inspect again, and continue until the file checks. This workflow is central to productive Lean use. Problem You want a reliable workflow for building definitions and proofs without guessing what Lean expects. Solution Work inside a Lake project, keep the editor goal...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.21 Error Messages and Debugging

Lean’s error messages report failed constraints during elaboration. Each message corresponds to a precise mismatch between what is required and what is available. Effective debugging means isolating the failing constraint, inspecting the local context, and adjusting types, arguments, or structure until the constraint is satisfied. Problem You encounter type errors, failed tactic steps, or unresolved instances, and you want a systematic method to diagnose and fix them. Solution Reduce the...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.22 Imports and Dependencies

Imports control what a Lean file can see. Dependencies control what a Lean project can use. Together, they define the environment in which definitions, theorems, tactics, notation, and instances are resolved. Problem You want to import declarations from other files, use external libraries, and keep project dependencies reproducible. Solution Use import at the top of a Lean file. import Std This makes declarations from Std available in the current file....

Programming › Lean › Chapter 1. Core Language and Environment ›

1.20 Holes and Goals

Lean development is driven by goals. A goal is the type of the term that Lean expects you to produce. A hole is a placeholder for a missing term. Together, they provide an interactive way to construct definitions and proofs incrementally. Problem You want to write incomplete code, inspect what Lean expects at each step, and refine it until the program or proof is complete. Solution Use _ to create...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.18 Basic Tactic Mode

Tactic mode is an interactive way to build proofs. Instead of writing a proof term directly, you write commands that transform the current goal into simpler goals. Lean checks that the final result is still a proof term of the required proposition. Problem You want to prove simple propositions by inspecting the goal, introducing assumptions, applying known facts, and closing goals step by step. Solution Use by to enter tactic...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.17 Structures and Records

A structure is a type whose values are built from named fields. Structures are used when a concept is best represented by several pieces of data grouped together. They are also the foundation for many larger interfaces in Lean, including algebraic structures, configuration records, and bundled mathematical objects. Problem You want to define a record type, construct values with named fields, access those fields, and prove simple facts about structured...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.19 Term Mode vs Tactic Mode

Lean proofs are terms. Tactic mode is a way to construct those terms incrementally. Term mode writes the final object directly. Both styles produce the same kernel-checked result. The choice affects readability, locality of reasoning, and how easily a proof evolves. Problem You want to decide when to write a proof as a term, when to use tactics, and how to translate between the two styles. Solution Recognize that every...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.16 Inductive Types Introduction

Inductive types define data by listing its constructors. Each constructor describes one way to build an element of the type. Once Lean knows the constructors, it automatically provides the principles needed to define functions by recursion and prove theorems by induction. Problem You want to define your own data types, construct values of those types, pattern match on them, and prove simple facts about them. Solution Use inductive to declare...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.12 Evaluation with `#eval`

Lean can execute many expressions during development. The command #eval asks Lean to compute an expression and print the result. This is useful for testing definitions, inspecting small examples, and confirming that executable code behaves as intended. Problem You want to run Lean expressions directly inside a source file and see their computed results. Solution Use #eval followed by an expression. #eval 2 + 3 #eval "Lean" ++ " Cookbook"...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.15 Pattern Matching Basics

Pattern matching defines functions by cases on the shape of their inputs. For inductive types such as Nat , List , and user-defined data, pattern matching is the canonical way to specify behavior and to expose structure for proofs. Problem You want to write definitions that branch on constructors, understand how patterns bind variables, and see how these definitions compile to recursors used in proofs. Solution Use pattern matching equations...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.11 Comments and Documentation

Lean files serve two readers at once: the compiler and the human maintainer. Comments and documentation strings give structure to a file without changing the mathematical content. Good comments explain intent, constraints, and design choices. They do not restate every line of code. Problem You want to document Lean code so that examples, definitions, and theorems remain understandable after the file grows. Solution Use ordinary comments for local notes and...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.14 Simple Rewriting

Rewriting replaces one expression with another using an equality. In Lean, equalities are values of type a = b . A rewrite step uses such a value to transform the current goal or a hypothesis. This is the basic mechanism behind many proofs that follow algebraic or equational reasoning. Problem You want to transform a goal by replacing a subexpression using a known equality, and you want to control the...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.13 Checking Types with `#check`

Type checking is the primary feedback mechanism in Lean. Before evaluating or proving anything, you should know the exact type of each expression. The command #check asks Lean to infer and display that type. Problem You want to understand what an expression means in Lean, diagnose type errors, and inspect functions, theorems, and intermediate terms. Solution Use #check on any expression. #check 5 #check "Lean" #check true #check Nat Typical...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.2 Project Structure with Lean and Lake

Lean development is organized around projects. A project defines a closed environment: it fixes the Lean version, declares dependencies, and specifies how code is compiled. The structure is simple, but small details determine whether imports resolve, builds succeed, and tooling behaves predictably. Problem You want a project layout that supports reproducible builds, clear module boundaries, and predictable imports. Solution Create and work inside a Lake project. The default layout produced...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.7 Types and Universes

Lean is a dependently typed system. Every expression has a type, and types themselves are classified by universes . Understanding this hierarchy explains why definitions typecheck, how polymorphism works, and why some constructions require explicit universe control. Problem You want to understand what Type , Prop , and universe levels mean, how Lean prevents paradoxes, and how to write definitions that work uniformly across many types. Solution Use #check to...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.8 Functions and Lambda Abstraction

Functions are the main form of computation in Lean. A function takes an input, produces an output, and has a type that records both the input type and the output type. Lambda abstraction is the syntax for constructing a function directly, without first giving it a global name. Problem You want to define functions, apply them to arguments, pass them to other functions, and understand the relation between named definitions...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.9 Implicit and Explicit Arguments

Lean functions often contain arguments that the user does not write. These are implicit arguments. They are reconstructed by elaboration from the surrounding context. Explicit arguments are written directly by the user. Good Lean code uses both: explicit arguments for data that matters to the reader, implicit arguments for information that Lean can infer reliably. Problem You want to understand why some arguments are written, why some are omitted, and...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.10 Notation and Infix Operators

Lean notation is ordinary syntax attached to ordinary declarations. Operators such as + , * , = , ∧ , and -> are not separate from the language of terms. They are parsed into expressions that the elaborator checks using types, namespaces, and instances. Problem You want to read and define notation, understand precedence and associativity, and avoid ambiguity when operators appear in programs and proofs. Solution Use existing notation...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.3 Files, Namespaces, and Modules

Lean organizes code as a hierarchy of modules. A module corresponds to a file, and a namespace provides a logical grouping of declarations inside that file. Correct use of files, namespaces, and imports determines whether a project remains manageable as it grows. Problem You want a consistent way to organize code so that names are predictable, imports resolve correctly, and large developments remain navigable. Solution Use a one-to-one mapping between...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.4 Basic Syntax and Expressions

Lean code is built from expressions. An expression may be a value, a function, a type, a proposition, or a proof. The same syntactic system is used for computation and reasoning, so learning the basic expression language is the first step toward writing both programs and theorems. Problem You want to read and write small Lean expressions, understand their types, and recognize how Lean parses ordinary definitions and proof terms....

Programming › Lean › Chapter 1. Core Language and Environment ›

1.5 Definitions with `def`

A definition introduces a named term together with its type. In Lean, definitions serve two roles at once: they define computations and they provide reusable building blocks for proofs. The kernel treats a definition as a constant whose value is an expression, and subsequent elaboration may unfold that value when needed. Problem You want to introduce reusable functions and constants, control how they are reduced during proofs, and understand how...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.6 Theorems with `theorem` and `lemma`

Lean treats a theorem as a named proof. The name is stored in the environment, the statement is its type, and the proof is the term assigned to that type. This is the same basic mechanism used by def , but the type of a theorem is a proposition. Problem You want to state mathematical facts, prove them, reuse them later, and understand the practical difference between theorem , lemma...

Programming › Lean ›

Chapter 1. Core Language and Environment

This chapter establishes the operational model of the Lean system. The goal is to make the interaction between code, types, and proofs explicit at a small scale, so that later constructions behave predictably. Each component introduced here appears throughout the rest of the book, often in more complex forms, so the emphasis is on exact behavior rather than surface syntax. Lean organizes work as a collection of modules compiled within...

Programming › Lean ›

Preface

This book is a working manual for the Lean proof assistant. It focuses on construction. Each section isolates a task, shows the minimal mechanism that solves it, and records the pattern in a form that you can reuse. The intent is operational fluency rather than exposition. Lean treats propositions as types and proofs as programs. This correspondence makes it possible to write proofs with the same discipline used in programming:...

Programming › Lean › Chapter 1. Core Language and Environment ›

1.1 Installation and Toolchain

Lean is distributed as a small toolchain rather than as a single editor plugin. The main pieces are the Lean compiler, the Lake build tool, the package manager configuration, and the editor integration. In normal use you install Lean once, create or open a Lake project, and let the project decide which Lean version it uses. This recipe sets up a working Lean environment and checks that the toolchain can...

Programming ›

Lean

Chapter 1. Core Language and Environment Installation and toolchain Project structure with Lean and Lake Files, namespaces, and modules Basic syntax and expressions Definitions with def Theorems with theorem and lemma Types and universes Functions and lambda abstraction Implicit and explicit arguments Notation and infix operators Comments and documentation Evaluation with #eval Checking types with #check Simple rewriting Pattern matching basics Inductive types introduction Structures and records Basic tactic mode...

#proof-assistant

4.5 Directed Rewriting with `rw`

4.2 Propositional Equality

4.16 Rewriting with Equivalences

4.15 Avoiding Rewrite Loops and Nontermination

4.6 Simplification with `simp`

4.11 Chained Rewriting and `calc`

4.13 Substitution and `subst`

4.7 Controlling the `simp` Set

4.18 Rewriting of Functions and Extensionality

4.10 Rewriting with Lemmas

4.3 Reflexivity, Symmetry, and Transitivity

4.4 Congruence and Contextual Rewriting

4.14 Dependent Rewriting and Transport

4.9 Rewriting with Hypotheses

4.17 Rewriting in Structures and Records

4.12 Rewriting Under Binders

4.8 Case Analysis and Rewriting

Chapter 4. Equality and Rewriting

4.1 Definitional Equality

4.20 Decidable Equality and Boolean Bridges

4.24 Rewriting Strategies and Heuristics

4.21 Rewriting in Pattern Matching

4.23 Rewriting in Goals vs Hypotheses

4.22 Rewriting with `conv`

4.19 Proof Irrelevance and Equality of Proofs

4.25 Common Pitfalls and Debugging

2.24 Simplification and Automation

2.25 Common Proof Mistakes and Debugging

2.22 Backward Reasoning

2.23 Rewriting Strategies

2.21 Forward Reasoning

2.20 Using Assumptions Effectively

2.19 Local Context Management

2.17 Proof Structuring Patterns

2.16 Introduction and Elimination Rules

2.18 Naming Conventions

2.15 Case Analysis

2.12 Universal Quantifiers

2.14 Proof by Contradiction

2.13 Classical vs Constructive Logic

2.9 Rewriting with Equality

2.11 Existential Quantifiers

2.10 Symmetry and Transitivity

2.8 Equality Basics

2.5 Negation

2.6 False and Contradiction

2.7 True and Trivial Proofs

2.4 Disjunction

2.2 Implication and Functions

2.3 Conjunction

2.1 Propositions as Types

Chapter 2. Propositions and Proofs

1.24 Editor Integration

1.25 Minimal Working Examples

1.23 Interactive Development Workflow

1.21 Error Messages and Debugging

1.22 Imports and Dependencies

1.20 Holes and Goals

1.18 Basic Tactic Mode

1.17 Structures and Records

1.19 Term Mode vs Tactic Mode

1.16 Inductive Types Introduction

1.12 Evaluation with `#eval`

1.15 Pattern Matching Basics

1.11 Comments and Documentation

1.14 Simple Rewriting

1.13 Checking Types with `#check`

1.2 Project Structure with Lean and Lake

1.7 Types and Universes

1.8 Functions and Lambda Abstraction

1.9 Implicit and Explicit Arguments

1.10 Notation and Infix Operators

1.3 Files, Namespaces, and Modules

1.4 Basic Syntax and Expressions

1.5 Definitions with `def`

1.6 Theorems with `theorem` and `lemma`

Chapter 1. Core Language and Environment

Preface

1.1 Installation and Toolchain