Lean 4 (leanprover/lean4)

Lean 4

https://github.com/leanprover/lean4
Admin
Lean 4 programming language and theorem prover

Tokens:67,864
Snippets:849
Trust Score:7.8
Update:1 week ago
Show doc for...
Context Summary (auto-generated)
Raw
# Lean 4

Lean 4 is a functional programming language and interactive theorem prover developed by Microsoft Research and the Lean FRO. It is a dependently-typed language where programs and mathematical proofs are first-class citizens, enabling formal verification of software and formalization of mathematics. The language features a powerful type system with universe polymorphism, dependent types, inductive types, and type class inference. It compiles to efficient native binaries via LLVM and C, and also supports a rich metaprogramming framework that allows users to extend the language with new syntax, tactics, and automation.

The core runtime is implemented in C++ and exposes a C FFI, while most of the standard library, compiler, tactic framework, and build system (Lake) are themselves written in Lean. The standard library (`Init`) provides foundational data structures—`List`, `Array`, `BitVec`, `HashMap`, `Option`, `Result`, iterators, and more—along with an extensive tactic framework for interactive theorem proving. Lean 4 uses a bootstrapping compilation model (stage0 → stage1) and ships with Lake, a full-featured build system and package manager that supports local and remote (Git/Reservoir) dependencies.

---

## Core Language — Basic Types and Functions

### `id`, `Function.comp`, `Function.const`, `flip`

`id` is the identity function; `Function.comp` (`∘`) composes two functions; `Function.const` creates a constant function; `flip` swaps the order of a two-argument function's parameters. These are the fundamental higher-order utilities available everywhere via `Init.Prelude`.

```lean
-- Function composition
#eval (List.reverse ∘ List.drop 2) [3, 2, 4, 1]
-- [1, 4]

-- flip: swap argument order
def gt : Nat → Nat → Bool := flip Nat.ble
#eval gt 3 5   -- false (5 ≤ 3 is false)
#eval gt 5 3   -- true

-- const: ignore the argument
#eval (Function.const Bool 42) true   -- 42
#eval (Function.const Bool 42) false  -- 42

-- id with explicit type to guide inference
#check @id Nat -- Nat → Nat
example : id 5 = 5 := rfl
```

---

## Core Language — Equality and Propositions

### `Eq`, `Eq.refl`, `Eq.subst`, `HEq`

`Eq a b` (written `a = b`) is propositional equality with a single constructor `Eq.refl`. `Eq.subst` enables substituting equals for equals in any motive. `HEq` (heterogeneous equality) relates values that may have different types, used rarely.

```lean
-- Basic equality
example : 1 + 1 = 2 := rfl

-- Substitution: given h1 : a = b and h2 : p a, derive p b
example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2   -- ▸ is sugar for Eq.subst + Eq.symm

-- Eq.trans and Eq.symm
example (a b c : Nat) (hab : a = b) (hbc : b = c) : a = c :=
  Eq.trans hab hbc

-- Congruence
example (f : Nat → Nat) (h : 2 = 3) : f 2 = f 3 :=
  congrArg f h
```

---

## Core Language — Inductive Types and Pattern Matching

### `inductive`, `structure`, `deriving`

Lean's inductive types are the primary way to define new data types, including enumerations, recursive types, and structures. The `deriving` keyword automatically generates common instances.

```lean
-- Enumeration
inductive Color where
  | red | green | blue
  deriving Repr, BEq, Hashable

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

def Tree.depth : Tree α → Nat
  | .leaf        => 0
  | .node l _ r  => 1 + max l.depth r.depth

-- Structure (record type)
structure Point where
  x : Float
  y : Float
  deriving Repr

def p : Point := { x := 3.0, y := 4.0 }
def dist (p : Point) : Float := Float.sqrt (p.x^2 + p.y^2)
#eval dist p  -- 5.0

-- Pattern matching
def describeList : List α → String
  | []      => "empty"
  | [_]     => "singleton"
  | _ :: _  => "has multiple elements"
```

---

## Core Language — Type Classes and Instances

### `class`, `instance`, `inferInstance`, `inferInstanceAs`

