lean-tp-foundations

name: lean-tp-foundations description: Dependent type theory fundamentals for theorem proving. Use when understanding universes, Type/Prop, dependent types, or the Calculus of Constructions foundation. allowed-tools: Read, Grep, Glob

Lean 4 Theorem Proving Foundations

Dependent type theory fundamentals for theorem proving in Lean 4. Use when understanding type universes, dependent types, or the theoretical foundation of proofs.

Trigger terms: "dependent type", "universe", "Type", "Prop", "type theory", "calculus of constructions", "Lean foundations"

Core Concept

Lean is based on the Calculus of Constructions with inductive types - a dependent type theory where:

Types are first-class objects with their own types
Propositions are types in Prop
Proofs are terms inhabiting proposition types

Universe Hierarchy

Types have types, organized in levels to avoid paradoxes:

#check Nat       -- Nat : Type
#check Type      -- Type : Type 1
#check Type 1    -- Type 1 : Type 2
-- Type n : Type (n+1)  for all n

#check Prop      -- Prop : Type (special universe for propositions)

Key distinction: Prop is proof-irrelevant (all proofs of same proposition are equal).

Function Types (Right-Associative)

-- These are equivalent (currying):
Nat → Nat → Nat
Nat → (Nat → Nat)

-- Partial application:
def add : Nat → Nat → Nat := fun m n => m + n
def add5 : Nat → Nat := add 5

Dependent Types

Return type depends on argument value:

-- Length-indexed vector
def Vec (α : Type) : Nat → Type
  | 0     => Unit
  | n + 1 => α × Vec α n

#check Vec Nat 0   -- Unit
#check Vec Nat 3   -- Nat × (Nat × (Nat × Unit))

-- Dependent function type
-- Π (n : Nat), Vec Nat n  (or ∀ (n : Nat), Vec Nat n)

When to use: Type-safe operations on length-indexed structures, refined types, proof-carrying data.

Universe Polymorphism

-- Definition works at any universe level
def List.{u} (α : Type u) : Type u := ...

#check List.{0} Nat     -- List in Type
#check List.{1} Type    -- List of Types

Commands

Command	Purpose
`#check expr`	Display type
`#eval expr`	Evaluate computationally
`#print name`	Show definition
`#reduce expr`	Reduce to normal form

When to Use

Pattern	Use Case
Simple types	`Nat`, `Bool` - ordinary data
Function types	`α → β` - computations, implications
Product types	`α × β` - pairs, conjunctions
Dependent types	`(x : α) → β x` - length-indexed, refined
Universe polymorphism	Generic across all type levels

Common Mistakes

Mixing universe levels:

-- ❌ Type mismatch
def bad : Type := Type

-- ✓ Proper universe
def good : Type 1 := Type

Forgetting right-associativity:

-- ❌ Misunderstanding
-- Nat → Nat → Nat is NOT (Nat → Nat) → Nat

-- ✓ Remember: Nat → Nat → Nat = Nat → (Nat → Nat)
-- This is a curried two-argument function