Preface

To Contact the Author

Email Kevin Sullivan at sullivan.kevinj at gmail.com.

Why This Book

The cost of constructing formal proofs even in specialized and deeply mathematical and sofware domains is collapsing, driven by advances in proof automation and AI-assisted verification. As these costs drop, the impracticality barrier that has historically confined certified software to research and high-criticality settings crumbles.

As costs drop, demand soars. Software that carries a machine-checked correctness proof — certified software — is on the verge of becoming a mainstream engineering expectation. Attention can finally shift to where it's needed: understanding what to specify and how to specify it in the first place.

The technology that makes this possible is the constructive logic proof assistant. The leading system today is Lean 4. To obtain the benefits of certified software, one must however work in the programming language of such a system. That in turn demands fluency in data/functions types and values, and in logical/mathematical propositions and their proofs values. The reward for gaining fluency in predicate logic and mathematics far more broadly, is that it is now made executable.

A thesis underlying the structuring of this course skeleton, hardly new, is learning to program with those types on the computational side of the Curry Howard correspondence will deeply prepare students to transition to the second (forthcoming) course skeleton: Computation and proof are the same thing viewed from two angles. A program and its correctness proof are not separate artifacts. They are one. A type-correct program in Lean 4 is a proof of its specification.

CS undergraduate curricula today are generally far from ready for the coming (I expect) surge in demand for certified software engineering to include certified programming.

This document is a hypothesized conceptual skeleton for a course where specification and programming are one from day one; proof-construction is not taught or expected of students; but where automated construction of proofs of decidable propositions (itself a topic) is systematic and routine, allowing students to focus attention on the language of specification not on explicit proofs.

What This Book Is

The course is squarely intended and formulated as a programming course: not just any programming but a course in certified programming. In this course, specification and the routine treatment of proofs as data, are integral from the outset. Every function is accompanied by a proposition stating what it must do. The type checker verifies that the implementation provided by the student satisfies that proposition. A correct program, in this setting, is by definition a proof-carrying program.

We further emphasize that the course is unique in surfacing specification while submersing proof construction, not by omitting it, but by leveraging automated proof construction in Lean to relieve students of having to prove anything themselves.

The mechanism is decidability: for propositions in sufficiently constrained formal languages (propositional logic, bounded arithmetic, finite equality), a decision procedure exists that either produces a proof or reports that none can be found. Lean 4's decide term is that procedure. Students learn to recognize which propositions fall within the decidable fragment and to invoke automation confidently for those that do.

Intellectual Foundations

This curriculum stands on the shoulders of two landmark works in programming education, and is informed by a third from the proof-assistant tradition.

The primary pedagogical influence is How to Design Programs (HtDP) by Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi (MIT Press, 2nd ed., 2018; freely available at htdp.org).¹ HtDP introduced the design recipe: a systematic, step-by-step methodology in which data definitions drive function structure, signatures and purpose statements precede code, and examples serve simultaneously as specification and automated tests. This course adopts that discipline directly — description, signature, specification, examples, implementation, verification — but replaces HtDP's informal type-comment signatures and dynamic check-expect tests with machine-checked types and theorem statements verified by the Lean kernel. Where HtDP's specifications are comments, this course's specifications are proofs.

A more distant influence is Structure and Interpretation of Computer Programs (SICP) by Harold Abelson, Gerald Jay Sussman, and Julie Sussman (MIT Press, 2nd ed., 1996; freely available via MIT OpenCourseWare).² SICP's ambition — to reveal computation and language as a single unified subject, culminating in the metacircular evaluator — resonates here. Week 14's treatment of the Curry-Howard correspondence plays the same role: not a capstone curiosity, but an explanation that the whole course was already doing logic. SICP's influence on the sequencing of abstraction (higher-order functions introduced to eliminate duplication, not as a language feature) is also present, though this course follows HtDP's more graduated approach.

Another more distant reference point — noted here to clarify what this course is not — is Software Foundations by Benjamin C. Pierce et al.³ Software Foundations is the landmark text for machine-checked reasoning in a proof assistant (Coq). It is not, however, an introductory programming course: it is pitched at the graduate level, it presupposes substantial fluency in the very functional-programming concepts this course teaches, and proof construction is its central activity. This course can be understood as the missing prerequisite — the CS1 that prepares students to engage with Software Foundations (or its Lean equivalents) in a subsequent course.

What's Novel

Novel features of this curriculum, no direct precedent in existing CS1 course proposal, to our knowledge, include the following:

1. Machine-checked specifications at CS1 level. Existing courses that achieve machine-checked correctness — Software Foundations (Pierce et al.) and Programming Language Foundations in Agda (PLFA) — do so at the graduate level. This course achieves the same immediate correctness guarantee at CS1 level by automating proof construction wherever possible, so that specification — not proof — is the primary logical focus.

2. Decidability as explicit curriculum content. The question of when automation works — and why it provably cannot work for certain propositions (unbounded quantification, floating-point equality) — is named, taught, and assessed. Students graduate with a principled understanding of the automation boundary, not merely a collection of tactics.

3. The data type suite as a covert Curry-Howard curriculum. The core types — →, ×, ⊕, Unit, Empty, ∀, ∃ — were chosen precisely because they are both deeply fundamental programming types and, from another perspective, precisely the logical connectives of the generalized predicate logic of Lean. Week 14 names what students have been doing all along. The revelation is structural, not incidental.

4. The #eval → rfl → decide → theorem verification ladder. Students experience concretely what it means for verification strength to increase, from dynamic spot-checking to universally-quantified, kernel-verified proofs.

5. An explicit two-course arc. The course is designed as the computational half of a pair. CS2: Certified Proofs flips the orientation from Type to Prop; every concept ports exactly. The architecture of the sequel, indeed of natural deducation proof, is the laid down for students by the overall structure of this course.

The Sequel

The sequel,CS2: Certified Proofs, flips the orientation: from Type to Prop, from computing a value to proving a proposition. Each concept introduced here in the realm of programming — algebraic data types, recursion, higher-order functions, specifications, sets, relations, type classes — ports intact to that setting. CS2 is thus not a new subject but the same, reread from the logical side of the Curry-Howard correspondence.

What's Missing Here

In its current form this book is fairly bare bones, not particularly warm and fuzzy. It's lacking in examples of applications that are fun, linked to real work domains, graphical or interactive, etc. Further skinning of this kind would be helpful. For now its bare bones character makes discussing the core content easier, perhaps.

Realistically, the amount of material covered is likely too much except for strong students. Subsetting would be needed. Numerous topics could be elided or shortened considerably. How to distill this integral course into one that has the same effect but really fits comfortably into a single semester is a good question to address.

Contact

If you're interested in discussing these materials or CS1 2030 more generally, feel free to drop a line. My personal email is sullivan.kevinj at gmail.com.

1. Felleisen, M., Findler, R. B., Flatt, M., & Krishnamurthi, S. How to Design Programs: An Introduction to Programming and Computing, 2nd ed. MIT Press, 2018. htdp.org ↩

2. Abelson, H., Sussman, G. J., & Sussman, J. Structure and Interpretation of Computer Programs, 2nd ed. MIT Press, 1996. mitpress.mit.edu ↩

3. Pierce, B. C., et al. Software Foundations, vol. 1: Logical Foundations. Electronic textbook, 2024. softwarefoundations.cis.upenn.edu ↩

CS1

Author: Kevin Sullivan (sullivan@virginia.edu)

Affiliation: University of Virginia

Pub Date: April 15, 2026; updated 3/17/2026 (HSPD)

Draft For Comment

CS1: Programming, Certified

A 14-week course in functional programming to establish foundations for proof construction in predicate logic, set theory and the theory of relations, and beyond. This web page is mirrored, modulo updates, by the Lean 4 project at kevinsullivan/Lean4CS1.

Design Commitments

Students should emerge fluent in computational and logical types. Knowledge of proof construction is not an objective of this course. The focus is instead on certified computation: writing functions, stating their specifications as propositions, and having the machine either verify or reject them as correct implementations or not. Except in particular cases, all proof constructions are automated.

• Propositions are types from Week 0.
• decide produces proofs for decidable propositions.
• The logic progression (Bool/Prop → propositional → predicate → set/relation) is distributed across all 14 weeks.
• The Float/DecidableEq lesson appears in Week 7 as a topic.

Among the types introduced in the first thirteen weeks, the core ones — function types (→), product types (×), sum types (⊕), Unit, Empty, and the quantifier types ∀ and ∃ — were chosen precisely because they are both fundamental programming types and, from another perspective, precisely the logical connectives of the generalized predicate logic of Lean.

Types such as Option, List, and BTree are useful programming types built on top of that foundation, but the Curry-Howard correspondence itself lives in the core. Week 14 does not introduce new material; it reveals that the course has established the entire foundation for proof constructions in the follow-on course. We just flip the orientation from Type to Prop. Each
concept here — data definitions, specifications, recursion, higher-order functions, sets, relations, type classes — ports directly to the setting of proof construction.

Course Structure

Assessment Forms

Students are assessed on five competencies:

1. Specification writing: given a function and English description, write the correct Lean type expressing its specification.
2. Specification reading: given a Lean proposition, state in English what it asserts; give a satisfying and falsifying example.
3. Type inhabitation: write a term the compiler accepts at a given type.
4. Counterexample finding: given a function and an incorrect specification, find a concrete input that witnesses the mismatch.
5. Decidability identification: given a proposition, state whether decide closes it, which other term if not, and why.

Building

lake build        # compile the Lean sources
make convert      # convert .lean → .md
mdbook serve      # serve locally at http://localhost:3000

How to Study These Materials

The recommended setup is to view this rendered book alongside the Lean 4 source files in VS Code, with the Lean language server running so that you see type information and error feedback in real time.

Step 1 — Clone the repository and open it in VS Code.

git clone https://github.com/kevinsullivan/Lean4CS1.git
cd Lean4CS1
code .