Type classes enable ad-hoc polymorphism. `inferInstance` synthesizes an instance by typeclass search. `inferInstanceAs` is used to adjust the inferred type.

```lean
-- Define a type class
class Printable (α : Type) where
  print : α → String

-- Instance for Nat
instance : Printable Nat where
  print n := s!"Nat({n})"

-- Instance for pairs (derived from components)
instance [Printable α] [Printable β] : Printable (α × β) where
  print p := s!"({Printable.print p.1}, {Printable.print p.2})"

#eval Printable.print (3, 42)   -- "(Nat(3), Nat(42))"

-- inferInstance: synthesize any class instance
#check (inferInstance : Inhabited Nat)

-- inferInstanceAs: provide explicit target type
def D := Nat
instance : Inhabited D := inferInstanceAs (Inhabited Nat)
```

---

## Standard Library — List Operations

### `List.map`, `List.filter`, `List.foldl`, `List.foldr`, `List.find?`, `List.zip`, `List.range`

The `List` API covers mapping, filtering, folding, searching, zipping, and more. Operations are organized in `Init.Data.List`.

```lean
-- map, filter, foldl
#eval [1, 2, 3, 4].map (· * 2)          -- [2, 4, 6, 8]
#eval [1, 2, 3, 4].filter (· % 2 == 0)  -- [2, 4]
#eval [1, 2, 3, 4].foldl (· + ·) 0      -- 10

-- find?, findIdx
#eval [1, 2, 3, 4].find? (· > 2)        -- some 3
#eval ["a", "bb", "ccc"].findIdx (·.length > 1) -- 1

-- zip, unzip, zipWith
#eval List.zip [1, 2, 3] ["a", "b", "c"]
-- [(1, "a"), (2, "b"), (3, "c")]
#eval List.zipWith (· + ·) [1, 2, 3] [4, 5, 6]   -- [5, 7, 9]

-- range, partition, take, drop
#eval List.range 5         -- [0, 1, 2, 3, 4]
let (evens, odds) := [1,2,3,4,5].partition (· % 2 == 0)
-- evens = [2,4], odds = [1,3,5]
#eval [1, 2, 3, 4, 5].take 3   -- [1, 2, 3]
#eval [1, 2, 3, 4, 5].drop 3   -- [4, 5]

-- membership and any/all
#eval 3 ∈ [1, 2, 3]     -- true
#eval [2, 4, 6].all (· % 2 == 0)  -- true
#eval [1, 2, 3].any (· > 2)       -- true
```

---

## Standard Library — Array Operations

### `Array.push`, `Array.get`, `Array.set`, `Array.map`, `Array.filter`, `Array.foldl`

`Array α` is the primary mutable-style efficient array type, backed by a Lean `List` but with O(1) amortized push and indexed access.

```lean
-- Construction
let a : Array Nat := #[1, 2, 3, 4, 5]
let a2 := a.push 6         -- #[1, 2, 3, 4, 5, 6]
let a3 := a.set! 2 99      -- #[1, 2, 99, 4, 5]

-- Access
#eval a[2]!                -- 3
#eval a.get! 0             -- 1
#eval a.size               -- 5

-- Functional transformations
#eval #[1,2,3].map (· * 10)              -- #[10, 20, 30]
#eval #[1,2,3,4].filter (· % 2 == 0)    -- #[2, 4]
#eval #[1,2,3,4].foldl (· + ·) 0        -- 10

-- Array extensionality proof
example (xs ys : Array Nat)
    (h1 : xs.size = ys.size)
    (h2 : ∀ i (hi1 : i < xs.size) (hi2 : i < ys.size), xs[i] = ys[i])
    : xs = ys :=
  Array.ext h1 h2
```

---

## Standard Library — HashMap (Std.Data.HashMap)

### `HashMap.insert`, `HashMap.find?`, `HashMap.erase`, `HashMap.toList`

`Std.Data.HashMap` provides a hash map with amortized O(1) operations. It requires `BEq` and `Hashable` instances for the key type.

