functional-programming

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.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.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.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.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.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.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.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.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.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 ›

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.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.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.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.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.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.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.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.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.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.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.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.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.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 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 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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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 ›

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.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...

#functional-programming

4.17 Rewriting in Structures and Records

4.15 Avoiding Rewrite Loops and Nontermination

4.7 Controlling the `simp` Set

4.10 Rewriting with Lemmas

4.16 Rewriting with Equivalences

4.13 Substitution and `subst`

4.9 Rewriting with Hypotheses

4.4 Congruence and Contextual Rewriting

4.11 Chained Rewriting and `calc`

4.8 Case Analysis and Rewriting

4.5 Directed Rewriting with `rw`

4.12 Rewriting Under Binders

4.6 Simplification with `simp`

4.2 Propositional Equality

4.3 Reflexivity, Symmetry, and Transitivity

4.18 Rewriting of Functions and Extensionality

4.14 Dependent Rewriting and Transport

4.1 Definitional Equality

4.24 Rewriting Strategies and Heuristics

4.19 Proof Irrelevance and Equality of Proofs

4.22 Rewriting with `conv`

4.20 Decidable Equality and Boolean Bridges

4.21 Rewriting in Pattern Matching

4.25 Common Pitfalls and Debugging

4.23 Rewriting in Goals vs Hypotheses

1.23 Interactive Development Workflow

1.24 Editor Integration

1.25 Minimal Working Examples

1.21 Error Messages and Debugging

1.20 Holes and Goals

1.22 Imports and Dependencies

1.19 Term Mode vs Tactic Mode

1.17 Structures and Records

1.18 Basic Tactic Mode

1.16 Inductive Types Introduction

1.14 Simple Rewriting

1.13 Checking Types with `#check`

1.15 Pattern Matching Basics

1.12 Evaluation with `#eval`

1.11 Comments and Documentation

1.7 Types and Universes

1.9 Implicit and Explicit Arguments

1.2 Project Structure with Lean and Lake

1.10 Notation and Infix Operators

1.8 Functions and Lambda Abstraction

1.4 Basic Syntax and Expressions

1.3 Files, Namespaces, and Modules

1.6 Theorems with `theorem` and `lemma`

1.5 Definitions with `def`

1.1 Installation and Toolchain