Step 2 — Start the local book server. In the VS Code terminal (`Ctrl+`` or Terminal → New Terminal):

mdbook serve

This builds the book and serves it at http://localhost:3000. The server watches for changes and refreshes automatically.

Step 3 — Open the browser panel inside VS Code.

1. Open the Command Palette (Cmd+Shift+P on macOS, Ctrl+Shift+P on Windows/Linux).
2. Type Simple Browser: Show and press Enter.
3. Enter http://localhost:3000 as the URL.

Step 4 — Arrange the panels side by side. Drag the Simple Browser tab to the right half of the editor area. Open the corresponding .lean source file (e.g., FPCourse/Unit1/Week00_AlgebraicTypes.lean) in the left panel. You now have the rendered prose on the right and the live, type-checked Lean source on the left.

Step 5 — Experiment. The most effective way to study is to read a section in the book, then find the corresponding code in the .lean file, hover over terms to inspect their types, and modify examples to see what the Lean kernel accepts or rejects. The exercises at the end of each chapter are meant to be worked directly in the .lean file.

Copyright © Kevin Sullivan. 2026.

-- Distillate/Unit1/Week00_TypesExpressions.lean
import Mathlib.Logic.Basic
import Mathlib.Data.Bool.Basic

Week 0: Types and Expressions

One language. Two readings.

A type classifies values. Nat classifies 0, 1, 2, 3, …. Bool classifies true and false. When you encounter a type, ask: what values inhabit this type?

This question works equally well for data and for logic.

This course is organized around six kinds of types. Every data structure in computing is built from some combination of them. Every proposition in logic is expressed by the same six constructors. This is not an analogy. It is one language with two readings.

By the end of the course you will have seen all six in both readings, and you will use one vocabulary — types and their inhabitants — for both.

namespace Week00

0.1 Basic types: atoms of computation and logic

Basic types are not constructed from anything else. They are given to you by the language. You encounter them by name.

-- Nat: natural numbers 0, 1, 2, 3, ...
#check (0 : Nat)
#check (42 : Nat)
#eval 2 + 3        -- 5
#eval 10 - 3       -- 7  (natural-number subtraction floors at 0)
#eval 10 - 15      -- 0  (not negative — Nat has no negative values)

-- Bool: exactly two values.
#check (true : Bool)
#check (false : Bool)
#eval true && false  -- false
#eval true || false  -- true
#eval !true          -- false

-- String: sequences of characters.
#check ("hello" : String)
#eval "hello" ++ ", world"   -- "hello, world"
#eval "hello".length          -- 5

0.2 The Lean notional machine

Think of Lean as a machine with one job: given an expression, apply reduction rules one step at a time until nothing more can be reduced. The irreducible result is called the normal form.

  expression  ──→  Lean kernel  ──→  normal form
   (source)        (evaluates)       (irreducible value)

Every #eval invokes this machine. Every proof you will see later runs the same machine on a decision procedure.

We write e ↝ v to mean "expression e reduces to value v in one step."

#check e inspects the type of e without evaluating it. Types are checked statically; values are produced dynamically. Both happen before you see any output.

0.3 Propositions are types; proofs are terms

Lean does something that at first looks surprising: it uses the same type machinery for logic that it uses for data.

A proposition is a claim that may or may not be true. In Lean, propositions are types. A proof of a proposition is a term of that type — the same relationship that holds between any type and its values.

A proposition with at least one proof is true. A proposition with no proof is false.

You do not need to construct proofs yourself in this course. Lean's decide term does that for you, for the class of propositions this course uses most.

-- Checking that a true proposition has a proof
#check (rfl : 1 + 1 = 2)       -- rfl : 1 + 1 = 2
#check (True.intro : True)      -- True.intro : True

-- decide: Lean evaluates a decision procedure and returns a proof (or fails)
#check (by decide : 2 + 3 = 5)
#check (by decide : true && false = false)
#check (by decide : ¬ (1 = 2))   -- negation: 1 ≠ 2

Notice: by decide is not magic. It runs the Lean reduction machine on a decision procedure — a function that outputs true or false — and, if the result is true, packages up the computation trace as a proof. You will understand exactly how this works by Week 5.

For now, the key point: when you can #eval an expression and get true, you can almost always close the corresponding proposition with by decide.

-- If #eval confirms it, decide can prove it
#eval (2 + 3 == 5)           -- true
#check (by decide : 2 + 3 = 5)  -- works: same fact, proven

-- The distinction: = is a proposition (logical claim); == is a Bool (computation)
-- = lives in Prop; the proof is a term
-- == lives in Bool; the result is a value
#check @Eq        -- Eq : α → α → Prop
#check @BEq.beq   -- BEq.beq : α → α → Bool

0.4 The Bool / Prop distinction

Bool and Prop both express "true or false" ideas, but they are different.

You will use both throughout this course:

• Bool when you need to compute a yes/no answer.
• Prop when you need to state and verify a logical claim.

The two worlds connect through Decidable: for many propositions, Lean can decide them — running a Bool computation to produce a proof. That connection is exactly what by decide exploits.

-- Bool computation: use if/then/else
def isEven (n : Nat) : Bool := n % 2 == 0

#eval isEven 4   -- true
#eval isEven 7   -- false

-- Prop claim: state and verify
#check (by decide : isEven 4 = true)
#check (by decide : isEven 7 = false)

0.5 The six constructors: a first pass

The table at the top of this week is your map for the entire course. Here is a brief first encounter with each constructor, in both readings. Subsequent weeks explore each in depth.

-- (1) Basic type: Nat — atoms that need no further construction
example : Nat := 7

-- (2) Function type: Nat → Nat — both a function and an implication
example : Nat → Nat := fun n => n + 1

-- (3) Product type: Nat × Bool — a pair, in logic also a conjunction
example : Nat × Bool := (3, true)

-- (4) Sum type: Bool ⊕ Nat — a choice, in logic also a disjunction
--   (⊕ is Sum in the Lean standard library)
example : Bool ⊕ Nat := Sum.inl true
example : Bool ⊕ Nat := Sum.inr 42

-- (5) Empty type: nothing inhabits it; in logic this is False
-- (we cannot write "example : Empty := ..." — no such term exists)
-- We can however state that:
#check (Empty)   -- Empty : Type

-- (6) α → Empty: a function TO the empty type; in logic this is negation ¬α
-- If α had an inhabitant, we could produce one of Empty — but Empty has none,
-- so this type is only inhabited when α itself is empty (false).
example : 1 = 2 → False := by decide  -- 1 ≠ 2, so this implication holds

Summary

• Every Lean expression has a type. Types classify values.
• Basic types: Nat, Bool, String — given, not constructed.
• #eval runs the reduction machine and shows the normal form.
• #check shows the type without evaluating.
• Propositions are types. Proofs are terms of propositional type.
• decide produces proofs of decidable propositions automatically.
• Bool vs Prop: computation vs. logical claim.
• Six type constructors cover all data structures and all of propositional logic. Same language, two readings.

end Week00

-- Distillate/Unit1/Week01_FunctionsImplication.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Logic.Basic

Week 1: Functions and Implication

The arrow that does double duty

The symbol → appears in two places that turn out to be one place.

Computational reading. α → β is the type of functions that take an input of type α and return a result of type β.

Logical reading. When P and Q are propositions, P → Q is the type of proofs that P implies Q. A term of this type converts any proof of P into a proof of Q.

These are not two different symbols. One symbol, two readings. A function is an implication proof. An implication proof is a function.

This identity is the heart of the Curry-Howard correspondence. We will name it explicitly in Week 8. For now, we live it.

namespace Week01

1.1 Defining functions

A function definition names the function, lists its parameters with their types, states the return type, and gives the body expression.

-- Basic function definitions
def double (n : Nat) : Nat := n * 2
def square (n : Nat) : Nat := n * n
def increment (n : Nat) : Nat := n + 1

#eval double 5      -- 10
#eval square 7      -- 49
#eval increment 0   -- 1

-- Anonymous functions (lambdas) — the same thing without a name
#eval (fun n => n * 2) 5        -- 10
#eval (fun n => n * n) 7        -- 49

-- The type of double is Nat → Nat
#check double    -- double : Nat → Nat
#check square    -- square : Nat → Nat

1.2 The reduction model for function application

When you apply a function to an argument, Lean substitutes the argument for the parameter throughout the body. This is called β-reduction.

  double 5
  ↝ (fun n => n * 2) 5      -- unfold definition
  ↝ 5 * 2                   -- β-reduction: substitute 5 for n
  ↝ 10                      -- arithmetic

Every #eval on a function application is exactly this chain of steps.

-- Multi-argument functions are curried: each argument consumed one at a time
def add (a b : Nat) : Nat := a + b

#check add        -- add : Nat → Nat → Nat
#eval add 3 4     -- 7

-- Partial application: supply only the first argument
#check add 3      -- add 3 : Nat → Nat   (still needs one more Nat)
#eval (add 3) 4   -- 7  (same as add 3 4)

Currying means: Nat → Nat → Nat is really Nat → (Nat → Nat). add 3 is a perfectly valid expression of type Nat → Nat. Supplying the second argument finishes the computation.

1.3 Type signatures as specifications

A function's type signature is more than bookkeeping. It is a machine-checked claim about what the function can accept and what it must return.

def double (n : Nat) : Nat := ...

This says: given any natural number, produce a natural number. Lean verifies that every definition lives up to its signature. The type IS the specification — enforced, not advisory.

For a stronger specification, we move from the type of the function to a proposition about it. We will explore this fully in Week 7. For now, notice that #check surfaces the type, and #eval checks the output on concrete inputs.

-- The type says what; the body says how
def max2 (a b : Nat) : Nat := if a ≥ b then a else b

#eval max2 3 7    -- 7
#eval max2 9 2    -- 9
#eval max2 5 5    -- 5

1.4 → as implication: the logical reading

When P and Q are propositions (terms of type Prop), P → Q is the claim "if P then Q." A proof of P → Q is a function that takes any proof of P and returns a proof of Q.

The syntax is identical to a function definition — because it IS a function definition.

-- Logical implication: if 1 + 1 = 2 then 2 + 2 = 4
-- A proof of this is a function from proofs of (1+1=2) to proofs of (2+2=4)
theorem implication_example : 1 + 1 = 2 → 2 + 2 = 4 :=
  fun _ => by decide   -- ignore the hypothesis; decide proves the conclusion directly

-- A more interesting implication: symmetry of equality
-- If a = b then b = a
theorem eq_symm_example (a b : Nat) : a = b → b = a :=
  fun h => h.symm       -- .symm reverses an equality proof

-- Universal quantification ∀ is also a function type
-- ∀ n : Nat, n + 0 = n   means   (n : Nat) → n + 0 = n
-- A proof is a function that takes any n and returns a proof of (n + 0 = n)
theorem add_zero_all : ∀ n : Nat, n + 0 = n :=
  fun n => Nat.add_zero n

-- decide can prove universally quantified propositions about finite domains
#check (by decide : ∀ b : Bool, b || true = true)

Unpacking the universal quantifier. The notation ∀ n : Nat, P n is definitionally equal to (n : Nat) → P n. A proof is a function. You have been writing proofs since the first example in this section.

1.5 The design recipe

Every function in this course follows the same design steps. The recipe makes specification explicit at each stage.

1. Description (English): what does the function do?
2. Signature: what are the input and output types?
3. Specification: what proposition must the function satisfy?
4. Examples: what does it do on concrete inputs?
5. Implementation: the body of the definition.

The specification step is where Lean distinguishes this course from ordinary programming. We do not merely test; we state a logical claim and (using decide for decidable propositions) verify it.

-- Example: applying the design recipe to `double`

-- 1. Description: given a natural number, return twice that number.
-- 2. Signature:
def double2 (n : Nat) : Nat :=
-- 5. Implementation:
  n * 2

-- 3. Specification (a proposition that must hold):
--    For all n, double2 n = n + n
-- 4. Examples:
#eval double2 0    -- 0
#eval double2 3    -- 6
#eval double2 10   -- 20

-- Verification: decide proves the specification for any concrete n it can check
#check (by decide : double2 0 = 0 + 0)
#check (by decide : double2 3 = 3 + 3)
#check (by decide : double2 10 = 10 + 10)

-- And universally (decide works over finite domains; Nat is infinite so
-- the universal claim needs a general proof — we'll explore this in Week 7):
theorem double2_spec : ∀ n : Nat, double2 n = n + n := by
  intro n; simp [double2]; omega

1.6 Functions to any type

Functions can map between any two types, not just Nat → Nat. They can take propositions as inputs or produce propositions as outputs. They can take types as inputs (polymorphism — more in Week 3).

-- Bool → Bool
def boolNot (b : Bool) : Bool := !b
#eval boolNot true   -- false

-- Nat → Bool (a predicate)
def isZero (n : Nat) : Bool := n == 0
#eval isZero 0   -- true
#eval isZero 5   -- false

-- String → Nat
def wordLength (w : String) : Nat := w.length
#eval wordLength "hello"   -- 5

-- Nat → String  (using Lean's built-in conversion)
def showNat (n : Nat) : String := toString n
#eval showNat 42   -- "42"

Summary

• → is the function/implication type constructor.
  • Computationally: α → β means "take an α, produce a β."
  • Logically: P → Q means "P implies Q"; a proof is a function.
• def f (x : α) : β := body defines a function named f.
• Currying: multi-argument functions α → β → γ can be partially applied.
• Reduction: applying a function substitutes the argument (β-reduction).
• ∀ x : α, P x is the dependent function type (x : α) → P x. A proof of ∀ is a function.
• The design recipe: description → signature → specification → examples → implementation. Specification is a proposition, enforced by Lean.

end Week01

-- Distillate/Unit1/Week02_ProductTypesConjunction.lean
import Mathlib.Logic.Basic
import Mathlib.Data.Prod.Basic

Week 2: Product Types and Conjunction

Bundling two things at once

The second constructor in our table is the product type α × β. A value of type α × β contains both an α and a β — held together, retrieved separately.

Computational reading. α × β is the type of pairs (a, b) where a : α and b : β. It models any situation where you need to carry two pieces of data together: a name and a score, a point's x-coordinate and y-coordinate, a key and its value.

Logical reading. When P and Q are propositions, P × Q (or equivalently P ∧ Q) is the type of proofs that P is true AND Q is true simultaneously. A term of this type packages a proof of P together with a proof of Q.

Same constructor. Two readings. One type system.

namespace Week02

2.1 Pairs: the anonymous product

The simplest product is an anonymous pair (a, b). The type is written α × β.

-- Constructing pairs
def myPair : Nat × Bool := (7, true)
def point  : Nat × Nat  := (3, 4)
def label  : String × Nat := ("score", 100)

-- Projecting: extract the first or second component
#eval myPair.1    -- 7
#eval myPair.2    -- true
#eval point.1     -- 3
#eval point.2     -- 4

-- Pairs in function types: a function that returns two things
def minMax (a b : Nat) : Nat × Nat :=
  if a ≤ b then (a, b) else (b, a)

#eval minMax 7 3    -- (3, 7)
#eval minMax 2 9    -- (2, 9)

2.2 Named products: structures

Lean's structure keyword gives names to the fields of a product. This is more readable than anonymous pairs for anything but small, transient bundles.

-- A named product: a 2D point
structure Point where
  x : Nat
  y : Nat

-- Constructing a Point
def origin : Point := { x := 0, y := 0 }
def p1     : Point := { x := 3, y := 4 }

-- Accessing fields by name
#eval p1.x    -- 3
#eval p1.y    -- 4

-- Using point in a function
def translate (p : Point) (dx dy : Nat) : Point :=
  { x := p.x + dx, y := p.y + dy }

#eval (translate p1 1 2).x   -- 4
#eval (translate p1 1 2).y   -- 6

A structure is syntactic sugar for an inductive type with a single constructor. Point is equivalent to α × β but with field names instead of .1 and .2.

The key idea: a structure value holds ALL its fields simultaneously. To have a Point, you must supply BOTH x AND y.

2.3 Product types and conjunction: the logical reading

When P and Q are propositions, P ∧ Q (read "P and Q") is the proposition that BOTH P AND Q are true.

In Lean's type theory, P ∧ Q is definitionally P × Q in Prop. A proof of P ∧ Q is a pair: a proof of P bundled with a proof of Q.

The connective ∧ is the logical reading of the same product constructor that gives you pairs and structures on the computational side.

-- A conjunction: both claims are true
#check (by decide : 1 + 1 = 2 ∧ 2 + 2 = 4)
#check (by decide : true = true ∧ false = false)

-- Constructing a conjunction manually with And.intro
-- And.intro takes a proof of P and a proof of Q; returns a proof of P ∧ Q
theorem conj_example : 1 + 1 = 2 ∧ 2 + 2 = 4 :=
  And.intro rfl rfl

-- Destructuring: if you have a proof of P ∧ Q, you can extract each part
theorem extract_left  (h : 1 + 1 = 2 ∧ 2 + 2 = 4) : 1 + 1 = 2 := h.left
theorem extract_right (h : 1 + 1 = 2 ∧ 2 + 2 = 4) : 2 + 2 = 4 := h.right

-- In practice, decide constructs the proof for decidable conjunctions
#check (by decide : 3 < 5 ∧ 5 < 10)

The table of correspondences so far:

The names differ but the structure is identical. This is not coincidence.

2.4 Proof-carrying types

One of the most powerful ideas in this course is proof-carrying types: embedding a logical condition directly into a data type.

Instead of a raw Nat, you can demand a Nat bundled together with a proof that it satisfies some property.

-- A type that packages a Nat together with a proof that it is even
def EvenNat : Type := { n : Nat // n % 2 = 0 }

-- To construct an EvenNat, you must supply the number AND the proof
def four_is_even : EvenNat := ⟨4, by decide⟩
def zero_is_even : EvenNat := ⟨0, by decide⟩

-- The value part and proof part are always available
#eval four_is_even.val    -- 4
-- four_is_even.property : 4 % 2 = 0  (a proof term, not a value to print)

The { n : Nat // P n } notation is Lean's subtype: the type of natural numbers satisfying predicate P. It is a dependent product: the proof depends on which number you chose.

This is precisely the connection between programs and specifications. When a function returns { n : Nat // n % 2 = 0 }, its return type itself guarantees the postcondition. The type IS the specification.

-- A function whose return type guarantees the postcondition
def double_with_proof (n : Nat) : { m : Nat // m = n * 2 } :=
  ⟨n * 2, rfl⟩

#eval (double_with_proof 5).val   -- 10
-- (double_with_proof 5).property : 10 = 5 * 2  (guaranteed by the type)

2.5 Products in specifications

Product types appear naturally in function specifications whenever a function must satisfy multiple independent conditions at once.

If a function f : α → β × γ must return both a β and a γ, then you can specify each component independently using ∧.

-- A function that splits a number into quotient and remainder
def divmod (n d : Nat) : Nat × Nat := (n / d, n % d)

-- Specification: both components must be correct
theorem divmod_spec (n d : Nat) (hd : d ≠ 0) :
    let (q, r) := divmod n d
    n = q * d + r ∧ r < d := by
  simp only [divmod]
  refine ⟨?_, Nat.mod_lt n (Nat.pos_of_ne_zero hd)⟩
  have h := Nat.div_add_mod n d
  rw [Nat.mul_comm] at h
  omega

#eval divmod 17 5   -- (3, 2):  17 = 3 * 5 + 2  and  2 < 5

Summary

• α × β is the product type: holds a value of type α AND a value of type β.
• Pairs: (a, b), accessed with .1 and .2.
• Structures: named fields; syntactic sugar for products.
• P ∧ Q (conjunction) is the logical reading of the same product: a proof holds a proof of P AND a proof of Q.
• And.intro constructs a conjunction; .left/.right destruct it.
• decide produces proofs of decidable conjunctions automatically.
• Proof-carrying types embed guarantees directly into the type: { n : Nat // P n } requires supplying the value AND its proof.

end Week02

-- Distillate/Unit1/Week03_SumTypesDisjunction.lean
import Mathlib.Logic.Basic

Week 3: Sum Types and Disjunction

Choosing between alternatives

The third constructor in our table is the sum type α ⊕ β. A value of type α ⊕ β contains either an α or a β — never both, never neither. To use it, you must consider both cases.

Computational reading. α ⊕ β models any situation where data comes in two distinct forms: success or failure, North or South, a number or a name. The two forms are disjoint; you know which you have.

Logical reading. When P and Q are propositions, P ∨ Q (equivalently P ⊕ Q in Prop) is the claim that AT LEAST ONE of P or Q is true. A proof must commit to which one it is establishing.

Same constructor. Two readings. One type system.

In Lean, sum types are written using the inductive keyword. Bool and Option are the canonical examples you will meet first.

namespace Week03

3.1 Bool: the simplest sum type

Bool is an inductive type with exactly two constructors, true and false. It is the sum type Unit ⊕ Unit with better names.

-- Bool is defined in the standard library as:
--   inductive Bool : Type
--     | false : Bool
--     | true  : Bool

-- To use a Bool value, you must pattern-match on it
def boolToNat (b : Bool) : Nat :=
  match b with
  | true  => 1
  | false => 0

#eval boolToNat true   -- 1
#eval boolToNat false  -- 0

-- if/then/else is syntactic sugar for match on Bool
def boolToNat' (b : Bool) : Nat := if b then 1 else 0

3.2 Defining your own sum types

The inductive keyword introduces a new type by listing its constructors — the ways to build a value of that type. A sum type has multiple constructors; a product type has one constructor with multiple fields.

Each constructor is a disjoint alternative. Together, they cover every possible value.

-- A simple enumeration: four compass directions
inductive Direction
  | North
  | South
  | East
  | West
  deriving DecidableEq

-- Pattern matching must cover all constructors
def opposite (d : Direction) : Direction :=
  match d with
  | Direction.North => Direction.South
  | Direction.South => Direction.North
  | Direction.East  => Direction.West
  | Direction.West  => Direction.East

-- open brings constructors into scope so you don't need the prefix
open Direction in
def isNorthSouth (d : Direction) : Bool :=
  match d with
  | North => true
  | South => true
  | East  => false
  | West  => false

-- Derived Bool operations: decide can reason about Direction
#check (by decide : opposite Direction.North = Direction.South)
#check (by decide : opposite (opposite Direction.East) = Direction.East)

3.3 Option: the prototypical proof-carrying sum type

Option α is one of the most important types in functional programming. It models computations that may or may not produce a value.

inductive Option (α : Type) : Type
  | none : Option α
  | some : α → Option α

none means "no value." some v means "the value v."

-- Safe list head: returns none if the list is empty
def head? (xs : List Nat) : Option Nat :=
  match xs with
  | []     => none
  | x :: _ => some x

#eval head? []          -- none
#eval head? [3, 1, 4]   -- some 3

-- Safe division: returns none if divisor is zero
def safeDiv (n d : Nat) : Option Nat :=
  if d = 0 then none else some (n / d)

#eval safeDiv 10 2    -- some 5
#eval safeDiv 10 0    -- none

-- Using an Option result: must pattern-match to handle both cases
def divOrZero (n d : Nat) : Nat :=
  match safeDiv n d with
  | none   => 0
  | some q => q

#eval divOrZero 10 2   -- 5
#eval divOrZero 10 0   -- 0

Option is a disciplined way of expressing "might fail." The type tells you that you MUST handle the none case. There is no way to access the value without writing the pattern match.

3.4 Constructors with data

Constructors can carry payloads. A sum type constructor is either a tag (nullary, like North) or a tag together with stored data (like some).

-- A result type: either an error message or a computed value
inductive Result (α : Type) : Type
  | error  : String → Result α
  | ok     : α → Result α

def safeSqrt (n : Int) : Result Float :=
  if n < 0
  then Result.error "cannot take square root of a negative number"
  else Result.ok (Float.sqrt n.toNat.toFloat)

-- Pattern-match to use the result
def showResult (r : Result Float) : String :=
  match r with
  | Result.error msg => "Error: " ++ msg
  | Result.ok v      => "Result: " ++ toString v

#eval showResult (safeSqrt 4)    -- "Result: 2.0"
#eval showResult (safeSqrt (-1)) -- "Error: cannot take sqrt of a negative number"

3.5 Disjunction: the logical reading of sum types

When P and Q are propositions, P ∨ Q (read "P or Q") is the claim that AT LEAST ONE of P or Q holds.

In Lean's type theory, P ∨ Q is definitionally P ⊕ Q in Prop. A proof of P ∨ Q is either:

• Or.inl hp — a proof that the left disjunct P holds, or
• Or.inr hq — a proof that the right disjunct Q holds.

You commit to which side you are proving. The type enforces this.

-- Proving a disjunction: commit to the true side
theorem one_lt_two_or_one_gt_two : 1 < 2 ∨ 1 > 2 :=
  Or.inl (by decide)   -- 1 < 2 is true, so take the left

theorem two_eq_two_or_two_eq_three : 2 = 2 ∨ 2 = 3 :=
  Or.inl rfl           -- take the left (2 = 2)

-- decide handles decidable disjunctions automatically
#check (by decide : 1 = 1 ∨ 1 = 2)   -- true because 1 = 1

-- Destructuring a disjunction: case split on which side holds
theorem or_elim_example (h : 1 = 1 ∨ 1 = 2) : True :=
  match h with
  | Or.inl _ => True.intro   -- left case: 1 = 1, conclusion is trivially True
  | Or.inr _ => True.intro   -- right case: 1 = 2, conclusion is trivially True

The table of correspondences so far:

Exhaustive pattern matching in code IS the completeness condition for disjunctive proofs. The compiler ensures you handle every case.

3.6 Pattern matching: the elimination form for sums

Every time you use a sum-type value, you must pattern-match. Pattern matching is the elimination rule for sum types: it consumes a sum value by handling each possible constructor.

This is not optional. You cannot reach inside a sum value without declaring what you will do with both alternatives. This exhaustiveness requirement is enforced at compile time.

-- Pattern matching on a custom inductive type
inductive Shape
  | Circle    : Float → Shape          -- radius
  | Rectangle : Float → Float → Shape -- width, height

def area (s : Shape) : Float :=
  match s with
  | Shape.Circle r       => 3.14159265 * r * r
  | Shape.Rectangle w h  => w * h

#eval area (Shape.Circle 1.0)           -- ≈ 3.14159
#eval area (Shape.Rectangle 3.0 4.0)   -- 12.0

-- If you forget a case, Lean errors:
-- def area' (s : Shape) : Float :=
--   match s with
--   | Shape.Circle r => Float.pi * r * r
--   -- ERROR: missing case Shape.Rectangle

Summary

• α ⊕ β (sum) holds either an α or a β; never both; never neither.
• inductive defines new sum types by listing constructors.
• Bool: the simplest sum — true or false.
• Option α: none (absent) or some v (present) — canonical "might fail."
• Pattern matching (match) is the elimination form for sum types; it must be exhaustive.
• P ∨ Q (disjunction) is the logical reading of the sum type: a proof commits to Or.inl (left) or Or.inr (right).
• decide produces proofs of decidable disjunctions automatically.
• Exhaustive case coverage in programs mirrors completeness in disjunctive proofs — one and the same requirement enforced by Lean.

end Week03

-- Distillate/Unit1/Week04_EmptyTypesNegation.lean
import Mathlib.Logic.Basic

Week 4: Empty Types and Negation

The type with no inhabitants

The fifth constructor in our table is Empty.

Computational reading. Empty is a type with no constructors — no values, no terms, no inhabitants whatsoever. You can declare Empty as a type, but you can never produce a value of type Empty. It is the void: not a single thing lives there.

Logical reading. False is the proposition with no proofs. A claim that is false has no witnesses. False in Lean is structurally identical to Empty — an inductive type with zero constructors.

Why does this matter? Because if you somehow had a proof of False, you could prove anything — by pattern-matching on it with zero cases. Impossibility is explosive.

The sixth constructor follows directly: α → Empty is the type of functions that, given an inhabitant of α, produce an inhabitant of Empty. Since Empty has no inhabitants, such a function could only exist if α also had no inhabitants. This is negation.

namespace Week04

4.1 The Empty type

Empty is defined with no constructors:

inductive Empty : Type
-- (no constructors)

There is no way to produce a value of type Empty. But there IS a function Empty.rec with a remarkable type:

-- Empty.rec : ∀ {α : Sort u}, Empty → α
-- Given an Empty, produce ANYTHING.
-- This is not magic — it is vacuously valid: you can never call it.
#check @Empty.rec

-- If you have an Empty, you can produce any type — vacuously
-- (This function exists but can never be called with a real argument)
def impossibleToNat : Empty → Nat := Empty.rec

-- The same pattern holds for False in Prop
-- False.elim : ∀ {α : Sort u}, False → α
-- If you have a proof of False, you can prove anything.
#check @False.elim

theorem from_false (h : False) : 1 = 2 :=
  False.elim h   -- vacuously true: h cannot exist

Why is this useful? You will never call Empty.rec or False.elim with a genuine argument — because no genuine argument can exist. Their value is precisely in case analysis: when you match on a value of an inductive type and one constructor is Empty (impossible), Lean knows that branch is unreachable, and closes it automatically.

4.2 Negation: functions to Empty

The sixth constructor is α → Empty.

In logic, the negation of a proposition P is written ¬P (read "not P"). In Lean, ¬P is definitionally equal to P → False.

¬P   :=   P → False

A proof of ¬P is a function: given any hypothetical proof of P, produce a proof of False. Since False has no proof, such a function can only exist when P is itself unprovable — i.e., when P is false.

This is the correct, constructive account of negation.

-- ¬P is definitionally P → False
#check @Not   -- Not : Prop → Prop

-- Proving ¬(1 = 2): provide a function from (1 = 2) to False
-- decide handles this for us
#check (by decide : ¬ (1 = 2))

-- Manually: if 1 = 2 were true, we could derive a contradiction
-- (Lean's discriminate/decide handle this behind the scenes)
theorem one_ne_two : ¬ (1 = 2) := by decide

-- Negation of Bool propositions
#check (by decide : ¬ (true = false))
#check (by decide : ¬ (1 + 1 = 3))

4.3 The explosion principle (ex falso quodlibet)

"From false, anything follows."

If you have a proof h : False, you can close any goal. False.elim h takes the proof of False and produces a proof of whatever type you need.

In a program, this corresponds to matching on Empty with zero cases: the match exhausts all constructors (there are none), so it trivially covers every case. The resulting function is total — it just never runs.

-- Pattern matching on Empty: zero cases needed, so it type-checks
-- (This function is total even though it seems to have no body)
def absurdFun (e : Empty) : Nat :=
  nomatch e   -- no cases needed: Empty has no constructors

-- The same for False in Prop
theorem exFalso (h : False) : 2 + 2 = 5 :=
  nomatch h   -- no cases needed

This is not a trick. It is a theorem-prover's version of the classical principle: a false hypothesis makes any implication vacuously valid. In formal logic, False → P holds for ALL P.

4.4 Negation in practice: contradictions and absurd

A common proof pattern is to derive a contradiction: you have h₁ : P and h₂ : ¬P, which together let you conclude anything.

Lean provides absurd : ∀ {a : Prop} {b : Prop}, a → ¬a → b for exactly this pattern.

-- absurd: given a proof of P and a proof of ¬P, conclude anything
theorem contradiction_example (h : 1 = 2) : 0 = 1 :=
  absurd h (by decide)   -- h claims 1=2, decide proves ¬(1=2); absurd closes goal

-- decide finds the negation automatically
#check (by decide : ¬ (2 + 3 = 7))
#check (by decide : ¬ (true && false = true))

4.5 Impossible branches in pattern matching

One of the most elegant uses of Empty/False in Lean is ruling out impossible cases. When you define a function by pattern matching, Lean sometimes allows you to assert that a constructor cannot appear.

If a constructor can only be inhabited by providing a proof of a false proposition, then that branch is unreachable, and Lean accepts a match expression with that branch omitted (or filled with nomatch).

-- An indexed type where some constructors are provably impossible
-- (A taste of dependent types — more in future courses)

-- Example: the Fin type enforces bounds
-- Fin n is the type of natural numbers strictly less than n
-- Fin 0 has no inhabitants — there is no Nat that is < 0
#check (Fin 3)    -- type of {0, 1, 2}
#check (⟨0, by decide⟩ : Fin 3)    -- 0 < 3, so 0 : Fin 3
#check (⟨2, by decide⟩ : Fin 3)    -- 2 < 3, so 2 : Fin 3

-- Fin 0 is empty: no proof of (n < 0) exists for any n
-- def absurdFin0 : Fin 0 → Nat := fun ⟨_, h⟩ => absurd h (Nat.not_lt_zero _)

4.6 Empty types in specifications

Functions to empty types matter most in specifications, even if they rarely appear in production code. When you want to say "this situation cannot occur," you state it as a function from the supposed witness to False.

Specifications that include negations (¬P) often look like:

• "this list is never empty after this operation" → ¬ (result = [])
• "these two outputs never coincide" → ¬ (f x = g x)
• "this function is injective" → ∀ x y, f x = f y → x = y

All of these can be proved by decide when the types are finite and decidable.

-- Specifications involving negation
def negate (b : Bool) : Bool := !b

-- Specification: negate never returns its input
#check (by decide : ∀ b : Bool, negate b ≠ b)

-- Specification: negate is its own inverse
#check (by decide : ∀ b : Bool, negate (negate b) = b)

-- Disequality: sometimes the specification IS a negation
#check (by decide : (0 : Nat) ≠ 1)
#check (by decide : true ≠ false)

Summary

• Empty: an inductive type with no constructors; no inhabitants. Computationally: uninhabitable. Logically: False (no proofs).
• Empty.rec / False.elim: given an Empty/False, produce any type — vacuously valid because the argument can never exist.
• Negation: ¬P is defined as P → False. A proof of ¬P is a function converting any proof of P into False.
• absurd: given h : P and h' : ¬P, conclude anything.
• Impossible branches: pattern matching on Empty requires zero cases — the exhaustiveness check is trivially satisfied.
• decide proves negations when the proposition is decidable.
• Specifications use negation to express constraints: "this cannot happen," "these are always distinct," "this function is injective."

end Week04

-- Distillate/Unit2/Week05_Recursion.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

Week 5: Recursion and Inductive Types

When the answer depends on a smaller answer

So far every function we have written terminates trivially: one step, and you are done. Most interesting computations are not like this. Computing the sum of a list requires visiting every element. Computing a factorial requires multiplying down to 1.

The way to express "repeat this until done" in functional programming is recursion: a function calls itself on a smaller input. The key guarantee Lean requires is that the input gets strictly smaller at each call — so the process always ends.

This is called structural recursion: recursion that follows the structure of an inductive data type. The base case handles the smallest possible value; the recursive case handles the constructor that builds larger values from smaller ones.

namespace Week05

5.1 Natural number recursion

Nat is an inductive type:

inductive Nat : Type
  | zero : Nat
  | succ : Nat → Nat   -- succ n is the successor of n, i.e., n + 1

Every natural number is either zero or succ n for some smaller n. A function defined by pattern matching on Nat has exactly two cases.

The slogan: a base case and a step, applied repeatedly, yields an answer for any input. This is both the definition of recursion and the content of the principle of mathematical induction.

-- Factorial: n! = n × (n-1) × ... × 1
def factorial : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

-- The recursive structure mirrors the inductive structure of Nat:
--   factorial 0 = 1                  (base case)
--   factorial (n+1) = (n+1) * factorial n  (step)

#eval factorial 0    -- 1
#eval factorial 5    -- 120
#eval factorial 10   -- 3628800

-- Fibonacci numbers
def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib n + fib (n + 1)

#eval fib 0    -- 0
#eval fib 7    -- 13
#eval fib 10   -- 55

-- Exponentiation
def pow (base : Nat) : Nat → Nat
  | 0     => 1
  | n + 1 => base * pow base n

#eval pow 2 10   -- 1024

Termination. Lean checks that every recursive call uses a strictly smaller argument. factorial n calls factorial (n-1) — that is, factorial n in the pattern n + 1 calls factorial n, which IS smaller. Lean accepts this automatically.

If your recursion does not obviously decrease, Lean will reject the definition. This guarantee means every function you define in Lean always terminates. There are no infinite loops.

5.2 Lists: the canonical recursive inductive type

A list of natural numbers is either empty or a head element prepended to a smaller list:

inductive List (α : Type) : Type
  | nil  : List α             -- the empty list, written []
  | cons : α → List α → List α  -- h :: t

Every list is either [] or h :: t for some head h and tail t. Functions on lists pattern-match on these two cases.

-- Length: count the elements
def myLength : List Nat → Nat
  | []      => 0
  | _ :: t  => 1 + myLength t

#eval myLength []           -- 0
#eval myLength [1, 2, 3]    -- 3
#eval myLength [10, 20]     -- 2

-- Sum: add all elements
def mySum : List Nat → Nat
  | []      => 0
  | h :: t  => h + mySum t

#eval mySum []           -- 0
#eval mySum [1, 2, 3]    -- 6
#eval mySum [10, 20, 30] -- 60

-- Append: join two lists
def myAppend : List Nat → List Nat → List Nat
  | [],     ys => ys
  | x :: xs, ys => x :: myAppend xs ys

#eval myAppend [1, 2] [3, 4]    -- [1, 2, 3, 4]
#eval myAppend [] [1, 2]        -- [1, 2]
#eval myAppend [1, 2] []        -- [1, 2]

-- Reverse
def myReverse : List Nat → List Nat
  | []     => []
  | h :: t => myReverse t ++ [h]

#eval myReverse [1, 2, 3, 4]   -- [4, 3, 2, 1]

5.3 Member test and search

A fundamental operation on lists is testing whether an element appears. This is a function from a value and a list to a Bool.

def myMember (x : Nat) : List Nat → Bool
  | []     => false
  | h :: t => if h == x then true else myMember x t

#eval myMember 3 [1, 2, 3, 4]   -- true
#eval myMember 5 [1, 2, 3, 4]   -- false
#eval myMember 1 []              -- false

-- The proposition version: ∈ for lists
-- x ∈ xs : Prop says "x appears in xs"
#check (3 ∈ [1, 2, 3, 4])     -- 3 ∈ [1, 2, 3, 4] : Prop
#check (by decide : 3 ∈ [1, 2, 3, 4])

5.4 Recursion on multiple arguments

Some functions need to recurse on more than one argument simultaneously, or choose which argument to decrease. A common pattern is recursion on the first list argument.

-- Zip: pair up elements from two lists
def myZip : List Nat → List Nat → List (Nat × Nat)
  | [],     _      => []
  | _,      []     => []
  | x :: xs, y :: ys => (x, y) :: myZip xs ys

#eval myZip [1, 2, 3] [10, 20, 30]   -- [(1, 10), (2, 20), (3, 30)]
#eval myZip [1, 2] [10, 20, 30]      -- [(1, 10), (2, 20)]  (shorter list wins)

-- Take: return the first n elements
def myTake : Nat → List Nat → List Nat
  | 0,     _      => []
  | _,     []     => []
  | n + 1, h :: t => h :: myTake n t

#eval myTake 3 [1, 2, 3, 4, 5]   -- [1, 2, 3]
#eval myTake 10 [1, 2, 3]         -- [1, 2, 3]  (fewer than 10 elements)

5.5 Specifications for recursive functions

Recursive functions can be given precise specifications using propositions. decide can verify these for concrete inputs.

For universally quantified statements about lists, we need either:

• decide (works when the proposition is over a decidable, finite domain)
• simp with library lemmas (for general proofs about list operations)

-- Concrete specifications verified by decide
#check (by decide : myLength [1, 2, 3] = 3)
#check (by decide : mySum [1, 2, 3] = 6)
#check (by decide : myAppend [1, 2] [3, 4] = [1, 2, 3, 4])
#check (by decide : myReverse [1, 2, 3] = [3, 2, 1])

-- Properties that hold universally (need simp/omega for general proofs)
-- e.g., length of append = sum of lengths
theorem myLength_append (xs ys : List Nat) :
    myLength (myAppend xs ys) = myLength xs + myLength ys := by
  induction xs with
  | nil       => simp [myLength, myAppend]
  | cons h t ih => simp [myLength, myAppend, ih]; omega

-- Reverse is its own inverse
theorem myReverse_reverse (xs : List Nat) :
    myReverse (myReverse xs) = xs := by
  induction xs with
  | nil       => simp [myReverse]
  | cons h t ih => simp [myReverse]; sorry  -- full proof requires auxiliary lemmas

Notice: the above proofs use induction in tactic mode. This is one case where decide cannot help (the universally quantified statement ranges over all lists, which is infinite). In this course we use decide for decidable propositions and accept standard Lean automation (simp, omega, ring) for general theorems. The goal is always to focus on the specification — what the theorem says — not on proof construction.

5.6 Totality: every function terminates

Lean accepts only total functions — functions that return an answer for every possible input. The termination checker ensures this by verifying that each recursive call uses a structurally smaller argument.

This is a guarantee, not a limitation. It means:

• No infinite loops.
• No crashes from missing cases.
• The type system can trust that f x always has a value.
• Specifications about f can use equational reasoning freely.

If you need to express a computation that might not terminate (e.g., search over an infinite space), you use Option to represent possible failure — or you prove that it always terminates in the relevant cases.

-- Lean rejects non-terminating definitions
-- def loop : Nat → Nat
--   | n => loop n   -- ERROR: failed to prove termination
-- This is a feature, not a bug.

Summary

• Structural recursion: a function calls itself on a strictly smaller argument, mirroring the inductive structure of the input type.
• Nat recursion: base case (zero) and step (succ n → ...). A base case and a step yield an answer for any input.
• List recursion: base case ([]) and step (h :: t → ...).
• Common list functions: length, sum, append, reverse, zip.
• Termination: Lean checks that every recursive call decreases the input. All defined functions are guaranteed to terminate.
• Specifications for recursive functions: decide for concrete instances; simp/omega/ring for universal statements.

end Week05

-- Distillate/Unit2/Week06_HigherOrderFunctions.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

Week 6: Higher-Order Functions

Functions as values

In Lean, functions are values. You can pass a function as an argument to another function, return a function from a function, and store a function in a data structure.

A higher-order function takes a function as an argument. The three canonical examples — map, filter, and fold — capture the three most common patterns of computation over lists. Once you can use these three fluently, you can express a remarkable range of programs without writing explicit recursion.

From the specification perspective, higher-order functions are especially important: the function argument is part of the specification. map f transforms every element using f; the specification of map refers to f as a parameter. This is parametric specification: propositions that say something about the behavior of a function in terms of the functions passed to it.

namespace Week06

6.1 Map: transforming every element

map f xs applies f to every element of xs and collects the results. The structure of the list is preserved; only the elements change.

-- map: apply f to every element
def myMap (f : Nat → Nat) : List Nat → List Nat
  | []     => []
  | h :: t => f h :: myMap f t

#eval myMap (fun n => n * 2) [1, 2, 3, 4]     -- [2, 4, 6, 8]
#eval myMap (fun n => n + 10) [1, 2, 3]        -- [11, 12, 13]
#eval myMap (fun n => n * n) [1, 2, 3, 4, 5]   -- [1, 4, 9, 16, 25]

-- The Lean standard library provides List.map for any element type
#eval List.map (· * 2) [1, 2, 3, 4]            -- [2, 4, 6, 8]
#eval List.map toString [1, 2, 3]               -- ["1", "2", "3"]

Specification of map: the Functor laws.

A correct map satisfies two laws:

1. Identity: map id xs = xs (mapping the identity does nothing)
2. Composition: map (f ∘ g) xs = map f (map g xs) (mapping a composition is the same as two passes)

These are not optional; they define what it means to be a correct map.

-- Functor identity law: verified by decide for a concrete list
#check (by decide : myMap id [1, 2, 3] = [1, 2, 3])

-- General proof (id applied elementwise does nothing)
theorem myMap_id (xs : List Nat) : myMap id xs = xs := by
  induction xs with
  | nil       => rfl
  | cons h t ih => simp [myMap, ih]

-- Functor composition law: map (f ∘ g) = map f ∘ map g
theorem myMap_comp (f g : Nat → Nat) (xs : List Nat) :
    myMap (f ∘ g) xs = myMap f (myMap g xs) := by
  induction xs with
  | nil       => rfl
  | cons h t ih => simp [myMap, Function.comp, ih]

6.2 Filter: keeping elements that satisfy a predicate

filter p xs returns the sublist of xs containing only the elements for which the predicate p returns true.

def myFilter (p : Nat → Bool) : List Nat → List Nat
  | []     => []
  | h :: t => if p h then h :: myFilter p t else myFilter p t

#eval myFilter (fun n => n % 2 == 0) [1, 2, 3, 4, 5, 6]   -- [2, 4, 6]
#eval myFilter (fun n => n > 3) [1, 2, 3, 4, 5]            -- [4, 5]
#eval myFilter (fun n => n == 0) [1, 2, 3]                  -- []

-- Standard library version
#eval List.filter (· % 2 == 0) [1, 2, 3, 4, 5, 6]   -- [2, 4, 6]

Specification of filter.

A correct filter p satisfies:

• Every element x in the output satisfies p x = true.
• Every element x that satisfies p x = true appears in the output (if it was in the input).

-- Concrete specification: filter only keeps even numbers
#check (by decide :
  myFilter (fun n => n % 2 == 0) [1, 2, 3, 4, 5, 6] = [2, 4, 6])

-- General specification: all elements of the result satisfy the predicate
theorem myFilter_subset (p : Nat → Bool) (xs : List Nat) :
    ∀ x, x ∈ myFilter p xs → p x = true := by
  induction xs with
  | nil       => simp [myFilter]
  | cons h t ih =>
    intro x hx
    simp only [myFilter] at hx
    split at hx
    · simp only [List.mem_cons] at hx
      cases hx with
      | inl heq => rw [heq]; assumption
      | inr hmem => exact ih x hmem
    · exact ih x hx

6.3 Fold: collapsing a list to a single value

fold (also called reduce) combines all elements of a list into a single result using a combining function and an initial value.

There are two variants:

• foldl (left fold): combines from left to right.
• foldr (right fold): combines from right to left.

For associative operations the result is the same; for non-associative ones it differs.

-- foldr: right fold
def myFoldr (f : Nat → Nat → Nat) (init : Nat) : List Nat → Nat
  | []     => init
  | h :: t => f h (myFoldr f init t)

-- foldl: left fold (tail-recursive; accumulator)
def myFoldl (f : Nat → Nat → Nat) (acc : Nat) : List Nat → Nat
  | []     => acc
  | h :: t => myFoldl f (f acc h) t

-- Sum via fold
#eval myFoldr (· + ·) 0 [1, 2, 3, 4]   -- 10
#eval myFoldl (· + ·) 0 [1, 2, 3, 4]   -- 10

-- Product via fold
#eval myFoldr (· * ·) 1 [1, 2, 3, 4]   -- 24
#eval myFoldl (· * ·) 1 [1, 2, 3, 4]   -- 24

-- Maximum (requires a non-empty list or a sensible default)
#eval myFoldr Nat.max 0 [3, 1, 4, 1, 5, 9, 2]   -- 9

-- Map derived from foldr: map is a special fold
def mapViaFoldr (f : Nat → Nat) (xs : List Nat) : List Nat :=
  List.foldr (fun h acc => f h :: acc) [] xs

#eval mapViaFoldr (· * 2) [1, 2, 3]   -- [2, 4, 6]

fold unifies map and filter. Both can be expressed as special cases of foldr. This means fold is the most fundamental of the three: map and filter are abbreviations.

In practice, use map when you are transforming elements, filter when you are selecting elements, and fold when you are accumulating.

6.4 Function composition and anonymous functions

Anonymous functions (fun x => ...) and function composition (∘) let you build complex transformations inline, without naming every intermediate step.

-- Composition: (f ∘ g) x = f (g x)
def doubleAndSquare : Nat → Nat := (fun n => n * n) ∘ (fun n => n * 2)
#eval doubleAndSquare 3   -- (3 * 2)² = 36

-- Point-free style: chain operations without naming the argument
def processNats : List Nat → List Nat :=
  List.map (· * 2) ∘ List.filter (· % 2 == 0)

#eval processNats [1, 2, 3, 4, 5, 6]   -- [4, 8, 12]   (keep evens, then double)

-- The same pipeline written with the pipe operator
#eval [1, 2, 3, 4, 5, 6]
  |> List.filter (· % 2 == 0)
  |> List.map (· * 2)               -- [4, 8, 12]

6.5 Polymorphic higher-order functions

The versions of map, filter, and fold above work only on List Nat. The standard library versions are polymorphic: they work on lists of any type.

The key ingredients:

• A type parameter α stands for any type.
• The function argument f : α → β transforms elements of type α into elements of type β.
• The predicate p : α → Bool tests elements of any type α.

-- Polymorphic map: List α → List β
-- (using the standard library version)
#eval List.map (fun s => s.length) ["hello", "world", "!"]   -- [5, 5, 1]
#eval List.map (· + 1) [1, 2, 3]                              -- [2, 3, 4]
#eval List.map (fun b => !b) [true, false, true]              -- [false, true, false]

-- Polymorphic filter
#eval List.filter (fun s => s.length > 3) ["hi", "hello", "bye", "world"]
-- ["hello", "world"]

-- Polymorphic fold
#eval List.foldl (fun acc s => acc ++ s ++ " ") "" ["hello", "world", "!"]
-- "hello world ! "

Specification of polymorphic map.

For polymorphic map, the Functor laws hold at every type:

• List.map id xs = xs for any xs : List α
• List.map (f ∘ g) xs = List.map f (List.map g xs)

decide cannot directly check universal polymorphic statements, but concrete instances for any specific type can be verified.

#check (by decide : List.map id [1, 2, 3] = [1, 2, 3])
#check (by decide : List.map ((· * 2) ∘ (· + 1)) [1, 2, 3] =
                    List.map (· * 2) (List.map (· + 1) [1, 2, 3]))

Summary

• Higher-order functions take functions as arguments, enabling abstraction over computation patterns.
• map f xs: apply f to every element; result is same length. Functor laws: identity and composition.
• filter p xs: keep only elements where p returns true.
• foldr f init xs / foldl f acc xs: collapse a list into one value using combining function f. Both map and filter can be expressed as foldr.
• Anonymous functions (fun x => ...) and composition (∘) build complex transformations inline.
• Polymorphic versions (List.map, List.filter, List.foldl) work on lists of any element type.
• Specifications of higher-order functions are parametric: they describe behavior in terms of the function argument.

end Week06

-- Distillate/Unit3/Week07_FormalSpecification.lean
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Perm.Basic
import Mathlib.Logic.Basic

Week 7: Formal Specification

What does it mean for a program to be correct?

Every function in this course has come with a type signature — and we have been saying that the type IS the specification. This week we make that claim precise, and introduce the full design recipe.

A specification is a formal statement of what a function must do. In Lean, specifications are propositions — types in Prop. A correct implementation is a term that inhabits that proposition.

This is the central insight of certified programming: a correct program is a proof of its specification. The type checker verifies both at once.

We also study the verification ladder: a sequence of increasingly strong ways to check that a function behaves as intended.

namespace Week07

7.1 The design recipe

The design recipe structures every function definition in five steps. We have used it informally throughout the course. Here it is in full.

1. Description (docstring): what does the function do, in English?
2. Signature: the type of the function — input and output types.
3. Specification: a proposition stating what the function must do.
4. Examples: concrete inputs and expected outputs.
5. Implementation: the body of the definition.

The signature is a necessary condition; the specification is sufficient. Lean enforces the signature automatically. The specification requires you to state and prove a theorem.

-- A fully worked example: absolute difference of two natural numbers
-- (Note: Nat subtraction floors at 0, so |a - b| needs care)

-- 1. Description
/-- `absDiff a b` computes the absolute difference |a - b|. -/
-- 2. Signature:
def absDiff (a b : Nat) : Nat :=
-- 5. Implementation:
  if a ≥ b then a - b else b - a

-- 4. Examples:
#eval absDiff 7 3    -- 4
#eval absDiff 3 7    -- 4
#eval absDiff 5 5    -- 0

-- 3. Specification: absDiff is commutative and non-negative
-- (non-negative is guaranteed by Nat; commutativity is the real claim)
theorem absDiff_comm : ∀ a b : Nat, absDiff a b = absDiff b a := by
  intro a b; simp only [absDiff]; split <;> split <;> omega

-- Verification: decide for concrete cases
#check (by decide : absDiff 7 3 = 4)
#check (by decide : absDiff 3 7 = 4)
#check (by decide : absDiff 5 5 = 0)

7.2 The verification ladder

There are four rungs on the ladder, from weakest to strongest.

  #eval          dynamic spot-check (one example)
  rfl            exact computation (type-checks only if literally equal)
  decide         decision procedure (decidable propositions, any concrete values)
  theorem        kernel-verified proof (universally quantified claims)

Each rung is strictly stronger than the one below it.

• #eval is useful but proves nothing.
• rfl proves equality by reduction to the same normal form.
• decide proves any decidable proposition, but requires finite/concrete values.
• theorem is the ultimate: Lean's kernel verifies the proof term itself.

-- Rung 1: #eval — dynamic spot check
#eval absDiff 7 3     -- 4  (we observe the output; nothing is proved)

-- Rung 2: rfl — exact computation
example : absDiff 7 3 = 4 := rfl     -- Lean reduces both sides to 4

-- Rung 3: decide — decision procedure
#check (by decide : absDiff 7 3 = 4)                     -- works
#check (by decide : absDiff 100 37 = absDiff 37 100)     -- works

-- Rung 4: theorem — universally quantified, kernel-verified
theorem absDiff_nonneg : ∀ a b : Nat, 0 ≤ absDiff a b := by
  intros; exact Nat.zero_le _

-- The ladder in one sentence: go as high as you need.
-- For this course: decide for decidable, theorem for universal.

7.3 Specifications as propositions

A specification states the relationship between inputs and outputs. It can involve:

• Equality: f x = expected_value
• Inequality: f x > 0
• Conjunction: P (f x) ∧ Q (f x) (multiple conditions at once)
• Universal quantification: ∀ x, f x = g x
• Implication: P x → Q (f x) (conditional)
• Negation: ¬ (f x = y) (something never happens)

-- Equality specification
def triple (n : Nat) : Nat := n * 3
theorem triple_spec : ∀ n, triple n = n + n + n := by
  intro n; simp [triple]; omega

-- Inequality specification
def increment (n : Nat) : Nat := n + 1
theorem increment_gt : ∀ n, increment n > n := by
  intro n; simp [increment]

-- Conjunction: two independent conditions must hold simultaneously
def sorted2 (a b : Nat) : Nat × Nat :=
  if a ≤ b then (a, b) else (b, a)

theorem sorted2_spec : ∀ a b : Nat,
    let (lo, hi) := sorted2 a b
    lo ≤ hi ∧ (lo = a ∨ lo = b) := by
  intros a b; simp only [sorted2]; split <;> constructor <;> omega

-- Decide for concrete cases of the conjunction spec
#check (by decide : let (lo, hi) := sorted2 7 3; lo ≤ hi ∧ (lo = 7 ∨ lo = 3))
#check (by decide : let (lo, hi) := sorted2 2 9; lo ≤ hi ∧ (lo = 2 ∨ lo = 9))

7.4 Specifications for sorting: a worked case study

What does it mean to sort a list correctly? This question has a precise answer: a correct sort satisfies TWO independent conditions.

1. Sorted: the output list is in non-decreasing order.
2. Permutation: the output contains exactly the same elements as the input, with the same multiplicities.

Neither condition alone is sufficient:

• A function that always returns [] satisfies (1) but not (2).
• A function that appends an extra element satisfies (2) ... no, actually it fails (2) too, but consider reversing: reverse [3, 1, 2] gives [2, 1, 3] — it satisfies (2) but not (1).

Both conditions together define correct sorting.

-- Lean's standard library provides the right tools
-- List.Pairwise r xs: every pair in xs satisfies relation r
-- List.Perm xs ys: xs and ys are permutations of each other (same elements)

-- A correct sort specification: both conditions in conjunction
def CorrectSort (sort : List Nat → List Nat) : Prop :=
  ∀ xs : List Nat,
    List.Pairwise (· ≤ ·) (sort xs) ∧ (sort xs).Perm xs

-- Insertion sort: a simple O(n²) sort
def insert (x : Nat) : List Nat → List Nat
  | []     => [x]
  | h :: t => if x ≤ h then x :: h :: t else h :: insert x t

def insertionSort : List Nat → List Nat
  | []     => []
  | h :: t => insert h (insertionSort t)

-- Examples
#eval insertionSort [3, 1, 4, 1, 5, 9, 2, 6]   -- [1, 1, 2, 3, 4, 5, 6, 9]
#eval insertionSort []                            -- []
#eval insertionSort [5, 4, 3, 2, 1]             -- [1, 2, 3, 4, 5]

-- Verify on concrete inputs with decide
#check (by decide : List.Pairwise (· ≤ ·) (insertionSort [3, 1, 4, 1, 5]))
#check (by decide : (insertionSort [3, 1, 4, 1, 5]).Perm [3, 1, 4, 1, 5])

The formal proof that insertionSort satisfies CorrectSort involves proving a series of lemmas by induction. This proof is the territory of the follow-on course. What matters for this course is:

1. You can state the specification precisely as a proposition.
2. You can verify it on concrete inputs with decide.
3. The type-checker enforces that the specification compiles.

The statement is the essential intellectual contribution.

7.5 Reading specifications

An equally important skill is reading a specification you did not write. Given a type like

∀ xs ys : List Nat, myAppend xs ys = xs ++ ys

you should be able to answer: what is this claim saying?

"For any two lists of natural numbers, myAppend xs ys produces the same result as Lean's built-in list append ++."

This is a correctness claim: it says our implementation agrees with the standard.

-- Reading exercise: what does each specification say?

-- (a) What does this say?
-- ∀ n : Nat, double n > n
-- Answer: every number doubled is strictly greater than itself.
-- (True for n ≥ 1; false for n = 0 since 0 doubled is still 0)
-- Lesson: the specification may be false — you must choose carefully.

-- (b) What does this say?
-- ∀ xs : List Nat, myLength (myReverse xs) = myLength xs
-- Answer: reversing a list does not change its length.

-- (c) What does this say?
-- ∀ f : Nat → Nat, ∀ xs : List Nat, myLength (myMap f xs) = myLength xs
-- Answer: mapping any function over a list does not change its length.

-- Verifying (b) and (c) for concrete inputs
#check (by decide : (List.reverse [1, 2, 3]).length = [1, 2, 3].length)
#check (by decide : (List.map (· * 2) [1, 2, 3]).length = [1, 2, 3].length)

7.6 The specification IS the documentation

In traditional programming, documentation lives in comments that can go out of date. In Lean, the specification is a theorem: if the code changes, the proof fails, and the discrepancy is immediately detected.

Specifications as propositions serve multiple roles simultaneously:

• Documentation: tells you what the function does.
• Testing: verified on concrete inputs by decide.
• Formal correctness proof: verified universally by the Lean kernel.
• Design guide: writing the specification before the implementation clarifies what you are trying to build.

This is why we always write the specification before the implementation. The design recipe forces this discipline.

-- Complete design recipe example: minimum of a non-empty list

/-- `listMin xs hne` returns the minimum element of `xs`,
    given a proof `hne` that `xs` is non-empty. -/
def listMin : (xs : List Nat) → xs ≠ [] → Nat
  | [x],    _  => x
  | x :: y :: rest, _ =>
      Nat.min x (listMin (y :: rest) (List.cons_ne_nil y rest))

-- Specification: the result is ≤ every element
theorem listMin_spec (xs : List Nat) (h : xs ≠ []) :
    ∀ x, x ∈ xs → listMin xs h ≤ x := by
  sorry  -- proof requires induction; deferred to follow-on course

-- Verify on concrete inputs
#check (by decide : listMin [3, 1, 4, 1, 5] (by decide) = 1)
#check (by decide : listMin [7] (by decide) = 7)

Summary

• A correct program is a proof of its specification. Types enforce the signature; theorems enforce the behavior.
• The design recipe: description → signature → specification → examples → implementation. Specification comes before code.
• The verification ladder: #eval < rfl < decide < theorem
• Specifications as propositions use equality, inequality, conjunction, implication, quantification, and negation.
• Sorting correctness: requires BOTH List.Pairwise (· ≤ ·) AND List.Perm. Neither condition alone is sufficient.
• Reading specifications is as important as writing them.
• Specifications are executable documentation: if the code breaks, the proof fails immediately.

end Week07

-- Distillate/Unit3/Week08_CurryHoward.lean
import Mathlib.Logic.Basic
import Mathlib.Data.List.Basic

Week 8: The Curry-Howard Correspondence

You have been doing logic all along

This is the week we name what you have been doing since Week 0.

Every type you have written in this course has two readings: computational and logical. Every function you have written is both a program and a proof. These are not analogies. They are identities.

The Curry-Howard correspondence (also called propositions as types or proofs as programs) states that:

Types are propositions. Terms are proofs.

This is not a philosophy. It is a mathematical theorem about the structure of type theory. Lean's type system is designed to make this identity literal: the same def keyword that defines a program also proves a theorem. There is no separate "proof mode" at the level of the type theory.

This week we:

1. Exhibit the full correspondence table.
2. Revisit every type constructor you have learned, now seeing both sides at once.
3. Explore what it means for a program to be a proof of its spec.
4. Describe the automation boundary — where decide works and why.
5. Preview what the sequel course does with the other side.

namespace Week08

8.1 The correspondence table

This table is not a list of analogies. Each row is an identity: the computational reading and the logical reading describe the same type, read two ways.

8.2 Inhabited types are true propositions

A type is inhabited when at least one term of that type exists. A proposition is true when at least one proof of it exists.

These are the same definition.

Under the correspondence:

• Nat is inhabited (by 0, 1, 2, …): it is "trivially true" as a proposition (or rather, it is too general to be interesting as a proposition — the interesting propositions are the constrained ones).
• 1 + 1 = 2 is inhabited (by rfl): this proposition is true.
• 1 + 1 = 3 is uninhabited: this proposition is false.
• Empty/False is uninhabited: there is no proof of False.
• ¬P is inhabited when P is uninhabited: ¬P is true when P is false.

-- Demonstrating inhabitation = truth
#check (rfl : 1 + 1 = 2)              -- rfl inhabits this type = proves this prop
#check (True.intro : True)             -- True.intro inhabits True
-- there is no term of type (1 + 1 = 3) — it is false

-- ¬P = P → False: proving something false
-- If 1 = 2 were provable, we could produce a False:
theorem one_ne_two : ¬ (1 = 2) := by decide
-- This is a function: given a proof of (1=2), produce False.
-- Since no proof of (1=2) exists, this function is vacuously valid.

8.3 Every function is a proof

In Lean, there is no distinction between a function definition and a theorem proof. Both are terms. Both inhabit a type. The only difference is whether we choose to read the type computationally or logically.

-- double as a FUNCTION
def double (n : Nat) : Nat := n * 2

-- double's specification as a THEOREM
-- This is also a function: given n, produce a proof that double n = n + n
theorem double_spec : ∀ n : Nat, double n = n + n := by
  intro n; simp [double]; omega

-- A function that DIRECTLY returns a proof (proof-carrying computation)
def doubleWithProof (n : Nat) : { m : Nat // m = n + n } :=
  ⟨n * 2, by omega⟩

-- The proof component is always available alongside the value
example : (doubleWithProof 5).val = 10 := rfl
-- (doubleWithProof 5).property : 10 = 5 + 5   ← this is the proof

8.4 The six constructors, both sides at once

Let us revisit each of the six type constructors introduced in Week 0, now reading each one from both sides simultaneously.

-- (1) BASIC TYPE: Nat (data) vs. propositional atoms (logic)
-- As data: values like 0, 1, 42
-- As propositions: claims like (1 + 1 = 2), (x < y)
example : Nat := 42                    -- computational
example : 1 + 1 = 2 := rfl            -- logical

-- (2) FUNCTION TYPE: α → β
-- As data: a function that computes
-- As proof: an implication — given proof of α, produce proof of β
def succ_positive : ∀ n : Nat, n + 1 > 0 := fun n => Nat.succ_pos n
-- This is simultaneously: a function Nat → (n + 1 > 0)
--                    and: a proof of ∀ n, n + 1 > 0

-- (3) PRODUCT TYPE: α × β
-- As data: holds an α AND a β simultaneously
-- As proof: conjunction — holds proof of P AND proof of Q
example : Nat × Bool := (42, true)                     -- data
example : 2 > 1 ∧ 3 > 2 := ⟨by decide, by decide⟩    -- proof

-- (4) SUM TYPE: α ⊕ β
-- As data: holds EITHER an α OR a β
-- As proof: disjunction — holds proof of P OR proof of Q
example : Bool ⊕ Nat := Sum.inl true                     -- data
example : 1 = 1 ∨ 1 = 2 := Or.inl rfl                   -- proof

-- (5) EMPTY TYPE: Empty / False
-- As data: no inhabitants — an impossible value
-- As proof: no proofs — a false proposition
-- (We cannot construct these, only prove things from them vacuously)
theorem vacuous (h : False) : 0 = 1 := False.elim h

-- (6) FUNCTION TO EMPTY: α → Empty / ¬P
-- As data: a function that produces an impossible value (only if α is also empty)
-- As proof: negation — establishes that P has no proof
example : ¬ (1 = 2) := by decide                -- logical
-- same as: (1 = 2) → False

8.5 Decidability: the automation boundary

decide works when a proposition is decidable: there exists an algorithm that always terminates and answers "provable" or "not provable."

For decidable propositions, decide runs the algorithm and packages the result as a proof term. The Lean kernel then checks the proof term (not the algorithm — just the witness) for correctness.

When does decide work?

• Equality of basic types with computable equality: Nat, Bool, String
• Bounded arithmetic: 2 + 3 = 5, 7 < 10
• Boolean predicates applied to finite values
• Finite universal quantification: ∀ b : Bool, ...
• Propositional logic connectives (∧, ∨, ¬) of decidable propositions

When does decide NOT work?

• Universally quantified claims over infinite types: ∀ n : Nat, P n (unless P is bounded or the quantifier is over a finite enumeration)
• Properties of functions in general: ∀ f : Nat → Nat, ...
• Floating-point equality: Float does not have DecidableEq because NaN ≠ NaN violates the reflexivity requirement

-- decide works here:
#check (by decide : 2 + 3 = 5)
#check (by decide : ∀ b : Bool, b || true = true)        -- Bool is finite
#check (by decide : ∀ n : Fin 10, n.val < 10)            -- Fin 10 is finite

-- decide does NOT work here (uncomment to see the error):
-- #check (by decide : ∀ n : Nat, n + 0 = n)  -- Nat is infinite

-- For infinite types, use theorem + standard tactics:
theorem add_zero_all : ∀ n : Nat, n + 0 = n := Nat.add_zero

8.6 Programs are proofs of their specifications

We close the loop on the central claim.

A function definition in Lean:

def f (x : α) : β := body

is the same thing as a proof:

theorem f : ∀ x : α, β := fun x => body

When β is a proposition (a type in Prop), the definition IS a proof. When β is a data type (a type in Type), the definition IS a program.

When β bundles data with a proof — a dependent type — the function is BOTH a program AND a proof simultaneously.

This is the unification of specification and implementation. When you write a function that returns { m : Nat // m = n * 2 }, you are not writing a program and separately a proof. You are writing one thing that is both.

-- A function that IS its own correctness proof
-- Return type bundles the value with a proof of the specification
def safeDivide (n d : Nat) (hd : d ≠ 0) :
    { q : Nat // n = q * d + n % d ∧ n % d < d } :=
  ⟨n / d, by
    constructor
    · have h := Nat.div_add_mod n d; rw [Nat.mul_comm] at h; omega
    · exact Nat.mod_lt n (Nat.pos_of_ne_zero hd)⟩

-- The definition:
--   - Computes the quotient (n / d)
--   - Simultaneously proves it satisfies the division algorithm
-- No separate proof needed.  The type IS the specification.

#eval (safeDivide 17 5 (by decide)).val     -- 3
-- (safeDivide 17 5 _).property : 17 = 3 * 5 + 2 ∧ 2 < 5  (always available)

8.7 Existential types: dependent pairs

One entry in the correspondence table we have not yet examined closely is the existential quantifier.

∃ x : α, P x (read "there exists an x of type α such that P x") is the dependent pair type: a pair ⟨witness, proof⟩ where the second component is a proof that the first component satisfies P.

This is precisely the subtype { x : α // P x } introduced in Week 2.

Under Curry-Howard:

• { x : α // P x } is the existential ∃ x : α, P x
• The witness is the data value
• The proof is the certificate of correctness

-- Existential: "there exists an even number greater than 4"
theorem exists_even_gt_4 : ∃ n : Nat, n % 2 = 0 ∧ n > 4 :=
  ⟨6, by decide⟩   -- 6 is the witness; decide proves 6 % 2 = 0 ∧ 6 > 4

-- Subtype form (computation-oriented)
def evenGt4 : { n : Nat // n % 2 = 0 ∧ n > 4 } :=
  ⟨6, by decide⟩

-- These are the same thing, one read computationally, one logically.

8.8 The two-course arc

This course has been the computational half of a pair.

In CS2, every concept from this course appears again — but the emphasis shifts from computing values to constructing proofs of the universally-quantified theorems that decide cannot touch.

The architecture of CS2 is already laid down in your understanding of this course. You know all six type constructors. You know what a proof term looks like. You know what a specification says. CS2 takes the same tools and drives them one level deeper: from automation to construction.

The central fact of this course, stated plainly: Every correct program in Lean is a proof that it satisfies its specification. Specification and implementation are one artifact, certified by the type checker.

Summary: the full correspondence

You have worked with every row in this table. The Curry-Howard correspondence is not a theorem about this course. It is what this course has been all along.

end Week08

-- FPCourse/Unit1/Week00_AlgebraicTypes.lean
import Mathlib.Logic.Basic
import Mathlib.Data.Bool.Basic

Week 0: Algebraic Types — The Language of Computation and Logic

One language. Two readings.

A type classifies values. Nat classifies the natural numbers. Bool classifies true and false. When you encounter a type, ask: what values of this type can exist?

This course is organized around six kinds of types. Every data structure in computing is built from some combination of these six. And every proposition in propositional logic is expressed by the same six constructors.

This is not an analogy. It is the same language, read two ways.

By the end of this week you will have seen all six in both readings. You will have one vocabulary — types and their inhabitants — that covers both. You do not need two languages. You are learning one.

namespace Week00

0.1 Basic Types: the atoms of computation and logic

Why basic types? Before you can build anything, you need raw material — types that are not constructed from anything else. Basic types are your atoms: given to you, not derived.

You encounter them by name: Nat, Bool, String. Their values are listed explicitly and cannot be broken down further.

-- Nat: the type of natural numbers.  Values: 0, 1, 2, 3, ...
#check (0 : Nat)
#check (42 : Nat)
#eval 2 + 3        -- 5
#eval 10 - 3       -- 7 (natural number subtraction, floors at 0)

-- Bool: two values.
#check (true : Bool)
#check (false : Bool)
#eval true && false  -- false
#eval true || false  -- true

-- String: sequences of characters.
#check ("hello" : String)
#eval "hello" ++ ", world"   -- "hello, world"
#eval "hello".length          -- 5

The Lean notional machine. Think of Lean as a machine with one job: given an expression, apply reduction rules one step at a time until no further reduction is possible. The irreducible result is the normal form.

  expression  ──→  Lean kernel  ──→  normal form
   (source)        (evaluates)       (irreducible value)

Every #eval you write invokes this machine. Every by decide runs it on a decision procedure. Every rfl succeeds because both sides of the equation reach the same normal form.

Each #eval above is a chain of named reductions:

The symbol ↝ means reduces to in one step. You will see it used throughout this course whenever a specific reduction rule is being named.

#check e inspects the type of e without evaluating it. Types are checked statically at elaboration time; values are produced dynamically at evaluation time. Both happen before you see any output.

An expression is any piece of Lean text that has a type and can be evaluated to a normal form.

The same question, two registers

We can ask of any type: what are its inhabitants?

We can ask the identical question of propositions:

A proposition with at least one inhabitant is true. A proposition with no inhabitant is false. In Lean, propositions ARE types.

-- Proofs are terms.  `rfl` inhabits `1 + 1 = 2` the way `42` inhabits `Nat`.
example : 1 + 1 = 2 := rfl   -- Evaluation: 1+1 ↝ 2, same as the right side
example : True      := True.intro

-- `decide` evaluates a decision procedure to produce a proof automatically.
example : 7 * 6 = 42       := by decide  -- Evaluation: 7*6 ↝ 42 ✓
example : 2 + 2 ≠ 5        := by decide  -- Evaluation: 2+2 ↝ 4 ≠ 5 ✓
example : 100 < 200         := by decide  -- Evaluation: comparison ↝ true ✓

-- `#check` works on proofs too.
#check (rfl : 1 + 1 = 2)    -- the type IS the proposition
#check (True.intro : True)

Evaluation. rfl proves a = b when a and b evaluate to the same normal form. 1 + 1 = 2 holds by rfl because both sides reduce to 2 — the equality is definitional, certified by computation.

Evaluation. decide works by evaluating the decision procedure for the proposition. For 7 * 6 = 42, Lean evaluates 7 * 6 to 42, confirms both sides are the same, and constructs the proof automatically. If evaluation had produced false, the file would not compile — the proof term would be absent, and the type would be uninhabited.

decide can only handle propositions for which evaluation terminates — decidable propositions. Concrete arithmetic is decidable; universal claims over all natural numbers are not. We return to this in Week 7.

0.2 Function Types: α → β

Why function types? Every transformation in programming — mapping, filtering, converting, composing — is a function. Functions are also how you prove implications: a proof of P → Q is literally a function from proofs of P to proofs of Q. Mastering → unlocks both.

  α → β

  ┌───┐           ┌───┐
  │ α │  ──f──→   │ β │
  └───┘  (apply)  └───┘

  Build:  fun a => ...   (introduce a function)
  Use:    f a            (apply it to an argument; β-reduction fires)

The arrow type α → β is the type of functions from α to β. A value of type α → β takes any input of type α and produces an output of type β.

Functions are the most fundamental type constructor. Every other construct — recursion, type classes, proofs — ultimately reduces to functions.

-- Defining functions with `def`:
def double  : Nat → Nat    := fun n => n * 2
def isZero  : Nat → Bool   := fun n => n == 0
def negate  : Bool → Bool  := fun b => !b
def greet   : String → String := fun name => "Hello, " ++ name

-- Evaluation: applying a function substitutes the argument for the parameter.
-- This substitution step is called β-reduction.
-- double 7 ↝ 7 * 2 ↝ 14        (β-reduction, then arithmetic)
-- isZero 0 ↝ 0 == 0 ↝ true      (β-reduction, then BEq)
-- greet "Alice" ↝ "Hello, " ++ "Alice" ↝ "Hello, Alice"
#eval double 7         -- 14
#eval isZero 0         -- true
#eval isZero 5         -- false
#eval greet "Alice"    -- "Hello, Alice"

-- Multi-argument functions are *curried*:
-- `Nat → Nat → Nat` means `Nat → (Nat → Nat)`.
-- Applying one argument returns a function waiting for the second.
def add : Nat → Nat → Nat := fun a b => a + b

#eval add 3 4          -- 7   (apply both arguments)
#eval (add 3) 4        -- 7   (same: add 3 is itself a Nat → Nat)

-- Named argument style (equivalent, more readable for multi-arg):
def max' (a b : Nat) : Nat := if a ≥ b then a else b

#eval max' 5 3         -- 5
#eval max' 2 8         -- 8

The logical reading: implication

When P and Q are propositions, P → Q is the type of proofs that P implies Q. A proof of P → Q is a function: given any proof of P, it returns a proof of Q.

This is not a metaphor. The same keyword (fun), the same syntax (fun h => ...), the same application rule — a proof of P → Q literally IS a function.

The identity function is simultaneously:

• Computational: given any value, return it.
• Logical: if P holds then P holds (reflexivity of implication).

-- Computational: identity function for data.
def myId (a : α) : α := a
#eval myId 42       -- 42
#eval myId "hello"  -- "hello"

-- Logical: if P holds, then P holds.
theorem p_implies_p (P : Prop) (h : P) : P := h
-- This IS the identity function, applied to a proof.

-- Implication is transitive: if P → Q and Q → R, then P → R.
-- Computation: function composition.
-- Logic: hypothetical syllogism.
theorem implies_trans (P Q R : Prop)
    (hpq : P → Q) (hqr : Q → R) : P → R :=
  fun hp => hqr (hpq hp)

-- The proof IS function composition: hqr ∘ hpq.
-- Compare with the computational version:
def compose (f : β → γ) (g : α → β) : α → γ := fun a => f (g a)

-- Their structures are identical.  The only difference is that
-- P, Q, R range over Prop instead of Type.

0.3 Product Types: α × β

Why product types? Real programs combine data: a point has an x coordinate AND a y coordinate; a database record has a name AND an age AND an address. Whenever you need to carry multiple pieces of data simultaneously, you reach for a product.

  α × β

  ┌──────────────┐
  │  .1  :  α    │   ← first component
  │  .2  :  β    │   ← second component
  └──────────────┘

  Build:  (a, b)   or   ⟨a, b⟩
  Use:    p.1, p.2       (projections; ι-reduction fires)

A product type α × β bundles a value of type α with a value of type β. To build a product you must supply BOTH components. To use a product you project out whichever component you need.

Products are how data is aggregated: a 2D point is an x AND a y; a person record is a name AND an age AND a city.

-- Building and projecting products:
def myPair : Nat × Bool := (7, true)
#eval myPair.1    -- 7       (first component)
#eval myPair.2    -- true    (second component)

-- Anonymous constructor ⟨_, _⟩ is equivalent to (_, _) for products:
def myPoint : Float × Float := ⟨3.0, 4.0⟩

-- Nested products (right-associative by default):
def myTriple : Nat × String × Bool := (42, "hello", false)
#eval myTriple.1        -- 42
#eval myTriple.2.1      -- "hello"
#eval myTriple.2.2      -- false

-- A function that takes a product and swaps its components:
def swap (p : α × β) : β × α := (p.2, p.1)
#eval swap (1, "one")    -- ("one", 1)
#eval swap (true, 42)    -- (42, true)

-- Products in function signatures (named arguments are sugar for products):
def hypotenuse (legs : Float × Float) : Float :=
  Float.sqrt (legs.1 ^ 2 + legs.2 ^ 2)
#eval hypotenuse (3.0, 4.0)   -- 5.0

The logical reading: conjunction (AND)

In logic, P ∧ Q holds when both P holds and Q holds. A proof of P ∧ Q is a pair: a proof of P together with a proof of Q.

And in Lean is literally a structure with two fields. It IS a product type, specialized to the case where the components are proofs.

-- Proving a conjunction: supply both halves.
example : 2 < 3 ∧ 3 < 4 := ⟨by decide, by decide⟩

-- Or: explicit constructor.
example : 1 + 1 = 2 ∧ 2 + 2 = 4 := And.intro rfl rfl

-- Extracting from a conjunction:
theorem use_left  (h : P ∧ Q) : P := h.left
theorem use_right (h : P ∧ Q) : Q := h.right

-- Commutativity: if P ∧ Q then Q ∧ P.
-- Computation: swap the pair.
-- Logic: swap the conjunction.
-- Evaluation: ⟨h.right, h.left⟩ ↝ ⟨proof-of-Q, proof-of-P⟩  (projections reduce)
theorem and_comm' (h : P ∧ Q) : Q ∧ P :=
  ⟨h.right, h.left⟩   -- this IS the swap function applied to proofs

-- Three-way conjunction:
example : 1 < 2 ∧ 2 < 3 ∧ 3 < 4 := by decide

0.4 Sum Types: Sum α β (written α ⊕ β)

Why sum types? Real programs handle alternatives: a network request either succeeds OR fails; a command is either add OR remove OR update; a shape is a circle OR a rectangle OR a triangle. Sums capture this structure in the type — and pattern-matching forces you to handle every case.

  α ⊕ β

  ┌──────────────────────────┐
  │  Sum.inl (a : α)         │   ← "I have an α"
  │    OR                    │
  │  Sum.inr (b : β)         │   ← "I have a β"
  └──────────────────────────┘

  Build:  Sum.inl a   or   Sum.inr b
  Use:    match s with | Sum.inl a => ... | Sum.inr b => ...

A sum type α ⊕ β carries either a value of type α or a value of type β. It represents a choice or variant: you get one kind of thing or the other, and the tag inl/inr tells you which.

Sums are how programs handle alternatives: a result is either a successful value or an error; a shape is a circle or a rectangle or a triangle.

-- Sum has two constructors: inl (left) and inr (right).
def aNum  : Nat ⊕ String := Sum.inl 42
def aStr  : Nat ⊕ String := Sum.inr "error"

-- To USE a sum, you must handle BOTH cases:
def describeNatOrStr (s : Nat ⊕ String) : String :=
  match s with
  | Sum.inl n => "a number: " ++ toString n
  | Sum.inr e => "a string: " ++ e

#eval describeNatOrStr aNum    -- "a number: 42"
#eval describeNatOrStr aStr    -- "a string: error"

-- The canonical programming sum: Option.
-- Option α represents either a value (some a) or absence (none).
-- It is a sum: Unit ⊕ α, roughly.
def safeDivide (a b : Nat) : Option Nat :=
  if b = 0 then none else some (a / b)

#eval safeDivide 10 2   -- some 5
#eval safeDivide 10 0   -- none

-- Using an Option:
def showResult (r : Option Nat) : String :=
  match r with
  | none   => "no result"
  | some n => "result: " ++ toString n

#eval showResult (safeDivide 10 2)    -- "result: 5"
#eval showResult (safeDivide 10 0)    -- "no result"

The logical reading: disjunction (OR)

In logic, P ∨ Q holds when at least one of P or Q holds. A proof of P ∨ Q is either a proof of P (tagged Or.inl) or a proof of Q (tagged Or.inr).

Or IS a sum type, specialized to propositions.

To prove a disjunction, pick one side and prove it. To use a disjunction, case-split on which side holds (just like match).

-- Proving a disjunction: choose a side.
example : 1 = 1 ∨ 1 = 2 := Or.inl rfl      -- left side
example : 1 = 2 ∨ 1 = 1 := Or.inr rfl      -- right side
example : 3 < 4 ∨ 4 < 3 := by decide       -- decide picks the right side

-- Using a disjunction: case analysis.
theorem or_comm' (h : P ∨ Q) : Q ∨ P :=
  match h with
  | Or.inl hp => Or.inr hp   -- had P; now tag it as inr
  | Or.inr hq => Or.inl hq   -- had Q; now tag it as inl
-- This IS `swap` applied to proofs of disjuncts.

-- Disjunction from an implication:
theorem or_weaken (h : P) : P ∨ Q := Or.inl h

0.5 The Empty Type: Empty and False

Why an empty type? Sometimes a situation is genuinely impossible: a division by zero that your types have already ruled out; a branch of a proof that leads to contradiction. When you can prove a situation is impossible, the empty type lets you discharge it cleanly — the type system certifies the branch is unreachable.

The empty type has no constructors and no values. It is impossible to produce a term of this type.

In computation: Empty represents a branch that can never be reached. A function returning Empty can never actually return. Pattern-matching on a value of type Empty needs zero branches — vacuously complete.

In logic: False is the proposition with no proof. A proposition that cannot be proved is false.

Empty : Type and False : Prop are the same idea in two universes.

-- `Empty` has no constructors — you cannot produce a value of it.
-- But you CAN write a function FROM Empty (with no cases to handle):
def fromEmpty (e : Empty) : α := nomatch e

-- In logic: `False → P` (ex falso quodlibet — from absurdity, anything).
theorem ex_falso {P : Prop} (h : False) : P := False.elim h

-- Why is this useful?  Because it discharges impossible cases.
-- If a case leads to `False`, the rest of the goal becomes irrelevant.
example (h : 2 + 2 = 5) : "pigs fly" = "pigs fly" :=
  absurd h (by decide)   -- decide proves ¬(2+2=5); absurd closes the goal

-- `absurd : P → ¬P → Q`
-- Given a proof of P and a proof of ¬P, produce anything.
-- This is the logical short-circuit: contradiction → done.

The power of the empty type: every impossible case reduces to one.

When your program reaches a state that "cannot happen," the right tool is to prove it is False and use False.elim (or absurd) to discharge the goal. The program does not crash; it never reaches that branch at all, because the type system certified the branch is unreachable.

nomatch e is Lean's syntax for pattern-matching on a value of a type with no constructors: the match is exhaustive with zero branches.

0.6 Functions to Empty: α → Empty and ¬P

Why functions to empty? Ruling out a case is as important as handling one. When you write a precondition h : n ≠ 0, you are carrying a function (n = 0) → False — proof that passing in a zero is impossible. Negation is not a primitive added to the language; it falls out of the function arrow and the empty type that you already have.

The most surprising type constructor: a function whose codomain is the empty type.

A value of type α → Empty is a function that, if given an α, would produce an Empty. But Empty has no values — so such a function can never complete its job. This means: if such a function exists, then α itself must have had no values to pass in. The function proves that α is uninhabited.

In computation: α → Empty certifies that α has no values.

In logic: ¬P is defined as P → False. A proof of ¬P is a function: given any proof of P, produce a proof of False. Since False has no proofs, the function can never fire — which means P has no proofs, i.e., P is false.

Negation is not a primitive. It IS the function arrow, aimed at False.

-- ¬P unfolds to P → False:
#print Not   -- def Not (a : Prop) : Prop := a → False

-- Every proof of ¬P is a function P → False.
-- `decide` constructs this function automatically for decidable cases.
example : ¬ (1 = 2)  := by decide
example : ¬ (3 > 5)  := by decide
example : ¬ (0 = 1)  := by decide

-- Negation from definitions:
-- ¬(1 = 2) means (1 = 2) → False.
-- 1 and 2 have different normal forms, so the Eq constructor cannot apply;
-- Lean sees there are zero cases to match, so `nomatch` closes the goal.
theorem one_ne_two : ¬ (1 = 2) := fun h => nomatch h

-- Contradiction: if P and ¬P both hold, everything follows.
theorem contradiction {P Q : Prop} (h : P) (hne : ¬P) : Q :=
  False.elim (hne h)   -- hne h : False, then ex falso

-- Double negation introduction (the direction that holds constructively):
-- "If P holds, then P is not contradictory."
theorem not_not_intro (h : P) : ¬¬P :=
  fun hnp => hnp h    -- hnp : ¬P = P → False; apply it to h : P

-- Example: ¬(P ∧ ¬P) — no proposition and its negation can both hold.
theorem not_and_not (h : P ∧ ¬P) : False :=
  h.right h.left      -- apply ¬P (= h.right) to P (= h.left)

0.7 The Six Constructors Together

Here is the complete picture. Every type you will write in this course is built from some combination of these six. Every proposition you will reason about is expressed by some combination of these six.

The question "what inhabits this type?" has two flavors:

• Computational types (Type): inhabitants are data.
• Logical types (Prop): inhabitants are proofs.

But the constructors are shared. Products bundle data AND proofs the same way. Sums tag data AND proofs the same way. Functions transform data AND convert proofs the same way. The empty type represents impossible data AND impossible proofs.

-- All six constructors demonstrated side by side:

-- Product / And
def dataPair  : Nat × Bool := ⟨5, true⟩
def proofPair : 2 < 3 ∧ 3 < 4 := ⟨by decide, by decide⟩

-- Sum / Or
def dataSum    : Nat ⊕ Bool  := Sum.inl 7
def proofDisj  : 2 < 3 ∨ 3 < 2 := Or.inl (by decide)

-- Function / Implication
def dataFun   : Nat → Nat   := fun n => n + 1
def proofImpl : 2 < 3 → 2 ≤ 3 := fun h => Nat.le_of_lt h

-- Negation / Uninhabited
def proofNeg  : ¬ (1 = 2) := by decide

-- Empty type: a function from Empty returns anything
def fromImpossible (e : Empty) : Nat × Bool × String := nomatch e

0.8 Challenges in programming with algebraic types

Understanding the six constructors is not yet fluency. The challenge is knowing which constructor fits each situation.

Here are the fundamental design questions:

Use a product when you need to carry multiple pieces of data at once. A point is x AND y. A function's return type is a product when it returns two things. A precondition bundled with a return value is a product of data and proof.

Use a sum when data has multiple, mutually exclusive forms. An API result is success OR error. A command is add OR remove OR update. Pattern-matching IS elimination of a sum — you must handle every case.

Use a function when you want to defer or parameterize computation. A callback, a comparator, a predicate — these are function-type arguments.

Use negation (function to False) when you need to rule out a case. A precondition h : x ≠ 0 is (x = 0) → False. It certifies the impossible before the program runs.

Use Empty/False when a branch cannot exist. The type system then verifies you never reach it; nomatch or False.elim closes the goal.

The payoff: once you have the right type, the program often writes itself. The type tells you what constructors to use; the exhaustiveness checker tells you which cases remain. Types are not just documentation — they are your co-programmer.

Exercises

1. Use decide to verify each claim. For each, identify which type constructor(s) from the six-constructor table the proposition uses: (a) 2 < 3 ∧ 3 < 4 (b) 2 < 3 ∨ 3 < 2 (c) ¬ (2 = 3) (d) ¬ (2 < 3 ∧ 3 < 2) (e) (2 < 3 ∧ ¬(3 < 2)) ∨ (3 < 2 ∧ ¬(2 < 3))

2. Explain in your own words why a function of type α → Empty certifies that α has no values. Then write a term of type False → Nat × Bool × String and explain what it means in both the computational and logical readings.

3. Write twice : (α → α) → α → α that applies a function twice — twice f x = f (f x). Test it with #eval:

   #eval twice double 3        -- 12
   #eval twice negate false    -- false
   

   When α is a Prop, what does twice say logically? Write the type (P → P) → P → P in Lean and read it aloud.

4. Write mapOption : (α → β) → Option α → Option β using match. It should apply f to the wrapped value if some, return none otherwise. Test it:

   #eval mapOption double (some 5)     -- some 10
   #eval mapOption double none         -- none
   #eval mapOption negate (some true)  -- some false
   

   Which two type constructors from the six-constructor table does the type of mapOption use?

5. For each description, write the Lean type using only the six constructors from §0.7. Write just the type — not a term inhabiting it. (a) A person's name (String) paired with their score (Nat) (b) A result that is either a computed Nat or an error String (c) A function that takes any proof of P ∧ Q and returns a proof of Q (d) Evidence that ¬ (2 + 2 = 5) (e) A value certifying that the type Empty is uninhabited Then use decide to verify (d). What does Lean do to check it?

end Week00

-- FPCourse/Unit1/Week01_ExpressionsTypesValues.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic

Week 1: Expressions, Types, and Values

The central idea of this course

Every expression in Lean has a type. Types do two jobs at once.

• Computational types classify data: Nat, Bool, String, Nat × Bool. A value of a computational type can be evaluated.

• Logical types (also called propositions) classify claims. A value of a logical type is a proof that the claim holds.

These two jobs are performed by the same language using the same syntax. That identity — programs and proofs living in one world — is the deepest idea in the course. You will see it demonstrated in every week that follows. By Week 14 you will have a name for it.

namespace Week01

1.1 Computational types

-- Every literal has a type.  Use #check to inspect it.
#check (42 : Nat)        -- Nat
#check (true : Bool)     -- Bool
#check ("hello" : String)

-- Functions have arrow types.
#check Nat.succ          -- Nat → Nat
#check Nat.add           -- Nat → Nat → Nat

-- #eval evaluates an expression to its normal form by reduction.
-- Nat.succ 7   ↝ 8        (successor of 7, by definition of Nat.succ)
-- Nat.add 3 4  ↝ 7        (addition, by recursive definition of Nat.add)
-- true && false ↝ false   (β-reduction: true && b ↝ b)
#eval Nat.succ 7         -- 8
#eval Nat.add 3 4        -- 7
#eval true && false      -- false  (Bool operations)

1.2 The Bool / Prop distinction

Bool is a two-element computational type: values true and false. It is the type of the result of a test you can run.

Prop is the type of logical claims. A term of type P : Prop is a proof that P holds. Prop is not two-valued; some propositions have no proof (they are false), some have many proofs.

This is the most important type-level distinction in Lean.

-- Bool: a computed result.
#eval (2 == 3 : Bool)       -- false  (uses BEq instance)
#eval (2 < 5 : Bool)        -- true   (uses DecidableLT)

-- Prop: a logical claim.
#check (2 = 3 : Prop)       -- 2 = 3 : Prop
#check (2 < 5 : Prop)       -- 2 < 5 : Prop
#check (∀ n : Nat, n + 0 = n)   -- Prop
#check (∃ n : Nat, n > 100)     -- Prop

-- A proof of a Prop is a term of that type.
-- `rfl` proves `a = b` when both sides evaluate to the same normal form.
-- Evaluation: 2 + 2 ↝ 4, and the right side is already 4.  Same normal form.
-- Evaluation: Nat.succ 7 ↝ 8, and the right side is already 8.
example : 2 + 2 = 4 := rfl      -- both sides evaluate to 4
example : Nat.succ 7 = 8 := rfl  -- both sides evaluate to 8

1.3 decide: mechanically proving decidable propositions

Some propositions are decidable: there is an algorithm that always produces either a proof or a refutation. For those propositions, the term decide acts as an automatic proof producer.

decide is a term, not a command. It inhabits a type P : Prop whenever P has a Decidable instance and reduces to true. The compiler checks this at elaboration time. If P reduces to false, the file fails to compile.

This is mechanical verification in its most direct form: the claim is part of the type, and the compiler certifies it.

-- Evaluation: `decide` evaluates the decision procedure for the proposition.
-- For each claim, Lean evaluates both sides and checks the result.
-- 2 + 2 ↝ 4, so 2 + 2 = 4 is confirmed.
-- 3 ↝ 3 and 5 ↝ 5, they differ, so ¬(3 = 5) is confirmed.
example : 2 + 2 = 4 := by decide
example : ¬ (3 = 5) := by decide
example : 2 < 100 := by decide
example : 10 % 3 = 1 := by decide

-- decide on a list: ∀ over a finite collection is decidable
-- when the predicate is decidable.
example : ∀ x ∈ ([1, 2, 3] : List Nat), x < 10 := by decide
example : ∃ x ∈ ([1, 2, 3] : List Nat), x > 2  := by decide

-- If the claim is FALSE, the file will not compile.
-- Uncomment the next line to see the error:
-- example : 2 + 2 = 5 := decide

1.4 Product types

A product type α × β pairs a value of type α with a value of type β.

def myPair : Nat × Bool := (7, true)

#check myPair.1    -- Nat
#check myPair.2    -- Bool
#eval  myPair.1    -- 7
#eval  myPair.2    -- true

-- Nested products
def triple : Nat × Bool × String := (3, false, "hi")
#eval triple.1          -- 3
#eval triple.2.1        -- false
#eval triple.2.2        -- "hi"

1.5 Proof-carrying types: a first look

Here is a function that divides two natural numbers. The type of the second argument includes a condition: a proof that the divisor is nonzero must be supplied by the caller.

def safeDiv (a : Nat) (b : Nat) (h : b ≠ 0) : Nat := a / b

The type b ≠ 0 is a proposition — a logical type. Calling safeDiv does not just pass a number; it passes a proof that the number is nonzero. The compiler enforces this before the program runs.

This pattern — conditions embedded in types, enforced at compile time — is what we mean by proof-carrying types. You will see it everywhere from Week 2 onward.

def safeDiv (a : Nat) (b : Nat) (h : b ≠ 0) : Nat := a / b

-- To call safeDiv we must supply a proof that the divisor ≠ 0.
-- For a concrete nonzero literal, `decide` produces the proof.
#eval safeDiv 10 2 (by decide)   -- 5
#eval safeDiv 17 3 (by decide)   -- 5

-- Attempting safeDiv 10 0 would require a proof of 0 ≠ 0,
-- which is false.  `decide` would refuse, and the file would
-- not compile.

1.6 Type derivation rules (summary)

Reading types is the foundational skill of this course. Every week adds new type constructors to this table.

Exercises

1. Use #check to find the types of Nat.add, Nat.mul, and String.append. For each, write in plain English what the type says the function does. Are these types curried? How many arguments does each take?

2. Write a product type that pairs a String with a Nat. Construct a value of that type.

3. Write example : 7 * 6 = 42 := _ and replace _ with the correct proof term. (Hint: both sides evaluate to the same normal form.)

4. Use decide to verify each claim: (a) 17 * 23 = 391 (b) 100 < 200 ∧ 200 < 300 (c) ¬ (5 * 5 = 26) (d) (7 + 3) * 2 = 7 * 2 + 3 * 2 For each, identify whether the proposition is atomic or built from connectives (∧, ¬).

5. Why can't you write example : (1.0 : Float) = 1.0 := decide? (Hint: think about what equality on Float would require. We will return to this in Week 7.)

end Week01

-- FPCourse/Unit1/Week02_FunctionsSpecifications.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Logic.Basic

Week 2: Functions and Specifications

The dual reading of →

The arrow → has two readings that are always simultaneously true.

Computational reading: α → β is the type of functions from α to β. A term of this type takes an input of type α and returns an output of type β.

Logical reading: P → Q (where P Q : Prop) is the type of proofs that P implies Q. A term of this type is a function that converts any proof of P into a proof of Q.

These are not two different symbols. They are one symbol with two readings. A function is an implication proof; an implication proof is a function. This identity is the beginning of the Curry-Howard correspondence, which we will name explicitly in Week 14.

namespace Week02

2.1 Defining functions

-- Named function definition
def double (n : Nat) : Nat := n * 2
def square (n : Nat) : Nat := n * n

-- Anonymous function (lambda)
def double' : Nat → Nat := fun n => n * 2

-- Multi-argument functions are curried by default
def add3 (a b c : Nat) : Nat := a + b + c
-- add3 has type Nat → Nat → Nat → Nat
-- Applying one argument returns a function: Nat → Nat → Nat

-- Evaluation (β-reduction): each application substitutes the argument.
--   add3 1 2 3
--   ↝ (fun a b c => a + b + c) 1 2 3
--   ↝ 1 + 2 + 3                        (three β-reductions)
--   ↝ 6
#eval add3 1 2 3    -- 6
#eval (add3 1) 2 3  -- same: (add3 1) is a Nat → Nat → Nat waiting for two more args

2.2 → as implication: logical reading

When P and Q are propositions, P → Q is the claim that P implies Q. A proof of P → Q is a function that takes any proof of P and returns a proof of Q. This is indistinguishable from an ordinary function — because it is an ordinary function.

-- A proof of P → Q is a term of type P → Q.
-- Here: "if n + 0 = n, then n = n + 0"
theorem add_zero_comm (n : Nat) : n + 0 = n → n = n + 0 :=
  fun h => h.symm

-- Universal claims: ∀ n : Nat, P n
-- This is also a function type: (n : Nat) → P n
-- A proof supplies the function.
theorem add_zero_all : ∀ n : Nat, n + 0 = n :=
  Nat.add_zero

-- The ∀ and → are the same thing: ∀ n, P n is (n : Nat) → P n
-- when P does not mention types not in scope.

2.3 The design recipe

Every function in this course is designed using the following steps. English descriptions are written as Lean docstrings (/-- ... -/ placed immediately before a definition) so the tooling surfaces them in hover text.

The description comes first so you understand what before how. The signature must precede the specification — the spec names the function, so the def must exist before the theorem can be stated.

-- Example: doubling a number.

-- Step 0 — Description:
/-- `double'' n` returns twice `n`. -/
-- Step 1 — Signature + Steps 4/5 Template and code:
def double'' (n : Nat) : Nat := n + n

-- Step 3 — Examples (two forms):
-- Form 1: #eval with expected value in comment (explore interactively)
#eval double'' 0    -- 0
#eval double'' 5    -- 10
-- Form 2: rfl-based test (machine-verified; both sides evaluate to the same normal form)
example : double'' 0 = 0  := rfl
example : double'' 5 = 10 := rfl

-- Step 2 — Specification (stated after the def, since it names double''):
--   ∀ n : Nat, double'' n = n + n
-- Step 6 — Check (provided proof):
-- Evaluation: double'' n ↝ n + n (δ-reduction).  Both sides are identical.
theorem double''_spec : ∀ n : Nat, double'' n = n + n :=
  fun n => rfl

2.4 Function composition

-- ∘ is function composition: (f ∘ g) x = f (g x)
def double_then_square : Nat → Nat := square ∘ double

#eval double_then_square 3    -- square (double 3) = square 6 = 36

-- Composition and identity satisfy algebraic laws.
-- These are propositions about functions — logical types.
theorem comp_id (f : α → β) : f ∘ id = f := rfl
theorem id_comp (f : α → β) : id ∘ f = f := rfl
theorem comp_assoc (f : γ → δ) (g : β → γ) (h : α → β) :
    (f ∘ g) ∘ h = f ∘ (g ∘ h) := rfl

2.5 Connectives as types

Logical connectives are type constructors. A proposition built with a connective has the same structure as a product or sum type in computation.

-- ∧ introduction: supply proofs of both conjuncts
example : 1 < 2 ∧ 2 < 3 :=
  And.intro (by decide) (by decide)

-- ∨ introduction: supply a proof of one disjunct
example : 1 = 1 ∨ 1 = 2 :=
  Or.inl rfl

-- ¬P is P → False
example : ¬ (1 = 2) :=
  by decide

-- ↔ introduction: supply both directions
example : (1 + 1 = 2) ↔ (2 = 1 + 1) :=
  Iff.intro (fun h => h.symm) (fun h => h.symm)

2.6 Reading function specifications

When a function's type contains propositions, the type IS the specification. The examples below show how to read proof-carrying function types.

-- The type tells you: given a proof that the list is nonempty,
-- return the first element.  No runtime null check needed.
#check List.head   -- (l : List α) → l ≠ [] → α
-- (Actual Lean name may vary; the pattern is the point.)

-- The type tells you: given proofs about the index being in bounds,
-- return the element at that index.
#check List.get    -- (l : List α) → Fin l.length → α
-- Fin n is the type of natural numbers < n.  It IS the bounds proof.

Exercises

1. Write a function pred' : Nat → Nat that returns the predecessor, treating 0 as 0. Write its specification as a ∀ proposition.

2. What is the type of And.intro? Use #check to find out. Explain in English what a term of that type represents both computationally and logically.

3. Use #print Iff to inspect the definition of ↔. What are its two fields? Use decide to verify: (a) (2 < 3) ↔ ¬(3 ≤ 2) (b) (True ∧ True) ↔ True (c) (True ∧ False) ↔ False For each, state in English what the biconditional asserts.

4. Use decide to verify ¬ (True ∧ False). Then explain: what is the type of ¬ (True ∧ False) in full, unfolding ¬ to → False?

5. State (as a Lean Prop) the specification for a function max' : Nat → Nat → Nat that returns the larger of two numbers. Your specification should assert: (a) the result is ≥ both inputs, and (b) the result equals one of the two inputs.

end Week02

-- FPCourse/Unit1/Week03_RecursionTermination.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring

Week 3: Recursion and Termination

Structural recursion

Here is a way to think about recursion that is the inverse of the usual story.

The usual story: "the function calls itself on a smaller input until it reaches a base case." That describes execution, but it does not explain why the definition gives a correct answer for every input.

The better story starts from what you actually need in order to define a function on the natural numbers:

1. A base case. You supply the answer for input 0 directly.
2. A step function. You supply a rule that, given any input n and the answer for n, produces the answer for n + 1.

Those two ingredients are enough to determine the answer for every natural number: start with the answer for 0, apply the step once to get the answer for 1, again to get the answer for 2, and so on. However large the input, you can always reach it by iterating the step enough times from the base.

This is the content of the principle of recursion (or primitive recursion) on the natural numbers. The recursive definition in Lean is just a compact way of writing down these two ingredients:

• The | 0 => ... clause supplies the base-case answer.
• The | n + 1 => ... clause supplies the step function. The right-hand side may refer to n (the previous input) and to the recursive call f n (the answer for n). That recursive call is not "calling itself" in some mysterious way — it is simply using the assumption that the answer for n is already in hand, which the step function is entitled to assume by construction.

Lean can verify termination automatically for structural recursion because it can see that the step clause only ever asks for the answer at n, not at any larger value.

namespace Week03

3.1 Factorial — direct recursive definition

def factorial : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 0   -- 1
#eval factorial 5   -- 120
#eval factorial 10  -- 3628800
-- rfl-based tests: both sides reduce to the same normal form
example : factorial 0 = 1   := rfl
example : factorial 5 = 120 := rfl

Reading the definition. Apply the two-ingredient view to factorial:

• Base case (| 0 => 1): the answer for 0 is 1.
• Step (| n + 1 => (n + 1) * factorial n): given input n + 1, and given that the answer for n is already factorial n, multiply them.

To see why this gives the right answer for 3, iterate the step up from the base:

factorial 0 = 1                              -- base case
factorial 1 = 1 * factorial 0 = 1 * 1 = 1   -- step: n = 0, answer for 0 = 1
factorial 2 = 2 * factorial 1 = 2 * 1 = 2   -- step: n = 1, answer for 1 = 1
factorial 3 = 3 * factorial 2 = 3 * 2 = 6   -- step: n = 2, answer for 2 = 2

Each line uses the answer from the line above — exactly the "answer for n already in hand" that the step clause is entitled to assume.

Lean's evaluator runs this in the opposite order — it unfolds factorial 3 toward the base case and assembles the result on the way back up. Either direction produces 6. The inductive framing explains why there is a well-defined answer for every input, not just how to compute it.

3.2 Tail recursion and accumulators

The direct definition rebuilds the product on the way back from the base case. A tail-recursive version accumulates the product on the way down, so the recursive call is the last thing done.

Tail-recursive functions are important in practice because they run in constant stack space. They can also have different proofs of correctness, which is why we need to state the relationship between the two versions.

def factorialAcc : Nat → Nat → Nat
  | 0,     acc => acc
  | n + 1, acc => factorialAcc n ((n + 1) * acc)

def factorialTR (n : Nat) : Nat := factorialAcc n 1

-- Evaluation: factorialTR 3
--   ↝ factorialAcc 3 1
--   ↝ factorialAcc 2 (3 * 1)   ↝ factorialAcc 2 3
--   ↝ factorialAcc 1 (2 * 3)   ↝ factorialAcc 1 6
--   ↝ factorialAcc 0 (1 * 6)   ↝ factorialAcc 0 6
--   ↝ 6                          (first clause: acc is returned)
-- Notice: the accumulator grows on the way DOWN; no work on the way back up.
#eval factorialTR 5   -- 120
example : factorialTR 5 = 120 := rfl

3.3 Specification: the two definitions agree

The following theorem states that the accumulator version computes the same value as the direct version, for any starting accumulator.

You are not expected to construct this proof. It is provided so you can see that such a proof exists and what it looks like. The proof is a term — a recursive function on n whose type is the specification.

Read the term as: "by induction on n; the base case is a calculation; the step uses the inductive hypothesis for n with a different accumulator."

-- Provided term-mode proof.  Read it; do not reproduce it.
theorem factorialAcc_spec : ∀ (n acc : Nat),
    factorialAcc n acc = acc * factorial n := by
  intro n
  induction n with
  | zero => intro acc; simp [factorialAcc, factorial]
  | succ n ih =>
    intro acc
    simp only [factorialAcc, factorial]
    rw [ih]
    ring

-- Corollary: factorialTR agrees with factorial
theorem factorialTR_spec (n : Nat) : factorialTR n = factorial n :=
  Eq.trans (factorialAcc_spec n 1) (Nat.one_mul (factorial n))

3.4 Non-structural termination

When recursion does not follow the structure of an inductive type, Lean requires an explicit termination measure: a quantity that strictly decreases at each recursive call with respect to some well-founded relation.

The termination_by clause names the measure.

-- Euclidean GCD — not structurally recursive on either argument,
-- but decreases on the second argument at each step.
def gcd : Nat → Nat → Nat
  | a, 0     => a
  | a, b + 1 => gcd (b + 1) (a % (b + 1))
termination_by _ b => b
decreasing_by apply Nat.mod_lt; omega

#eval gcd 48 18   -- 6
#eval gcd 100 75  -- 25
-- Note: rfl-based tests do NOT work for gcd.
-- gcd uses well-founded (non-structural) recursion; the kernel cannot reduce it.
-- Neither rfl nor decide can close goals about gcd on concrete values.
-- #eval works because it uses the compiled code path, not the kernel.
-- This distinction matters: rfl-based tests are available only for
-- structurally recursive functions (like factorial above).

-- Specification: gcd divides both arguments.
-- This is a Prop.  The proof is provided for you to read.
def divides (d n : Nat) : Prop := ∃ k, n = d * k

-- Nat.gcd_dvd_left and Nat.gcd_dvd_right are Mathlib lemmas.
-- Our gcd coincides with Nat.gcd (provable, provided here):
theorem gcd_eq_nat_gcd : ∀ a b : Nat, gcd a b = Nat.gcd a b := by
  intro a b
  induction b using Nat.strongRecOn generalizing a with
  | ind b ih =>
    cases b with
    | zero =>
      simp only [gcd, Nat.gcd_zero_right]
    | succ b =>
      simp only [gcd]
      have key := ih (a % (b + 1)) (Nat.mod_lt a (Nat.succ_pos b)) (b + 1)
      rw [key, Nat.gcd_comm, ← Nat.gcd_rec, Nat.gcd_comm]

3.5 The termination / totality distinction

A function in Lean must be total: it must return a value for every input. Lean enforces totality through two mechanisms:

• Structural recursion: automatically verified by checking recursive calls are on strict subterms.
• Well-founded recursion: you provide a termination measure; Lean verifies it decreases at each call.

A function that does not terminate cannot be given a type in Lean without using the partial keyword — which removes termination guarantees and disables proof of properties about the function.

This is not a limitation. It is a feature: if a function has a type in Lean, it terminates on all inputs. This means any specification you write about it is asking a question that always has an answer.

3.6 Reading specifications about recursive functions

A specification for a recursive function is almost always a ∀ proposition: "for all inputs, the output satisfies this condition."

Practice reading these:

-- "For all n, factorial n is positive"
-- You should be able to read and understand the proposition.
-- The proof term is here for your curiosity; you are not expected to produce it.
theorem factorial_pos : ∀ n : Nat, 0 < factorial n :=
  fun n => Nat.recOn n (Nat.lt_add_one 0) (fun n ih => Nat.mul_pos (Nat.succ_pos n) ih)

-- "factorial is monotone: each value is no greater than the next"
-- You should be able to read and understand the proposition.
-- The proof term is here for your curiosity; you are not expected to produce it.
theorem factorial_mono : ∀ n : Nat, factorial n ≤ factorial (n + 1) :=
  fun n => Nat.le_mul_of_pos_left (factorial n) (Nat.succ_pos n)

/-
## Worked out in class
-/


-- Check out the induction axiom for Nat!
#check (@Nat.rec)

Formatted more nicely:

@Nat.rec :
  {motive : ℕ → Sort u_1} →
  motive Nat.zero →
  ((n : ℕ) → motive n → motive n.succ) →
  (t : ℕ) → motive t

Problems worked out in class. Define some familar functions on ordinary data types by induction. Any recursive function is basically a universal built by applicaiton of the induction axiom for a given type to answer for base cases and step functions.

def fac0 := 1
def facStep (n facn : Nat) : Nat := (n+1) * facn
#check @Nat.rec (fun _ => Nat) fac0 facStep
#eval (@Nat.rec (fun _ => Nat) fac0 facStep) 5

@List.rec : {α : Type u_2} → {motive : List α → Sort u_1} → motive [] → ((head : α) → (tail : List α) → motive tail → motive (head :: tail)) → (t : List α) → motive t

def listLenBase := 0
def stepListLen (_ : String) (_ : List String) (ansL : Nat) := ansL + 1

#check @List.rec String (fun _ => Nat) listLenBase stepListLen
#eval (@List.rec String (fun _ => Nat) listLenBase stepListLen) ["", "", ""]
#check (@List.rec)

@BinTreeNat.rec : {motive : BinTreeNat → Sort u_1} → motive BinTreeNat.empty → ((n : ℕ) → (l r : BinTreeNat) → motive l → motive r → motive (BinTreeNat.node n l r)) → (t : BinTreeNat) → motive t

inductive BinTreeNat where
| empty
| node (n : Nat) (l r : BinTreeNat)

open BinTreeNat

#check (@BinTreeNat.rec)
#reduce (@BinTreeNat.rec (fun _ => Nat) 0 (fun n _ _ al ar => n + al + ar)) BinTreeNat.empty

def myTree : BinTreeNat :=
  node 1
  (node 2 empty empty)
  (node 5 empty empty)

#reduce (@BinTreeNat.rec (fun _ => Nat) 0 (fun n _ _ al ar => n + al + ar)) myTree

Exercises

1. Define sumTo : Nat → Nat that computes 0 + 1 + ... + n. Write its specification as a ∀ proposition: ∀ n, sumTo n = n * (n + 1) / 2.

2. Define a tail-recursive version sumToAcc : Nat → Nat → Nat. State (as a Prop) the relationship between sumToAcc and sumTo.

3. Use gcd_eq_nat_gcd and Mathlib's Nat.Coprime to state the proposition: "8 and 15 are coprime." Use decide to prove it.

4. Why does the following definition NOT satisfy Lean's termination checker? What termination measure would you supply?

   def collatz : Nat → Nat
     | 0 => 0
     | 1 => 1
     | n => if n % 2 == 0 then collatz (n / 2) else collatz (3 * n + 1)
   

5. State the specification for gcd as two ∀ propositions expressing that it divides both arguments.

end Week03

-- uncomment to see error
-- def collatz : Nat → Nat
--   | 0 => 0
--   | 1 => 1
--   | n => if n % 2 == 0 then collatz (n / 2) else collatz (3 * n + 1)

/-
```lean
fail to show termination for
  collatz
with errors
failed to infer structural recursion:
Cannot use parameter #1:
  failed to eliminate recursive application
    collatz (n / 2)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
n : ℕ
h✝ : (n % 2 == 0) = true
⊢ n / 2 < nLean 4
collatz : ℕ → ℕ

-/

-- FPCourse/Unit2/Week04_AlgebraicDatatypes.lean
import Mathlib.Data.Option.Basic
import Mathlib.Logic.Basic

Week 4: Algebraic Datatypes

Sum types and product types

Lean's inductive keyword lets us define new types by listing their constructors. The resulting type is either a sum (one of several alternatives) or a product (bundling several fields) — or both.

These are called algebraic datatypes because they obey the same algebraic laws as sums and products of numbers: a type with n values of type A and m values of type B as alternatives has n + m values.

namespace Week04

4.1 Enumeration types (pure sums)

inductive Direction where
  | North | South | East | West
deriving Repr, DecidableEq

#eval Direction.North      -- Direction.North
example : Direction.North ≠ Direction.South := by decide

4.2 Record types (pure products)

structure Point where
  x : Float
  y : Float
deriving Repr

def origin : Point := { x := 0.0, y := 0.0 }

4.3 Option: the prototypical proof-carrying type

Option α is either none (no value) or some a (a value a : α). It is Lean's answer to null.

But notice: Option.get does not simply hope the value is present. Its type requires a proof:

def Option.get : (o : Option α) → o.isSome = true → α

The caller must supply evidence before the function will run. This is the proof-carrying pattern from Week 1, now applied to a realistic data type.

-- Option.get requires a proof.
def safeHead (xs : List α) (h : xs ≠ []) : α :=
  xs.head h

-- For concrete lists, `decide` produces the proof.
#eval safeHead [1, 2, 3] (by decide)    -- 1

-- Option.map: lift a function into an optional context
-- Specification: ∀ f o, (Option.map f o).isSome = o.isSome
theorem option_map_isSome (f : α → β) :
    ∀ o : Option α, (Option.map f o).isSome = o.isSome :=
  fun o => Option.recOn o rfl (fun _ => rfl)

4.4 ∀ and ∃ in datatype specifications

When we define a new type, its specifications typically quantify over all values of that type. Here is the vocabulary:

-- ∀ example: a property of all options
theorem none_map_always_none (f : α → β) :
    Option.map f none = none :=
  rfl

-- ∃ example: witness a specific value satisfying a property
example : ∃ n : Nat, n > 100 := ⟨101, by decide⟩

private def factorial' : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial' n

example : ∃ n : Nat, factorial' n > 1000 :=
  ⟨7, by decide⟩

4.5 Recursive types: expressions

A recursive inductive type refers to itself in its constructor arguments. This is how we build trees, lists, and other inductively structured data.

inductive Expr where
  | num  : Int → Expr
  | add  : Expr → Expr → Expr
  | mul  : Expr → Expr → Expr
  | neg  : Expr → Expr
deriving Repr

-- Evaluation by structural recursion on Expr.
-- The function is named `eval` deliberately: it IS evaluation —
-- the process of reducing an expression tree to its integer value.
def Expr.eval : Expr → Int
  | .num n    => n
  | .add e₁ e₂ => e₁.eval + e₂.eval
  | .mul e₁ e₂ => e₁.eval * e₂.eval
  | .neg e    => -e.eval

-- Evaluation trace: Expr.eval (.add (.num 3) (.mul (.num 4) (.num 5)))
--   ↝ (.num 3).eval + (.mul (.num 4) (.num 5)).eval    -- add clause
--   ↝ 3 + (.mul (.num 4) (.num 5)).eval                -- num clause
--   ↝ 3 + ((.num 4).eval * (.num 5).eval)              -- mul clause
--   ↝ 3 + (4 * 5)                                      -- num clause ×2
--   ↝ 3 + 20 ↝ 23                                      -- arithmetic
#eval Expr.eval (.add (.num 3) (.mul (.num 4) (.num 5)))  -- 23

-- Specification: eval distributes over add.
-- Evaluation: (.add e₁ e₂).eval ↝ e₁.eval + e₂.eval by the add clause.
-- Both sides are definitionally equal, so rfl applies.
theorem eval_add (e₁ e₂ : Expr) :
    (Expr.add e₁ e₂).eval = e₁.eval + e₂.eval :=
  rfl

4.6 The template principle

Every inductive type T has a corresponding elimination principle: to define a function from T, provide one clause per constructor. The types of the clauses are determined by the constructor signatures.

For Expr:

• A clause for num n — has access to n : Int
• A clause for add e₁ e₂ — has access to both subexpressions and their recursively computed results
• A clause for mul e₁ e₂ — same
• A clause for neg e — access to e and its result

This is the template principle: the type tells you the shape of the function.

Exercises

1. Define an inductive type Shape with constructors for Circle (radius : Float), Rectangle (width height : Float), and Triangle (base height : Float).

2. Define a function area : Shape → Float.

3. State (as a Prop) the specification: "the area of any circle with radius r equals π * r * r." You may use Float.pi from Lean. (We will not prove this — Float lacks decidable equality. But we can state it.)

4. Add a sub : Expr → Expr → Expr constructor and extend eval. State its specification as a ∀ proposition.

5. Use ∃ to state: "there exists an Expr that evaluates to 42." Prove it by providing a witness.

end Week04

-- FPCourse/Unit2/Week05_Lists.lean
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Lemmas

Week 5: Lists

Lists as the canonical inductive type

List α is defined inductively:

• [] (nil) — the empty list
• h :: t (cons) — a head element h : α followed by a tail t : List α

Every function on lists follows this structure: one clause for [], one clause for h :: t (which may recurse on t).

The specifications for list functions are propositions that quantify over all lists. Some of these propositions are decidable — when the element type has DecidableEq and the list is finite, we can check them with decide.

namespace Week05

5.1 Standard list functions and their specifications

The specifications below are ALL provided as term-mode proofs. Read them; understand the proposition being stated; observe how the proof term mirrors the function definition.

-- Length
theorem length_nil : ([] : List α).length = 0 := rfl
theorem length_cons (h : α) (t : List α) :
    (h :: t).length = t.length + 1 := rfl

-- Append
theorem append_nil (xs : List α) : xs ++ [] = xs :=
  List.append_nil xs

theorem nil_append (xs : List α) : [] ++ xs = xs :=
  List.nil_append xs

theorem append_assoc (xs ys zs : List α) :
    (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
  List.append_assoc xs ys zs

-- Length distributes over append
theorem length_append (xs ys : List α) :
    (xs ++ ys).length = xs.length + ys.length :=
  List.length_append

-- Membership and append: ∈ distributes over ++
theorem mem_append_iff (a : α) (xs ys : List α) :
    a ∈ xs ++ ys ↔ a ∈ xs ∨ a ∈ ys :=
  List.mem_append

5.2 Decide on finite lists

When the element type has DecidableEq, propositions of the form ∀ x ∈ xs, P x are decidable for finite xs (when P is decidable). This means decide can verify them automatically.

-- Evaluation: `decide` checks finite-list claims by evaluating the predicate
-- on each element in turn.  ∀ x ∈ [2,4,6,8], x%2=0 becomes:
--   2%2=0 ↝ true,  4%2=0 ↝ true,  6%2=0 ↝ true,  8%2=0 ↝ true  ✓
example : ∀ x ∈ ([2, 4, 6, 8] : List Nat), x % 2 = 0 := by decide
example : ∀ x ∈ ([1, 3, 5, 7] : List Nat), x % 2 = 1 := by decide
example : ∃ x ∈ ([10, 20, 30] : List Nat), x > 15    := by decide

-- Membership in a concrete list:
example : 3 ∈ ([1, 2, 3, 4] : List Nat) := by decide
example : ¬ (5 ∈ ([1, 2, 3, 4] : List Nat)) := by decide

-- Equality of concrete lists:
example : ([1, 2] ++ [3, 4] : List Nat) = [1, 2, 3, 4] := by decide

5.3 Reverse and the auxiliary lemma pattern

reverse is defined recursively. Its specification — that reversing twice returns the original list — requires a helper lemma about how reverse interacts with ++.

This illustrates a general pattern: when a direct proof gets stuck, look at what the inductive step requires and name it as a separate lemma. The provided proofs below demonstrate this pattern explicitly.

theorem reverse_append (xs ys : List α) :
    (xs ++ ys).reverse = ys.reverse ++ xs.reverse :=
  List.reverse_append

theorem reverse_reverse (xs : List α) : xs.reverse.reverse = xs :=
  List.reverse_reverse xs

-- The proof of reverse_reverse in Mathlib uses reverse_append.
-- The dependency is: reverse_reverse requires reverse_append,
-- which in turn requires nil_append and append_assoc.
-- Each lemma is proved by structural recursion on the first list.

5.4 Map and its specification

List.map f applies f to every element. Its specification:

1. Map preserves length.
2. Map distributes over append.
3. Mapping the identity function is the identity on lists.
4. Mapping a composition equals composing two maps.

theorem map_length (f : α → β) (xs : List α) :
    (xs.map f).length = xs.length :=
  List.length_map f

theorem map_append (f : α → β) (xs ys : List α) :
    (xs ++ ys).map f = xs.map f ++ ys.map f :=
  List.map_append

theorem map_id_eq (xs : List α) : xs.map id = xs :=
  List.map_id xs

theorem map_comp (f : β → γ) (g : α → β) (xs : List α) :
    xs.map (f ∘ g) = (xs.map g).map f := by
  simp [← List.map_map]

5.5 Specifications students should practice writing

Reading a specification is easier than writing one. The following are propositions about list functions. Practice writing them yourself, then check against these.

"filter keeps exactly the elements satisfying the predicate":

-- ∀ x, x ∈ filter p xs ↔ x ∈ xs ∧ p x = true
theorem mem_filter_iff (p : α → Bool) (xs : List α) (x : α) :
    x ∈ xs.filter p ↔ x ∈ xs ∧ p x = true :=
  List.mem_filter

-- "length of filter is at most length of input"
theorem filter_length_le (p : α → Bool) (xs : List α) :
    (xs.filter p).length ≤ xs.length :=
  List.length_filter_le p xs

Exercises

1. State (as a Prop) the specification: "if n ∈ xs, then n ∈ xs ++ ys." Prove it using List.mem_append.

2. Use decide to verify: every element of [2, 4, 6, 8, 10] is even.

3. Use decide to verify: there exists an element in [3, 7, 12, 5] that is greater than 10.

4. State the specification: "map f (reverse xs) = reverse (map f xs)." This is List.map_reverse. Look it up and read the type.

5. Write a function myZip : List α → List β → List (α × β) that pairs corresponding elements. State its length specification: (myZip xs ys).length = min xs.length ys.length.

end Week05

-- FPCourse/Unit2/Week06_Trees.lean
import Mathlib.Data.List.Sort
import Mathlib.Order.Basic

Week 6: Trees and BST Invariants

Binary trees

A binary tree over type α is either a leaf or a node carrying a value and two subtrees. Like lists, trees are defined inductively, and functions on them are defined by structural recursion.

The key new idea this week: invariants. A BST (binary search tree) is not just any tree — it is a tree satisfying a predicate that constrains the relationship between each node's value and the values in its subtrees. That predicate is a proposition, and preserving it is a specification.

namespace Week06

6.1 The BTree type

inductive BTree (α : Type) where
  | leaf : BTree α
  | node : BTree α → α → BTree α → BTree α
deriving Repr

6.2 Basic tree functions

def BTree.size : BTree α → Nat
  | .leaf         => 0
  | .node l _ r   => l.size + 1 + r.size

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

def BTree.member [DecidableEq α] (x : α) : BTree α → Bool
  | .leaf         => false
  | .node l v r   => x == v || l.member x || r.member x

-- In-order traversal produces a list
def BTree.toList : BTree α → List α
  | .leaf         => []
  | .node l v r   => l.toList ++ [v] ++ r.toList

-- Specification of toList and size:
theorem toList_length_eq_size (t : BTree α) :
    t.toList.length = t.size := by
  induction t with
  | leaf => rfl
  | node l v r ihl ihr =>
    simp only [BTree.toList, BTree.size, List.length_append, List.length_cons,
               List.length_nil]
    omega

6.3 The BST predicate

A BST (for BTree Nat) is a tree where:

• Every value in the left subtree is strictly less than the root value.
• Every value in the right subtree is strictly greater than the root value.
• Both subtrees are themselves BSTs.

We express "every value in the subtree satisfies P" using an auxiliary predicate BTree.ForAll.

-- ForAll: every element of a tree satisfies a predicate
def BTree.ForAll (p : α → Prop) : BTree α → Prop
  | .leaf         => True
  | .node l v r   => p v ∧ l.ForAll p ∧ r.ForAll p

-- IsBST: the binary search tree invariant for Nat
inductive IsBST : BTree Nat → Prop where
  | leaf : IsBST .leaf
  | node : IsBST l → IsBST r
         → l.ForAll (· < v)
         → r.ForAll (v < ·)
         → IsBST (.node l v r)

-- We can check IsBST on concrete trees using decide,
-- once we make BTree.ForAll decidable:
instance decForAll (p : Nat → Prop) [DecidablePred p] :
    DecidablePred (BTree.ForAll p)
  | .leaf       => Decidable.isTrue trivial
  | .node l v r =>
    match decForAll p l, decForAll p r, inferInstanceAs (Decidable (p v)) with
    | Decidable.isTrue hl, Decidable.isTrue hr, Decidable.isTrue hv =>
      Decidable.isTrue ⟨hv, hl, hr⟩
    | Decidable.isFalse hl, _, _ =>
      Decidable.isFalse (fun ⟨_, h, _⟩ => hl h)
    | _, Decidable.isFalse hr, _ =>
      Decidable.isFalse (fun ⟨_, _, h⟩ => hr h)
    | _, _, Decidable.isFalse hv =>
      Decidable.isFalse (fun ⟨h, _, _⟩ => hv h)

6.4 BST insertion

Insert x into a BST, maintaining the invariant:

• If x < v, insert into the left subtree.
• If v < x, insert into the right subtree.
• If x = v, the element is already present.

def bstInsert (x : Nat) : BTree Nat → BTree Nat
  | .leaf         => .node .leaf x .leaf
  | .node l v r   =>
    if x < v then .node (bstInsert x l) v r
    else if v < x then .node l v (bstInsert x r)
    else .node l v r   -- x = v: already present

6.5 Preservation of ForAll

A key lemma: if all elements of t satisfy p, and p x holds, then all elements of bstInsert x t also satisfy p.

The provided proof is by structural recursion on t, mirroring the structure of bstInsert.

-- Provided term-mode proof of ForAll preservation.
theorem forAll_bstInsert (p : Nat → Prop) (x : Nat) (hx : p x) :
    ∀ t : BTree Nat, t.ForAll p → (bstInsert x t).ForAll p
  | .leaf,         _              => by simp [bstInsert, BTree.ForAll]; exact hx
  | .node l v r,  ⟨hv, hfl, hfr⟩ => by
    simp only [bstInsert]
    split_ifs with hlt hgt
    · exact ⟨hv, forAll_bstInsert p x hx l hfl, hfr⟩
    · exact ⟨hv, hfl, forAll_bstInsert p x hx r hfr⟩
    · exact ⟨hv, hfl, hfr⟩

6.6 Preservation of IsBST

If t is a BST and x : Nat, then bstInsert x t is also a BST.

The proof uses forAll_bstInsert twice per recursive case — once for the left bound and once for the right — along with the structurally recursive IsBST assumption.

theorem bstInsert_isBST (x : Nat) :
    ∀ t : BTree Nat, IsBST t → IsBST (bstInsert x t)
  | .leaf,        _ => by
    simp [bstInsert]
    exact IsBST.node IsBST.leaf IsBST.leaf trivial trivial
  | .node l v r,  IsBST.node hl hr hfl hfr => by
    simp only [bstInsert]
    split_ifs with hlt hgt
    · exact IsBST.node (bstInsert_isBST x l hl) hr
        (forAll_bstInsert (· < v) x hlt l hfl) hfr
    · exact IsBST.node hl (bstInsert_isBST x r hr)
        hfl (forAll_bstInsert (v < ·) x hgt r hfr)
    · exact IsBST.node hl hr hfl hfr

6.7 Mutual recursion: Rose trees

A rose tree has nodes with arbitrarily many children (stored as a list). Defining rose trees requires mutual recursion between the tree type and the forest (list of trees) type.

mutual
  inductive RoseTree (α : Type) where
    | node : α → Forest α → RoseTree α

  inductive Forest (α : Type) where
    | nil  : Forest α
    | cons : RoseTree α → Forest α → Forest α
end

mutual
  def roseSize : RoseTree α → Nat
    | .node _ f => forestSize f + 1

  def forestSize : Forest α → Nat
    | .nil      => 0
    | .cons t f => roseSize t + forestSize f
end

Exercises

1. Define BTree.map (f : α → β) : BTree α → BTree β and state its specification: "map f preserves size."

2. Define a BTree.search (x : Nat) (t : BTree Nat) (h : IsBST t) : Bool that searches efficiently (O(log n) on balanced trees, O(n) worst case) by exploiting the BST invariant.

3. State (as a Prop) the correctness specification for bstInsert x t: "x is a member of bstInsert x t." You may use BTree.member.

4. Use decide to verify that the following tree IS a BST:

       5
      / \
     3   7
   

   Construct it as a BTree Nat value, then apply IsBST and check with decide.

5. State the specification for roseSize analogous to toList_length_eq_size.

end Week06

-- FPCourse/Unit2/Week07_PolymorphismDecidability.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

Week 7: Polymorphism and Decidability

Type variables and parametric polymorphism

A polymorphic function works uniformly for any type. Type variables (written with lowercase letters like α, β) stand for any type.

A function is parametrically polymorphic if its behavior does not depend on which type the variable is instantiated to. The type alone constrains what the function can do — a polymorphic f : List α → List α cannot inspect element values, so it can only permute, drop, or duplicate them.

namespace Week07

7.1 Polymorphic functions and their types

-- id works for any type
#check @id        -- (α : Type u) → α → α

-- const ignores its second argument
def myConst (a : α) (_ : β) : α := a
#check @myConst   -- (α β : Type u) → α → β → α

-- flip swaps argument order
def myFlip (f : α → β → γ) : β → α → γ := fun b a => f a b
#check @myFlip    -- (α β γ : Type u) → (α → β → γ) → β → α → γ

7.2 Bounded polymorphism: type class constraints

Sometimes a polymorphic function needs some knowledge about the type. Type classes express this: [DecidableEq α] says "α must have a decidable equality test." The constraint is explicit in the type.

-- Without DecidableEq, we cannot compare elements
def contains [DecidableEq α] (x : α) : List α → Bool
  | []      => false
  | h :: t  => x == h || contains x t

-- The type class constraint is part of the specification:
-- "for any type α with decidable equality, ..."
theorem contains_spec [DecidableEq α] (x : α) (xs : List α) :
    contains x xs = true ↔ x ∈ xs := by
  induction xs with
  | nil => simp [contains]
  | cons h t ih =>
    simp only [contains, List.mem_cons]
    constructor
    · intro hc
      by_cases heq : x = h
      · left; exact heq
      · right
        have : contains x t = true := by
          have hne : (x == h) = false := beq_eq_false_iff_ne.mpr heq
          simp [hne] at hc
          exact hc
        exact ih.mp this
    · intro hm
      cases hm with
      | inl heq => simp [contains, heq]
      | inr ht  =>
        simp [contains]
        right
        exact ih.mpr ht

7.3 The DecidableEq type class

DecidableEq α is a type class that provides, for every pair a b : α, a decision: either a proof that a = b or a proof that a ≠ b.

class DecidableEq (α : Type u) where
  decEq : (a b : α) → Decidable (a = b)

Instances of Decidable:

inductive Decidable (p : Prop) where
  | isFalse : ¬p → Decidable p
  | isTrue  :  p → Decidable p

A Decidable value IS either a proof of p or a proof of ¬p. When decide is used as a proof term, it extracts the isTrue h component and provides h : p.

Types with DecidableEq: Nat, Int, Bool, Char, String, List α (when α has it), Option α (when α has it), and all types you define with deriving DecidableEq.

Types WITHOUT DecidableEq: functions α → β in general (you cannot check f = g by running them), and — crucially — Float.

-- Nat has DecidableEq:
example : DecidableEq Nat := inferInstance
example : (3 : Nat) = 3 ∨ (3 : Nat) ≠ 3 := by decide

-- Bool has DecidableEq:
example : DecidableEq Bool := inferInstance

-- List Nat has DecidableEq:
example : DecidableEq (List Nat) := inferInstance
example : ([1, 2, 3] : List Nat) = [1, 2, 3] := by decide

7.4 Float and the absence of DecidableEq

Float represents IEEE 754 double-precision floating-point numbers. IEEE 754 specifies that NaN ≠ NaN — the special "not a number" value is not equal to itself.

This violates the reflexivity of equality: ∀ x, x = x. Lean's equality is reflexive by definition (rfl : a = a). If Float had DecidableEq, we could derive NaN = NaN (by rfl), contradicting IEEE 754.

Therefore Float does NOT have a DecidableEq instance in Lean. This is not a missing feature. It is the type system correctly refusing to certify something that is not true.

The practical consequence:

• You CANNOT use decide to prove propositions involving Float equality.
• You CANNOT use Float values as keys in structures requiring DecidableEq.
• Specifications about floating-point programs must use Real or Rat for the mathematical content, with a separate claim about approximation.

More importantly, this is a lesson that applies in every programming language: never use == to compare floating-point values. The same IEEE 754 semantics that breaks DecidableEq here — NaN ≠ NaN, and rounding means two computations of "the same" value may produce slightly different results — make floating-point equality unreliable in Python, Java, C, and everywhere else. Always compare floats with a tolerance: |x - y| < ε.

-- Float DOES have BEq (Boolean equality), but that is NOT the same as =
#check (inferInstance : BEq Float)   -- BEq Float is available

-- BEq.beq : α → α → Bool   -- a computation returning Bool
-- Decidable (a = b)          -- a proof of a logical claim
-- These are different things.

-- The == operator on Float uses BEq, not DecidableEq.
-- It handles NaN by returning false, matching IEEE 754.
-- #eval (Float.nan == Float.nan : Bool)    -- false  (IEEE 754)

-- But we CANNOT write:
-- example : (1.0 : Float) = 1.0 := decide   -- DOES NOT COMPILE

-- We CAN write specifications using Real (the mathematical reals):
-- "the floating-point addition of x and y approximates real addition"
-- ∀ x y : Float, |Float.toReal (x + y) - (Float.toReal x + Float.toReal y)| < ε
-- This is a real-valued specification; its verification uses a different
-- methodology (floating-point error analysis).

7.5 Summary: the decidability boundary

Reading ∀ and ∃. Two quantifiers appear throughout this table and the rest of the course. Read them aloud as follows:

• ∀ x : α, P x — "for every x of type α, the proposition P x holds"
• ∃ x : α, P x — "there exists some x of type α such that P x holds"

Both are types. A proof of ∀ x : α, P x is a function (x : α) → P x — given any x, produce a proof of P x. A proof of ∃ x : α, P x is a dependent pair ⟨witness, proof⟩ — a specific value together with a proof that the claim holds for that value.

This table is one of the most important things in the course.

Exercises

1. Define a polymorphic function myNub [DecidableEq α] : List α → List α that removes duplicate elements. State its specification: "every element of the result appears in the input, and no element appears twice."

2. Explain in your own words why Float cannot have DecidableEq. What goes wrong if you assume it does?

3. Use decide to check: "hello" = "hello" as a Prop. Then explain why this works but (1.0 : Float) = 1.0 does not.

4. Give an example of a type you define yourself, add deriving DecidableEq, and use decide to check an equality proposition about it.

5. Define a type Color with constructors Red, Green, Blue and add deriving DecidableEq. Use decide to prove: (a) Color.Red ≠ Color.Blue (b) ∀ c ∈ [Color.Red, Color.Green, Color.Blue], c = Color.Red ∨ c ≠ Color.Red Explain why decide can handle this but could not handle the same claim over all Nat values.

end Week07

-- FPCourse/Unit3/Week08_HigherOrderFunctions.lean
import Mathlib.Data.List.Basic

Week 8: Higher-Order Functions

Functions as values

A higher-order function takes other functions as arguments or returns functions as results. In a typed functional language, this is not a special case — functions are values like any other, and → is a type constructor like × or List.

Higher-order functions enable abstraction over computation patterns. Rather than writing separate functions for "sum all elements" and "product all elements," we write one function fold parameterized by the combining operation.

Every abstraction in this course corresponds to a specification pattern: a family of propositions that all instances must satisfy.

namespace Week08

8.1 map, filter, fold: the canonical trio

These three functions together cover an enormous range of list computations.

-- map: transform every element
#check @List.map      -- (α → β) → List α → List β

-- filter: keep elements satisfying a predicate
#check @List.filter   -- (α → Bool) → List α → List α

-- foldl: accumulate from the left
#check @List.foldl    -- (β → α → β) → β → List α → β

-- foldr: accumulate from the right
#check @List.foldr    -- (α → β → β) → β → List α → β

-- Evaluation traces for the three canonical operations:
-- map (·*2) [1,2,3]  ↝  [1*2, 2*2, 3*2]  ↝  [2, 4, 6]   (β-reduce per element)
-- filter even [1,2,3,4] ↝ keep 2, keep 4 ↝ [2, 4]        (evaluate predicate per element)
-- foldl (+) 0 [1,2,3]  ↝  foldl (+) 1 [2,3]              (0+1=1)
--                       ↝  foldl (+) 3 [3]                (1+2=3)
--                       ↝  foldl (+) 6 []                 (3+3=6)
--                       ↝  6                               (base case)
#eval [1,2,3,4,5].map (· * 2)              -- [2,4,6,8,10]
#eval [1,2,3,4,5].filter (· % 2 == 0)      -- [2,4]
#eval [1,2,3,4,5].foldl (· + ·) 0          -- 15
#eval [1,2,3,4,5].foldr (· :: ·) []        -- [1,2,3,4,5]

8.2 Deriving map from fold

map can be expressed as a foldr:

def mapViaFoldr (f : α → β) (xs : List α) : List β :=
  xs.foldr (fun x acc => f x :: acc) []

-- Specification: mapViaFoldr agrees with List.map
theorem mapViaFoldr_eq_map (f : α → β) (xs : List α) :
    mapViaFoldr f xs = xs.map f :=
  List.recOn xs
    rfl
    (fun h t ih => congrArg (f h :: ·) ih)

-- Similarly, filter can be expressed as foldr:
def filterViaFoldr (p : α → Bool) (xs : List α) : List α :=
  xs.foldr (fun x acc => if p x then x :: acc else acc) []

8.3 The functor laws

List.map satisfies two functor laws. These are propositions — logical types — that any correct implementation of map must inhabit.

Law 1 (Identity): mapping the identity function does nothing. Law 2 (Composition): mapping a composition equals composing two maps.

These laws are not just bureaucratic requirements. They are the algebraic content of what it means to "transform elements without changing structure."

-- Functor Law 1: map id = id
-- Read: "for all lists, mapping the identity is the identity"
theorem map_id_law : ∀ xs : List α, xs.map id = xs :=
  List.map_id

-- Functor Law 2: map (f ∘ g) = map f ∘ map g
-- Read: "for all f, g, lists: mapping their composition equals
--        mapping g then mapping f"
theorem map_comp_law : ∀ (f : β → γ) (g : α → β) (xs : List α),
    xs.map (f ∘ g) = (xs.map g).map f :=
  fun f g xs => by simp [← List.map_map]

8.4 Writing law statements for other types

A key skill: given a new type with a map-like operation, state the functor laws for it. The laws have the same FORM regardless of the type.

Here are the laws for Option.map:

-- You should read these and understand their form.
-- Then practice writing them for new types (see exercises).

theorem option_map_id : ∀ o : Option α, o.map id = o :=
  fun o => congr_fun Option.map_id o

theorem option_map_comp : ∀ (f : β → γ) (g : α → β) (o : Option α),
    o.map (f ∘ g) = (o.map g).map f :=
  fun f g o => (Option.map_map f g o).symm

8.5 fold and its specification pattern

foldr f z replaces each :: constructor with f and the terminal [] with z.

The key specification insight: many list properties are theorems about foldr. Length, sum, map, filter, append — all can be stated as foldr computations. The specification of foldr itself is therefore the specification of a whole family of operations.

-- foldr specification: reconstructing the list
theorem foldr_cons_nil (xs : List α) :
    xs.foldr (· :: ·) [] = xs :=
  List.foldr_cons_nil

-- foldr and append:
theorem foldr_append (f : α → β → β) (z : β) (xs ys : List α) :
    (xs ++ ys).foldr f z = xs.foldr f (ys.foldr f z) :=
  List.foldr_append

8.6 The fusion law

When a map is followed immediately by a fold, they can be fused into a single fold. This is a semantic optimization: the two-pass computation is equal to the single-pass computation.

Fusion laws are propositions. Compilers use them as rewrite rules. We state them here as types; applying them requires knowing they hold.

-- map-foldr fusion:
-- foldr f z (map g xs) = foldr (f ∘ g) z xs
theorem map_foldr_fusion (f : β → γ → γ) (z : γ) (g : α → β) (xs : List α) :
    (xs.map g).foldr f z = xs.foldr (f ∘ g) z :=
  List.recOn xs
    rfl
    (fun h t ih => congrArg (f (g h) ·) ih)

Exercises

1. State the functor laws for a type you define:

   inductive MyPair (α : Type) where
     | mk : α → α → MyPair α
   def MyPair.map (f : α → β) : MyPair α → MyPair β
     | .mk a b => .mk (f a) (f b)
   

   Write the identity and composition laws as Prop terms. Use decide on concrete instances to check them.

2. Define sumList : List Nat → Nat using foldl. State the specification: sumList xs = xs.foldl (· + ·) 0.

3. State (as a Prop) the specification that filter p and filter q commute: filter p (filter q xs) = filter q (filter p xs). Is this always true? If not, give a counterexample.

4. Write flatMap (f : α → List β) : List α → List β using foldr. State its specification in terms of List.bind.

5. Write flatten : List (List α) → List α using foldr that concatenates a list of lists. Test it:

   #eval flatten [[1, 2], [3], [4, 5, 6]]   -- [1, 2, 3, 4, 5, 6]
   #eval flatten ([] : List (List Nat))      -- []
   

   State its specification: ∀ xss, flatten xss = List.join xss. Then write countWhere : (α → Bool) → List α → Nat using foldr that counts elements satisfying a predicate. Test:

   #eval countWhere Nat.even [1, 2, 3, 4, 5]   -- 2
   

end Week08

-- FPCourse/Unit3/Week09_Specifications.lean
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Pairwise

open scoped List

Week 9: Specifications in Practice

What is a correct sort?

Sorting is one of the most studied problems in computer science, yet most textbooks define correctness informally. We will define it precisely as a type.

A correct sorting function must satisfy two independent conditions:

1. Sorted output: the result list is in non-decreasing order.
2. Permutation: the result contains exactly the same elements as the input, in the same multiplicity.

Both conditions are needed. Without "sorted": returning the empty list or a constant list would satisfy "permutation" alone. Without "permutation": returning [] would satisfy "sorted" alone.

Together, they express exactly what we mean by "correctly sorts."

namespace Week09

-- List.Sorted is now List.Pairwise in Lean 4.28 / Mathlib
abbrev List.Sorted (r : α → α → Prop) (xs : List α) : Prop := List.Pairwise r xs

9.1 The Sorted predicate

List.Sorted r xs holds iff every adjacent pair in xs satisfies r. We use (· ≤ ·) for ascending order.

-- Sorted is now an alias for List.Pairwise:
#check @List.Pairwise   -- (r : α → α → Prop) → List α → Prop

-- Examples — use decide on concrete lists:
example : List.Sorted (· ≤ ·) ([1, 2, 3, 4] : List Nat) := by decide
example : ¬ List.Sorted (· ≤ ·) ([1, 3, 2] : List Nat) := by decide
example : List.Sorted (· ≤ ·) ([] : List Nat) := by decide   -- vacuously

9.2 The Perm predicate

List.Perm xs ys (written xs ~ ys) holds iff xs is a permutation of ys. Equivalently: both lists contain the same elements with the same multiplicities.

#check @List.Perm   -- List α → List α → Prop

-- Examples:
example : ([1, 2, 3] : List Nat) ~ [3, 1, 2] := by decide
example : ([1, 2, 3] : List Nat) ~ [1, 2, 3] := List.Perm.refl _
example : ¬ ([1, 2] : List Nat) ~ [1, 2, 3] := by decide

-- Perm is symmetric, transitive, and congruent with respect to cons.
theorem perm_symm (xs ys : List α) : xs ~ ys → ys ~ xs :=
  List.Perm.symm

9.3 The CorrectSort specification

This is the heart of the week: a single type that captures what it means for a function to be a correct sorting function.

-- Read aloud: "for every list xs of Nat,
--   (sort xs is sorted) AND (sort xs is a permutation of xs)"
-- The ∀ quantifies over all possible inputs.
-- The ∧ bundles the two conditions that must BOTH hold.
def CorrectSort (sort : List Nat → List Nat) : Prop :=
  ∀ xs : List Nat,
    List.Sorted (· ≤ ·) (sort xs) ∧   -- output is sorted
    sort xs ~ xs                        -- output is a permutation of input

9.4 Insertion sort: implementation

Insertion sort inserts each element of the input into the correct position in an already-sorted list.

def insert' (x : Nat) : List Nat → List Nat
  | []      => [x]
  | h :: t  => if x ≤ h then x :: h :: t else h :: insert' x t

def insertionSort : List Nat → List Nat
  | []      => []
  | h :: t  => insert' h (insertionSort t)

#eval insertionSort [5, 3, 1, 4, 2]    -- [1, 2, 3, 4, 5]
#eval insertionSort []                  -- []

9.5 Proving CorrectSort — provided term-mode proofs

Proving CorrectSort insertionSort requires two sub-proofs. Both are provided here as term-mode proofs for you to read.

Helper 1: inserting into a sorted list produces a sorted list.

-- Local helper for insert_sorted
private theorem insert_perm' (x : Nat) :
    ∀ xs : List Nat, insert' x xs ~ x :: xs
  | []      => List.Perm.refl _
  | h :: t  => by
    simp only [insert']
    split_ifs with hle
    · exact List.Perm.refl _
    · exact List.Perm.trans
        (List.Perm.cons h (insert_perm' x t))
        (List.Perm.swap x h t)

theorem insert_sorted (x : Nat) :
    ∀ xs : List Nat, List.Sorted (· ≤ ·) xs →
      List.Sorted (· ≤ ·) (insert' x xs)
  | [], _ => List.pairwise_singleton (· ≤ ·) x
  | h :: t, hst => by
    simp only [insert']
    split_ifs with hle
    · -- x ≤ h: insert x at front
      apply List.Pairwise.cons
      · intro y hy
        simp only [List.mem_cons] at hy
        cases hy with
        | inl heq =>
          exact heq ▸ hle
        | inr hmem =>
          exact Nat.le_trans hle ((List.pairwise_cons.mp hst).1 y hmem)
      · exact hst
    · -- x > h: insert into tail
      have hxh : h ≤ x := Nat.le_of_not_le hle
      apply List.Pairwise.cons
      · intro y hy
        have : y ∈ x :: t := (insert_perm' x t).subset hy
        simp only [List.mem_cons] at this
        cases this with
        | inl heq => exact heq ▸ hxh
        | inr hmem => exact (List.pairwise_cons.mp hst).1 y hmem
      · exact insert_sorted x t (List.pairwise_cons.mp hst).2

Helper 2: inserting preserves the permutation relation.

theorem insert_perm (x : Nat) :
    ∀ xs : List Nat, insert' x xs ~ x :: xs
  | []      => List.Perm.refl _
  | h :: t  => by
    simp only [insert']
    split_ifs with hle
    · exact List.Perm.refl _
    · exact List.Perm.trans
        (List.Perm.cons h (insert_perm x t))
        (List.Perm.swap x h t)

Helper 3: insertion sort produces a sorted list.

theorem insertionSort_sorted :
    ∀ xs : List Nat, List.Sorted (· ≤ ·) (insertionSort xs)
  | []      => List.Pairwise.nil
  | h :: t  => insert_sorted h (insertionSort t) (insertionSort_sorted t)

Helper 4: insertion sort is a permutation.

theorem insertionSort_perm :
    ∀ xs : List Nat, insertionSort xs ~ xs
  | []      => List.Perm.refl _
  | h :: t  =>
    List.Perm.trans
      (insert_perm h (insertionSort t))
      (List.Perm.cons h (insertionSort_perm t))

Main theorem: insertion sort is correct.

theorem insertionSort_correct : CorrectSort insertionSort :=
  fun xs => ⟨insertionSort_sorted xs, insertionSort_perm xs⟩

9.6 Verifying on concrete instances

Because Sorted and Perm are decidable on List Nat, we can check correctness on concrete examples with decide.

example : List.Sorted (· ≤ ·) (insertionSort [3, 1, 4, 1, 5, 9]) := by decide
example : insertionSort [3, 1, 4, 1, 5] ~ [3, 1, 4, 1, 5] := by decide

9.7 Specifications with pre- and postconditions

A more general specification pattern uses explicit pre- and postconditions attached to function types. This is the proof-carrying type pattern generalized.

-- A function with a precondition in its type:
def sortedMerge
    (xs ys : List Nat)
    (hxs : List.Sorted (· ≤ ·) xs)
    (hys : List.Sorted (· ≤ ·) ys) :
    { zs : List Nat // List.Sorted (· ≤ ·) zs ∧ zs ~ xs ++ ys } :=
  -- Implementation omitted; the TYPE is the specification.
  -- Any implementation must produce a Σ-type (subtype) carrying the proof.
  ⟨(xs ++ ys).mergeSort (· ≤ ·),
   ⟨List.pairwise_mergeSort' (· ≤ ·) (xs ++ ys),
    List.mergeSort_perm (xs ++ ys) (· ≤ ·)⟩⟩

Exercises

1. Use decide to check that insertionSort [9, 1, 3, 7, 2, 6] produces a sorted list.

2. State the specification for a dedup : List Nat → List Nat function that removes duplicate elements. What two properties must it satisfy?

3. Define CorrectSort' for descending order and show insertionSort does NOT satisfy it by giving a counterexample with decide.

4. State (as a Prop) the specification: "if xs is already sorted, then insertionSort xs = xs." (You need not prove it.)

5. Write the type of a hypothetical mergeSort : List Nat → List Nat such that its type INCLUDES the proof that it satisfies CorrectSort. Use a subtype { f : List Nat → List Nat // CorrectSort f }.

end Week09

-- FPCourse/Unit4/Week10_SetsRelations.lean
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Function
import Mathlib.Logic.Relation

Week 10: Sets and Relations

Sets as predicates

In Lean (and in Mathlib), a set over type α is simply a predicate:

def Set (α : Type u) : Type u := α → Prop

A set s : Set α is a function that takes an element x : α and returns a proposition s x : Prop — the claim that x belongs to s.

This definition is mathematically natural and computationally illuminating: membership is a proposition, and propositions are types. A proof that x ∈ s is a term of type s x.

The connection to the course themes: sets are logical types indexed by their elements. Every operation on sets is an operation on propositions.

namespace Week10

10.1 Set membership and basic notation

-- Set α is defined in Mathlib as α → Prop
#check @Set        -- (α : Type u) → Type u
#print Set         -- def Set (α : Type u) := α → Prop

-- Membership: x ∈ s is notation for s x
example : (3 : Nat) ∈ ({1, 2, 3} : Set Nat) := by decide
example : (5 : Nat) ∉ ({1, 2, 3} : Set Nat) := by decide

-- The universal set (all elements)
#check @Set.univ   -- Set α  (= fun _ => True)

-- The empty set
#check (∅ : Set _)  -- Set α  (= fun _ => False)

-- Membership in univ and empty:
theorem mem_univ (x : α) : x ∈ (Set.univ : Set α) :=
  trivial

theorem not_mem_empty (x : α) : x ∉ (∅ : Set α) :=
  False.elim

10.2 Set operations as proposition operations

Because sets are predicates, every set operation corresponds to a propositional connective.

Read s ⊆ t aloud: "for every x, if x belongs to s then x belongs to t." Read s ∩ t = s ∪ t would mean: "for every x, x ∈ s ∧ x ∈ t iff x ∈ s ∨ x ∈ t" — which is false.

Notice the pattern: every set statement reduces to a statement about propositions, quantified over elements. When you prove something about sets, you are doing propositional logic with ∀ threading through.

-- Intersection is ∧:
theorem mem_inter_iff (x : α) (s t : Set α) :
    x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t :=
  Set.mem_inter_iff x s t

-- Union is ∨:
theorem mem_union_iff (x : α) (s t : Set α) :
    x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t :=
  Set.mem_union x s t

-- Subset is ∀/→:
theorem subset_def (s t : Set α) :
    s ⊆ t ↔ ∀ x, x ∈ s → x ∈ t :=
  Iff.intro (fun h x hx => h hx) (fun h x hx => h x hx)

10.3 Set algebraic laws as propositions

These laws are propositions that hold for all sets. The proofs are provided as term-mode proofs.

-- Commutativity:
theorem inter_comm (s t : Set α) : s ∩ t = t ∩ s :=
  Set.inter_comm s t

theorem union_comm (s t : Set α) : s ∪ t = t ∪ s :=
  Set.union_comm s t

-- Distributivity:
theorem inter_union_distrib (r s t : Set α) :
    r ∩ (s ∪ t) = (r ∩ s) ∪ (r ∩ t) :=
  Set.inter_union_distrib_left r s t

-- De Morgan:
theorem compl_union (s t : Set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ :=
  Set.compl_union s t

-- Subset is transitive:
theorem subset_trans {s t u : Set α} (h1 : s ⊆ t) (h2 : t ⊆ u) : s ⊆ u :=
  Set.Subset.trans h1 h2

10.4 Relations

A relation between types α and β is a predicate on pairs:

def Rel (α β : Type u) : Type u := α → β → Prop

A term r : Rel α β applied to a : α and b : β gives a proposition r a b: the claim that a and b are related.

Sets are the special case Rel α α (homogeneous relations), or Rel α Prop (which is just Set α).

-- Rel is a binary predicate (defined locally for compatibility)
abbrev Rel (α β : Type*) := α → β → Prop

-- Example relations:
def divides : Rel Nat Nat := fun m n => ∃ k, n = m * k
def sameLength : Rel (List α) (List β) := fun xs ys => xs.length = ys.length
def lePair : Rel Nat Nat := (· ≤ ·)

-- Membership in a relation:
example : divides 3 12 := ⟨4, rfl⟩
example : divides 1 n := ⟨n, (Nat.one_mul n).symm⟩   -- for any n

10.5 Properties of relations

Key relational properties are propositions. We state each as a type so that checking a relation has the property means inhabiting the type.

-- Reflexive: every element is related to itself
def RelReflexive (r : Rel α α) : Prop := ∀ a, r a a

-- Symmetric: if a is related to b then b is related to a
def RelSymmetric (r : Rel α α) : Prop := ∀ a b, r a b → r b a

-- Transitive: r a b and r b c implies r a c
def RelTransitive (r : Rel α α) : Prop := ∀ a b c, r a b → r b c → r a c

-- An equivalence relation satisfies all three:
def Equivalence' (r : Rel α α) : Prop :=
  RelReflexive r ∧ RelSymmetric r ∧ RelTransitive r

-- ≤ on Nat is reflexive and transitive but not symmetric:
example : RelReflexive (· ≤ · : Rel Nat Nat) :=
  fun a => Nat.le_refl a

example : RelTransitive (· ≤ · : Rel Nat Nat) :=
  fun _ _ _ => Nat.le_trans

example : ¬ RelSymmetric (· ≤ · : Rel Nat Nat) :=
  fun h => absurd (h 0 1 (Nat.zero_le 1)) (by decide)

-- = on Nat is an equivalence relation:
example : Equivalence' (· = · : Rel Nat Nat) :=
  ⟨fun _ => rfl,
   fun _ _ h => h.symm,
   fun _ _ _ h1 h2 => h1.trans h2⟩

10.6 Relational composition and image

Composition of relations: r composed with s relates a to c if there exists a b such that r a b and s b c.

Image of a set under a relation: the set of all elements reachable from s by following r.

-- Relational composition:
def relComp (r : Rel α β) (s : Rel β γ) : Rel α γ :=
  fun a c => ∃ b, r a b ∧ s b c

-- Image of a set under a function (as a relation):
#check @Set.image
-- Set.image : (α → β) → Set α → Set β
-- (Set.image f s) b ↔ ∃ a ∈ s, f a = b

-- Preimage:
#check @Set.preimage
-- Set.preimage : (α → β) → Set β → Set α
-- (Set.preimage f t) a ↔ f a ∈ t

-- Image of the universal set is the range:
theorem image_univ (f : α → β) :
    Set.image f Set.univ = Set.range f :=
  Set.image_univ

10.7 Functions as total relations

A function f : α → β determines a functional relation: the set of pairs {(a, f a) | a : α}. A relation is functional if every element of the domain is related to exactly one element of the codomain.

Sets and relations are the language in which we write specifications for programs dealing with collections of data. The Dict type class (Week 11) is a partial function — a relation where each key relates to at most one value. Sorting is about relations between the input and output lists.

Exercises

1. State De Morgan's laws for sets as Lean Prop terms. Do not prove them — just write the types: (a) ∀ (s t : Set α) (x : α), x ∈ (s ∪ t)ᶜ ↔ x ∈ sᶜ ∧ x ∈ tᶜ (b) ∀ (s t : Set α) (x : α), x ∈ (s ∩ t)ᶜ ↔ x ∈ sᶜ ∨ x ∈ tᶜ Look up Set.compl_union and Set.compl_inter in Mathlib and compare your statements to theirs. Notice that De Morgan's law for sets IS De Morgan's law for propositions, applied pointwise to elements.

2. Define the relation IsPrefix : Rel (List α) (List α) where xs is a prefix of ys if there exists zs such that xs ++ zs = ys:

   def IsPrefix (xs ys : List α) : Prop := ∃ zs, xs ++ zs = ys
   

   State (as Props, without proving them) that IsPrefix is reflexive and transitive. What would a proof of reflexivity look like? (Hint: what zs witnesses xs ++ zs = xs?)

3. Show that divides is reflexive and transitive. Is it symmetric?

4. State what it means for a relation r : Rel α α to be an order (reflexive, transitive, and antisymmetric: r a b → r b a → a = b). Show that (· ≤ ·) on Nat satisfies this.

5. State the specification: "the image of s ∩ t under f is a subset of (Set.image f s) ∩ (Set.image f t)." This is Set.image_inter_subset. Look it up in Mathlib and read the type.

end Week10

-- FPCourse/Unit5/Week11_AbstractTypes.lean
import Mathlib.Data.List.Basic
import Mathlib.Data.Option.Basic

Week 11: Abstract Types

Abstraction via type classes

An abstract type presents an interface — a collection of operations with specified types — while hiding the implementation. Callers program against the interface; the implementation can change without affecting callers.

In Lean, type classes express abstract types. A class declaration is an interface. An instance declaration is an implementation. Laws stated in the class are the specification: propositions that every implementation must satisfy.

The connection to Week 10: the specification for Dict is relational. A dictionary is a partial function — a relation where each key maps to at most one value. The laws of Dict are laws of partial functions.

namespace Week11

11.1 The Dict interface

A dictionary maps keys to values. Operations: empty dict, insert, lookup, and delete.

class Dict (d : Type → Type → Type) where
  empty  : d k v
  insert : k → v → d k v → d k v
  lookup : [DecidableEq k] → k → d k v → Option v
  delete : [DecidableEq k] → k → d k v → d k v

11.2 Laws: the specification for Dict

The laws below are propositions that every Dict implementation must satisfy. They define what it MEANS to be a dictionary.

These are relational specifications in the sense of Week 10: they describe how the abstract state (a partial function from keys to values) changes under each operation.

class LawfulDict (d : Type → Type → Type) [DecidableEq k] extends Dict d where
  lookup_empty  : ∀ (key : k), lookup key (empty : d k v) = none
  lookup_insert_same : ∀ (key : k) (val : v) (m : d k v),
      lookup key (insert key val m) = some val
  lookup_insert_diff : ∀ (k1 k2 : k) (val : v) (m : d k v),
      k1 ≠ k2 → lookup k1 (insert k2 val m) = lookup k1 m
  lookup_delete_same : ∀ (key : k) (m : d k v),
      lookup key (delete key m) = none
  lookup_delete_diff : ∀ (k1 k2 : k) (m : d k v),
      k1 ≠ k2 → lookup k1 (delete k2 m) = lookup k1 m

11.3 Association list implementation

An association list stores key-value pairs in a list.

def AList (k v : Type) := List (k × v)

def AList.empty : AList k v := []

def AList.insert (key : k) (val : v) (m : AList k v) : AList k v :=
  (key, val) :: m

def AList.lookup [DecidableEq k] (key : k) : AList k v → Option v
  | []            => none
  | (k, v) :: t  => if key == k then some v else AList.lookup key t

def AList.delete [DecidableEq k] (key : k) : AList k v → AList k v
  | []            => []
  | (k, v) :: t  => if key == k then AList.delete key t
                    else (k, v) :: AList.delete key t

instance : Dict AList where
  empty  := AList.empty
  insert := AList.insert
  lookup := AList.lookup
  delete := AList.delete

-- Verify the laws hold.  Provided as term-mode proofs:
theorem alist_lookup_empty [DecidableEq k] (key : k) :
    AList.lookup key (AList.empty : AList k v) = none :=
  rfl

theorem alist_lookup_insert_same [DecidableEq k] (key : k) (val : v) (m : AList k v) :
    AList.lookup key (AList.insert key val m) = some val := by
  simp [AList.lookup, AList.insert]

theorem alist_lookup_insert_diff [DecidableEq k] {k1 k2 : k} (val : v)
    (m : AList k v) (hne : k1 ≠ k2) :
    AList.lookup k1 (AList.insert k2 val m) = AList.lookup k1 m := by
  simp [AList.lookup, AList.insert, hne]

11.4 Opaque types: hiding implementation details

The opaque keyword makes an identifier's definition irreducible to the elaborator. Proofs about an opaque value must work through the interface, not by unfolding the definition.

This is abstraction enforced by the type system: callers cannot depend on the implementation details even if they tried.

-- A counter type with an opaque implementation
opaque Counter : Type := Nat

@[instance] axiom Counter.instNonempty : Nonempty Counter

noncomputable opaque Counter.zero  : Counter
noncomputable opaque Counter.incr  : Counter → Counter
noncomputable opaque Counter.value : Counter → Nat

-- The specification is stated separately as axioms about the interface:
axiom Counter.value_zero : Counter.value Counter.zero = 0
axiom Counter.value_incr : ∀ c, Counter.value (Counter.incr c) =
                                Counter.value c + 1

-- Note: in a production library, these axioms would be proved as theorems
-- using the concrete implementation.  The opaque/axiom pattern separates
-- the interface (what callers see) from the implementation.

11.5 Stack: another abstract type

A stack supports push, pop, and peek, with a size operation. The specification: push then pop returns the original element and stack.

class Stack (s : Type → Type) where
  empty : s α
  push  : α → s α → s α
  pop   : s α → Option (α × s α)
  size  : s α → Nat

class LawfulStack (s : Type → Type) extends Stack s where
  pop_empty  : pop (empty : s α) = none
  pop_push   : ∀ (x : α) (st : s α),
      pop (push x st) = some (x, st)
  size_empty : size (empty : s α) = 0
  size_push  : ∀ (x : α) (st : s α),
      size (push x st) = size st + 1

-- List implementation of Stack:
instance : Stack List where
  empty := []
  push  := List.cons
  pop   := fun
    | []      => none
    | h :: t  => some (h, t)
  size  := List.length

instance : LawfulStack List where
  pop_empty  := rfl
  pop_push   := fun _ _ => rfl
  size_empty := rfl
  size_push  := fun _ _ => rfl

11.6 Representation independence

The key property of abstract types: any two implementations satisfying the laws are observationally equivalent from the caller's perspective.

This is not just informal. Given two LawfulDict instances D1 and D2, any sequence of empty, insert, lookup, delete operations produces the same lookup results in both.

This can be stated as a theorem schema — for each sequence of operations, the lookup results agree. We will not prove this in full generality; stating it precisely is the skill being practiced.

Exercises

1. Add a size : d k v → Nat operation to Dict and extend LawfulDict with laws relating size to insert and delete.

2. Implement Dict using a sorted association list. The lookup function can binary search (well, linear search in the sorted order). Verify the first two laws.

3. Write the LawfulStack instance for a new implementation:

   structure TwoListStack (α : Type) where
     front : List α
     back  : List α
   

   where push appends to back and pop takes from front (rebalancing by reversing back when front is empty).

4. State the representation independence theorem for Stack: "for any two LawfulStack instances S1 and S2, any program that only uses push, pop, size, and empty produces the same observable results in both." Write this as precisely as you can in Lean.

5. Define a Queue type class with enqueue/dequeue operations and state its laws.

end Week11

-- FPCourse/Unit5/Week12_TypeClassesDecidable.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

Week 12: Type Classes and the Decidable Type

What a type class really is

A type class is an interface with implementations provided by instances. We have seen type classes as abstract types (Week 11). This week we examine type classes as algebraic structures — sets with operations satisfying laws.

More importantly, we examine Decidable itself as an inductive type. Understanding Decidable as a data type — not magic — completes the picture of how decide works as a term-mode proof producer.

namespace Week12

12.1 Decidable: an inductive type carrying proofs

Decidable is defined in Lean's core library as:

inductive Decidable (p : Prop) where
  | isFalse : ¬p → Decidable p
  | isTrue  :  p → Decidable p

This is an ordinary inductive type. A value of type Decidable p is either:

• isFalse h where h : ¬p — a proof that p is false, OR
• isTrue h where h : p — a proof that p is true.

Decidable p does not just say "p is true or false" — it provides the proof of whichever is the case.

Evaluation. decide is not magic — it evaluates. When you write by decide to prove p, Lean:

1. Looks up the Decidable p instance (a value of type Decidable p).
2. Evaluates that instance to its normal form.
3. If the normal form is isTrue h, the proof h : p is extracted and used. The goal is closed.
4. If the normal form is isFalse h, elaboration fails — the goal is p but only a refutation exists.

The whole operation is reduction: evaluate the Decidable term, inspect the constructor, extract the payload. Every by decide in this course is exactly these four steps.

decide used as a proof term extracts the isTrue h component and returns h : p. If the instance is isFalse _, the file fails to compile.

-- We can inspect Decidable values directly:
#check @Decidable.isTrue   -- ∀ {p : Prop}, p → Decidable p
#check @Decidable.isFalse  -- ∀ {p : Prop}, ¬p → Decidable p

-- A Decidable value IS the proof:
example : Decidable (1 < 2) := Decidable.isTrue (by decide)
example : Decidable (2 < 1) := Decidable.isFalse (by decide)

-- The decEq function for Nat:
#check @Nat.decEq   -- (a b : Nat) → Decidable (a = b)

-- For any decidable proposition, we can extract the proof or refutation:
def toProofOrRefutation (p : Prop) [d : Decidable p] : p ∨ ¬p :=
  match d with
  | Decidable.isTrue h  => Or.inl h
  | Decidable.isFalse h => Or.inr h

12.2 DecidableEq as a type class instance

DecidableEq α is a type class (an alias for (a b : α) → Decidable (a = b)). An instance provides, for every pair of elements, a decision procedure.

-- Inspecting a DecidableEq instance:
#check (@Nat.decEq : DecidableEq Nat)

-- Using a DecidableEq instance explicitly:
def eqTest [DecidableEq α] (a b : α) : String :=
  match decEq a b with
  | Decidable.isTrue _  => "equal"
  | Decidable.isFalse _ => "not equal"

#eval eqTest (3 : Nat) 3    -- "equal"
#eval eqTest (3 : Nat) 4    -- "not equal"

12.3 Functor as a type class

A Functor is a type constructor F : Type → Type equipped with a map operation satisfying the two functor laws.

-- Our own Functor class with laws:
class MyFunctor (F : Type → Type) where
  fmap : (α → β) → F α → F β
  map_id  : ∀ (x : F α), fmap id x = x
  map_comp : ∀ (f : β → γ) (g : α → β) (x : F α),
      fmap (f ∘ g) x = fmap f (fmap g x)

-- List instance: the laws are theorems we proved in Week 8.
instance : MyFunctor List where
  fmap     := List.map
  map_id   := List.map_id
  map_comp := fun f g xs => by simp [← List.map_map]

-- Option instance:
instance : MyFunctor Option where
  fmap     := Option.map
  map_id   := fun o => congr_fun Option.map_id o
  map_comp := fun f g o => (Option.map_map f g o).symm

12.4 Foldable as a type class

class MyFoldable (F : Type → Type) where
  fold : (α → β → β) → β → F α → β

instance : MyFoldable List where
  fold := List.foldr

instance : MyFoldable Option where
  fold := fun f z o => o.elim z (fun x => f x z)

-- Specification: fold on List with cons/nil reconstructs the list
theorem list_fold_spec (xs : List α) :
    MyFoldable.fold (· :: ·) [] xs = xs :=
  List.foldr_cons_nil

-- Specification: fold on Option
theorem option_fold_none (f : α → β → β) (z : β) :
    MyFoldable.fold f z (none : Option α) = z :=
  rfl

theorem option_fold_some (f : α → β → β) (z : β) (x : α) :
    MyFoldable.fold f z (some x) = f x z :=
  rfl

12.5 Monoid: an algebraic structure with laws

class MyMonoid (α : Type) where
  one  : α
  mul  : α → α → α
  mul_one   : ∀ a : α, mul a one = a
  one_mul   : ∀ a : α, mul one a = a
  mul_assoc : ∀ a b c : α, mul (mul a b) c = mul a (mul b c)

-- Nat under addition:
instance : MyMonoid Nat where
  one       := 0
  mul       := (· + ·)
  mul_one   := Nat.add_zero
  one_mul   := Nat.zero_add
  mul_assoc := Nat.add_assoc

-- List under append:
instance : MyMonoid (List α) where
  one       := []
  mul       := (· ++ ·)
  mul_one   := List.append_nil
  one_mul   := List.nil_append
  mul_assoc := List.append_assoc

12.6 The boundary, revisited

After twelve weeks, we can state the decidability boundary precisely.

Decidable p holds (has an instance) when there is a terminating algorithm that produces either isTrue h : p or isFalse h : ¬p.

The boundary is not arbitrary:

• Nat equality: decidable. Algorithm: compare digit by digit.
• List equality (when element equality is decidable): decidable. Algorithm: compare element by element.
• Float equality: NOT decidable soundly, because NaN ≠ NaN would require an algorithm that produces isFalse h : ¬(NaN = NaN), but rfl : NaN = NaN would refute it. The instance cannot exist.
• Function equality: NOT decidable in general. To check f = g you would need to check all inputs — infinitely many.
• ∀ n : Nat, P n: NOT decidable in general. There is no algorithm that terminates and checks all natural numbers. (This is related to the halting problem.)

Understanding what is and is not decidable — and WHY — is one of the foundational concepts of computer science.

Exercises

1. Implement MyFunctor for the binary tree type from Week 6. State and prove the two functor laws for your implementation.

2. Show that Bool forms a MyMonoid under && with identity true. State and prove all three laws.

3. Write a function

   def mapDecide [DecidableEq α] (xs ys : List α) :
       List (α ⊕ α) := ...
   

   that pairs each element of xs with itself if it appears in ys (Sum.inl) and marks it missing otherwise (Sum.inr).

4. State the specification for MyFoldable.fold on lists: it must satisfy a "homomorphism" property with respect to append. Write this as a ∀ proposition.

5. Explain why Decidable (∀ n : Nat, n + 0 = n) nonetheless has an instance (inferInstance works). What is different about this ∀ compared to an arbitrary ∀ n : Nat, P n?

end Week12

-- FPCourse/Unit6/Week13_Streams.lean
import Mathlib.Data.List.Basic
import Mathlib.Data.Nat.Basic

Week 13: Streams and Lazy Types

Infinite data and lazy evaluation

Every data type we have defined so far is finite: you can always reach a leaf. But some computations naturally produce infinite sequences: the natural numbers, the Fibonacci sequence, an infinite stream of sensor readings.

Lean's reduction strategy is strict (call-by-value): arguments are evaluated before being passed. To build infinite structures, we must delay evaluation explicitly using Thunk.

A Thunk α is a suspended computation of type α. It is not evaluated until forced. By building infinite structures out of Thunks, we can represent them finitely in memory and compute as many elements as needed.

namespace Week13

13.1 Thunk: explicit laziness

-- Thunk is defined in Lean's core library:
-- structure Thunk (α : Type u) where mk ::
--   fn : Unit → α
-- A Thunk wraps a function from Unit → α.
-- Calling .get on a Thunk forces evaluation.

#check @Thunk      -- Type u → Type u
#check @Thunk.get  -- Thunk α → α
#check @Thunk.mk   -- (Unit → α) → Thunk α

-- Creating and forcing a Thunk:
def lazyFive : Thunk Nat := Thunk.mk (fun _ => 2 + 3)
#eval lazyFive.get   -- 5  (computed only when forced)

13.2 Lazy lists (streams)

A lazy list is either empty or a head value paired with a thunked tail. The tail is not computed until needed.

inductive LList (α : Type) where
  | nil  : LList α
  | cons : α → Thunk (LList α) → LList α

-- Take the first n elements as a strict list:
def LList.take : Nat → LList α → List α
  | 0,     _            => []
  | _,     .nil         => []
  | n + 1, .cons h t    => h :: LList.take n t.get

-- Drop the first n elements:
def LList.drop : Nat → LList α → LList α
  | 0,     s            => s
  | _,     .nil         => .nil
  | n + 1, .cons _ t    => LList.drop n t.get

13.3 Canonical infinite streams

-- LList is always nonempty (it has a constructor)
instance : Nonempty (LList α) := ⟨.nil⟩

-- The infinite stream of a constant value:
partial def LList.repeat (x : α) : LList α :=
  .cons x (Thunk.mk (fun _ => LList.repeat x))

-- The natural numbers: 0, 1, 2, 3, ...
private partial def natsFrom (n : Nat) : LList Nat :=
  .cons n (Thunk.mk (fun _ => natsFrom (n + 1)))

def nats : LList Nat := natsFrom 0

-- Fibonacci numbers: 1, 1, 2, 3, 5, 8, ...
private partial def fibsFrom (a b : Nat) : LList Nat :=
  .cons a (Thunk.mk (fun _ => fibsFrom b (a + b)))

def fibs : LList Nat := fibsFrom 0 1

-- Test:
#eval LList.take 10 nats    -- [0,1,2,3,4,5,6,7,8,9]
#eval LList.take 10 fibs    -- [0,1,1,2,3,5,8,13,21,34]

13.4 Map on streams

def LList.map (f : α → β) : LList α → LList β
  | .nil       => .nil
  | .cons h t  => .cons (f h) (Thunk.mk (fun _ => LList.map f t.get))

-- Specification: map f on the first n elements equals
-- mapping f on the taken list.
-- This is a provided term-mode proof.
theorem map_take (f : α → β) (n : Nat) :
    ∀ xs : LList α, (xs.map f).take n = (xs.take n).map f := by
  induction n with
  | zero => intro xs; rfl
  | succ n ih =>
    intro xs
    cases xs with
    | nil  => simp [LList.take, LList.map]
    | cons h t =>
        simp only [LList.map, LList.take]
        exact congrArg (f h :: ·) (ih t.get)

13.5 Filter on streams

Filter on an infinite stream is partial: if the predicate is always false, filter never terminates. We cannot define a total filter on streams in Lean without restricting the predicate or using partial.

This is a fundamental difference from lists. On a finite list, filter always terminates. On an infinite stream, it may not.

This connects back to Week 3: Lean's type system only accepts total functions. A stream filter would require partial, losing the ability to prove properties about it.

We CAN define filter on a taken prefix:

def LList.takeWhile (p : α → Bool) : LList α → List α
  | .nil       => []
  | .cons h t  => if p h then h :: LList.takeWhile p t.get else []

#eval LList.takeWhile (· < 5) nats    -- [0,1,2,3,4]

13.6 Coinduction: specifications about infinite streams

For finite data, we use induction to prove properties: "for all finite inputs, the property holds."

For infinite data (streams), we use coinduction: "the property holds at every finite prefix."

The specification of nats is a good example:

-- Specification: the nth element of nats is n.
-- Note: with partial definitions, we state the property but defer the proof.
theorem nats_take_eq : ∀ n : Nat, LList.take n nats = List.range n := by
  intro n
  induction n with
  | zero => rfl
  | succ n _ =>
    simp only [LList.take, nats, natsFrom, List.range_succ]
    sorry

13.7 Non-termination and the Thunk boundary

The Thunk type makes explicit what is delayed. Every time you see Thunk α in a type, you know: "this computation has not run yet."

The boundary between finite and infinite structures is the boundary between:

• Lean's total function world (Week 3: structural recursion, well-founded recursion)
• The partial world (where termination is not guaranteed)

Thunks do not cross this boundary. A Thunk value IS a term — it is just a function waiting to be called. The infinite structure exists as a description of how to produce any finite prefix; it does not actually exist as an infinite object in memory.

This is computationally honest: real programs do not hold infinite structures; they hold descriptions and lazily demand pieces.

Exercises

1. Define LList.zip : LList α → LList β → LList (α × β) that pairs corresponding elements. State its specification: (zip xs ys).take n = (xs.take n).zip (ys.take n).

2. Define LList.interleave : LList α → LList α → LList α that alternates between two streams. State its specification.

3. Define the stream of squares: 0, 1, 4, 9, 16, ... using LList.map on nats. Check with #eval that the first 10 elements are correct.

4. Explain why we cannot define:

   def LList.filter (p : α → Bool) : LList α → LList α
   

   as a total function in Lean. What would happen to the termination checker?

5. State the specification for LList.map in terms of take: "map f xs is the stream where the nth element is f applied to the nth element of xs." This is exactly map_take; read it and explain each part.

end Week13

-- FPCourse/Unit6/Week14_CurryHoward.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

Week 14: The Curry-Howard Correspondence

Naming what you already know

By this point in the course you have been living the Curry-Howard correspondence for thirteen weeks. This week we name it, state it precisely, and see it embodied in the capstone: a type-checker whose type is its correctness proof.

The Curry-Howard correspondence is the observation — discovered independently by Haskell Curry (1934) and William Howard (1969) — that the system of propositions and their proofs is isomorphic to the system of types and their terms. They are not analogous. They are the same thing, viewed from two angles.

Lean does not implement this correspondence. Lean is a system in which the correspondence is the foundational design principle. You have not been using an analogy; you have been using the real thing.

Look back at the core types introduced in this course: → is implication. × is conjunction. ⊕ is disjunction. Unit is truth. Empty is falsehood. ∀ is the dependent function type; ∃ is the dependent pair type. These are the constituents of the Curry-Howard correspondence. Types such as Option, List, and BTree are useful programming types built on top of that foundation, but the correspondence itself lives here. You have been working inside it since Week 0. This week names it.

That is also why this course is the direct prerequisite for CS2: Certified Proofs. CS2 does not introduce a new subject. It flips the orientation: from Type to Prop, from computing a value to proving a proposition. Every concept covered here — data definitions, specifications, recursion, higher-order functions, sets, relations, type classes — ports intact to that setting. The entire structure of this course is the foundation.

namespace Week14

14.1 The correspondence table

Each row of the following table presents two views of the same concept.

This is not a mapping we impose. These are the same thing.

-- Every row of the table, demonstrated:

-- Proposition / Type:
#check (1 + 1 = 2 : Prop)          -- a proposition
#check (1 + 1 = 2)                  -- the same proposition, as a type

-- Proof / Term:
example : 1 + 1 = 2 := rfl         -- rfl is the proof term

-- Implication / Function:
example : (1 = 1) → (1 = 1) := id  -- implication IS function type

-- Conjunction / Product:
example : 1 < 2 ∧ 2 < 3 :=
  And.intro (by decide) (by decide)  -- And.intro IS Prod.mk for Props

-- Disjunction / Sum:
example : 1 = 1 ∨ 1 = 2 := Or.inl rfl  -- Or.inl IS Sum.inl for Props

-- ∀ / Π type:
example : ∀ n : Nat, n + 0 = n := Nat.add_zero  -- a dependent function

-- ∃ / Σ type:
example : ∃ n : Nat, n > 100 := ⟨101, by decide⟩  -- a dependent pair

14.2 Proofs ARE terms: a demonstration

The following function and theorem look syntactically identical. That is not a coincidence.

-- A computational function:
def addOne : Nat → Nat := fun n => n + 1

-- A proof of an implication:
theorem oneImpliesOne : (1 = 1) → (1 = 1) := fun h => h

-- They have the same structure.  The types are different —
-- Nat and Prop — but the TERMS are constructed identically.

-- More striking: ∧-introduction and pair construction
def makePair : α → β → α × β := fun a b => (a, b)
theorem makeConjunction (h1 : P) (h2 : Q) : P ∧ Q := And.intro h1 h2

-- And.intro IS (essentially) Prod.mk, working on Props.

14.3 The capstone: a type-checker whose type is its proof

We define a small typed language and a type-checker for it. The type-checker's return type includes a proof that the expression is well-typed. Any expression that passes the checker comes with a certificate.

This is Curry-Howard in its most direct form: the act of type-checking IS the act of proof construction.

-- Types of our mini-language:
inductive Ty where
  | Nat  : Ty
  | Bool : Ty
  | Arr  : Ty → Ty → Ty   -- function type
deriving DecidableEq, Repr

-- Terms of our mini-language:
inductive Term where
  | natLit  : Nat → Term
  | boolLit : Bool → Term
  | var     : String → Term
  | app     : Term → Term → Term
  | lam     : String → Ty → Term → Term
deriving Repr

-- A typing context maps variable names to types:
def Context := List (String × Ty)

-- Context lookup:
def ctxLookup : Context → String → Option Ty
  | [],            _   => none
  | (x, τ) :: ctx, y  => if x == y then some τ else ctxLookup ctx y

14.4 The typing relation

The typing relation Typed ctx e τ is an inductive proposition: it holds exactly when expression e has type τ in context ctx.

This is the specification for the type-checker.

inductive Typed : Context → Term → Ty → Prop where
  | natLit  : Typed ctx (.natLit n) .Nat
  | boolLit : Typed ctx (.boolLit b) .Bool
  | var     : ctxLookup ctx x = some τ →
              Typed ctx (.var x) τ
  | app     : Typed ctx f (.Arr τ₁ τ₂) →
              Typed ctx e τ₁ →
              Typed ctx (.app f e) τ₂
  | lam     : Typed ((x, τ₁) :: ctx) body τ₂ →
              Typed ctx (.lam x τ₁ body) (.Arr τ₁ τ₂)

14.5 The type-checker

typecheck ctx e returns some ⟨τ, h⟩ where h : Typed ctx e τ if e is well-typed, and none otherwise.

The return type Option (Σ τ, Typed ctx e τ) IS the correctness specification. Any some result carries a proof.

def typecheck : (ctx : Context) → (e : Term) →
    Option (Σ' τ, Typed ctx e τ)
  | ctx, .natLit n  =>
    some ⟨.Nat, Typed.natLit⟩
  | ctx, .boolLit b =>
    some ⟨.Bool, Typed.boolLit⟩
  | ctx, .var x     =>
    match h : ctxLookup ctx x with
    | none   => none
    | some τ => some ⟨τ, Typed.var h⟩
  | ctx, .app f e   =>
    match typecheck ctx f, typecheck ctx e with
    | some ⟨.Arr τ₁ τ₂, hf⟩, some ⟨τ₁', he⟩ =>
      if h : τ₁ = τ₁' then
        some ⟨τ₂, Typed.app hf (h ▸ he)⟩
      else none
    | _, _ => none
  | ctx, .lam x τ₁ body =>
    match typecheck ((x, τ₁) :: ctx) body with
    | some ⟨τ₂, hbody⟩ => some ⟨.Arr τ₁ τ₂, Typed.lam hbody⟩
    | none              => none

14.6 Soundness: every result is correct

Soundness follows immediately from the return type: any time typecheck returns some ⟨τ, h⟩, h IS the proof that the term has type τ. There is no gap between the checker and the proof.

Evaluation. The type-checker is an evaluator — it reduces the term e through the pattern-match clauses of typecheck, each step applying one rule of the typing relation, until it reaches a leaf (natLit, boolLit, var) or fails. The proof h is not constructed separately; it is the value produced by evaluation of typecheck. This is Curry-Howard lived from the inside: type-checking IS proof construction, and proof construction IS evaluation.

This is in contrast with conventional type-checkers, which return a type or an error, and whose correctness requires a separate proof (in a meta-theory) that the checker matches the typing relation.

In our checker, the correctness proof is built into the return value. The type-checker and the proof of soundness are the same program.

-- Soundness: if typecheck returns some ⟨τ, h⟩, then h : Typed ctx e τ.
-- This is immediate from the return type — no proof needed separately.
-- Any result of the form `some ⟨τ, h⟩` already carries h : Typed ctx e τ.
theorem typecheck_sound (ctx : Context) (e : Term) (τ : Ty) (h : Typed ctx e τ) :
    ∃ τ', ∃ h' : Typed ctx e τ', typecheck ctx e = some ⟨τ', h'⟩ := by
  cases typecheck ctx e with
  | none => exact absurd h (by sorry)  -- completeness not proved here
  | some p => exact ⟨p.1, p.2, rfl⟩

14.7 What you have learned

You entered this course knowing that programs have types. You leave it knowing that:

1. Propositions are types. A logical claim is a Lean type. Its proofs are the terms inhabiting that type.

2. Proof-carrying types are programs. A function whose type includes a proposition requires that proposition to be proved before it can be called. The compiler enforces this.

3. Decidability is structured. Some propositions have decidable instances — algorithms that mechanically produce the proof or the refutation. Others do not. The Decidable type class captures this. Float lacks DecidableEq for a precise mathematical reason.

4. Specifications are types. CorrectSort, IsBST, LawfulDict, Typed — these are all types. Satisfying a specification means inhabiting the type.

5. The compiler is the verifier. When a file type-checks, every claim in every type has been verified by the elaborator.

This is the Curry-Howard correspondence, lived from the inside.

Exercises

1. Add a cond : Term → Term → Term → Term constructor to Term (conditional: if-then-else). Extend Typed with a rule: if the condition is Bool and both branches have type τ, the whole expression has type τ. Extend typecheck to handle it.

2. Add a pair : Term → Term → Term constructor and a Prod : Ty → Ty → Ty type. Extend Typed and typecheck accordingly.

3. State (as a Prop): "the type assigned by typecheck is unique — if typecheck ctx e = some ⟨τ₁, _⟩ and typecheck ctx e = some ⟨τ₂, _⟩ then τ₁ = τ₂." Why is this immediate from the determinism of the function?

4. The Curry-Howard table has two columns. Write five rows of your own, different from those in Section 14.1, connecting logical concepts you have used in this course to type-theoretic concepts.

5. State (as a Prop) what it would mean for typecheck to be complete as well as sound: "if Typed ctx e τ holds, then typecheck ctx e returns some ⟨τ, _⟩." This is a stronger statement than soundness. Do you think the implementation above is complete?

end Week14