```lean
import Std.Data.HashMap

open Std

-- Build a map
let m : HashMap String Nat :=
  HashMap.empty
  |>.insert "alice" 30
  |>.insert "bob" 25
  |>.insert "carol" 28

-- Lookup
#eval m.find? "alice"    -- some 30
#eval m.find? "dave"     -- none
#eval m.findD "bob" 0    -- 25

-- Erase and update
let m2 := m.erase "bob"
#eval m2.contains "bob"  -- false

-- Iterate
for (k, v) in m do
  IO.println s!"{k} → {v}"

-- Convert to list (unordered)
#eval m.toList   -- [("alice", 30), ("carol", 28), ("bob", 25)] (order may vary)
```

---

## Standard Library — BitVec

### `BitVec.ofNat`, `BitVec.add`, `BitVec.and`, `BitVec.shiftLeft`, `BitVec.allOnes`, `BitVec.zero`

`BitVec n` is a fixed-width bitvector of size `n`, backed by `Fin (2^n)`. It is central to hardware verification and implements operations from the SMT-LIB `QF_BV` logic.

```lean
-- Construction
def x : BitVec 8 := BitVec.ofNat 8 255   -- 0xFF
def y : BitVec 8 := 0b10101010           -- 0xAA
def z : BitVec 8 := BitVec.allOnes 8     -- 0xFF

-- Arithmetic and bitwise
#eval x + BitVec.ofNat 8 1   -- 0x00 (wraps around)
#eval x &&& y                -- 0xAA
#eval x ||| y                -- 0xFF
#eval y ^^^ z                -- 0x55
#eval y <<< 1                -- 0x54 (shift left by 1)
#eval y >>> 1                -- 0x55 (logical shift right by 1)

-- Concatenation and extraction
def hi : BitVec 4 := 0xA
def lo : BitVec 4 := 0xB
def full : BitVec 8 := hi ++ lo   -- 0xAB
def slice := full.extractLsb 3 0  -- 0xB (bits 3..0)

-- Theorem about bitvectors proven by bv_decide
example (a b : BitVec 32) : a + b = b + a := by bv_decide
```

---

## Iterators (Std.Iterators)

### `Iterator`, `Iter.map`, `Iter.filter`, `Iter.take`, `Iter.toArray`, `Iter.forIn`

`Std.Iterators` provides lazy, composable iterators for collections. Iterators avoid building intermediate data structures and can be used with `for`-`in` loops.

```lean
import Init.Data.Iterators

open Std

-- Build an iterator from a list, chain combinators
let result :=
  [1, 2, 3, 4, 5, 6, 7, 8].iter
  |>.filter (· % 2 == 0)   -- [2, 4, 6, 8]
  |>.map (· * 10)           -- [20, 40, 60, 80]
  |>.take 3                 -- [20, 40, 60]
  |>.toArray                -- #[20, 40, 60]

-- Use in a for loop
for x in [1, 2, 3].iter.map (· * 2) do
  IO.println s!"{x}"  -- prints 2, 4, 6

-- flatMap (monadic)
let nested := #[#[1,2], #[3,4], #[5,6]]
let flat := nested.iter.flatMap (·.iter) |>.toArray
-- #[1, 2, 3, 4, 5, 6]
```

---

## Tactics — `intro`, `apply`, `exact`, `refine`

### Hypothesis introduction and term-mode proof assembly

Core tactics for interactively assembling proofs. `intro` introduces hypotheses from the goal; `apply` unifies the goal against a theorem's conclusion; `exact` closes the goal with a given term; `refine` allows holes.

```lean
-- intro: introduce multiple hypotheses
example (p q : Prop) : p → q → p := by
  intro hp _hq
  exact hp

-- apply: match goal against a theorem's conclusion
example (n : Nat) : n ≤ n + 1 := by
  apply Nat.le_succ

-- refine: leave holes with ?_
example (n : Nat) : n + 0 = n := by
  refine ?_
  exact Nat.add_zero n

-- intro with pattern matching
example (h : ∃ n : Nat, n > 0) : True := by
  intro ⟨n, _hn⟩
  trivial
```

---

## Tactics — `simp` and `simp only`

### Automated simplification with lemma sets

`simp` applies tagged `@[simp]` rewrite lemmas (and given extras) repeatedly to close or simplify the goal. `simp only` restricts to a specified set. `simpa` combines simplification with `assumption`.

```lean
-- simp closes the goal using @[simp] lemmas
example : [1, 2, 3].length = 3 := by simp

-- simp only: restrict to explicit lemmas
example (n : Nat) : n + 0 = n := by
  simp only [Nat.add_zero]

-- simp with additional hypotheses
example (h : n = 5) : n + 0 = 5 := by
  simp [h]

-- simp at hypothesis
example (h : [1, 2] ++ [3] = l) : l.length = 3 := by
  simp at h
  -- h : l = [1, 2, 3]
  simp [h]

-- simp with arithmetic
example (a b : Nat) : a + b + 0 = a + b := by simp

-- simpa: simplify goal and hypothesis simultaneously
example (h : n + 0 = 5) : n = 5 := by
  simpa using h
```

---

## Tactics — `rw` and `rewrite`

### Targeted rewriting with equalities

`rw [e]` rewrites the first occurrence of the LHS of `e` to its RHS in the goal (then applies `rfl`). `rewrite` is the same without the final `rfl` attempt. The `←` prefix reverses the direction.

```lean
-- Forward rewrite
example (h : a = b) (h2 : b = c) : a = c := by
  rw [h, h2]

-- Backward rewrite (← reverses direction)
example (h : b = a) : a + 0 = b := by
  rw [Nat.add_zero, ← h]

-- Rewrite at a hypothesis
example (h : a + 0 = b) : a = b := by
  rw [Nat.add_zero] at h
  exact h

-- Rewrite specific occurrences
example (a : Nat) : a + a = a + a := by
  rw (occs := .pos [1]) [show a = a from rfl]

-- rwa: rewrite then assumption
example (h1 : a = b) (h2 : b + 1 = c) : a + 1 = c := by
  rwa [h1]
```

---

## Tactics — `omega`

### Linear arithmetic decision procedure for integers and naturals

`omega` decides linear arithmetic goals over `Nat` and `Int` automatically. It handles inequalities, modular constraints, and arithmetic expressions.

```lean
-- Simple inequality
example (n : Nat) : n ≤ n + 1 := by omega

-- System of constraints
example (a b : Int) (h1 : a > 0) (h2 : b > a) : b ≥ 2 := by omega

-- With modular arithmetic hints
example (n : Nat) (h : n % 2 = 1) : n ≥ 1 := by omega

-- Combining multiple hypotheses
example (x y z : Nat) (hxy : x + y = 10) (hyz : y + z = 7) (hz : z = 3) : x = 6 := by
  omega

-- Negation handling
example (n : Nat) (h : ¬(n ≥ 5)) : n ≤ 4 := by omega
```

---

## Tactics — `induction` and `cases`

### Structural recursion and case analysis

`induction` applies an inductive eliminator; `cases` splits on a value's constructors without generating inductive hypotheses.

```lean
-- induction on Nat
theorem add_comm (n m : Nat) : n + m = m + n := by
  induction n with
  | zero      => simp
  | succ n ih => simp [Nat.succ_add, ih]

-- cases on Option
example (o : Option Nat) : o.isSome = true ∨ o.isNone = true := by
  cases o with
  | none   => right; rfl
  | some n => left; rfl

-- cases with hypothesis naming
example (h : n = 0 ∨ n = 1) : n ≤ 1 := by
  cases h with
  | inl h => rw [h]
  | inr h => rw [h]

-- induction on a list
theorem List.length_append (l1 l2 : List α) : (l1 ++ l2).length = l1.length + l2.length := by
  induction l1 with
  | nil        => simp
  | cons h t ih => simp [List.length_cons, ih, Nat.succ_add]
```

---

## Tactics — `decide` and `native_decide`

### Closed-form decidability for computable propositions

`decide` reduces a `Decidable` proposition to `true` or `false` using kernel reduction. `native_decide` compiles and runs the decision procedure natively for large computations.

```lean
-- decide: small decidable goals
example : 2 + 2 = 4 := by decide
example : ¬(3 > 5) := by decide
example : [1,2,3].length = 3 := by decide
example : Nat.Prime 17 := by decide

-- native_decide: computationally intensive checks
example : Nat.Prime 1000003 := by native_decide

-- Decidable equality used in a proof
example : (42 : Nat) ≠ 0 := by decide

-- decide on a finite structure
def allUnder5AreSmall : ∀ n : Fin 5, n.val < 10 := by decide
```

---

## Tactics — `bv_decide`

### Bitblasting decision procedure for BitVec

`bv_decide` proves goals about `BitVec` by translating them to Boolean satisfiability (SAT) and calling a LRAT-certified SAT solver.

```lean
-- Commutativity of bitwise AND
example (a b : BitVec 32) : a &&& b = b &&& a := by bv_decide

-- Absorption law
example (a b : BitVec 8) : a &&& (a ||| b) = a := by bv_decide

-- Shift and mask
example (x : BitVec 16) : (x &&& 0xFF00) ||| (x &&& 0x00FF) = x := by bv_decide

-- Complex arithmetic identity
example (a : BitVec 8) : a + a = a <<< 1 := by bv_decide

-- With hypotheses
example (a b : BitVec 32) (h : a &&& b = 0) : (a ||| b) ^^^ a = b := by
  bv_decide
```

---

## Tactics — `grind`

### Automated E-matching / ground rewriting tactic

`grind` is a powerful automation tactic that combines congruence closure, E-matching (instantiation of universally quantified lemmas), AC reasoning, linear arithmetic, and splitting. It subsumes many uses of `simp + omega`.

```lean
-- Basic usage: closes simple goals
example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by grind

-- With universally-quantified lemmas via @[grind]
@[grind] theorem mul_comm' (a b : Nat) : a * b = b * a := Nat.mul_comm a b

example (x y z : Nat) : x * y * z = z * (y * x) := by grind

-- Combining arithmetic and rewriting
example (a b : Int) (h1 : a > 0) (h2 : a = b + 1) : b ≥ 0 := by grind

-- grind can split on disjunctions
example (n : Nat) : n = 0 ∨ n ≥ 1 := by grind [Nat.eq_zero_or_pos]

-- With a custom simp lemma in the grind set
@[grind =] theorem add_zero' (n : Nat) : n + 0 = n := Nat.add_zero n
example (x : Nat) : x + 0 + 0 = x := by grind
```

---

## Tactics — `conv`

### Focused rewriting inside sub-expressions

The `conv` tactic block allows navigating into specific sub-expressions of a goal before applying rewrites.

```lean
-- Rewrite only the left-hand side
example (a b c : Nat) (h : a = b) : a + c = b + c := by
  conv_lhs => rw [h]

-- Navigate with lhs / rhs
example (a b : Nat) : a + b + 0 = a + b := by
  conv_rhs => rw [← Nat.add_zero (a + b)]
  rfl

-- Navigate into a function application
example (f : Nat → Nat) (h : f 0 = 1) : f 0 + 2 = 3 := by
  conv_lhs =>
    rw [h]

-- Use ring_nf or simp inside conv
example (a b : Nat) : (a + b) * 2 = 2 * a + 2 * b := by
  conv_lhs => ring_nf
  ring

-- change inside conv
example (n : Nat) : n + 0 = n := by
  conv_lhs => change n + 0
  simp
```

---

## Tactics — `ext`

### Extensionality for functions and structures

`ext` applies registered `@[ext]` lemmas to reduce equality of composed values to equality of their components.

```lean
-- Function extensionality
example (f g : Nat → Nat) (h : ∀ n, f n = g n) : f = g := by
  ext n
  exact h n

-- Structure extensionality (fields must be equal)
@[ext] structure MyPair (α β : Type) where
  fst : α
  snd : β

example (p q : MyPair Nat Nat) (h1 : p.fst = q.fst) (h2 : p.snd = q.snd) : p = q := by
  ext
  · exact h1
  · exact h2

-- Finset extensionality
example (s t : Finset Nat) (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := by
  ext x
  exact h x
```

---

## Tactics — `exact?`, `apply?`, `simp?`

### Proof search and suggestion tactics

These tactics search the library for lemmas that close the current goal (`exact?`) or can be applied to make progress (`apply?`). `simp?` suggests a minimal `simp only` call.

```lean
-- exact?: finds a lemma that closes the goal exactly
example (n : Nat) : 0 ≤ n := by
  exact?   -- suggests: exact Nat.zero_le n

-- apply?: finds a lemma whose conclusion unifies with the goal
example (h : n > 0) : n ≠ 0 := by
  apply?   -- suggests: exact Nat.not_eq_zero_of_lt h

-- simp?: suggests minimal simp only invocation
example (l : List Nat) : (l ++ []).length = l.length := by
  simp?   -- suggests: simp only [List.append_nil]

-- exact? with required lemmas
example (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c := by
  exact? using h1, h2  -- suggests: exact Nat.le_trans h1 h2
```

---

## Metaprogramming — Macros and Syntax Extensions

### `macro`, `syntax`, `macro_rules`, `notation`

Lean 4's macro system allows defining new syntax that expands to existing terms or tactics. `syntax` declares grammar rules; `macro_rules` maps syntax to expansions.

```lean
-- Simple notation macro
notation:50 a " |> " f => f a
#eval [1, 2, 3] |> List.reverse   -- [3, 2, 1]

-- Custom infix operator
infixl:65 " ⊕ " => Nat.xor
#eval 5 ⊕ 3   -- 6

-- syntax + macro_rules for a new tactic
syntax (name := myTac) "myTac" : tactic
macro_rules
  | `(tactic| myTac) => `(tactic| simp; omega)

example (n : Nat) : n + 0 ≤ n + 1 := by myTac

-- Defining a do-notation shorthand
macro "unless " cond:term " do " body:doSeq : doElem =>
  `(doElem| if !($cond) then do $body)

-- Example: new syntax for swapping
macro "swap " x:ident " " y:ident : tactic =>
  `(tactic| (have t := $x; rw [show $x = $y from by assumption] at *; rw [show $y = t from by assumption]))
```

---

## Metaprogramming — Custom Tactics via `TacticM`

### `TacticM`, `MetaM`, `getMainGoal`, `mkFreshExprMVar`, `isDefEq`

The `TacticM` monad provides access to the proof state. `MetaM` handles metavariables, unification, and definitional equality. Together they form the basis for custom tactic implementations.

```lean
import Lean.Elab.Tactic

open Lean Meta Elab Tactic

-- A custom tactic that closes goals of the form `n = n`
elab "my_rfl" : tactic => do
  let goal ← getMainGoal
  let ty ← goal.getType
  let .app (.app (.const ``Eq _) _) lhs rhs := ty
    | throwError "goal is not an equality"
  if ← isDefEq lhs rhs then
    goal.assign (← mkEqRefl lhs)
  else
    throwError "lhs and rhs are not definitionally equal"

-- Use the tactic
example : 1 + 1 = 2 := by my_rfl

-- A tactic that adds a hypothesis
elab "add_hyp" e:term : tactic => do
  let val ← elabTerm e none
  let ty ← inferType val
  let fvar ← (← getMainGoal).define `h ty val
  replaceMainGoal [fvar.snd]

example : True := by
  add_hyp (rfl : 1 = 1)
  trivial
```

---

## Metaprogramming — `#check`, `#eval`, `#print`, `#reduce`

### Interactive commands for exploration and debugging

These commands are available at the top level of a Lean file for inspecting types, evaluating expressions, printing definitions, and kernel-reducing terms.

```lean
-- #check: inspect the type of a term
#check List.map            -- List.map : (α → β) → List α → List β
#check @Eq.subst           -- Eq.subst : {α : Sort u} → {motive : α → Prop} → ...

-- #eval: evaluate to a value using the compiler
#eval [1,2,3].map (· * 2)         -- [2, 4, 6]
#eval IO.println "hello world"    -- prints: hello world

-- #print: print the full definition
#print Nat.add
-- Nat.add : Nat → Nat → Nat
-- ...

-- #print axioms: list all axioms a proof relies on
theorem my_thm : 1 + 1 = 2 := rfl
#print axioms my_thm   -- 'my_thm' does not depend on any axioms

-- #reduce: kernel-reduce a term (slow, use sparingly)
#reduce (1 + 1 : Nat)   -- 2

-- set_option pp.all true: full verbose output
set_option pp.all true in
#check @id
```

---

## Lake — Package Manager and Build System

### `lake new`, `lake build`, `lake exe`, `lake script run`, `lake update`

Lake is the official build system for Lean 4. It reads a `lakefile.toml` (or `lakefile.lean`) and manages compilation, dependencies, scripts, and artifacts.

```bash
# Create a new package
lake new myproject
cd myproject

# Build all default targets
lake build

# Run the compiled executable
lake exe myproject

# Add a dependency in lakefile.toml and fetch it
# Then run:
lake update

# Run a script defined in lakefile.lean
lake script run greet Alice

# Build only a specific target
lake build MyLib

# Build a specific module facet (e.g., C source)
lake build +MyLib.Basic:c

# Upload release artifact to GitHub
lake upload v1.0.0
```

---

## Lake — `lakefile.toml` Configuration

### Package, library, executable, and dependency declarations

A `lakefile.toml` (or `lakefile.lean`) defines the package metadata, build targets, and dependencies for a Lake project.

```toml
# lakefile.toml
name = "myproject"
version = "0.1.0"
description = "An example Lean 4 project"
license = "Apache-2.0"
defaultTargets = ["myproject"]

# Lean library target
[[lean_lib]]
name = "MyLib"
roots = ["MyLib"]
globs = ["MyLib", "MyLib.*"]

# Binary executable target
[[lean_exe]]
name = "myproject"
root = "Main"
supportInterpreter = false

# Dependency from Reservoir (package registry)
[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.x.0"

# Dependency from a local path
[[require]]
name = "utils"
path = "../utils"

# Dependency from a Git repository
[[require]]
name = "somelib"
git = "https://github.com/example/somelib"
rev = "main"
```

---

## Lake — `lakefile.lean` DSL

### `package`, `lean_lib`, `lean_exe`, `require`, `script`, `target`, `module_facet`

The Lean-based lakefile DSL provides more expressive power than TOML, including custom targets, scripts, and facet definitions.

```lean
-- lakefile.lean
import Lake
open Lake DSL

package myproject where
  version := v!"1.0.0"
  description := "My Lean project"

@[default_target]
lean_lib MyLib where
  globs := #[.submodules `MyLib]

@[default_target]
lean_exe myproject where
  root := `Main

require "leanprover-community" / "mathlib"

-- Script callable via `lake script run greet <name>`
script greet (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0

-- Custom target (builds a file)
target genHeader (pkg : NPackage _package.name) : System.FilePath := do
  let headerPath := pkg.buildDir / "generated.h"
  Job.async do
    IO.FS.writeFile headerPath "#define VERSION \"1.0.0\"\n"
    return headerPath

-- Custom module facet
module_facet myFacet (mod : Module) : FilePath := do
  Job.async do
    let srcPath := mod.srcFilePath
    -- process srcPath ...
    return mod.srcFilePath
```

---

## Do Notation and IO

### `IO`, `do`, `let`, `←`, `IO.println`, `IO.FS`, `IO.mkRef`

Lean's `do` notation desugars to monadic bind. The `IO` monad handles side effects. `IO.mkRef` creates mutable references.

```lean
-- Basic IO
def main : IO Unit := do
  let name ← IO.getLine
  IO.println s!"Hello, {name.trim}!"

-- IO.FS: file system operations
def readAndPrint (path : String) : IO Unit := do
  let contents ← IO.FS.readFile path
  IO.println contents

def writeFile (path : String) (data : String) : IO Unit := do
  IO.FS.writeFile path data

-- Mutable references via IO.mkRef
def counter : IO Unit := do
  let ref ← IO.mkRef (0 : Nat)
  for i in List.range 5 do
    ref.modify (· + i)
  let val ← ref.get
  IO.println s!"Sum = {val}"   -- Sum = 10

-- Error handling with try/catch
def safeDiv (a b : Nat) : IO Nat := do
  if b == 0 then
    throw (IO.userError "division by zero")
  return a / b

-- Using EIO and ExceptT
def runComputation : IO Unit := do
  try
    let result ← safeDiv 10 2
    IO.println s!"Result: {result}"
  catch e =>
    IO.println s!"Error: {e}"
```

---

## Command Elaboration — `def`, `theorem`, `abbrev`, `noncomputable`

### Declaring definitions and theorems

`def` introduces a computable definition; `theorem` introduces a proof (erased at runtime); `abbrev` introduces a transparent alias; `noncomputable` marks definitions that use classical logic or are otherwise not computable.

```lean
-- def: computable definition with type inference
def double (n : Nat) : Nat := n * 2
#eval double 21   -- 42

-- theorem: proof term (erased by code generator)
theorem double_even (n : Nat) : 2 ∣ double n := ⟨n, rfl⟩

-- abbrev: transparent alias (unfolds during typeclass search)
abbrev MyNat := Nat
instance : Inhabited MyNat := inferInstance  -- finds Inhabited Nat

-- noncomputable: uses classical logic (e.g., Classical.choice)
noncomputable def arbitraryNat : Nat := Classical.choice ⟨0⟩

-- where clause for local definitions
def fibonacci (n : Nat) : Nat :=
  go n 0 1
where
  go : Nat → Nat → Nat → Nat
    | 0,   a, _ => a
    | n+1, a, b => go n b (a + b)

#eval fibonacci 10   -- 55

-- Mutual recursion
mutual
  def isEven : Nat → Bool
    | 0     => true
    | n + 1 => isOdd n

  def isOdd : Nat → Bool
    | 0     => false
    | n + 1 => isEven n
end
```

---

## Well-Founded Recursion and Termination

### `termination_by`, `decreasing_by`, `partial def`

For non-structurally recursive functions, Lean requires a termination proof. `termination_by` specifies the decreasing measure; `decreasing_by` provides the proof obligation. `partial def` skips termination checking.

```lean
-- termination_by: explicit termination measure
def ackermann : Nat → Nat → Nat
  | 0,   n   => n + 1
  | m+1, 0   => ackermann m 1
  | m+1, n+1 => ackermann m (ackermann (m+1) n)
termination_by m n => (m, n)

-- decreasing_by: custom termination proof
def collatz : Nat → Nat → Nat
  | 1, steps => steps
  | n, steps =>
    if n % 2 == 0 then collatz (n / 2) (steps + 1)
    else collatz (3 * n + 1) (steps + 1)
termination_by n _ => n    -- Lean will try to prove this terminates
decreasing_by omega

-- partial def: skips termination checking (unsafe)
partial def infiniteLoop : IO Unit := do
  IO.println "looping..."
  infiniteLoop
```

---

Lean 4 is used in two primary contexts: as an interactive theorem prover for formalizing mathematics (building on libraries like Mathlib) and as a systems programming language for writing verified software. In the theorem-proving context, users write `theorem` and `lemma` declarations, interact with the goal state in an IDE (VS Code with the Lean 4 extension), and use tactics (`simp`, `omega`, `grind`, `decide`, `induction`, `rw`, `ext`, etc.) to construct proofs. The automation pipeline—from `simp` lemmas through `omega` for arithmetic, `bv_decide` for bitvectors, and `grind` for general automation—reduces manual proof effort significantly. Mathlib, the community mathematics library, provides thousands of `@[simp]` lemmas and domain-specific tactics for algebra, analysis, and combinatorics.

In the software engineering context, Lean 4 serves as both the specification and implementation language. Developers write programs in `do`-notation against the `IO` monad, define data structures using inductive types, and use Lake to manage multi-package projects. Lake's `lakefile.toml` or `lakefile.lean` DSL supports Reservoir (the Lean package registry), GitHub release prebuilds, and custom build targets. The FFI (`@[extern]`) enables interoperability with C libraries, and metaprogramming via `macro`/`syntax`/`TacticM` allows extending the language with domain-specific notation and proof automation—making Lean 4 particularly well-suited for verified compilers, hardware description, and formal security proofs.