Cover

Greetingss

There is good reason today to believe that every serious software engineer of the future will be expected to know how to use and produce software artifacts that, in a single language, intelligibly express everything from the abstract mathematics of the application domain to low-level hardware operational dynamics, inflected with machine-verified proofs blended seamlessly throughout, attesting to the consistency of every single detail of the entire construct.

The magnitude of this impending paradigm shift in programming is going to be of a very different nature and magnitude than in the past. Binary, assembly, imperative programming, functional, structured, object-oriented, parallel, functional, concurrent languages are all languages for expressing computations. What the paradigm shift does is to move abstract formal languages into the very heart of everyday programming. This is what our students now need to begin to learn about from the first class in computer science.

The Basic Claim

The main premise of this course is that future programmers will have to understand not only how to translate informal ideas but how to weave abstract mathematical specifications and proofs with code single theoretically clean programming and reasoning language.

This book is intended to satisfy this need. Dependently types languages, such as Lean 4, are the languages today in which it’s possible to program in this new manner. This book teaches integral specification, coding, and formal but fully automated verification in Lean. This book is derived generated from literate code (see Knuth) in Lean, enabling |students to read a well formatted book simultaneously with interacting with the actual Lean code and programming toosl.

Navigating the Book

At the top of the page, from the left, one finds a sequence of icons. The hamburger (three-line-stack) menu shows/hides the table of contents; the paintbrush icon is for changing the presentation color scheme; the magnifying icon is for text search over this book; the printer icon is for printing it (or saving it as a PDF for offline reading); and the last, GitHub, icon takes you to the GitHub repo where this book is stored.

Setting up Your Computer

Everything in this course runs inside a Docker development container, a preconfigured Linux environment defined by files in this repository, that Docker builds on your laptop. You do not install Lean, Mathlib, or the book tooling yourself. You install Docker and VS Code, open this project, and let the container supply the rest.

The best way to use this book is to open it in a browser within VSCode, right alongside the Lean 4 code that was processed to create it. To be able to do that, follow the directions here. In a nutshell, you will fork our repo, clone your fork of our repo, open your clone in VSCode; activate the Dev Containers VSCode plug-in; start up the “container”; then arrange your editor layout. Voila! Up and running. The benefit is that every student has an identical environment, with low effort.

Work through the steps in order. Step 4 takes the longest; start it before you need it.

1. Install the prerequisites

You need four things on your laptop. Install them in this order.

Then install one VS Code extension by hand — the Dev Containers extension (ms-vscode-remote.remote-containers). Open the Extensions view (Cmd+Shift+X / Ctrl+Shift+X), search for “Dev Containers”, and install it. Every other extension you need, including Lean 4, is installed automatically inside the container.

Give Docker enough room. This container requests 10 GB of memory, and a built Mathlib occupies roughly 7 GB on disk. Before continuing:

• Open Docker Desktop → Settings → Resources.
• Set memory to at least 10 GB (12 GB or more if your laptop has 16 GB).
• Confirm you have 15 GB of free disk space.

On Windows, Docker Desktop must use the WSL 2 backend; its installer will offer to set this up.

Start Docker Desktop and leave it running. The container cannot start if the Docker engine is not running — the single most common setup failure.

2. Fork this repository

A fork is your own copy of the repository on GitHub. You will do your work in your fork, so your changes are yours and cannot disturb the course repository.

1. Go to github.com/kevinsullivan/Lean4CS1.
2. Click Fork (top right).
3. Leave the name as Lean4CS1 and click Create fork.

You now have https://github.com/YOUR-USERNAME/Lean4CS1.

3. Clone your fork and open it in VS Code

Windows users: configure Git first

Do this before you clone. These settings affect how files are written to disk during the clone, so applying them afterward means re-cloning.

This repository is Linux-based: every file in it ends its lines with a single newline (LF), and the container runs Linux. Git for Windows, by default, converts line endings to Windows style (CRLF) on checkout. That conversion breaks things inside the container — shell scripts fail with errors like bash\r: command not found, and scripts/convert.py and the Makefile misbehave in ways whose cause is not obvious from the symptom.

Open Git Bash or PowerShell and run:

git config --global core.autocrlf false
git config --global core.eol lf
git config --global core.longpaths true

What each one does:

Confirm they took effect:

git config --global --list | findstr core

You should see core.autocrlf=false, core.eol=lf, and core.longpaths=true.

Set your editor to write LF too. VS Code shows the current line ending in the status bar, at the right, as LF or CRLF. To make LF the default, open Settings (Ctrl+,), search for Files: Eol, and choose \n.

Already cloned with the wrong settings? Apply the three settings above, then delete the folder and clone again. Re-checking-out in place will not reliably fix line endings that are already on disk.

A note on where you clone. Everything below works from an ordinary Windows folder such as C:\Users\you\Lean4CS1. If builds feel slow, the cause is usually that Docker reaches Windows files through a translation layer. Cloning into the WSL 2 filesystem instead — from a WSL terminal, into your Linux home directory — is substantially faster. Do that only if you are comfortable with WSL; it is a performance improvement, not a requirement.

Clone

Clone your fork, not the original. Substitute your GitHub username:

git clone https://github.com/YOUR-USERNAME/Lean4CS1.git
cd Lean4CS1
code .

If code is not a recognized command, open VS Code, press Cmd+Shift+P / Ctrl+Shift+P, run Shell Command: Install ‘code’ command in PATH, then try again — or simply use File → Open Folder and select the cloned directory.

While you are here, connect your fork back to the course repository so you can pull in updates later:

git remote add upstream https://github.com/kevinsullivan/Lean4CS1.git

4. Reopen the project in the container

With the project open in VS Code, a notification should appear in the lower-right corner:

Folder contains a Dev Container configuration file. Reopen folder to develop in a container.

Click Reopen in Container.

If the notification does not appear, press Cmd+Shift+P / Ctrl+Shift+P and run Dev Containers: Reopen in Container.

The first build takes a long time — plan on 15 to 45 minutes, depending on your laptop and network. Docker is downloading a base image and building the environment. Click show log in the notification if you want to watch. Do not close VS Code; interrupting it means starting over.

Later launches reuse the built image and take well under a minute.

You know it worked when the green indicator in the bottom-left corner of the VS Code window reads Dev Container: CS1. Open a terminal (Ctrl+`, or Terminal → New Terminal) — you are now a user named dev inside Linux, whatever your laptop actually runs.

5. Install the Lean toolchain and Mathlib

Two steps remain, both run in the VS Code terminal inside the container.

Open any Lean file first — for example FPCourse/T01_ExpressionsFunctionsRecursion/W00_AlgebraicTypes.lean. The Lean 4 extension activates, notices the lean-toolchain file, and installs the exact compiler version this course uses. A progress notice appears in the status bar. Wait for it to finish, then confirm:

lean --version

It should report the version named in lean-toolchain.

Then fetch prebuilt Mathlib. Mathlib is large; compiling it from source takes hours, and there is no reason to. Download the prebuilt libraries instead:

lake exe cache get

This retrieves several gigabytes — expect ten minutes or so on a good connection. Once it finishes, compile the course sources:

lake build

The first run works through the course files; later runs only rebuild what changed. If lake build completes without errors, your environment is correct and complete.

If lake exe cache get fails or you skip it, lake build will try to compile Mathlib from scratch. If a build seems to run forever with unfamiliar file names streaming past, stop it with Ctrl+C, run lake exe cache get, and try again.

6. Read the book beside the code

The intended way to study is the rendered book on one side of the screen and the live, type-checked Lean source on the other.

Three commands keep the book current

You never call mdBook directly. Three make targets, run from the project root in the container terminal, cover everything you need:

Both make build and make serve render the Markdown that is already in src/. The chapters are themselves generated from the .lean files, so after editing Lean source run plain make, which converts and then builds. Reach for make clean only when a build looks stale or inconsistent; nothing you wrote is lost, since it removes generated files only.

Start the server

In the container terminal:

make serve

This runs mdbook serve -n 0.0.0.0 for you. The -n 0.0.0.0 matters: left to its default, mdBook binds only the IPv6 loopback address, while VS Code’s port forwarding reaches the container over IPv4. The browser then reports ERR_CONNECTION_REFUSED even though the server is running and rebuilding normally. Wait for the line Serving on: http://0.0.0.0:3000 before going on.

Then find the address your own browser should use. Port 3000 is the port inside the container. VS Code forwards it to a port on your laptop, and that port is frequently not 3000 — it is often a high number such as 64461, and it can change from one session to the next. Do not guess it, and do not assume http://localhost:3000 will work.

Open the PORTS panel — the tab beside TERMINAL — and read the Local Address column on the row labeled mdBook. Whatever it says is the address that works. Right-click that row and choose Open in Browser, or copy the address.

Then put the book beside the source, not on top of it. The order of these steps matters; dragging tabs around is the unreliable way to do it.

1. Open the chapter you are working on, so that a .lean file is the active editor.
2. From the Command Palette, run Simple Browser: Show and paste the forwarded address. The browser opens as a tab in the same column, so it hides the source. That is expected; the next step fixes it.
3. With the Simple Browser tab still focused, run View: Move Editor into Next Group from the Command Palette. VS Code creates a second column on the right and moves the browser into it.
4. Click the .lean tab in the left column. Both are now visible at once, with no tab switching.

Dragging works too, but only if you drop the tab on the right edge of the editor area, where a vertical highlight appears down the side. Dropped anywhere else, the tab joins the column it came from and you are back to flipping between tabs.

The book page for a chapter follows the source path exactly. Editing

FPCourse/T01_ExpressionsFunctionsRecursion/W00_AlgebraicTypes.lean

corresponds to

.../FPCourse/T01_ExpressionsFunctionsRecursion/W00_AlgebraicTypes.html

in the book, so you can edit the address directly rather than clicking through the sidebar.

The Lean infoview competes for the same column. It also opens beside the source, so with the book already there you can end up with three narrow columns and no room to read. Toggle it off while reading and back on while working a proof: Lean 4: Toggle Infoview, or Ctrl+Shift+Enter (Cmd+Shift+Enter on macOS).

The server rebuilds and refreshes automatically as files change. Leave it running while you work. If you stop it, or close the terminal it is running in, the forwarded address stops serving and the page goes blank instead of reporting an error.

7. Track the course repository

Steps 1 through 6 leave you able to work. This step connects the course repository to your editor, so that new assignments, corrections, and answers to other students’ questions reach you where you are already working.

Nothing in this step needs installing. The container already supplies both extensions it uses — GitHub Pull Requests and Issues and GitLens — exactly as it supplies Lean 4 and the rest of the toolchain. They are there the moment the container finishes building.

If you open the Extensions view to look for them — the Extensions icon in the Activity Bar, or Ctrl+Shift+X (Cmd+Shift+X on a Mac) — find them under the Dev Container: CS1 heading rather than Local. An extension installed locally does not run in the container window, which is where you work, so installing either one by hand would leave you with a copy in the wrong place and no visible benefit.

Sign in to GitHub

Click the GitHub icon — the Octocat silhouette — in the Activity Bar, the narrow strip down the left edge. If a Login view greets you, click Sign in and authorize VS Code in the browser that opens. The container reuses the account and Git credentials of the VS Code running on your laptop, so you may instead be asked only to approve access with a single click, or not asked at all.

Signed in, the GitHub view holds three lists: Pull Requests, Issues, and Notifications.

The extension reads the repository’s origin and upstream remotes — that is the default of its githubPullRequests.remotes setting — which is why adding upstream back in step 3 matters here.

Watch the repository

Open the course repository — github.com/kevinsullivan/Lean4CS1 — and click Watch, at the top right beside Fork. Choose All Activity, or Custom and tick Issues. GitHub will then email you when something is opened, changed, or answered.

Watching is the feature that notifies you. Starring a repository bookmarks it on your account and pinning displays it on your profile page; neither sends you anything, and neither changes what VS Code shows you.

Optional: Show course issues in the editor

The Issues view ships with queries about your repository and your issues. The course issues are not in your fork: a fork begins with none of the original’s issues, and GitHub leaves the Issues tab switched off on forks by default. So add a query that names the course repository outright.

Open the Command Palette and run Preferences: Open User Settings (JSON), then add:

"githubIssues.queries": [
  {
    "label": "Course Issues",
    "query": "repo:kevinsullivan/Lean4CS1 is:open sort:updated-desc"
  },
  {
    "label": "Assigned to Me",
    "query": "repo:kevinsullivan/Lean4CS1 is:open assignee:${user}"
  }
]

Each entry becomes a collapsible group in the Issues view. The query text is ordinary GitHub search syntax; ${user} expands to whoever is signed in. Note that this setting replaces the built-in queries rather than adding to them, so list everything you want to see.

Hovering a query row in the Issues view reveals a pencil, Edit Query, which brings you back to this setting. There is no Configure Queries item in the view’s ... menu or in the Command Palette; the setting is the route.

User settings are reused inside the container, so this survives a container rebuild. If you would rather the query travel with your fork, put the same block in .vscode/settings.json in the project instead — workspace settings take precedence over user ones.

The Notifications view is a narrower thing than its name suggests: it reports on pull requests only, and is off until you set githubPullRequests.notifications to pullRequests. Email from watching the repository remains the dependable alert.

Optional: See new upstream commits

VS Code and GitLens show you the remote as of your last git fetch. Nothing streams in on its own, and git.autofetch is off by default; even set to true it fetches only the repository’s default remote, which is origin — your fork, where course commits never appear. To have upstream polled too, add to the same settings file:

"git.autofetch": "all",
"git.autofetchPeriod": 180

The period is in seconds, and 180 is the default.

New commits then show up without your asking. In the Source Control side bar, expand Remotes → upstream — that view comes from GitLens, and lives there rather than in the GitLens side bar, which holds the Commit Graph and Home. Either will show you what the instructor has pushed.

Fetching only updates what you can see. To bring the changes into your own files, merge them as described under “Working from day to day” below.

8. Verify your setup

Work down this list. If every line holds, you are ready.

• VS Code’s bottom-left indicator reads Dev Container: CS1.
• lean --version matches the version in lean-toolchain.
• lake build finishes without errors.
• Opening a .lean file shows the Lean infoview; placing the cursor on a #eval or #check line displays its result.
• make build finishes without errors and writes a book/ directory.
• make serve prints Serving on: http://0.0.0.0:3000, and the Local Address shown in the PORTS panel opens this book in a browser.
• git remote -v lists both origin (your fork) and upstream.
• The GitHub view’s Issues list shows the course repository’s open issues under Course Issues.

9. Working from day to day

Save your work. The container is disposable; your files live in the cloned folder on your laptop and are safe. Commit and push regularly so your work also exists on GitHub:

git add .
git commit -m "Week 3 exercises"
git push origin main

Collect course updates. When new material is published:

git fetch upstream
git merge upstream/main

If the update changes lean-toolchain or lake-manifest.json, run lake exe cache get again afterward.

10. When something goes wrong

Still stuck? Bring the exact command you ran and the exact message you saw — copy the text rather than describing it — and ask in office hours or by email.

Course Page and Schedule

• Instructor: Kevin Sullivan · sullivan@virginia.edu
• Department: Computer Science, University of Virginia
• Meetings: Mondays & Wednesdays, 11:00 AM – 12:15 PM · Rice 508 — 28 sessions
• Office hours: Tuesdays, 1:00 – 3:00 PM · Rice 508
• Course book (living): https://kevinsullivan.github.io/Lean4CS1 · source: https://github.com/kevinsullivan/Lean4CS1

This syllabus is subject to change. Any such changes will be pre-announced and documented here.

About This Course

Software development is being transformed by AI in at least two big ways. First, AI is automating the production of a great deal of imperative code. Second, combined with the breakout success of proof assistants for formalization of abstract mathematical statements and proofs, AI promises far greater practicality and utility of formal specification and proof construction in routine industrial software production.

As of Fall 2026 there is exploding interest in the use of Lean for both formal mathematics and formal software specification and verification. A snapshot of where that stood at the start of this semester is in the appendix, Lean 4 beyond research.

However big challenges remain. Even with formal and machine-checked specifications, the rate at which generative AIs can produce specifications and proofs, now mixed together with ordinary programming types and functions and effects, means that one’s constructions can easily escape one’s intellectual control, even when it’s all formalized and proven.

The problem with loss of intellectual control is that it’s antithetical to good faith acceptance of accountability for harmful failures that were, or could and should have been, foreseen and averted. The social equation is you-are-accountable implies you-are-less-likely-to-fail implies I-can-trust-you-more and act accordingly. That trust is what a user pays for: assurances that the product is fit for use in all agreed respects, and the freedom to ignore the complexity behind them because someone else has taken care of it. The same reasoning underpins a legal system in which real people are punished. (At least that’s the theory.) And trust of that kind is crucial to the success of a system and of the society around it.

This course will emphasize the development of formal specification architectures as a vital practice for both guiding generative AIs to produce useful results and to maintain the intellectual control necessary for human beings to be held accountable for the harmful failures their systems produce.

Durable intellectual control depends on abstract software specification and proofs rooted in the generalized mathematics of the application domain, stating that theory precisely, and certifying separate computable implementations against it. It is also required for the sustained quality of evolving, long-lived software systems.

What formal methods give the developer is justified confidence that they can actually uphold the assurances their users are paying for and then relying upon. That confidence rests on two distinct objects of trust: the validity of the statements of the formal theory itself and verification of the proof certificates that connect implementation to the abstract theories they are required to implement in some form. Lean 4 provides a practical language in which theories, implementations, and proofs can coexist, but it does not eliminate either obligation: one must understand the mathematics being formalized, and one must understand the trusted proof-checking base on which that confidence depends.

This is a course for graduate students in computer science. The course has two main threads: learning to think and express concepts formally in Lean 4, and learning deep and abiding principles of intellectual control over software through readings of seminal papers leading up to the present moment.

Mathematical Thread: Two Parts

The mathematical thread in this course is in two parts.

• Part I — Certified Computation (the FP book). A functional-programming foundation, taught through the Curry–Howard correspondence, in which specifications are types. Students learn to read and write specifications as types, to derive terms that inhabit them, and to check their claims with the compiler. Part I does not assess proof construction. The proofs it contains are provided for students to read.
• Part II — Proof Construction. Part II builds on the Part I foundations and asks students to produce proofs of their own. The objects of study carry over (data, specifications, recursion, higher-order functions, sets, relations, type classes), reoriented from Type to Prop. Part II follows the discipline general theory → separate computable realization → certified bridge, and works toward the endpoint the semester is designed around: institutions and the satisfaction condition.

Lean is used from Week 1 onward. Part II changes the kind of work students do in Lean; it does not introduce Lean.

Schedule (Fall 2026 · Mondays & Wednesdays)

Two tracks run in parallel and are scheduled independently. Paper readings (Line I) keep their weekly cadence: one theme per paper-week, with full bibliographic references and PDF links given in each paper cell. A set is due at the session where it is listed and, where a ↳ (cont.) cell appears, carries into that week’s second session. The exception is Week 2, which carries two sets: set 1 due Wed Sep 2 and set 2 due Mon Sep 7. The Part I book track is compressed to two chapters per class session (one each on Wed Sep 16 and Mon Sep 28), run in order, beginning Wed Sep 2; once the book is complete (Mon Sep 28) the class proceeds to Part II (Lean programming and proof construction). Class does not meet Mon Oct 5 (fall reading days) or Wed Nov 25 (Thanksgiving); Labor Day (Mon Sep 7) meets. 28 sessions total.

‡ Part II topics (sessions 11–28) are tentative. The per-topic pacing (≈3 sessions each) is provisional. Part II keeps the discipline general theory → separate computable realization → certified bridge.

Grading

Course grades will be based on two components, weighted equally.

Participation means demonstrated preparation for and participation in class, including attendance and active participation in discussions. You have two “just out” days for the semester: two class meetings you may miss for any reason, with no explanation needed and no cost to your grade. Beyond those, habitual absences or inattention will result in losses against full credit, assessed periodically by the instructor. If you have special circumstances, talk with the instructor to reach a common understanding.

The competencies above describe what the work is assessed against. Weekly exercise sets are machine-checked for immediate feedback and count as preparation for class.

Course Materials in This Book

The Part I book track above draws on the CS1 Full Course chapters listed here. Part II builds new theory on top of these chapters. It introduces no further book chapters.

Unit 1 — Expressions, Functions, Recursion

• Week 0: Algebraic Types — Computation and Logic
• Week 1: Expressions, Types, and Values
• Week 2: Functions and Specifications
• Week 3: Recursion and Termination

Unit 2 — Algebraic Datatypes, Lists, Trees, Decidability

• Week 4: Algebraic Datatypes
• Week 5: Lists
• Week 6: Trees and BST Invariants
• Week 7: Polymorphism and Decidability

Unit 3 — Higher-Order Functions, Specifications

• Week 8: Higher-Order Functions
• Week 9: Specifications in Practice

Unit 4 — Sets and Relations

• Week 10: Sets and Relations

Unit 5 — Abstract Types, Type Classes

• Week 11: Abstract Types
• Week 12: Type Classes and Decidability

Unit 6 — Curry-Howard

• Week 14: The Curry-Howard Correspondence

-- FPCourse/T01_ExpressionsFunctionsRecursion/W00_AlgebraicTypes.lean
import Mathlib.Logic.Basic
import Mathlib.Data.Bool.Basic

One language. Two readings.

When we write, we write about something. The something could be almost anything, real or imaginary: characters in a story or game, numbers in an arithmetic puzzle, the salinity of a parcel of ocean measured on a 10km x 10km x 1k grid. We can call these distinct domains of discourse, or just domains, for short.

The writing itself, on the other hand, is strictly made up of symbolic expressions. If the writing is a novel, a poem, a market report, these expressions are written in some natural language, the kind of language people learn to speak. What’s magical is that our mind interprets the symbols as meaning

A type defines and classifies a collection of values. For our purposes, any value has exactly one type, and types thus strictly partition values into such classes.

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. These types are sufficient to support a broad range of programming needs. Moreover, we will see that the logical analogs of these types provide a basis for expressing mathematical propositions in the language we can call higher-order predicate logic.

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 W00

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

Checkpoint — Nat subtraction floors at 0. Subtraction on Nat is truncated: it never produces a negative number. Predict the value of 3 - 10 — it is not -7 — before reading it.

#eval 3 - 10   -- predict first (truncated subtraction)

Checkpoint — Bool connectives. &&, ||, and ! are ordinary computations on Bool values. Predict the result of (false || true) && !false, then check.

#eval (false || true) && !false   -- predict first

Checkpoint — String length after concatenation. ++ joins two strings and .length counts characters. Predict the length of "hello" ++ ", world" — remember to count the comma and the space — before reading it.

#eval ("hello" ++ ", world").length   -- predict firstw

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.

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 encoded as 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 a decision procedure for the proposition, an operation that determines if the proposition is true or false and that returns the corresponding Boolean answer. 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.

Checkpoint — decide evaluates a decision procedure. For a decidable proposition, decide runs its decision procedure and returns a Bool. Predict decide (7 * 6 = 42) — does 7 * 6 reach the same normal form as 42? — then check.

#eval decide (7 * 6 = 42)   -- predict first

Checkpoint — a false proposition has no proof. 2 + 2 = 5 is uninhabited, so its decision procedure returns false (and the file would not compile if you tried to prove it). Predict decide (2 + 2 = 5) before reading it.

#eval decide (2 + 2 = 5)   -- predict first (an uninhabited proposition)

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. Many other constructs — recursion, type classes, proofs — ultimately reduce 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"

Checkpoint — β-reduction (double). double n ↝ n * 2: applying the function substitutes the argument for the parameter, then arithmetic fires. Predict double 21 from that rule, then check.

#eval double 21   -- predict first

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

Checkpoint — currying and partial application (add). add : Nat → Nat → Nat is Nat → (Nat → Nat), so add 40 is itself a function awaiting one more argument. Predict (add 40) 2, then check.

#eval (add 40) 2   -- predict first

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

Checkpoint — max' at the tie boundary. max' is if a ≥ b then a else b, and ≥ includes equality. Predict max' 7 7 — which branch fires when the arguments are equal? — then check.

#eval max' 7 7   -- predict first (the a = b boundary)

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

Checkpoint — projecting a nested product. In (1, "two", true) : Nat × String × Bool the middle field is reached with .2.1 (products are right-associative). Predict (1, "two", true).2.1, then check.

#eval (1, "two", true).2.1   -- predict first

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

Checkpoint — swap exchanges the components. swap (p : α × β) : β × α returns (p.2, p.1) — the component types swap along with the values. Predict swap (99, "z"), then check.

#eval swap (99, "z")   -- predict first

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

Checkpoint — conjunction is a product, and it is decidable. A proof of P ∧ Q is a pair of proofs; when P and Q are each decidable, so is P ∧ Q. Predict decide (2 < 3 ∧ 3 < 4), then check.

#eval decide (2 < 3 ∧ 3 < 4)   -- predict first

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"

Checkpoint — eliminating a sum (describeNatOrStr). match must handle both inl and inr; the tag chooses the branch. Predict describeNatOrStr (Sum.inr "oops"), then check.

#eval describeNatOrStr (Sum.inr "oops")   -- predict first

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

Checkpoint — Option guards a partial operation (safeDivide). safeDivide returns none exactly when the divisor is 0, and some otherwise — the two arms of a sum. Predict both values below (which one is none?), then check.

#eval safeDivide 20 4   -- predict first
#eval safeDivide 7 0    -- predict first

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

Checkpoint — disjunction is a sum, and it is decidable. A proof of P ∨ Q tags one side; decide finds a true side when one exists. Predict decide (3 < 4 ∨ 4 < 3) — which disjunct holds? — then check.

#eval decide (3 < 4 ∨ 4 < 3)   -- predict first

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.

Checkpoint — False has no proof. False (like Empty) is uninhabited, so its decision procedure returns false. Predict decide False, and say why no #eval could ever print a proof of it.

#eval decide False   -- predict first

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

Checkpoint — ¬P is P → False. decide builds the function ¬(1 = 2) automatically because the equality is decidably false. Predict decide (¬ (1 = 2)), then check.

#eval decide (¬ (1 = 2))   -- predict first

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

Checkpoint — no P and ¬P together. not_and_not says P ∧ ¬P is contradictory; on a concrete decidable P the whole negation is checkable. Predict decide (¬ ((3 < 4) ∧ ¬(3 < 4))), then check.

#eval decide (¬ ((3 < 4) ∧ ¬(3 < 4)))   -- predict first

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        (data is built with `def`; a proof of a Prop uses `theorem`)
def dataPair      : Nat × Bool := ⟨5, true⟩
theorem proofPair : 2 < 3 ∧ 3 < 4 := ⟨by decide, by decide⟩

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

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

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

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

Checkpoint — the six constructors, combined and decidable. This proposition wires together ∧, ∨, and ¬ over decidable atoms. Predict decide ((2 < 3 ∧ 3 < 4) ∨ ¬(1 = 1)) — is the left disjunct already enough? — then check.

#eval decide ((2 < 3 ∧ 3 < 4) ∨ ¬(1 = 1))   -- predict first

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

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E0.1] · decidability identification · tier 1 · core

For each claim, say whether decide can close it and why (finite domain? decidable predicate?) and which of the six constructors (§0.7) the proposition uses — then check it. The judgment is the point, not the tool-use:

(a) 2 < 3 ∧ 3 < 4 (b) 2 < 3 ∨ 3 < 2 (c) ¬ (2 = 3) (d) ¬ (2 < 3 ∧ 3 < 2)

#guard decide (2 < 3 ∧ 3 < 4) = true
#guard decide (2 < 3 ∨ 3 < 2) = true
#guard decide (¬ (2 = 3)) = true
#guard decide (¬ (2 < 3 ∧ 3 < 2)) = true

Every atom here is a decidable comparison over concrete Nats, so each connective stays decidable.

[E0.2] · type-directed derivation · tier 2 · core · target twice

Derive twice : (α → α) → α → α that applies its function twice (twice f x = f (f x)). Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. First-step hint: the type is two nested arrows, so →I twice introduces f : α → α and x : α; the only way to reach the goal α is to apply f, and applying it once leaves another α to feed back in. Effort: ~3 trace steps, 2 lines of code.

#guard twice (· * 2) 3 = 12
#guard twice (fun b => !b) false = false
#guard twice (· + 1) 0 = 2

When α is a Prop, read (P → P) → P → P aloud: what does twice say logically?

[E0.3] · specification writing (+ type reading) · tier 1 · core · target mapOption

Build mapOption : (α → β) → Option α → Option β with a match: apply f under some, pass none through. State its spec in one line — “some a ↦ some (f a), and none ↦ none” — then confirm on instances. Which two of the six constructors does the type of mapOption use? Effort: one match, ~3 lines.

#guard mapOption (· * 2) (some 5) = some 10
#guard mapOption (· * 2) (none : Option Nat) = none
#guard mapOption (fun b => !b) (some true) = some false

[E0.4] · counterexample finding · tier 1 · core

A student claims “Nat subtraction is invertible: (a - b) + b = a for all a b : Nat.” It is wrong — subtraction on Nat is truncated (§0.1). Find concrete inputs witnessing the failure and encode the witness so the check succeeds (it confirms the two sides differ):

#guard (3 - 10) + 10 ≠ 3

Then state, in one line, the side condition on a and b under which (a - b) + b = a does hold.

[E0.5] · specification reading · tier 3 (+ tier-1 check) · stretch

Read the provided proof of not_and_not (§0.6): fun h => h.right h.left. It shows that P ∧ ¬P is contradictory. In one or two sentences, name the type of h.left, the type of h.right, and explain why applying h.right to h.left produces False — do not author a new proof. As a decidable by-product on a concrete P, confirm:

#guard decide (¬ ((3 < 4) ∧ ¬(3 < 4))) = true

In one line: which tier does the general statement not_and_not live in, and which does the concrete check?

[E0.6] · type reading (free theorems) · tier 2 · stretch

Look only at the type Empty → α, polymorphic in α. Without running anything, state what every inhabitant does with its input and why it needs zero match cases; then say one thing no total function α → Empty can do when α is inhabited (§0.5–0.6). Finally, read the provided term fromImpossible : Empty → Nat × Bool × String := nomatch e (§0.7) in both registers — the computational one (an unreachable branch) and the logical one (ex falso quodlibet). No code to submit.

end W00

-- FPCourse/T01_ExpressionsFunctionsRecursion/W01_ExpressionsTypesValues.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Data.Bool.Basic
import Mathlib.Logic.Basic

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 W01

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)

Checkpoint — Nat.add reduces. Nat.add is defined by recursion, so an application reduces to a single normal form. Predict that normal form of Nat.add 5 4 — before reading the result — then check.

#eval Nat.add 5 4        -- predict first

Checkpoint — Bool operators. && and || are runnable two-valued operations (β-reduction, not logic). Predict the value of true && (false || true), then check.

#eval (true && (false || true))   -- predict first

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)

Checkpoint — a Bool test. == and < on Nat return a Bool you can run. Predict the value of (4 == 4 && 2 < 1 : Bool) — one conjunct is false — then check.

#eval (4 == 4 && 2 < 1 : Bool)   -- predict first

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

Checkpoint — rfl and normal forms. rfl proves a = b exactly when both sides reduce to one normal form. Predict the normal form of Nat.succ 7, then check that it is the 8 that makes the example above type-check.

#eval Nat.succ 7   -- predict first

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

Checkpoint — decide. decide certifies a decidable Prop by running its decision procedure. Predict whether ¬ (5 * 5 = 26) is true (what is 5 * 5?), then check.

#eval decide (¬ (5 * 5 = 26))   -- predict first

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

Checkpoint — decide on a finite list. A bounded ∀ x ∈ [...] over a literal list is decidable. Predict the Boolean below — note the bound is < 3, and 3 is in the list — then check.

#eval decide (∀ x ∈ ([1, 2, 3] : List Nat), x < 3)   -- predict first (note the 3)

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

Checkpoint — product projections. .1 and .2 extract the two components. Predict the swapped pair (myPair.2, myPair.1) — its type is Bool × Nat — then check.

#eval (myPair.2, myPair.1)   -- predict first

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

Checkpoint — nested products. Nat × Bool × String nests as Nat × (Bool × String), so triple.2 is a pair and triple.2.1 reaches into it. Predict triple.2.1, then check.

#eval triple.2.1   -- predict first

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.

-- `_h` is never used in the body: the proof is a *precondition* the caller must
-- supply, not data the computation consumes.  A leading underscore is how Lean
-- marks a binder as deliberately unused.
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

Checkpoint — proof-carrying safeDiv. The third argument _h : b ≠ 0 is a proof the caller must supply; by decide manufactures it for a concrete nonzero divisor. Predict safeDiv 20 4 (by decide), then check. (by decide is allowed here — it only builds the nonzero proof.)

#eval safeDiv 20 4 (by decide)   -- predict first


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

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E1.1] · type reading (free theorems) · tier 2 · core

Use #check on Nat.add, Nat.mul, and String.append. For each, write in plain English what the type says the function does, whether it is curried, and how many arguments it takes. Then read one type you were not given a body for: a function of type ∀ α, α → α → α, polymorphic in α. State one thing every inhabitant can do with its two inputs and one thing it cannot do (can it manufacture a fresh α? compare the two?). This previews the free theorems of Week 7 (§7.2). No code to submit.

[E1.2] · specification writing · tier 1 · core · target myStrNat

Define a product type pairing a String with a Nat, and a value myStrNat : String × Nat := ("lean", 4). Then state, as a Prop, the specification “the first component is \"lean\" and the second is positive,” and confirm it on your instance. The projections .1 and .2 are your spec vocabulary (§1.4).

-- def MyStrNatSpec : Prop := myStrNat.1 = "lean" ∧ myStrNat.2 > 0
#guard myStrNat.1 = "lean"
#guard myStrNat.2 = 4
#guard decide (myStrNat.1 = "lean" ∧ myStrNat.2 > 0) = true

[E1.3] · decidability identification · tier 1 · core

For each proposition, say whether decide can close it and why — is it atomic or built from connectives (∧, ¬), and does its type carry a decision procedure? — then check only the ones that are decidable:

(a) 17 * 23 = 391 (b) 100 < 200 ∧ 200 < 300 (c) ¬ (5 * 5 = 26) (d) (1.0 : Float) = 1.0

#guard decide (17 * 23 = 391) = true
#guard decide (100 < 200 ∧ 200 < 300) = true
#guard decide (¬ (5 * 5 = 26)) = true
-- (d) has no check on purpose: say why `decide` cannot close Float equality.
--     (Hint: what would DecidableEq Float have to certify about NaN?  §1.2, revisited Week 7.)

#eval decide Float.NaN

[E1.4] · counterexample finding · tier 1 · core · target subCancelCex

A student claims “for all naturals a b, a - b + b = a.” On Nat, subtraction is truncated (3 - 5 = 0), so the claim is wrong. Find concrete inputs witnessing the mismatch and encode the witness as the inequality that must hold, so the check succeeds:

#guard 3 - 5 + 5 ≠ 3

First-step hint: pick a < b so the subtraction underflows to 0. Then state, in one line, the side condition under which the original equation does hold. Effort: 1 line.

[E1.5] · type-directed derivation · tier 2 · stretch · target swapPair

Derive swapPair : Nat × Bool → Bool × Nat (swap the two components). Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. First-step hint: the input is a product, so eliminate it with .1 and .2 (×-elimination), then introduce the target pair in swapped order (×-introduction). Effort: ~3 trace steps, 1 line of code. (The trace format is introduced next week; this previews it.)

#guard swapPair (7, true) = (true, 7)
#guard swapPair (0, false) = (false, 0)

[E1.6] · specification reading · tier 3 (reading) · stretch

Read the proof-carrying type of safeDiv (§1.5): (a b : Nat) → (_h : b ≠ 0) → Nat. Do not author any proof. Explain (a) what the caller must supply beyond two numbers, and (b) why safeDiv 10 0 (by decide) fails to compile — trace the failure to the proof obligation 0 ≠ 0 that has no inhabitant. Then confirm the two working calls:

#guard safeDiv 10 2 (by decide) = 5
#guard safeDiv 17 3 (by decide) = 5

end W01

-- FPCourse/T01_ExpressionsFunctionsRecursion/W02_FunctionsSpecifications.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Logic.Basic

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 W02

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

Checkpoint — defining functions. double n = n * 2 and square n = n * n. Predict both values below from the definitions, then check.

#eval double 7    -- predict first
#eval square 6    -- predict first

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

Checkpoint — currying. add3 : Nat → Nat → Nat → Nat, so (add3 10 20) is itself a function still waiting for one Nat. Predict the value once the last argument arrives, then check.

#eval (add3 10 20) 30    -- predict first

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

Checkpoint — → as implication. An implication between decidable propositions is itself decidable. In (2 + 0 = 2) → (2 = 2 + 0) the hypothesis holds and so does the conclusion. Predict the Boolean — and say why the implication is true — then check.

#eval decide ((2 + 0 = 2) → (2 = 2 + 0))   -- predict first

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

Checkpoint — ∀ as a function type. A proof of ∀ n, n + 0 = n is a function sending each n to a proof. Over a finite list the claim is decidable. Predict the Boolean below, then check.

#eval decide (∀ n ∈ ([0, 1, 2, 3] : List Nat), n + 0 = n)   -- predict first

-- 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 _ => rfl

Checkpoint — double'' and its spec. double''_spec states double'' n = n + n. Predict the value below from the spec (not by re-deriving the body), then check.

#eval double'' 7   -- predict from double''_spec

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

Checkpoint — function composition. (square ∘ double) x = square (double x) — inner function first. Predict the value below (double 5, then square), then check.

#eval double_then_square 5   -- predict:  square (double 5)

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

Checkpoint — ∧ (conjunction). 1 < 2 ∧ 2 < 3 is true only when both conjuncts are. Predict the Boolean, then check.

#eval decide (1 < 2 ∧ 2 < 3)   -- predict first

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

Checkpoint — ∨ (disjunction). 1 = 1 ∨ 1 = 2 is true when at least one disjunct is — here the left. Predict the Boolean, then check.

#eval decide (1 = 1 ∨ 1 = 2)   -- predict first

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

Checkpoint — ¬ (negation). ¬ (1 = 2) unfolds to (1 = 2) → False; it holds exactly when 1 = 2 is false. Predict the Boolean, then check.

#eval decide (¬ (1 = 2))   -- predict first

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

Checkpoint — ↔ (biconditional). (1 + 1 = 2) ↔ (2 = 1 + 1) needs both directions to hold. Predict the Boolean, then check.

#eval decide ((1 + 1 = 2) ↔ (2 = 1 + 1))   -- predict first

2.6 Deriving terms from types

A term the compiler accepts is worth little if you found it by trial and error. #check and the red squiggle are an oracle — they answer accepted or rejected — but an oracle is not a method: it never tells you how to arrive at a term. Type-directed derivation is the method. The structure of the goal type dictates the structure of the term, built top-down, each step forced or chosen for a stated reason. You should be able to predict acceptance before you build.

Introduction and elimination

Each type constructor comes with a way to build a value (introduction) and a way to use one (elimination) — the natural-deduction discipline we name in Week 14.

Read the goal, pick the move its outermost constructor licenses, write that much of the term, and read off the smaller goal(s) that remain. Recall from §2.5 that ∧ behaves like × and ∨ like ⊕, so the same moves derive proofs of logical claims.

How Lean shows you the goal

A hole _ in a term is Lean printing the goal: it reports the expected type and the local context — the “remaining goal” of your derivation. Try it: def e : Empty := _ reports ⊢ Empty. In VS Code, type the hole and watch the InfoView shrink as you fill each step. Use the compiler as a confirmer of a step you predicted, not as a blind search engine.

The derivation trace

Record a derivation as a short trace. The trace — not the final term — is the artifact you are graded on; the final term is its by-product. RULE at each step is one of →I, →E, ×I, ×E, ⊕I, ⊕E, or “use h”. Worked derivation 1 — Nat → Nat.

DERIVATION of  addSelf : Nat → Nat
  goal: Nat → Nat
  step 1 [→I]    fun (a : Nat) => ?   ⟶ goal: Nat, with a : Nat
  step 2 [use a] a + a                ⟶ closed (a is the only Nat in scope)
  ∎

def addSelf : Nat → Nat := fun a => a + a

Checkpoint — addSelf (derived). The derivation closed with a + a. Predict addSelf 21 — the by-product of the trace — then check.

#eval addSelf 21   -- predict first

Worked derivation 2 — (P → Q) → (Q → R) → (P → R). Composition; under the logical reading, transitivity of implication — one derivation certifies both.

  step 1 [→I]  fun (f : P → Q) => ?   ⟶ goal: (Q → R) → (P → R)
  step 2 [→I]  fun (g : Q → R) => ?   ⟶ goal: P → R
  step 3 [→I]  fun (p : P) => ?       ⟶ goal: R, with f, g, p
  step 4 [→E]  f p : Q
  step 5 [→E]  g (f p) : R            ⟶ closed

def compose {P Q R : Type} : (P → Q) → (Q → R) → (P → R) :=
  fun f g p => g (f p)

Checkpoint — compose (derived). compose f g p = g (f p). With f = (· + 1) and g = (· * 2), predict compose f g 3, then check.

#eval compose (fun n => n + 1) (fun n => n * 2) 3   -- predict:  g (f 3)

Worked derivation 3 — A × B → B × A.

  step 1 [→I]  fun (p : A × B) => ?   ⟶ goal: B × A, with p : A × B
  step 2 [×E]  p.1 : A,  p.2 : B
  step 3 [×I]  (p.2, p.1) : B × A     ⟶ closed

def swapProd {A B : Type} : A × B → B × A :=
  fun p => (p.2, p.1)

Checkpoint — swapProd (derived). swapProd (a, b) = (b, a). Predict swapProd (1, 2), then check.

#eval swapProd (1, 2)   -- predict:  (2, 1)

Worked derivation 4 — A ⊕ B → B ⊕ A. The goal B ⊕ A would call for ⊕I, but which side is right depends on the input — so eliminate the hypothesis first.

  step 1 [→I]  fun (s : A ⊕ B) => ?
  step 2 [⊕E]  match s with .inl a => ? | .inr b => ?   ⟶ two goals B ⊕ A
  step 3 [⊕I]  .inr a   (case inl)    ⟶ closed
  step 4 [⊕I]  .inl b   (case inr)    ⟶ closed

def swapSum {A B : Type} : A ⊕ B → B ⊕ A :=
  fun s => match s with
    | .inl a => .inr a
    | .inr b => .inl b

Checkpoint — swapSum (derived). swapSum (.inl a) = .inr a — swapping an inl lands in inr. Predict the Boolean below, then check.

#eval decide (swapSum (Sum.inl 1 : Nat ⊕ Nat) = Sum.inr 1)   -- predict first

Grading the trace

A derivation exercise is graded on the trace, not merely on whether the term compiles. Full credit: (1) name the correct rule at each step; (2) state the remaining goal after each step; (3) close every goal by a hypothesis in scope. A term that compiles but whose trace mis-names a rule or skips a goal is not full credit — it may be correct by luck.

The inverse direction

Derivation builds a term from a type. Its inverse reads a type to learn what every inhabitant must do — free theorems, developed in Week 7 (§7.2). Where a type is fully polymorphic the derivation is forced and the free theorem is total: ∀ α, α → α has one inhabitant; ∀ α, α → α → α has exactly two. Building a term from a type and reading what every term of a type must do are one skill in two directions.

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

Checkpoint — a proof-carrying type. List.head demands a proof the list is nonempty; by decide discharges it for a concrete list. Predict which element is returned below, then check.

#eval ([10, 20, 30] : List Nat).head (by decide)   -- predict first

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E2.1] · specification writing · tier 1 · core · target pred'

Write pred' : Nat → Nat returning the predecessor, treating 0 as 0 (match on 0 vs. n + 1). State its specification as a ∀ proposition — “pred' undoes successor: ∀ n, pred' (n + 1) = n, with pred' 0 = 0” — then confirm on instances:

#guard pred' 0 = 0
#guard pred' 1 = 0
#guard pred' 5 = 4
#guard decide (∀ n ∈ ([0, 1, 2, 3, 10] : List Nat), pred' (n + 1) = n) = true

[E2.2] · counterexample finding · tier 1 · core

A student claims “double n = n + 2 for every n” (double from §2.1). It is wrong — the two lines cross at a single point and disagree everywhere else. Find inputs where they differ and encode each witness so the check succeeds (it confirms the two sides are unequal):

#guard double 5 ≠ 5 + 2
#guard double 0 ≠ 0 + 2

At which single n does double n = n + 2 accidentally hold? State the correct spec of double in one line.

[E2.3] · specification reading · tier 2 (+ tier-3 reading) · core

Use #check @And.intro to read its type. In one sentence each, say what a term of that type is computationally (the constructor that builds a pair of proofs) and logically (a proof of P ∧ Q from a proof of P and a proof of Q). Then read the provided proof add_zero_comm := fun h => h.symm (§2.2) and explain why .symm closes the goal — do not author a proof of your own. One confirmation that ∧-introduction lands in a true proposition:

#guard decide ((1 < 2) ∧ (2 < 3)) = true

[E2.4] · decidability identification · tier 1 · core

For each proposition, say whether decide can close it and why (finite domain? decidable predicate?) before checking — the judgment is the point, not the tool-use:

(a) (2 < 3) ↔ ¬(3 ≤ 2) (b) (True ∧ True) ↔ True (c) (True ∧ False) ↔ False (d) ¬ (True ∧ False) (e) ∀ n : Nat, n + 0 = n

#guard decide ((2 < 3) ↔ ¬(3 ≤ 2)) = true
#guard decide ((True ∧ True) ↔ True) = true
#guard decide ((True ∧ False) ↔ False) = true
#guard decide (¬ (True ∧ False)) = true
-- (e) has no check on purpose: say why decide cannot close an unbounded ∀ over Nat,
--     and what unfolding of ¬ makes (d) the type (True ∧ False) → False.

[E2.5] · specification writing · tier 1 · stretch · target max'

Write max' : Nat → Nat → Nat returning the larger of two numbers, then state its specification as a Prop: the result is ≥ both inputs and equals one of them. Confirm on instances, including the tie a = b:

#guard max' 3 7 = 7
#guard max' 9 4 = 9
#guard max' 5 5 = 5
#guard decide (∀ a ∈ ([0, 3, 7] : List Nat), ∀ b ∈ ([0, 3, 7] : List Nat),
  max' a b ≥ a ∧ max' a b ≥ b ∧ (max' a b = a ∨ max' a b = b)) = true

First step: the spec is a conjunction of three clauses — write the ∀ a b proposition first, then read each clause off the English. Effort: ~4 lines.

Deriving terms (§2.6). For E2.6–E2.9 the derivation trace is the graded artifact; the term is its by-product. RULE at each step is one of →I, →E, ×I, ×E, ⊕I, ⊕E, or “use h”. Recall from §2.5 that ∧ behaves like × and ∨ like ⊕.

[E2.6] · type-directed derivation · tier 2 · core · target andComm

Derive andComm : P ∧ Q → Q ∧ P (with P Q : Prop). Give the derivation trace in the §2.6 format, then the term; state which rule closes each goal. Effort: 2 trace steps after the opening →I. (No #guard here: the value is a proof, not data, so the trace alone is graded.)

First-step hint: the outermost goal is an arrow P ∧ Q → Q ∧ P, so the first move is forced (→I); then eliminate the hypothesis (×E) before building the swapped pair (×I).

[E2.7] · type-directed derivation · tier 2 · stretch · target curry

Derive curry : (A × B → C) → (A → B → C) (with A B C : Type). Give the derivation trace then the term. How many →I steps appear before the first elimination, and why? Effort: ~4 trace steps.

#guard curry (fun (p : Nat × Nat) => p.1 + p.2) 3 4 = 7
#guard curry (fun (p : Nat × Nat) => p.1 * p.2) 6 7 = 42

First-step hint: the goal is an arrow into an arrow into an arrow — introduce all three arguments (f, a, b) before you can build the A × B pair to feed f.

[E2.8] · type-directed derivation · tier 2 · core · target orElim

Derive orElim : (A → C) → (B → C) → (A ⊕ B → C) (with A B C : Type). Give the derivation trace then the term. Name the step that must come before you can use either function, and why. Effort: ~4 trace steps.

#guard orElim (fun n => n + 1) (fun n => n * 10) (Sum.inl 5 : Nat ⊕ Nat) = 6
#guard orElim (fun n => n + 1) (fun n => n * 10) (Sum.inr 5 : Nat ⊕ Nat) = 50

First-step hint: after →I on the two functions and the sum, the sum’s side is unknown — ⊕E (match) must come before you can apply f or g.

[E2.9] · type-directed derivation · type reading (free theorems) · tier 2 · stretch

Two directions on the same type (A → B → C) → B → A → C (with A B C : Type), no term to submit:

(a) Method: which introduction- or elimination-step must come first, and which hypothesis closes the final goal?

(b) Free theorem (previewing Week 7 §7.2): reading only the type, how many inhabitants does it have when A B C are fully polymorphic, and why can the code not invent a C? This is the inverse of (a): where the derivation is forced, the reading is total.

end W02

-- FPCourse/T01_ExpressionsFunctionsRecursion/W03_RecursionTermination.lean
import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Ring

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 W03

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.

Checkpoint — factorial. Iterate the step once more from factorial 3 = 6: factorial 4 = 4 * factorial 3. Predict the value below before reading it.

#eval factorial 4   -- predict first  (4 * 6)

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

Checkpoint — factorialTR accumulates on the way down. The accumulator carries the running product, so the recursive call is the last thing done. Predict factorialTR 4 (trace the accumulator from 1), then check.

#eval factorialTR 4   -- predict first

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

Checkpoint — the two definitions agree. factorialTR_spec says factorialTR n = factorial n for every n. Predict the Boolean below from the spec (not by computing both sides), then check.

#eval decide (factorialTR 6 = factorial 6)   -- predict from factorialTR_spec

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

Checkpoint — gcd (non-structural termination). gcd recurses on a decreasing measure (the second argument), not on a strict subterm. Predict gcd 24 36, then check. Because gcd is well-founded, only #eval reduces it — rfl/decide cannot, as the note below explains.

#eval gcd 24 36   -- predict first

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

Checkpoint — factorial is positive. factorial_pos says 0 < factorial n for every n. Predict the Boolean below from that spec (not by computing factorial 6), then check.

#eval decide (0 < factorial 6)   -- predict from factorial_pos

-- "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)

Checkpoint — factorial is monotone. factorial_mono says factorial n ≤ factorial (n + 1) for every n. Predict the Boolean below from that spec, then check.

#eval decide (factorial 4 ≤ factorial 5)   -- predict from factorial_mono

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

Checkpoint — recursion is the recursor. Applying Nat.rec to a base value and a step function rebuilds factorial. Predict the value below (it is factorial 4), then check.

#eval (@Nat.rec (fun _ => Nat) fac0 facStep) 4   -- predict first

@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)

Checkpoint — length from List.rec. The same universal shape computes list length: base 0, step +1 per element. Predict the length below, then check.

#eval (@List.rec String (fun _ => Nat) listLenBase stepListLen) ["a", "b"]   -- predict first

@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

Checkpoint — folding a tree with BinTreeNat.rec. The recursor sums a tree: base 0 at empty, step n + al + ar at each node. Predict the sum for myTree (its node labels are 1, 2, 5), then check. (A custom recursor has no compiled code path, so this checkpoint uses #reduce — the kernel reducer — not #eval.)

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

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E3.1] · type-directed derivation · tier 2 · core · target sumTo

Derive sumTo : Nat → Nat computing 0 + 1 + ... + n. Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. First-step hint: the input is a Nat, so eliminate on its constructor (0 vs n + 1) first, exactly as factorial does (§3.1); the step clause may use the answer sumTo n already in hand. Effort: ~4 trace steps, 3 lines of code.

#guard sumTo 0 = 0
#guard sumTo 1 = 1
#guard sumTo 3 = 6
#guard sumTo 10 = 55

[E3.2] · specification writing · tier 1 (+ tier-3 reading) · core · target SumToClosedForm

State, as a Prop, the closed-form specification “∀ n, sumTo n = n * (n + 1) / 2.” Do not prove the general statement (that is a proof by induction, off-limits here). Instead confirm the spec on instances and on one bounded, decidable slice:

-- def SumToClosedForm : Prop := ∀ n : Nat, sumTo n = n * (n + 1) / 2
#guard sumTo 5 = 5 * (5 + 1) / 2
#guard sumTo 10 = 10 * (10 + 1) / 2
#guard decide (∀ n ∈ List.range 20, sumTo n = n * (n + 1) / 2) = true

In one line: which tier does the general ∀ n : Nat statement live in, and which the three checks?

[E3.3] · counterexample finding · tier 1 · core

A student proposes the closed form “sumTo n = n * n / 2.” It is wrong. Find concrete inputs witnessing the mismatch and encode each witness as an inequality, so the check succeeds (it confirms the two sides differ):

#guard sumTo 3 ≠ 3 * 3 / 2
#guard sumTo 5 ≠ 5 * 5 / 2

First-step hint: evaluate sumTo 3 and 3 * 3 / 2 by hand and compare. Then state, in one line, the single edit to the student’s formula that makes it correct (compare with the spec in E3.2).

[E3.4] · decidability identification · tier 1 · core

For each claim, say whether decide (equivalently an rfl-test) can close it, and why — is the function structural (kernel-reducible, like factorial) or well-founded (only #eval/#guard reduce it, like gcd — §3.4), and is the quantifier bounded or unbounded? The judgment is the point; then check only the ones that are decidable:

(a) factorial 5 = 120 (b) gcd 48 18 = 6 (c) ∀ n ∈ ([0, 1, 2, 3] : List Nat), sumTo n = n * (n + 1) / 2 (d) ∀ n : Nat, sumTo n = n * (n + 1) / 2

#guard decide (factorial 5 = 120) = true
#guard decide (∀ n ∈ ([0, 1, 2, 3] : List Nat), sumTo n = n * (n + 1) / 2) = true
-- (b) and (d) have no check on purpose: say why decide/rfl cannot close each
--     (hint for (b): §3.4 — gcd is well-founded, so the kernel cannot reduce it;
--      for (d): the domain of n is infinite).

[E3.5] · specification writing · tier 1 · stretch · target GcdDividesSpec

State the specification for gcd as two ∀ propositions expressing “gcd a b divides a” and “gcd a b divides b.” Do not prove the general statements; confirm the divisibility on instances (using the remainder-is-zero form a % gcd a b = 0), and — reusing gcd_eq_nat_gcd and Mathlib’s Nat.Coprime — check that 8 and 15 are coprime:

#guard 48 % gcd 48 18 = 0
#guard 18 % gcd 48 18 = 0
#guard 100 % gcd 100 75 = 0
#guard Nat.gcd 8 15 = 1        -- Nat.Coprime 8 15 unfolds to this

First-step hint: divides d n := ∃ k, n = d * k (§3.4); the raw ∃ k is not decidable, so the checks use the equivalent remainder-is-zero form, which is. Note that gcd is well-founded — #guard/#eval reduce it (compiled path), but rfl/decide cannot.

[E3.6] · specification reading · tier 3 (read-only) · stretch

Read the provided proof of factorialAcc_spec (§3.3): ∀ n acc, factorialAcc n acc = acc * factorial n. In two or three sentences explain why the specification is generalized over acc — what breaks in the succ step if you try to prove only the special case factorialAcc n 1 = factorial n, without the ∀ acc? Then identify which line of the provided proof applies the inductive hypothesis at a different accumulator. No code to submit.

[E3.7] · specification writing + type-directed derivation · tier 1 · stretch · target sumToAcc

Define a tail-recursive companion to sumTo (E3.1): sumToAcc : Nat → Nat → Nat, carrying the running total in its second argument. State, as a Prop, the relationship between the two — the accumulator-generalized ∀ n acc, sumToAcc n acc = acc + sumTo n — and confirm it on instances. Do not prove the general statement; instead say, in one or two sentences and reusing the reasoning of E3.6, why it must be stated for every acc rather than only for acc = 0.

#guard sumToAcc 0 0 = 0
#guard sumToAcc 4 0 = 10          -- 0 + 1 + 2 + 3 + 4
#guard sumToAcc 4 5 = 15          -- the incoming accumulator is added in
#guard sumToAcc 10 0 = 55

First-step hint: recurse on the first argument; the accumulator grows on the way down, so the recursive call is the last thing done. Effort: ~4 lines of code.

end W03

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

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/T02_InductiveTypes/W04_AlgebraicDatatypes.lean
import Mathlib.Data.Option.Basic
import Mathlib.Logic.Basic

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 W04

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

Checkpoint — Direction has DecidableEq. deriving DecidableEq makes every pair of constructors comparable, so decide can settle any (in)equality between them. Predict the Boolean below — are North and South distinct? — then check.

#eval decide (Direction.North ≠ Direction.South)   -- predict first

4.2 Record types (pure products)

structure Point where
  x : Float
  y : Float
deriving Repr

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

Checkpoint — record projection. A record bundles named fields; projection reads one back. Predict the value of origin.x from the definition of origin, then check.

#eval origin.x   -- predict first

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)

Checkpoint — Option.map preserves isSome. By option_map_isSome, mapping can neither create nor destroy the value’s presence. Predict both Booleans, then check.

#eval (Option.map (· + 1) (some 3)).isSome              -- predict from option_map_isSome
#eval (Option.map (· + 1) (none : Option Nat)).isSome   -- predict

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

Checkpoint — Option.map of none. none_map_always_none says mapping any f over none yields none. Predict the value below (not just its isSome), then check.

#eval (Option.map (· + 1) (none : Option Nat))   -- predict from none_map_always_none

-- ∃ 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⟩

Checkpoint — witnessing ∃. The proof above offers 7 as the witness. Predict the Boolean below — is factorial' 7 really over 1000? — then check the witness works.

#eval decide (factorial' 7 > 1000)   -- predict first

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

Checkpoint — Expr.eval on neg. eval recurses into subexpressions; the neg clause negates its operand’s value. Predict the integer below, then check.

#eval Expr.eval (.neg (.add (.num 2) (.num 3)))   -- predict first

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

Checkpoint — eval_add. eval_add states (add e₁ e₂).eval = e₁.eval + e₂.eval, and it holds by rfl. Predict the Boolean below from that spec (not by computing), then check.

#eval decide (Expr.eval (.add (.num 3) (.num 4)) = Expr.eval (.num 3) + Expr.eval (.num 4))   -- predict from eval_add

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

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E4.1] · type-directed derivation · tier 2 · core · target numSides

Define inductive Shape with Circle (radius : Float), Rectangle (width height : Float), and Triangle (base height : Float). Then derive numSides : Shape → Nat, the count of straight sides (Circle 0, Triangle 3, Rectangle 4). The graded artifact is a derivation trace (Week 2 §2.6): show how the template principle (§4.6) forces one clause per constructor and fixes the data each clause may use. First-step hint: eliminate the Shape argument with a match — its three constructors give three clauses. Effort: ~3 trace steps, 5 lines of code.

#guard numSides (Shape.Circle 5.0) = 0
#guard numSides (Shape.Rectangle 2.0 3.0) = 4
#guard numSides (Shape.Triangle 1.0 1.0) = 3

[E4.2] · specification writing · tier 1 (+ decidability identification) · core · target area, AreaCircleSpec

Define area : Shape → Float (Circle r ↦ Float.pi * r * r, Rectangle w h ↦ w * h, Triangle b h ↦ 0.5 * b * h). State the circle specification as a Prop:

-- def AreaCircleSpec : Prop := ∀ r : Float, area (Shape.Circle r) = Float.pi * r * r

Then answer in one line: why does this exercise ship no #guard acceptance check for area? Name the type class #guard/decide needs and the type (see §4.2 and the Float discussion) that lacks it. The judgment — not a passing check — is the deliverable here.

[E4.3] · counterexample finding · tier 1 · core · target mulNotSum

A student claims “Expr.eval (.mul a b) = Expr.eval a + Expr.eval b” — confusing mul with add. It is wrong. Find a concrete mul expression witnessing the mismatch and encode it as the inequality that must hold, so the check succeeds:

#guard Expr.eval (.mul (.num 3) (.num 4)) ≠ Expr.eval (.num 3) + Expr.eval (.num 4)

Then state the correct one-line spec for mul (the eval_mul analogue of eval_add, §4.5).

[E4.4] · specification writing · tier 1 · core · target MyExpr, MyExpr.eval

The Expr of §4.5 has no subtraction. Define your own inductive MyExpr with at least num : Int → MyExpr, add : MyExpr → MyExpr → MyExpr, and sub : MyExpr → MyExpr → MyExpr; give MyExpr.eval : MyExpr → Int extending §4.5 with a sub clause. State the subtraction spec as a ∀ proposition — ∀ a b, (MyExpr.sub a b).eval = a.eval - b.eval — then confirm it on instances (mind the negative-result boundary):

#guard MyExpr.eval (.sub (.num 10) (.num 3)) = 7
#guard MyExpr.eval (.sub (.num 3) (.num 10)) = -7
#guard MyExpr.eval (.add (.num 5) (.sub (.num 2) (.num 8))) = -1

First-step hint: copy the four Expr.eval clauses of §4.5 and add .sub a b ↦ a.eval - b.eval. Effort: ~6 lines of code.

[E4.5] · specification writing (∃ witness) · tier 1 · stretch · target answer

Rewrite the old “prove there exists an Expr that evaluates to 42” without producing a proof. Define a witness answer : Expr and let the compiler confirm it (tier 1); the existential ∃ e : Expr, Expr.eval e = 42 is then witnessed by ⟨answer, by decide⟩ — which you read, not author.

#guard Expr.eval answer = 42

First-step hint: any tree of num/add/mul/neg whose value is 42 works — e.g. combine add and mul of nums.

[E4.6] · type reading (free theorems) · tier 2 · stretch

Look only at the type Option.map : (α → β) → Option α → Option β, polymorphic in α and β. Without running anything, state two things every inhabitant must satisfy (does it ever turn none into a some? can it manufacture a β when handed none?) and one thing it cannot do. Relate your answer to option_map_isSome (§4.3): the spec you read there is one of these free theorems. No code to submit.

end W04

-- FPCourse/T02_InductiveTypes/W05_Lists.lean
import Mathlib.Data.List.Basic
import Mathlib.Data.List.Lemmas

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 W05

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

Checkpoint — specifications of ++. Using length_append and mem_append_iff (not evaluation), predict both values below, then check.

#eval (([1, 2, 3] ++ [4, 5] : List Nat)).length          -- predict from length_append
#eval decide (3 ∈ (([1, 2, 3] ++ [4, 5]) : List Nat))    -- predict from mem_append_iff

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

Checkpoint — decide on finite lists. Before evaluating, predict the Boolean, and say why decide can settle it (finite list, decidable predicate). Then check.

#eval decide (∀ x ∈ ([2, 4, 7] : List Nat), x % 2 = 0)   -- predict first (note the 7)

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.

Checkpoint — reverse. Using reverse_reverse (not evaluation), predict the second value; predict the first from what reverse does. Then check.

#eval ([1, 2, 3].reverse : List Nat)           -- predict
#eval ([1, 2, 3].reverse.reverse : List Nat)   -- predict from reverse_reverse

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]

Checkpoint — map preserves length. Use map_length (not evaluation) to predict the value below, then check it.

#eval ([1, 2, 3, 4].map (· + 100)).length   -- predict from the spec, then read

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

Checkpoint — filter. Using mem_filter_iff and filter_length_le, predict the filtered list and its length (note it is ≤ 6), then check.

#eval ([1, 2, 3, 4, 5, 6].filter (· % 2 == 0) : List Nat)       -- predict
#eval (([1, 2, 3, 4, 5, 6].filter (· % 2 == 0)).length : Nat)   -- predict; ≤ 6

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E5.1] · specification writing · tier 1 (+ tier-3 reading) · core · target MemAppendSpec

State, as a Prop, the specification “if n ∈ xs then n ∈ xs ++ ys.” Do not prove the general statement — that proof is List.mem_append, given in §5.1 for you to read (tier 3). Instead confirm the spec on instances where the hypothesis holds:

-- def MemAppendSpec : Prop := ∀ (n : Nat) (xs ys : List Nat), n ∈ xs → n ∈ xs ++ ys
-- 3 ∈ [1,2,3] holds, so the spec predicts:
#guard 3 ∈ (([1, 2, 3] ++ [4, 5]) : List Nat)
#guard 9 ∈ (([9] ++ ([] : List Nat)))

In one line: which tier does the general statement live in, and which the two checks?

[E5.2] · decidability identification · tier 1 · core

For each proposition, say whether decide can close it and why (finite domain? decidable predicate?) before checking — the judgment is the point, not the tool-use:

(a) ∀ x ∈ ([2,4,6,8,10] : List Nat), x % 2 = 0 (b) ∃ x ∈ ([3,7,12,5] : List Nat), x > 10 (c) ∀ xs : List Nat, xs.reverse.reverse = xs

#guard ∀ x ∈ ([2, 4, 6, 8, 10] : List Nat), x % 2 = 0
#guard ∃ x ∈ ([3, 7, 12, 5] : List Nat), x > 10
-- (c) has no check on purpose: say why `decide` cannot close it, and name the
--     term that settles it instead (hint: it is in §5.3).

[E5.3] · counterexample finding · tier 1 · core · target zipLenCounterexample

A student proposes this length spec for pairing two lists: “(zip xs ys).length = xs.length + ys.length.” It is wrong. Find concrete inputs witnessing the mismatch and encode the witness so the check succeeds (it confirms the two sides differ). List.zip is in Mathlib.

#guard (List.zip [1, 2, 3] [10]).length ≠ ([1, 2, 3].length + [10].length)

Then state the correct length spec in one line (you will build it in E5.5).

[E5.4] · type-directed derivation · tier 2 · core · target headOr

Derive headOr : α → List α → α (return the head, or the default on []). Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. First-step hint: the second argument is a List α; its constructor ([] vs h :: t) is what you eliminate first (⊕E-style match). Effort: ~4 trace steps, 3 lines of code.

#guard headOr 0 ([] : List Nat) = 0
#guard headOr 0 [7, 8, 9] = 7

[E5.5] · inhabitation + specification writing · tier 1 · stretch · target myZip

Write myZip : List α → List β → List (α × β) pairing corresponding elements and stopping at the shorter list. State its length spec as a Prop ((myZip xs ys).length = min xs.length ys.length) and confirm on instances. Effort: one match on both lists at once; ~5 lines.

#guard myZip [1, 2, 3] ['a', 'b'] = [(1, 'a'), (2, 'b')]
#guard (myZip ([1, 2, 3, 4] : List Nat) ([10, 20] : List Nat)).length = 2   -- min 4 2
#guard (myZip ([] : List Nat) ([1] : List Nat)).length = 0

[E5.6] · type reading (free theorems) · tier 2 · stretch

Look only at the type of List.map, namely (α → β) → List α → List β, polymorphic in α and β. Without running anything, state two things every inhabitant of this type must do, and one thing it cannot do (can it invent a β from nowhere? change the length? inspect an α it was not handed a function for?). This is the inverse of E5.4 and previews the free theorems of Week 7 (§7.2). No code to submit.

[E5.7] · specification writing · tier 1 (+ tier-3 reading) · stretch

State, as a Prop, the specification “mapping after reversing is reversing after mapping.” The general statement is Mathlib’s List.map_reverse, whose type is List.map f l.reverse = (List.map f l).reverse — read it (tier 3) rather than proving it. Confirm the spec on instances, covering the empty and singleton boundaries:

#guard ([1, 2, 3] : List Nat).reverse.map (· * 10) = (([1, 2, 3] : List Nat).map (· * 10)).reverse
#guard ([] : List Nat).reverse.map (· + 1) = (([] : List Nat).map (· + 1)).reverse
#guard ([7] : List Nat).reverse.map (· + 1) = (([7] : List Nat).map (· + 1)).reverse

In one line: which orientation does List.map_reverse state, and why does the orientation matter if you want to use it as a left-to-right rewrite?

end W05

-- FPCourse/T02_InductiveTypes/W06_Trees.lean
import Mathlib.Data.List.Sort
import Mathlib.Order.Basic

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 W06

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

Checkpoint — toList (in-order traversal). toList flattens a tree left-value-right. Predict the list below, then check.

#eval (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)).toList   -- predict

Checkpoint — height. height returns the longest root-to-leaf path. Predict the value below from the tree’s shape, then check.

#eval (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)).height   -- predict

Checkpoint — member. member tests presence anywhere in the tree. Predict both Booleans, then check.

#eval (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)).member 7   -- predict
#eval (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)).member 4   -- predict

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)

Checkpoint — ForAll is decidable. decForAll makes BTree.ForAll decidable, so decide can settle it. Predict the Boolean below, and say why it is decidable, before reading the result.

#eval decide (BTree.ForAll (· < 5) (BTree.node BTree.leaf 3 BTree.leaf))   -- predict first

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

Checkpoint — bstInsert keeps order. Inserting maintains the BST ordering. Predict the in-order toList after inserting 4, then check that it stayed sorted.

#eval (bstInsert 4 (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 BTree.leaf)).toList   -- predict

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⟩

Checkpoint — insertion preserves a bound. forAll_bstInsert says inserting an element that satisfies p keeps every element satisfying p. Predict the Boolean (is every element still < 10 after inserting 4?), then check.

#eval decide (BTree.ForAll (· < 10) (bstInsert 4 (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 BTree.leaf)))   -- predict

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

Checkpoint — mutual recursion (roseSize). roseSize counts nodes by calling forestSize on its children. Predict the count for the tree below (a root with two children), then check.

#eval roseSize (RoseTree.node 1 (Forest.cons (RoseTree.node 2 Forest.nil) (Forest.cons (RoseTree.node 3 Forest.nil) Forest.nil)))   -- predict

Exercises

Banners read [id] · competency · tier · level · target; build exercises ship a #guard acceptance check to paste beneath your definition (see EXERCISE_CONVENTIONS.md). Do every core exercise; stretch is optional.

[E6.1] · inhabitation + specification writing · tier 1 · core · target BTree.map

Define BTree.map (f : α → β) : BTree α → BTree β (apply f at every node, keep the shape) and state its specification “map preserves size” as a Prop. Confirm that map preserves size and commutes with toList:

-- def BTree.map (f : α → β) : BTree α → BTree β
--   | .leaf => .leaf
--   | .node l v r => .node (l.map f) (f v) (r.map f)
#guard ((BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 BTree.leaf).map (· * 10)).size = 2
#guard ((BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 BTree.leaf).map (· * 10)).toList = [30, 50]

[E6.2] · decidability identification · tier 1 · core

§6.3 gives a Decidable instance for BTree.ForAll (decForAll) but none for IsBST. So: can decide close IsBST t directly? If not, name the instance that is missing, and confirm the ingredient propositions decide can settle (these compile; decide (IsBST …) would not):

#guard decide (BTree.ForAll (· < 5) (BTree.node BTree.leaf 3 BTree.leaf)) = true
#guard decide (BTree.ForAll (5 < ·) (BTree.node BTree.leaf 7 BTree.leaf)) = true

One line: what would you have to provide to make decide (IsBST t) typecheck?

[E6.3] · counterexample finding · tier 1 · core

A student claims “(bstInsert x t).size = t.size + 1 for all x, t.” It is wrong. Find x, t witnessing the mismatch (hint: what if x is already in t?) and encode the witness so the check succeeds:

#guard (bstInsert 5 (BTree.node BTree.leaf 5 BTree.leaf)).size
         ≠ (BTree.node BTree.leaf 5 BTree.leaf).size + 1

State the correct relationship between (bstInsert x t).size and t.size in words.

[E6.4] · type-directed derivation · tier 2 · core · target BTree.mirror

Derive BTree.mirror : BTree α → BTree α that swaps every node’s left and right subtrees. Give a derivation trace (Week 2 §2.6 format; the trace is graded), then the def. First-step hint: match the input’s constructor (.leaf vs .node l v r) — ⊕E — then rebuild, recursing on both subtrees. Effort: ~3 trace steps, 3 lines.

#guard (BTree.node (BTree.node BTree.leaf 1 BTree.leaf) 2 BTree.leaf).mirror.toList = [2, 1]
#guard (BTree.node (BTree.node BTree.leaf 1 BTree.leaf) 2 BTree.leaf).mirror.mirror.toList
         = (BTree.node (BTree.node BTree.leaf 1 BTree.leaf) 2 BTree.leaf).toList

[E6.5] · inhabitation (exploiting an invariant) · tier 2 · stretch · target bstSearch

Define bstSearch (x : Nat) : BTree Nat → Bool that uses the BST ordering to visit one subtree per node (O(height), not O(size)): compare x with v and recurse left or right accordingly. (The IsBST proof is not needed for the computation — the ordering is what you exploit.) Effort: one match + if/else if; ~5 lines.

#guard bstSearch 7 (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)) = true
#guard bstSearch 6 (BTree.node (BTree.node BTree.leaf 3 BTree.leaf) 5 (BTree.node BTree.leaf 7 BTree.leaf)) = false

[E6.6] · inhabitation + specification writing (mutual recursion) · tier 1 · stretch · target roseToList

Define roseToList : RoseTree α → List α and its mutual helper forestToList : Forest α → List α, collecting every value. State the spec (roseToList t).length = roseSize t, analogous to toList_length_eq_size, and confirm on an instance. Effort: a mutual block, ~6 lines.

#guard (roseToList (RoseTree.node 1
          (Forest.cons (RoseTree.node 2 Forest.nil)
            (Forest.cons (RoseTree.node 3 Forest.nil) Forest.nil)))).length = 3

end W06

-- FPCourse/T02_InductiveTypes/W07_PolymorphismDecidability.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

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 W07

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) → (α → β → γ) → β → α → γ

Checkpoint — myConst. myConst : α → β → α returns its first argument. Predict the value below — does the second argument affect it? — then check.

#eval myConst 7 "ignored"   -- predict first

Checkpoint — myFlip. myFlip swaps a function’s two arguments. Predict the value of the flipped subtraction below, then check.

#eval myFlip (fun a b => a - b) 3 10   -- predict:  (fun a b => a - b) 10 3

7.2 Free theorems: what a polymorphic type guarantees

The intro claimed a polymorphic f : List α → List α “can only permute, drop, or duplicate.” That is not a remark about some implementation — it is forced by the type, for every inhabitant. When a function is polymorphic in α, its code is handed a type it cannot name: it cannot test a value of α, compare two, or manufacture one. The only αs it can return are those it was given. This is parametricity (Reynolds 1983); the theorems it hands you for free are Wadler’s “theorems for free” (2015). Read every signature below by asking:

What does this type forbid every inhabitant from doing? ∀ α, α → α has essentially one inhabitant. One value of an unknown type in, one out; the only α available is the input, so it must be returned. Free theorem: for every g, g (f x) = f (g x).

def myId : ∀ α : Type, α → α := fun _ x => x
#eval myId String (toString 3)   -- "3"  = g (f 3)
#eval toString (myId Nat 3)      -- "3"  = f (g 3)

∀ α, α → α → α has exactly two inhabitants — the two projections; nothing else can be built.

def fst' : ∀ α : Type, α → α → α := fun _ x _ => x
def snd' : ∀ α : Type, α → α → α := fun _ _ y => y

∀ α, List α → Nat can only measure shape. It cannot inspect elements, so the result depends only on the length. Free theorem: f (xs.map g) = f xs.

def len' : ∀ α : Type, List α → Nat := fun _ xs => xs.length
#eval len' Nat ([1, 2, 3].map (· * 10))   -- 3  = f (map g xs)
#eval len' Nat [1, 2, 3]                    -- 3  = f xs

∀ α, List α → List α: rearrange, drop, duplicate — never invent. Every output element came from the input; which positions are kept is chosen by shape alone. So f commutes with map, and the output length depends only on the input length. reverse, id, tail, and fun _ => [] inhabit it; “the singleton of the largest element” does not — it would have to compare elements the type forbids it to inspect.

def rev' : ∀ α : Type, List α → List α := fun _ xs => xs.reverse
#eval rev' Nat ([1, 2, 3].map (· * 10))   -- [30, 20, 10]  = f (map g xs)
#eval (rev' Nat [1, 2, 3]).map (· * 10)    -- [30, 20, 10]  = (map g) (f xs)

The boundary of free theorems

A polymorphic signature can force naturality, no-invention, and shape-only behaviour — but never a property that depends on the element values. No ∀ α, List α → List α forces “the output is a permutation of the input” (reverse satisfies it, but fun _ => [] inhabits the same type); “sorted” is further out of reach, since sorting must compare elements. Those properties need a specification carried in addition to the type — the subtype/Prop specifications of Weeks 9 and 11. Free theorems tell you what you get for free; their boundary tells you where a written specification becomes unavoidable.

This reading is the inverse of the derivation method of Week 2 (§2.6): where the derivation is forced, the free theorem is total. Building a term from a type and reading what every term of a type must do are one skill in two directions.

7.3 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 [heq]
      | inr ht  =>
        simp
        right
        exact ih.mpr ht

Checkpoint — contains. contains needs [DecidableEq α] to test elements. Predict both Booleans, then check.

#eval contains 3 [1, 2, 3]   -- predict
#eval contains 9 [1, 2, 3]   -- predict

7.4 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

Checkpoint — DecidableEq (List Nat). Predict the Boolean below, and say why List Nat has DecidableEq (but List Float would not), before reading the result.

#eval decide (([1, 2, 3] : List Nat) = [1, 2, 3])   -- predict first

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

Checkpoint — Float has BEq, not DecidableEq. == on Float is IEEE 754 BEq (a Bool), not provable equality. Predict the Boolean below — is NaN equal to itself? — then check, and say why this is exactly what forbids DecidableEq Float.

#eval ((0.0 / 0.0 : Float) == (0.0 / 0.0 : Float))   -- 0/0 is NaN; predict (IEEE 754)

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

Checkpoint — the decidability boundary. A bounded quantifier over a literal list is decidable; an unbounded one over Nat is not. Predict the Boolean below, then say why the ∀ n : Nat, … version could not be checked this way.

#eval decide (∀ x ∈ ([1, 2, 3] : List Nat), x < 10)   -- predict

Exercises

Banners read [id] · competency · tier · level · target; build exercises ship a #guard acceptance check (see EXERCISE_CONVENTIONS.md). Do every core exercise; stretch is optional.

[E7.1] · inhabitation + specification writing · tier 1 · core · target myNub

Define myNub [DecidableEq α] : List α → List α removing duplicates. State its spec — “every result element is in the input, and no element repeats” — then confirm via checkable properties (order-independent, so any correct implementation passes):

#guard (myNub [1, 1, 2, 3, 3, 3]).Nodup
#guard (myNub [1, 1, 2, 3, 3, 3]).length = 3
#guard decide (∀ x ∈ myNub [1, 1, 2, 3, 3, 3], x ∈ [1, 1, 2, 3, 3, 3]) = true

[E7.2] · decidability identification · tier 1 · core

For each, state whether decide can close it and why, using the §7.6 boundary table — then check only the ones that are decidable:

(a) ("hello" : String) = "hello" (b) (1.0 : Float) = 1.0 (c) ([1,2,3] : List Nat) = [1,2,3] (d) ∀ n : Nat, n + 0 = n

#guard decide (("hello" : String) = "hello") = true
#guard decide (([1, 2, 3] : List Nat) = [1, 2, 3]) = true
-- (b) and (d) have no check on purpose: say why decide cannot close each.

[E7.3] · counterexample finding · tier 1 · core

A student claims “contains x xs = true iff x is the head of xs.” It is wrong. Find inputs where contains is true but x is not the head, and encode the witness so the check succeeds:

#guard contains 3 [1, 2, 3] = true
#guard [1, 2, 3].head? ≠ some 3

What is the correct characterization of contains x xs = true? (It is contains_spec, §7.3 — read it.)

[E7.4] · type-directed derivation · tier 2 · core · target second

Derive second : α → β → β (return the second argument). Give a derivation trace (Week 2 §2.6) and show every step is forced — this type has exactly one inhabitant. Contrast with myConst : α → β → α (§7.1): same shape, the other projection. Effort: 2 trace steps.

#guard second 1 2 = 2
#guard second "x" (5 : Nat) = 5

[E7.5] · type reading (free theorems) · tier 2 · core

The chapter intro says a polymorphic f : List α → List α “can only permute, drop, or duplicate.” Read that off the type: state two things every inhabitant of ∀ α, List α → List α must satisfy and one thing it cannot do. Then: how many inhabitants does ∀ α β, α → β → α have, and why? (Builds on §7.2 — no code to submit.)

[E7.6] · inhabitation + decidability identification · tier 1 · stretch · target Color

Define inductive Color where | Red | Green | Blue deriving DecidableEq. Use decide to settle both, then explain why the bounded ∀ c ∈ […] is decidable here but the same shape over all Nat (§7.6) is not:

#guard decide (Color.Red ≠ Color.Blue) = true
#guard decide (∀ c ∈ [Color.Red, Color.Green, Color.Blue], c = Color.Red ∨ c ≠ Color.Red) = true

end W07

-- FPCourse/T03_HigherOrderAndSpecification/W08_HigherOrderFunctions.lean
import Mathlib.Data.List.Basic

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 W08

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]

Checkpoint — map. map f applies f to every element and preserves length and order. Predict the list below — three elements, each multiplied by 10 — before you read it.

#eval [1, 2, 3].map (· * 10)   -- predict first

Checkpoint — filter. filter p keeps exactly the elements where p is true, in order. Predict which of 1..6 survive (· % 3 == 0), then check.

#eval [1, 2, 3, 4, 5, 6].filter (· % 3 == 0)   -- predict first

Checkpoint — foldl (accumulate from the left). foldl threads the accumulator left-to-right: it sees 1, then 2, … Predict the digits-to-number accumulation below (start 0; each step is acc * 10 + x), then check.

#eval [1, 2, 3, 4, 5].foldl (fun acc x => acc * 10 + x) 0   -- predict first

Checkpoint — foldr (accumulate from the right). foldr f z nests from the right: 1 - (2 - (3 - (4 - 0))). Direction matters when f is not associative. Predict this Int value — it is not the same as the left fold — then check.

#eval ([1, 2, 3, 4] : List Int).foldr (fun x acc => x - acc) 0   -- predict first

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)

Checkpoint — mapViaFoldr agrees with map. mapViaFoldr rebuilds the list, replacing each x with f x :: …. Predict the result from mapViaFoldr_eq_map (not by tracing the fold), then check.

#eval mapViaFoldr (· + 1) [10, 20, 30]   -- predict from mapViaFoldr_eq_map

-- 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) []

Checkpoint — filterViaFoldr. Each step keeps x only when p x. Predict which of 1..4 survive (· % 2 == 0), then check that it matches ordinary filter.

#eval filterViaFoldr (· % 2 == 0) [1, 2, 3, 4]   -- predict first

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]

Checkpoint — Functor Law 1 (map id = id). By map_id_law, mapping id returns the list unchanged. Predict the Boolean below from the law (not by evaluating the map), then check.

#eval decide ((([1, 2, 3] : List Nat).map id) = [1, 2, 3])   -- predict from map_id_law

Checkpoint — Functor Law 2 (map (f ∘ g) = map f ∘ map g). One pass with the composition equals two passes. Predict the Boolean below from map_comp_law with g = (· * 2), f = (· + 1), then check.

#eval decide ((([1, 2, 3] : List Nat).map ((· + 1) ∘ (· * 2)))
              = ((([1, 2, 3] : List Nat).map (· * 2)).map (· + 1)))   -- predict from map_comp_law

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

Checkpoint — Option.map obeys the same functor laws. The identity law has one shape across all functors. Predict both Booleans from option_map_id — some and none — then check that the form matched List.

#eval decide ((some 5 : Option Nat).map id = some 5)   -- predict from option_map_id
#eval decide ((none  : Option Nat).map id = none)      -- predict from option_map_id

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

Checkpoint — foldr (· :: ·) [] reconstructs the list. Replacing every :: with :: and [] with [] is the identity. Predict the result from foldr_cons_nil, then check.

#eval ([1, 2, 3, 4] : List Nat).foldr (· :: ·) []   -- predict from 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

Checkpoint — foldr_append. Folding over xs ++ ys folds ys first, then feeds that result in as the base for xs. Predict the Boolean below from foldr_append (both sides sum to the same number), then check.

#eval decide ((([1, 2] ++ [3, 4] : List Nat).foldr (· + ·) 0)
              = (([1, 2] : List Nat).foldr (· + ·) (([3, 4] : List Nat).foldr (· + ·) 0)))
              -- predict from 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)

Checkpoint — map-foldr fusion. By map_foldr_fusion, mapping (· * 2) and then summing equals a single fold with (· + ·) ∘ (· * 2). Predict the Boolean below from the law (both fold the same total), then check.

#eval decide (((([1, 2, 3] : List Nat).map (· * 2)).foldr (· + ·) 0)
              = (([1, 2, 3] : List Nat).foldr ((· + ·) ∘ (· * 2)) 0))   -- predict from map_foldr_fusion

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E8.1] · specification writing · tier 1 · core · target MyPair.map

Define the type and its map, deriving DecidableEq so the laws are decide-checkable:

inductive MyPair (α : Type) where
  | mk : α → α → MyPair α
  deriving DecidableEq
def MyPair.map (f : α → β) : MyPair α → MyPair β
  | .mk a b => .mk (f a) (f b)

State the two functor laws for MyPair as Props (identity and composition — same form as §8.3), then confirm them on concrete instances. Do not prove the general laws; the point is to write the specification and check it holds on data:

-- identity law, one instance
#guard (MyPair.mk (1 : Nat) 2).map id = MyPair.mk 1 2
-- composition law, one instance (g = (· * 2), f = (· + 1))
#guard (MyPair.mk (1 : Nat) 2).map ((· + 1) ∘ (· * 2))
       = ((MyPair.mk (1 : Nat) 2).map (· * 2)).map (· + 1)

In one line: which tier does the general law live in, and which the two checks?

[E8.2] · type-directed derivation · tier 2 · core · target sumList

Derive sumList : List Nat → Nat (the sum of the elements) as a foldl. The graded artifact is a derivation trace in the Week 2 §2.6 format, then the def. First-step hint: read the type List Nat → Nat — the seed is the unit of + (which Nat?), and foldl (· + ·) threads it left across the list. Effort: ~3 trace steps, 1 line of code.

#guard sumList [] = 0
#guard sumList [5] = 5
#guard sumList [1, 2, 3, 4] = 10

[E8.3] · counterexample finding · tier 1 · core

A student claims “foldl f z xs and foldr f z xs always compute the same result.” It is wrong whenever f is not associative/commutative. Find one f, z, and xs witnessing the mismatch and encode the witness so the check succeeds (it confirms the two sides differ):

#guard ([1, 2, 3] : List Int).foldl (· - ·) 0 ≠ ([1, 2, 3] : List Int).foldr (· - ·) 0

In one line: for which class of operators f do the two folds agree?

[E8.4] · type reading (free theorems) · tier 2 · core

Look only at the type of List.map, namely (α → β) → List α → List β, polymorphic in α and β. Without running anything, state two things every inhabitant must do and one thing it cannot do. Prompts: can it change the length? reorder? invent a β out of nowhere, with no α in hand and no f applied? inspect an α (compare two, branch on a value) when all it holds is f : α → β? Then, second: what extra does the type of List.foldr, (α → β → β) → β → List α → β, let an inhabitant do that map’s type does not? (Builds on §8.3–§8.5 and Week 7 §7.2. No code to submit.)

[E8.5] · specification writing · tier 1 · stretch · target flatten

Write flatten : List (List α) → List α using foldr (concatenate a list of lists). State its specification as a Prop relating it to the library function — “for every xss, flatten xss = xss.flatten” — then confirm on instances. Do not prove the general spec; write it and check it. Effort: one foldr (· ++ ·) []; ~1 line.

#guard flatten [[1, 2], [3], [4, 5, 6]] = [1, 2, 3, 4, 5, 6]
#guard flatten ([] : List (List Nat)) = []
#guard flatten [[], [1], []] = [1]
#guard flatten ([[1, 2], [3], [4, 5, 6]] : List (List Nat)) = ([[1, 2], [3], [4, 5, 6]] : List (List Nat)).flatten

[E8.6] · decidability identification · tier 1 · stretch

For each proposition, say whether decide can close it and why (finite domain? decidable predicate? quantifier over a function type or an unbounded Nat?) before checking — the judgment is the point, not the tool-use:

(a) ([1, 2, 3] : List Nat).map (· + 1) = [2, 3, 4] (b) ∀ x ∈ ([1, 2, 3] : List Nat), (· + 1) x > x (c) ∀ xs : List Nat, xs.map id = xs (d) ∀ f : Nat → Nat, [1, 2].map f = [f 1, f 2]

#guard decide (([1, 2, 3] : List Nat).map (· + 1) = [2, 3, 4]) = true
#guard decide (∀ x ∈ ([1, 2, 3] : List Nat), (· + 1) x > x) = true
-- (c) and (d) have no check on purpose: say why `decide` cannot close each
--     (name the obstacle — unbounded `Nat`; equality/quantification over a function type).

[E8.7] · type-directed derivation + specification writing · tier 2 · stretch · target flatMap

Derive flatMap : (α → List β) → List α → List β using foldr: apply f to every element and concatenate the results. Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. Then state, as a Prop, that your flatMap agrees with the standard library’s list bind, which in this toolchain is List.flatMap : (α → List β) → List α → List β (named List.bind in earlier versions); look it up and read its type rather than proving the agreement.

#guard flatMap (fun n => [n, n]) [1, 2, 3] = [1, 1, 2, 2, 3, 3]
#guard flatMap (fun n => List.replicate n 0) [0, 2] = [0, 0]
#guard flatMap (fun n => [n]) ([] : List Nat) = ([] : List Nat)

First-step hint: foldr consumes the List α; its step function receives one α and the already-folded List β, so the step is an append. Effort: ~3 trace steps, 2 lines of code.

end W08

-- FPCourse/T03_HigherOrderAndSpecification/W09_Specifications.lean
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Pairwise

open scoped List

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 W09

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

Checkpoint — Sorted. List.Sorted (· ≤ ·) holds iff every adjacent pair is non-decreasing. Predict the Boolean below — is [1, 2, 3, 4] in order? — then check.

#eval decide (List.Sorted (· ≤ ·) ([1, 2, 3, 4] : List Nat))   -- predict first

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

Checkpoint — Perm. xs ~ ys holds iff the two lists have the same elements with the same multiplicities (order aside). Predict the Boolean below — is [1, 2, 3] a rearrangement of [3, 1, 2]? — then check.

#eval decide (([1, 2, 3] : List Nat) ~ [3, 1, 2])   -- predict first

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

Checkpoint — CorrectSort needs BOTH conjuncts. The constant-empty function fun _ => [] returns a sorted list but loses elements. Predict the Boolean below — which of the two conjuncts fails on input [1]? — then check that the bundle is false.

#eval decide (List.Sorted (· ≤ ·) ([] : List Nat) ∧ (([] : List Nat) ~ [1]))   -- predict first

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

Checkpoint — insert'. insert' drops x into an already-sorted list at the first position where x ≤ h. Predict the result of inserting 4 into [1, 3, 5] before reading it.

#eval insert' 4 [1, 3, 5]   -- predict first

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 []                  -- []

Checkpoint — insertionSort. insertionSort folds insert' over the input, one element at a time. Predict its output on [3, 1, 2] — what does insertion sort always return? — then check.

#eval insertionSort [3, 1, 2]   -- predict first

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 preserves the permutation relation — insert' x xs is a permutation of x :: xs. Both insert_sorted (Helper 2) and insertionSort_perm (Helper 4) reuse this single lemma.

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)

Checkpoint — insert_perm. The provided proof guarantees: insert' x xs is a permutation of x :: xs (nothing added or lost). Predict the Boolean below, then check.

#eval decide (insert' 4 [1, 3, 5] ~ 4 :: [1, 3, 5])   -- predict first

Helper 2: inserting into a sorted list produces a sorted list.

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

Checkpoint — insert_sorted. The provided proof guarantees: insert into a sorted list, stay sorted. Predict the Boolean below — is insert' 4 [1, 3, 5] sorted? — then check that the theorem’s conclusion holds on this instance.

#eval decide (List.Sorted (· ≤ ·) (insert' 4 [1, 3, 5]))   -- predict first

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)

Checkpoint — insertionSort_sorted. This chains insert_sorted down the recursion, so every output is sorted. Predict the Boolean below, then check.

#eval decide (List.Sorted (· ≤ ·) (insertionSort [5, 3, 1, 4, 2]))   -- predict first

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

Checkpoint — insertionSort_perm. This chains insert_perm down the recursion, so the output always has exactly the input’s elements. Predict the Boolean below, then check.

#eval decide (insertionSort [5, 3, 1, 4, 2] ~ [5, 3, 1, 4, 2])   -- predict first

Main theorem: insertion sort is correct.

theorem insertionSort_correct : CorrectSort insertionSort :=
  fun xs => ⟨insertionSort_sorted xs, insertionSort_perm xs⟩

Checkpoint — insertionSort_correct. The main theorem simply pairs the two helpers ⟨sorted, perm⟩. Predict the Boolean below — both conjuncts hold on [4, 2, 3, 1] — then check.

#eval decide (List.Sorted (· ≤ ·) (insertionSort [4, 2, 3, 1]) ∧ insertionSort [4, 2, 3, 1] ~ [4, 2, 3, 1])   -- predict first

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

Checkpoint — decidable verification on instances. Perm on List Nat is decidable, so decide settles it — and it tracks multiplicity, not just membership. Predict the Boolean below (note the repeated 1), then check.

#eval decide (insertionSort [3, 1, 4, 1, 5, 9] ~ [3, 1, 4, 1, 5, 9])   -- predict first

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) (· ≤ ·)⟩⟩

Checkpoint — the postcondition value. sortedMerge’s subtype { zs // Sorted zs ∧ zs ~ xs ++ ys } is carried by the value (xs ++ ys).mergeSort (· ≤ ·). Predict what that value computes for [1, 3] ++ [2, 4], then check.

#eval (([1, 3] ++ [2, 4] : List Nat)).mergeSort (· ≤ ·)   -- predict first

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E9.1] · specification reading · tier 1 · core

CorrectSort (§9.3) demands both Sorted and Perm; §9.3 argued each is needed because a bogus sorter can satisfy one alone. Make that concrete. For the two bogus sorters below, say which single conjunct each violates, then encode the witnesses so every check succeeds (each is decidable on List Nat):

-- `fun _ => []` : sorted, but NOT a permutation of a non-empty input →
#guard List.Sorted (· ≤ ·) ([] : List Nat)
#guard decide (¬ (([] : List Nat) ~ [1, 2])) = true
-- `id` : a permutation, but NOT always sorted →
#guard ([3, 1, 2] : List Nat) ~ [3, 1, 2]
#guard decide (¬ List.Sorted (· ≤ ·) ([3, 1, 2] : List Nat)) = true

In one line: which conjunct fails for fun _ => [], and which for id?

[E9.2] · specification writing · tier 1 · core · target dedup

Define dedup : List Nat → List Nat that removes duplicate elements, and state its specification DedupSpec : Prop — “the result has no duplicates, and it has exactly the elements of the input.” You need not prove DedupSpec; confirm it on instances with decidable, order-independent checks (any correct implementation passes):

#guard (dedup [1, 1, 2, 3, 3, 3]).Nodup
#guard decide (∀ x ∈ ([1, 1, 2, 3, 3, 3] : List Nat), x ∈ dedup [1, 1, 2, 3, 3, 3]) = true
#guard dedup ([] : List Nat) = []

First-step hint: recurse on the list; on h :: t, test h ∈ t (decidable, Nat has DecidableEq) to decide whether to keep h. Effort: ~4 lines.

[E9.3] · counterexample finding · tier 1 · core · target CorrectSortDesc

Define CorrectSortDesc — CorrectSort but for descending order, i.e. List.Sorted (· ≥ ·) in place of (· ≤ ·). Insertion sort does not satisfy it. Find an input on which the output is not (· ≥ ·)-sorted, and encode the witness so the check succeeds (a correct counterexample makes the negation true):

#guard decide (¬ List.Sorted (· ≥ ·) (insertionSort [2, 1, 3])) = true
#guard List.Sorted (· ≥ ·) ([3, 2, 1] : List Nat)   -- what a descending-sorted list looks like

In one line: which conjunct of CorrectSortDesc does insertionSort break, and which does it still satisfy?

[E9.4] · specification reading · tier 3 · core

Read the provided proof of insertionSort_correct (§9.5) — do not write a proof. In prose, answer: (a) insertionSort_correct is fun xs => ⟨_, _⟩; what are the two components, and which conjunct of CorrectSort does each discharge? (b) insertionSort_sorted depends on insert_sorted, and insertionSort_perm on insert_perm; explain in one sentence each what property of insert' the two helpers establish, and why the recursion needs them. (c) The [] case of insertionSort_sorted is List.Pairwise.nil; why is the empty list vacuously sorted? No code to submit.

[E9.5] · decidability identification · tier 1 · stretch

For each proposition, say whether decide can close it and why (finite domain? decidable predicate?) before checking — the judgment is the point, not the tool-use:

(a) List.Sorted (· ≤ ·) (insertionSort [9, 1, 3, 7, 2, 6]) (b) insertionSort [3, 1, 2] ~ [3, 1, 2] (c) CorrectSort insertionSort

#guard decide (List.Sorted (· ≤ ·) (insertionSort [9, 1, 3, 7, 2, 6])) = true
#guard decide (insertionSort [3, 1, 2] ~ [3, 1, 2]) = true
-- (c) has no check on purpose: say why `decide` cannot close `CorrectSort insertionSort`,
--     and name the term that settles it instead (hint: it is in §9.5).

[E9.6] · type-directed derivation · tier 2 (+ tier-3 reading) · stretch · target correctSorter

The subtype { f : List Nat → List Nat // CorrectSort f } is a proof-carrying type: an inhabitant bundles a sorting function with a proof it is correct. Build one inhabitant, correctSorter, by reusing the provided term insertionSort_correct (§9.5) as the proof component — you author no proof:

-- def correctSorter : { f : List Nat → List Nat // CorrectSort f } :=
--   ⟨insertionSort, insertionSort_correct⟩
#guard (correctSorter.val [4, 2, 3, 1] : List Nat) = [1, 2, 3, 4]
#guard (correctSorter.val ([] : List Nat)) = []

First-step hint: the anonymous constructor ⟨_, _⟩ for a subtype takes the value then its proof; the value is insertionSort, the proof is already proved for you. In one line: what does .val project out, and what guarantee did the second component add to the type?

end W09

-- FPCourse/T04_SetsAndRelations/W10_SetsRelations.lean
import Mathlib.Data.Set.Basic
import Mathlib.Data.Set.Function
import Mathlib.Logic.Relation

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 W10

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

Checkpoint — set membership. x ∈ s is just s x, the proposition that x satisfies the predicate. Predict the Boolean below — is 3 one of the listed elements? — then check.

#eval decide ((3 : Nat) ∈ ({1, 2, 3} : Set Nat))   -- predict first

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

Checkpoint — Set.univ and ∅. univ = fun _ => True and ∅ = fun _ => False are the two constant sets. Predict both Booleans — everything is in univ, nothing is in ∅ — then check.

#eval decide ((7 : Nat) ∈ (Set.univ : Set Nat))   -- predict first
#eval decide ((7 : Nat) ∈ (∅ : Set Nat))          -- predict first

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

Checkpoint — intersection ∩. By mem_inter_iff, x ∈ s ∩ t means x ∈ s ∧ x ∈ t. Predict whether 3 is in both sets below, then check.

#eval decide ((3 : Nat) ∈ (({1, 2, 3} ∩ {3, 4, 5}) : Set Nat))   -- predict first

-- Union is ∨:
theorem mem_union_iff (x : α) (s t : Set α) :
    x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t :=
  Set.mem_union x s t

Checkpoint — union ∪. By mem_union_iff, x ∈ s ∪ t means x ∈ s ∨ x ∈ t. Predict whether 1 is in either set below, then check.

#eval decide ((1 : Nat) ∈ (({1, 2, 3} ∪ {3, 4, 5}) : Set Nat))   -- predict first

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

Checkpoint — complement ᶜ. x ∈ sᶜ means ¬ (x ∈ s). Predict whether 5, which is not listed, belongs to the complement below, then check.

#eval decide ((5 : Nat) ∈ (({1, 2, 3} : Set Nat)ᶜ))   -- predict first

Checkpoint — difference \. x ∈ s \ t means x ∈ s ∧ ¬ (x ∈ t). Predict whether 1 survives removing {3, 4} from {1, 2, 3}, then check.

#eval decide ((1 : Nat) ∈ (({1, 2, 3} \ {3, 4}) : Set Nat))   -- predict first

Checkpoint — subset ⊆. s ⊆ t is ∀ x, x ∈ s → x ∈ t — one implication per element, so it is not decidable over all of Nat. Predict that single implication at x = 2 (is 2 ∈ {1,2} → 2 ∈ {1,2,3} true?), then check.

#eval decide ((2 : Nat) ∈ ({1, 2} : Set Nat) → (2 : Nat) ∈ ({1, 2, 3} : Set Nat))   -- predict first

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

Checkpoint — ∩ commutativity. inter_comm says s ∩ t = t ∩ s, so membership must agree on either side. Predict the Boolean (an ↔ of memberships at x = 2), then check.

#eval decide ((2 : Nat) ∈ (({1, 2, 3} ∩ {2, 3, 4}) : Set Nat) ↔ (2 : Nat) ∈ (({2, 3, 4} ∩ {1, 2, 3}) : Set Nat))   -- predict first

-- Distributivity:
theorem inter_union_distrib (r s t : Set α) :
    r ∩ (s ∪ t) = (r ∩ s) ∪ (r ∩ t) :=
  Set.inter_union_distrib_left r s t

Checkpoint — ∩/∪ distributivity. r ∩ (s ∪ t) = (r ∩ s) ∪ (r ∩ t). Predict the membership ↔ below at x = 2, then check.

#eval decide ((2 : Nat) ∈ (({1, 2} ∩ ({2, 3} ∪ {4, 5})) : Set Nat) ↔ (2 : Nat) ∈ ((({1, 2} ∩ {2, 3}) ∪ ({1, 2} ∩ {4, 5})) : Set Nat))   -- predict first

-- De Morgan:
theorem compl_union (s t : Set α) : (s ∪ t)ᶜ = sᶜ ∩ tᶜ :=
  Set.compl_union s t

Checkpoint — De Morgan. (s ∪ t)ᶜ = sᶜ ∩ tᶜ: not-in-either equals not-in-each. Predict the membership ↔ at x = 5 (in neither {1,2} nor {3,4}), then check.

#eval decide ((5 : Nat) ∈ ((({1, 2} ∪ {3, 4}) : Set Nat)ᶜ) ↔ (5 : Nat) ∈ ((({1, 2} : Set Nat)ᶜ ∩ ({3, 4} : Set Nat)ᶜ)))   -- predict first

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

Checkpoint — divides. divides m n is ∃ k, n = m * k; the example above witnesses divides 3 12 with k = 4. Predict whether that witness equation holds, then check.

#eval decide (12 = 3 * 4)   -- predict first (the witness for divides 3 12)

Checkpoint — sameLength. sameLength xs ys unfolds to xs.length = ys.length. Predict whether a 3-element list and a 3-element list are related, then check.

#eval decide ([1, 2, 3].length = ['a', 'b', 'c'].length)   -- predict first (sameLength unfolded)

Checkpoint — lePair. lePair is (· ≤ ·) packaged as a Rel Nat Nat. Predict whether 3 and 5 are related, then check (using ≤ directly).

#eval decide ((3 : Nat) ≤ 5)   -- predict first (lePair 3 5)

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⟩

Checkpoint — reflexivity. RelReflexive r is ∀ a, r a a; over all Nat it is not decidable, but any single instance is. Predict the reflexivity instance 3 ≤ 3, then check.

#eval decide ((3 : Nat) ≤ 3)   -- predict first

Checkpoint — symmetry fails for ≤. Symmetry would need r a b → r b a for all a, b. Predict the witness that breaks it — 0 ≤ 1 holds but 1 ≤ 0 does not — then check.

#eval decide ((0 : Nat) ≤ 1 ∧ ¬ ((1 : Nat) ≤ 0))   -- predict first (a counterexample to symmetry)

Checkpoint — transitivity. RelTransitive r needs r a b → r b c → r a c. Predict this instance chaining 1 ≤ 2 and 2 ≤ 3, then check.

#eval decide (((1 : Nat) ≤ 2) → ((2 : Nat) ≤ 3) → ((1 : Nat) ≤ 3))   -- predict first

Checkpoint — equivalence (=). = on Nat is reflexive, symmetric, and transitive. Predict this bundle — 2 = 2 and (2 = 3 → 3 = 2) — then check.

#eval decide ((2 : Nat) = 2 ∧ ((2 : Nat) = 3 → (3 : Nat) = 2))   -- predict first

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

Checkpoint — relational composition. relComp (· ≤ ·) (· ≤ ·) 1 3 is ∃ b, 1 ≤ b ∧ b ≤ 3. The ∃ over Nat is not decidable, but a witness settles it. Predict whether b = 2 works — 1 ≤ 2 ∧ 2 ≤ 3 — then check.

#eval decide (((1 : Nat) ≤ 2) ∧ ((2 : Nat) ≤ 3))   -- predict first (b = 2 witnesses relComp)

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

Checkpoint — image / range. b ∈ Set.image f s means ∃ a ∈ s, f a = b, and image f univ = range f. A witness a settles one such membership. Predict whether 6 lies in the image of (· * 2) because 3 ↦ 6, i.e. that (· * 2) 3 = 6, then check.

#eval decide ((fun (x : Nat) => x * 2) 3 = 6)   -- predict first (3 ↦ 6, so 6 ∈ image)

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.

Checkpoint — functional relation. A function f induces the relation fun a b => f a = b, in which each input relates to exactly one output. Predict whether 2 relates to 4 under (· * 2), i.e. that (· * 2) 2 = 4, then check.

#eval decide ((fun (x : Nat) => x * 2) 2 = 4)   -- predict first

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E10.1] · specification writing · tier 1 (+ tier-3 reading) · core · target DeMorganInterSpec

State, as a Prop, De Morgan’s law for intersection: “for all sets s t and every x, x ∈ (s ∩ t)ᶜ ↔ x ∈ sᶜ ∪ tᶜ.” Do not prove the general statement — that proof is Set.compl_inter (§10.3 provides the union form Set.compl_union; read it, tier 3). Confirm the spec on concrete sets, covering an element in both, in neither, and in exactly one:

-- def DeMorganInterSpec : Prop :=
--   ∀ (s t : Set Nat) (x : Nat), x ∈ (s ∩ t)ᶜ ↔ x ∈ sᶜ ∪ tᶜ
#guard decide ((2 : Nat) ∈ ((({1,2} ∩ {2,3}) : Set Nat)ᶜ) ↔ (2 : Nat) ∈ ((({1,2} : Set Nat)ᶜ) ∪ (({2,3} : Set Nat)ᶜ)))   -- 2 in both
#guard decide ((5 : Nat) ∈ ((({1,2} ∩ {2,3}) : Set Nat)ᶜ) ↔ (5 : Nat) ∈ ((({1,2} : Set Nat)ᶜ) ∪ (({2,3} : Set Nat)ᶜ)))   -- 5 in neither
#guard decide ((1 : Nat) ∈ ((({1,2} ∩ {2,3}) : Set Nat)ᶜ) ↔ (1 : Nat) ∈ ((({1,2} : Set Nat)ᶜ) ∪ (({2,3} : Set Nat)ᶜ)))   -- 1 in exactly one

In one line: which tier does the general statement live in, and which the three checks?

[E10.2] · decidability identification · tier 1 · core

For each proposition, say whether decide can close it and why — a finite literal set is decidable, but ⊆ and an unbounded ∀ both range over all of Nat — the judgment is the point, not the tool-use. Then check only the decidable ones:

(a) (3 : Nat) ∈ ({1, 2, 3} : Set Nat) (b) ({1, 2} : Set Nat) ⊆ {1, 2, 3} (c) ∀ a : Nat, a ≤ a (d) (1 : Nat) ∈ (({1, 2} ∪ {3}) : Set Nat)

#guard decide ((3 : Nat) ∈ ({1, 2, 3} : Set Nat)) = true
#guard decide ((1 : Nat) ∈ (({1, 2} ∪ {3}) : Set Nat)) = true
-- (b) and (c) have no check on purpose: say why decide cannot close each
--     (both quantify over every Nat, not over a finite literal set).

[E10.3] · counterexample finding · tier 1 · core

A student claims “divides is symmetric: if m divides n then n divides m.” It is wrong. On Nat, divides m n (∃ k, n = m * k, §10.4) is exactly m ∣ n. Find a witness where one direction holds and the other fails, and encode it as the fact that must hold, so the check succeeds:

#guard decide ((3 : Nat) ∣ 12 ∧ ¬ ((12 : Nat) ∣ 3)) = true
#guard decide (¬ ((2 : Nat) ∣ 3)) = true

Which single property of ≤ (§10.5) also fails, with the same shape of witness?

[E10.4] · type-directed derivation · tier 2 · core · target converseB

Derive converseB : (α → β → Bool) → (β → α → Bool), the converse of a Boolean relation — swap the two arguments (cf. the Rel converse behind symmetry, §10.5). Produce a derivation trace in the Week 2 §2.6 format — the trace is the graded artifact — then the def. First-step hint: the result type is β → α → Bool, so introduce the relation r, then b : β, then a : α; only r a b type-checks as the body. Effort: ~3 trace steps, 1 line of code.

#guard converseB (fun a b => decide (a ≤ b)) 5 3 = true    -- swaps to decide (3 ≤ 5)
#guard converseB (fun a b => decide (a ≤ b)) 3 5 = false   -- swaps to decide (5 ≤ 3)
#guard converseB (fun a b => a == b) 2 (2 : Nat) = true

[E10.5] · specification writing + decidability identification · tier 1 · stretch · target IsOrder

State, as a Prop, what it means for r : Rel Nat Nat to be an order: reflexive, transitive, and antisymmetric (∀ a b, r a b → r b a → a = b). Do not prove the general claim for ≤; instead confirm each of the three clauses on concrete Nat instances — antisymmetry holds vacuously when the two ≤s cannot both point the same way:

-- def IsOrder (r : Rel Nat Nat) : Prop :=
--   (∀ a, r a a) ∧ (∀ a b c, r a b → r b c → r a c) ∧ (∀ a b, r a b → r b a → a = b)
#guard decide ((3 : Nat) ≤ 3) = true                                         -- reflexive instance
#guard decide (((1 : Nat) ≤ 2) → ((2 : Nat) ≤ 5) → ((1 : Nat) ≤ 5)) = true   -- transitive instance
#guard decide (((2 : Nat) ≤ 3) → ((3 : Nat) ≤ 2) → (2 : Nat) = 3) = true     -- antisymmetric instance

Why is the general IsOrder (· ≤ ·) statement itself not decide-checkable?

[E10.6] · type reading (free theorems) · tier 2 · stretch

Look only at the type of relComp, namely Rel α β → Rel β γ → Rel α γ, polymorphic in α, β, γ. Without running anything, state two things every inhabitant must respect (can it manufacture a bridging b : β out of nowhere? can it inspect the elements it threads through?) and one thing the type forbids. This is the inverse of E10.4 and echoes the free theorems of Week 7 (§7.2). No code to submit.

[E10.7] · specification writing + decidability identification · tier 1 · stretch · target IsPrefix

Define the relation IsPrefix : Rel (List α) (List α) — xs is a prefix of ys when some zs extends it:

def IsPrefix (xs ys : List α) : Prop := ∃ zs, xs ++ zs = ys

Using the §10.4 vocabulary (RelReflexive, RelTransitive), state — do not prove — that IsPrefix is reflexive and transitive. Hint for reflexivity: which zs witnesses xs ++ zs = xs? The bare ∃ zs ranges over an unbounded domain, so decide cannot close it; check instances through the decidable Boolean List.isPrefixOf instead, and say in one line why that one computes while the ∃ does not:

#guard ([1, 2] : List Nat).isPrefixOf [1, 2, 3]
#guard ([] : List Nat).isPrefixOf [1, 2, 3]
#guard ([1, 2, 3] : List Nat).isPrefixOf [1, 2, 3]   -- reflexivity, on an instance
#guard !(([2, 3] : List Nat).isPrefixOf [1, 2, 3])

[E10.8] · specification reading + counterexample finding · tier 3 (reading) + tier 1 · stretch

State the specification “the image of s ∩ t under f is a subset of Set.image f s ∩ Set.image f t.” This is Mathlib’s Set.image_inter_subset, whose type is f '' (s ∩ t) ⊆ f '' s ∩ f '' t — look it up and read it. Then explain in two or three sentences why this is only a subset and not an equality, exhibit concrete f, s, t over Nat for which the two sides genuinely differ, and name the property of f that would buy you the reverse inclusion. No code to submit.

end W10

-- FPCourse/T05_AbstractTypesAndTypeClasses/W11_AbstractTypes.lean
import Mathlib.Data.List.Basic
import Mathlib.Data.Option.Basic

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 W11

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]

theorem alist_lookup_delete_same [DecidableEq k] (key : k) (m : AList k v) :
    AList.lookup key (AList.delete key m) = none := by
  induction m with
  | nil => rfl
  | cons hd t ih =>
    obtain ⟨k', v'⟩ := hd
    by_cases h : key = k'
    · subst h; simp [AList.delete, ih]
    · simp [AList.delete, AList.lookup, h, ih]

theorem alist_lookup_delete_diff [DecidableEq k] {k1 k2 : k} (m : AList k v)
    (hne : k1 ≠ k2) :
    AList.lookup k1 (AList.delete k2 m) = AList.lookup k1 m := by
  induction m with
  | nil => rfl
  | cons hd t ih =>
    obtain ⟨k', v'⟩ := hd
    by_cases h : k2 = k'
    · subst h; simp [AList.delete, AList.lookup, ih, hne]
    · by_cases h1 : k1 = k'
      · subst h1; simp [AList.delete, AList.lookup, h]
      · simp [AList.delete, AList.lookup, h, h1, ih]

All five laws now hold for AList, so we can package the implementation together with its proofs as a LawfulDict instance — the formal claim that AList satisfies the dictionary specification, not merely that it type-checks against the Dict interface.

instance {k : Type} [DecidableEq k] : LawfulDict (d := AList) (k := k) where
  toDict := inferInstance
  lookup_empty := alist_lookup_empty
  lookup_insert_same := alist_lookup_insert_same
  lookup_insert_diff := fun _ _ val m h => alist_lookup_insert_diff val m h
  lookup_delete_same := alist_lookup_delete_same
  lookup_delete_diff := fun _ _ m h => alist_lookup_delete_diff m h

Checkpoint — AList.insert then AList.lookup. insert conses (key, val) onto the front; lookup scans front-to-back. Predict what looking up a just-inserted key returns, then check.

#eval (AList.lookup 1 (AList.insert 1 100 (AList.empty : AList Nat Nat)))   -- predict first

Checkpoint — AList.lookup on an absent key (lookup_empty). Predict, from lookup_empty, what lookup returns for a key that was never inserted, then check.

#eval (AList.lookup 5 (AList.insert 1 100 (AList.empty : AList Nat Nat)))   -- predict first

Checkpoint — the most recent insert wins (lookup_insert_same). insert never deletes the old pair, but lookup finds the front one first. Predict, from lookup_insert_same, which value survives after inserting key 1 twice, then check.

#eval (AList.lookup 1 (AList.insert 1 200 (AList.insert 1 100 (AList.empty : AList Nat Nat))))   -- predict first

Checkpoint — AList.delete removes a key (lookup_delete_same). Predict, from lookup_delete_same, what lookup returns for a key after it is deleted, then check.

#eval (AList.lookup 1 (AList.delete 1 (AList.insert 1 100 (AList.empty : AList Nat Nat))))   -- predict first

Checkpoint — delete leaves other keys alone (lookup_delete_diff). Deleting key 1 must not disturb key 2. Predict, from lookup_delete_diff, the lookup of 2, then check.

#eval (AList.lookup 2 (AList.delete 1 (AList.insert 2 20 (AList.insert 1 10 (AList.empty : AList Nat Nat)))))   -- predict first

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.

Checkpoint — an opaque value cannot be evaluated. Unlike AList, a Counter has no reducible definition, so #eval Counter.value Counter.zero would fail to compute — everything you can know about it lives in the axioms. So here we #check instead of #eval. Predict the type Lean reports for Counter.value_incr (a ∀-statement about the interface), then check.

#check @Counter.value_incr   -- predict the ∀-statement; opaque, so no #eval

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

Checkpoint — pop undoes push (pop_push). For the List stack, push is cons and pop splits head from tail. Predict, from pop_push, the pair returned after pushing 5, then check.

#eval (Stack.pop (Stack.push 5 ([1, 2, 3] : List Nat)))   -- predict first

Checkpoint — push grows size by one (size_push). Predict, from size_push, the size after one push onto a 3-element stack, then check.

#eval (Stack.size (Stack.push 5 ([1, 2, 3] : List Nat)))   -- predict first

Checkpoint — pop on the empty stack (pop_empty). Predict, from pop_empty, what pop returns when there is nothing to remove, then check.

#eval (Stack.pop ([] : List Nat))   -- predict first

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.

Checkpoint — observations are what implementations must share. Representation independence says two lawful stacks agree on every observation (pop, size), even if their internals differ. A push-push-pop sequence is such an observation. Predict the LIFO result below, then check.

#eval (Stack.pop (Stack.push 9 (Stack.push 8 ([] : List Nat))))   -- predict first (LIFO)

11.7 Representation invariants and abstraction functions

A concrete representation usually admits values the abstract type should never observe. An AList can hold duplicate keys — [(1, 10), (1, 20)] — yet a dictionary is a partial function, so a key must map to at most one value. A representation invariant carves the legal representations out of the concrete type, and an abstraction function maps each legal representation to the abstract value it denotes.

Lean expresses “the values satisfying an invariant” with a refinement type (subtype) { x // Inv x }: a pair of a value x and a proof that Inv x holds. The invariant below is “keys are distinct” — (m.map Prod.fst).Nodup. The provided value carries a machine-checked proof that its three keys are distinct. You will read this proof in the exercises, never author one.

def wfExample : { m : AList Nat Nat // (m.map Prod.fst).Nodup } :=
  ⟨[(1, 10), (2, 20), (3, 30)], by decide⟩

Checkpoint — the representation invariant is decidable. Nodup over a concrete list of DecidableEq keys is decidable — which is exactly why by decide can discharge the proof inside wfExample. Predict the Boolean below — do wfExample’s keys satisfy the invariant? — then check.

#eval decide ((([(1, 10), (2, 20), (3, 30)] : AList Nat Nat).map Prod.fst).Nodup)   -- predict first

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E11.1] · specification writing · tier 1 · core · target AList.size

Add a size operation to the association-list dictionary and specify how it relates to the other operations. Define AList.size (m : AList k v) : Nat, then state — as Props in your own words — the two laws “the empty dict has size 0” and “insert grows size by exactly one” (AList never deduplicates, so the second holds literally, even for a repeated key). Confirm them on instances; the checks are the grader. Effort: 1 line of code; then say which check is the boundary case and which law each remaining check witnesses.

#guard AList.size (AList.empty : AList Nat Nat) = 0
#guard AList.size (AList.insert 1 10 (AList.empty : AList Nat Nat)) = 1
#guard AList.size (AList.insert 1 99 (AList.insert 1 10 (AList.empty : AList Nat Nat))) = 2
#guard AList.size (AList.delete 1 (AList.insert 1 10 (AList.empty : AList Nat Nat))) = 0

[E11.2] · decidability identification · tier 1 · stretch

For each proposition about the dictionary, say whether decide can close it and why (finite domain? decidable predicate? DecidableEq keys?) before checking — the judgment is the point, not the tool-use:

(a) AList.lookup 2 (AList.insert 2 20 (AList.insert 1 10 (AList.empty : AList Nat Nat))) = some 20 (b) ∀ key ∈ ([1,2,3] : List Nat), AList.lookup key (AList.insert key 0 (AList.empty : AList Nat Nat)) = some 0 (c) ∀ (m : AList Nat Nat) (key : Nat), AList.lookup key (AList.insert key 0 m) = some 0

#guard AList.lookup 2 (AList.insert 2 20 (AList.insert 1 10 (AList.empty : AList Nat Nat))) = some 20
#guard decide (∀ key ∈ ([1, 2, 3] : List Nat),
    AList.lookup key (AList.insert key 0 (AList.empty : AList Nat Nat)) = some 0) = true
-- (c) has no check on purpose: say why decide cannot close a ∀ over ALL AList values,
--     and name the §11.2 law that settles it instead.

[E11.3] · counterexample finding · tier 1 · core · target insertOrderCounterexample

A student claims “insert order never matters: inserting two pairs and then looking up any key gives the same answer regardless of the order of the two inserts.” It is wrong whenever the two keys coincide (the shadowing from §11.3). Find inputs where swapping two inserts changes a lookup, and encode the witness so the check succeeds (it confirms the two sides differ):

#guard AList.lookup 1 (AList.insert 1 200 (AList.insert 1 100 (AList.empty : AList Nat Nat)))
     ≠ AList.lookup 1 (AList.insert 1 100 (AList.insert 1 200 (AList.empty : AList Nat Nat)))

Then state, in one line, the correct condition under which insert order is irrelevant (it is exactly the hypothesis of lookup_insert_diff).

[E11.4] · type-directed derivation · tier 2 · core · target peek

Derive peek [Stack s] : s α → Option α — the top element without removing it — from the Stack interface alone. Produce a derivation trace in the Week 2 §2.6 format (the trace is the graded artifact), then the def. First-step hint: the only operation that inspects a stack is pop : s α → Option (α × s α); apply it first, then turn Option (α × s α) into Option α — which functor operation does that with a projection? Effort: ~3 trace steps, 1 line of code.

#guard peek ([1, 2, 3] : List Nat) = some 1
#guard peek ([] : List Nat) = none
#guard peek (Stack.push 7 ([1, 2] : List Nat)) = some 7

[E11.5] · type reading (free theorems) · tier 2 · stretch

Read two abstract signatures without running anything.

(a) Stack.pop : s α → Option (α × s α), polymorphic in the element type α and abstract in the container s. State two things every inhabitant must satisfy (can it manufacture an α it was never given? can a returned α be anything other than one already in the stack?) and one thing the type cannot force (e.g. LIFO vs FIFO order — why is that beyond the reach of the type?).

(b) Dict.lookup : k → d k v → Option v. What does polymorphism in v forbid lookup from doing to the values it returns, and why must every non-none result be a value that was previously inserted? (Builds on §7.2. No code to submit.)

[E11.6] · specification reading · tier 3 · core

§11.7 provides wfExample : { m : AList Nat Nat // (m.map Prod.fst).Nodup } — a well-formed dictionary carrying a machine-checked proof of its representation invariant. Read it (do not author any proof) and explain, in prose:

(a) what the invariant (m.map Prod.fst).Nodup asserts about the representation, and why a dictionary needs it (relate it to “a key maps to at most one value” from §11.2); (b) what the by decide inside wfExample actually verified, and why that check is decidable here; (c) the abstraction function — which partial function from keys to values does wfExample denote? (d) which AList operation from §11.3 can produce a value that violates the invariant, and confirm the violation with the check below (a correct duplicate-key witness makes the inequality-to-false check succeed):

#guard decide ((([(1, 10), (1, 20)] : List (Nat × Nat)).map Prod.fst).Nodup) = false

This is a reading task: the graded artifact is your four-part explanation, not a proof.

[E11.7] · specification writing · tier 1 · stretch · target Queue

Define a Queue type class in the style of §11.4’s Stack — empty, enqueue, dequeue : q α → Option (α × q α), and size — together with a LawfulQueue extension stating its laws. The decisive law is FIFO: dequeuing returns the oldest element, not the most recently enqueued. State the laws; do not prove them. Give the List-backed instance and confirm the laws on instances:

#guard (Queue.dequeue (Queue.enqueue 2 (Queue.enqueue (1 : Nat) (Queue.empty : List Nat)))).map Prod.fst = some 1
#guard (Queue.dequeue (Queue.empty : List Nat)).isNone
#guard Queue.size (Queue.enqueue 2 (Queue.enqueue (1 : Nat) (Queue.empty : List Nat))) = 2

Compare with LawfulStack (§11.4): exactly one law changes. Which one, and why does that single change reverse the order of every observation?

[E11.8] · type-directed derivation · tier 2 · stretch · target TwoListStack

Give a second Stack implementation with a different representation:

structure TwoListStack (α : Type) where
  front : List α
  back  : List α

push conses onto back; pop takes from front, and when front is empty it first rebalances by reversing back into it. Produce a derivation trace for pop — the trace is the graded artifact — then the defs, and write the LawfulStack law statements for this representation (statements only). First-step hint: pop eliminates front first ([] vs y :: ys); only the [] branch touches back. Effort: ~5 trace steps, ~8 lines.

#guard (TwoListStack.push 2 (TwoListStack.push (1 : Nat) TwoListStack.empty)).size = 2
#guard ((TwoListStack.push 2 (TwoListStack.push (1 : Nat) TwoListStack.empty)).pop).map Prod.fst = some 1
#guard (TwoListStack.pop (TwoListStack.empty : TwoListStack Nat)).isNone

[E11.9] · specification writing · tier 1 (+ tier-3 reading) · core

State the representation-independence theorem for Stack: for any two LawfulStack instances S1 and S2, any program built only from push, pop, size, and empty produces the same observable results in both. Write it as precisely as you can in Lean — you must first decide what “program” and “observable result” are, as types, before the statement can be written at all; that decision is the exercise. Do not prove it. Then, using E11.8’s TwoListStack alongside the List instance of §11.4, confirm the claim on one concrete program by checking that both representations yield the same observation.

Say in two sentences which of the LawfulStack laws your statement actually depends on. This is the exercise the unit points at: a client may rely on the laws, never on the representation.

end W11

-- FPCourse/T05_AbstractTypesAndTypeClasses/W12_TypeClassesDecidable.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

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 W12

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:
theorem toProofOrRefutation (p : Prop) [d : Decidable p] : p ∨ ¬p :=
  match d with
  | Decidable.isTrue h  => Or.inl h
  | Decidable.isFalse h => Or.inr h

Checkpoint — decide evaluates the Decidable instance. decide p reduces the Decidable p value and reports the constructor it lands on: isTrue shows as true, isFalse as false. Predict both Booleans below, and say which constructor each instance evaluates to, before reading the result.

#eval decide (1 < 2)   -- predict first (which constructor?)
#eval decide (2 < 1)   -- predict first (which constructor?)

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"

Checkpoint — eqTest reads the DecidableEq decision. eqTest matches on decEq a b, branching on whether the decision is isTrue or isFalse. Predict both strings below — and which constructor each decEq call produces — then check.

#eval eqTest (3 : Nat) 3    -- predict first ("equal" / "not equal"?)
#eval eqTest (3 : Nat) 4    -- predict first ("equal" / "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

Checkpoint — MyFunctor.fmap. The List instance sets fmap := List.map, the Option instance fmap := Option.map; the same overloaded fmap dispatches on the container. Predict both results below, then check.

#eval MyFunctor.fmap (· + 1) [1, 2, 3]            -- predict (List instance)
#eval MyFunctor.fmap (· + 1) (some (5 : Nat))     -- predict (Option instance)

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

Checkpoint — MyFoldable.fold on List. The List instance is List.foldr, so fold (· + ·) 0 sums the elements. Predict the total below, then check.

#eval MyFoldable.fold (· + ·) 0 [1, 2, 3, 4]   -- predict first

Checkpoint — list_fold_spec. Folding with the list constructors themselves, fold (· :: ·) [], rebuilds the input (that is exactly list_fold_spec). Predict the result below from the spec — not by simulating the fold — then check.

#eval MyFoldable.fold (· :: ·) ([] : List Nat) [1, 2, 3]   -- predict from list_fold_spec

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

Checkpoint — MyMonoid Nat (addition). This instance reads one := 0, mul := (· + ·). Predict the two values below — the product and the identity — then check.

#eval MyMonoid.mul (3 : Nat) 4     -- predict first (mul is +)
#eval (MyMonoid.one : Nat)         -- predict first (the identity)

Checkpoint — MyMonoid (List α) (append). Here one := [], mul := (· ++ ·). Predict the concatenation and the identity below — the same class methods, a different instance — then check.

#eval MyMonoid.mul [1, 2] ([3, 4] : List Nat)   -- predict first (mul is ++)
#eval (MyMonoid.one : List Nat)                 -- predict first (the identity)

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.

Checkpoint — bounded vs. unbounded ∀. A ∀ n ∈ xs over a literal list is decidable (finitely many checks); the unbounded ∀ n : Nat on the last table row is not. Predict the Boolean below, then say why replacing the list with “all of Nat” would put it past the boundary.

#eval decide (∀ n ∈ ([0, 1, 2, 3] : List Nat), n + 0 = n)   -- predict first

Exercises

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

[E12.1] · specification writing · tier 1 (+ tier-3 reading) · core · target MonoidIdSpec

The MyMonoid Nat instance (§12.5) claims 0 is a two-sided identity for +. State the two identity laws as Props — MulOneSpec : Prop := ∀ a : Nat, MyMonoid.mul a MyMonoid.one = a and its mirror OneMulSpec. Do not prove the general ∀; that proof is Nat.add_zero / Nat.zero_add, wired into the instance in §12.5 for you to read (tier 3). Confirm the spec on instances — including the identity element itself and a different monoid (List, where one = []):

#guard MyMonoid.mul (5 : Nat) MyMonoid.one = 5
#guard MyMonoid.mul MyMonoid.one (5 : Nat) = 5
#guard MyMonoid.mul (0 : Nat) MyMonoid.one = 0
#guard (MyMonoid.mul ([1, 2] : List Nat) MyMonoid.one) = [1, 2]

In one line: which tier does the general ∀ law live in, and which the four checks?

[E12.2] · decidability identification · tier 1 · core

For each proposition, deliver a judgment before touching decide: does a Decidable instance exist at all, and if so can decide be the grader? The judgment — not the tool-use — is the point (§12.6).

(a) (5 : Nat) = 5 (b) ([1,2,3] : List Nat) = [1,2,3] (c) (1.0 : Float) = 1.0 (d) ∀ n : Nat, n < n + 1 (e) (id : Nat → Nat) = (fun n => n)

#guard decide (((5 : Nat) = 5)) = true
#guard decide (([1, 2, 3] : List Nat) = [1, 2, 3]) = true
-- (c), (d), (e) have no check on purpose.  For each, state whether a Decidable
-- instance exists at all, and — when it does not (Float, functions) — name the
-- semantic reason from §12.6; for (d) say why an unbounded ∀ escapes decide even
-- though every instance of the body is provable.

[E12.3] · counterexample finding · tier 1 · core

A student claims “every MyMonoid is commutative: mul a b = mul b a.” It is wrong — commutativity is not one of the three monoid laws (mul_one, one_mul, mul_assoc). Find a witness in the List monoid (mul = ++) and encode it two ways, so each check succeeds on a correct counterexample:

#guard (MyMonoid.mul ([1, 2] : List Nat) [3]) ≠ MyMonoid.mul ([3] : List Nat) [1, 2]
#guard decide (¬ (MyMonoid.mul ([0, 1] : List Nat) [1] = MyMonoid.mul ([1] : List Nat) [0, 1]))

In one line: which of the three laws, if any, does your witness still satisfy?

[E12.4] · type-directed derivation · tier 2 · core · target fork

Derive fork : (α → β) → (α → γ) → α → β × γ applying both functions to the same input (fork f g a = (f a, g a)). The derivation trace (Week 2 §2.6) is the graded artifact — then the def. First-step hint: the type is three nested arrows, so start with →I three times (introduce f, g, a); the goal β × γ is a product, so close with ×I, pairing one application under each component. Effort: ~4 trace steps, 2 lines of code.

#guard fork (· + 1) (· * 2) 5 = (6, 10)
#guard (fork (fun n => n) (fun n => n + 100) 0 : Nat × Nat) = (0, 100)
#guard (fork List.length List.reverse [7, 8, 9] : Nat × List Nat) = (3, [9, 8, 7])

[E12.5] · specification reading · tier 3 (reading) · stretch

Read the provided toProofOrRefutation (§12.1): it turns any [Decidable p] into a proof of p ∨ ¬p. Without authoring a proof, explain in one or two lines what each match branch returns and why p ∨ ¬p is exactly the information a Decidable p value already carries. Then read list_fold_spec (§12.4): which library lemma discharges it, and what proposition (in words) does it assert about folding with the list constructors?

[E12.6] · decidability identification · tier 1 · stretch · target Suit

Part A (build + decide). Define inductive Suit where | hearts | diamonds | clubs | spades deriving DecidableEq, Repr. Use decide to settle a disequality and a bounded ∀:

#guard decide (Suit.hearts ≠ Suit.spades) = true
#guard decide (∀ s ∈ [Suit.hearts, Suit.diamonds, Suit.clubs, Suit.spades],
                 s = Suit.hearts ∨ s ≠ Suit.hearts) = true

Part B (judgment). Consider ∀ n : Nat, n + 0 = n. Every instance of the body is trivially true — n + 0 reduces definitionally to n, so n + 0 = n is rfl. Predict: does inferInstance : Decidable (∀ n : Nat, n + 0 = n) succeed? It does not — and that is the lesson. In one or two lines, explain the gap: Lean ships no Decidable instance for an unbounded ∀ over Nat, even when each body is decidable and even trivially provable, because deciding it would require checking infinitely many n (§12.6). What does settle the proposition — a proof such as fun n => rfl (or Nat.add_zero), not a decision procedure? Why is “every case is provable” strictly weaker than “the whole ∀ is decidable”? Contrast with the false ∀ n : Nat, n = n + 1.

[E12.7] · type-directed derivation + decidability identification · tier 1 · stretch · target mapDecide

Write

def mapDecide [DecidableEq α] (xs ys : List α) : List (α ⊕ α) := ...

tagging each element of xs with Sum.inl when it also occurs in ys, and with Sum.inr when it does not. Say first why the [DecidableEq α] constraint is exactly what makes this definable — which step of the computation consumes it, and what could you not write without it?

#guard mapDecide [1, 2, 3] [2, 3, 4] = [Sum.inr 1, Sum.inl 2, Sum.inl 3]
#guard mapDecide ([] : List Nat) [1] = []
#guard mapDecide [5] ([] : List Nat) = [Sum.inr 5]

First-step hint: the shape is a map over xs; the decision inside is x ∈ ys, decidable exactly because of the instance. Effort: 2 lines of code.

end W12

-- FPCourse/T06_StreamsAndCurryHoward/W14_CurryHoward.lean
import Mathlib.Data.List.Basic
import Mathlib.Logic.Basic

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 W14

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

Checkpoint — → is implication. Under Curry-Howard the function arrow and the implication arrow are one symbol. An implication between decidable propositions is itself decidable. Predict the Boolean — is (1 = 1) → (2 = 2) true? — then check.

#eval decide ((1 = 1) → (2 = 2))   -- predict first

-- Conjunction / Product:
example : 1 < 2 ∧ 2 < 3 :=
  And.intro (by decide) (by decide)  -- And.intro IS Prod.mk for Props

Checkpoint — ∧ is a product. A proof of P ∧ Q is a pair of proofs, so it holds only when both conjuncts do. Predict the Boolean, then check.

#eval decide (1 < 2 ∧ 2 < 3)   -- predict first

-- Disjunction / Sum:
example : 1 = 1 ∨ 1 = 2 := Or.inl rfl  -- Or.inl IS Sum.inl for Props

Checkpoint — ∨ is a sum. A proof of P ∨ Q is a tagged proof — inl or inr — so it holds when at least one disjunct does. Here the left side carries it. Predict the Boolean, then check.

#eval decide (1 = 1 ∨ 1 = 2)   -- predict first

Checkpoint — ¬P is P → False. Negation is the function type into the empty type: ¬P holds exactly when P is false (so the function is vacuous). Predict the Boolean for ¬ (1 = 2), then check.

#eval decide (¬ (1 = 2))   -- predict first

-- ∀ / Π type:
example : ∀ n : Nat, n + 0 = n := Nat.add_zero  -- a dependent function

Checkpoint — ∀ is a dependent function. A proof of ∀ n, P n is a function sending each n to a proof of P n. Over a finite list the claim is decidable. Predict the Boolean below, then check.

#eval decide (∀ n ∈ ([0, 1, 2, 3] : List Nat), n + 0 = n)   -- predict first

-- ∃ / Σ type:
example : ∃ n : Nat, n > 100 := ⟨101, by decide⟩  -- a dependent pair

Checkpoint — ∃ is a dependent pair. A proof of ∃ n, P n is a pair ⟨w, proof⟩: a witness and a proof it works. Over a finite list the search is decidable. Predict the Boolean — is there an element > 100 in [50, 101]? — then check.

#eval decide (∃ n ∈ ([50, 101] : List Nat), n > 100)   -- predict first

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

Checkpoint — a proof IS a term. addOne = fun n => n + 1 and oneImpliesOne = fun h => h are built the same way; only the types differ. addOne is data, so it evaluates. Predict addOne 41, then check.

#eval addOne 41   -- predict first

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

Checkpoint — And.intro IS Prod.mk. makePair a b builds a × pair exactly as makeConjunction builds an ∧ proof — same constructor, one on data, one on Prop. Predict makePair 3 "hi", then check.

#eval makePair 3 "hi"   -- predict first

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

Checkpoint — ctxLookup. ctxLookup walks the context returning the first binding whose name matches, or none. Predict the result of looking up "y" below, then check.

#eval ctxLookup [("x", Ty.Nat), ("y", Ty.Bool)] "y"   -- predict first

Checkpoint — DecidableEq Ty. Ty derives DecidableEq, so the type-checker can compare types (it does exactly this in the app rule, τ₁ = τ₁'). Predict the Boolean — is Nat the same type as Bool → Nat? — then check.

#eval decide (Ty.Nat = Ty.Arr Ty.Bool Ty.Nat)   -- predict first

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 τ)
  | _, .natLit _  =>
    some ⟨.Nat, Typed.natLit⟩
  | _, .boolLit _ =>
    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

Checkpoint — the checker types a literal. (typecheck ctx e).map (·.1) reads off the type the checker assigns (discarding the proof). A natLit always types as Nat. Predict the Option Ty below, then check.

#eval (typecheck [] (Term.natLit 5)).map (·.1)   -- predict first

Checkpoint — the checker types the identity λ. λx:Nat. x should type as Nat → Nat — the lam rule wraps the body’s type in an Arr. Predict the Option Ty below, then check.

#eval (typecheck [] (Term.lam "x" Ty.Nat (Term.var "x"))).map (·.1)   -- predict first

Checkpoint — the checker rejects an ill-typed term. Applying 1 to 2 (app of a natLit to a natLit) has no typing: the function position is not an Arr, so the app rule fails and the result is none. Predict the Option Ty below, then check.

#eval (typecheck [] (Term.app (Term.natLit 1) (Term.natLit 2))).map (·.1)   -- predict first

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: whenever `typecheck ctx e` returns `some p`, the term genuinely has the
-- type `p.1` that the checker reports — witnessed by `p.2`.  There is nothing to
-- construct: the proof IS the value the checker already produced, so soundness holds by
-- `p.2` alone.  (The converse — *completeness*, that every well-typed term is accepted —
-- is a separate property the return type does NOT give for free; it is Exercise E14.6.)
theorem typecheck_sound (ctx : Context) (e : Term)
    (p : Σ' τ, Typed ctx e τ) (_h : typecheck ctx e = some p) :
    Typed ctx e p.1 :=
  p.2

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

Each exercise carries a banner — [id] · competency · tier · level · target — and, where it asks you to build something, an acceptance check: paste it beneath your definition in your own file and it must succeed. #guard is silent on success and errors on failure, so the compiler is your grader. See EXERCISE_CONVENTIONS.md for the schema. Do every core exercise; stretch exercises go deeper and are optional.

This is the Curry-Howard capstone, so the emphasis is on type-directed derivation (building a term from its type — proofs as programs) and its inverse, type reading (reading a type to learn what every inhabitant must do). For the derivation exercises the graded artifact is the derivation trace in the Week 2 §2.6 format — not merely a term that compiles. RULE at each step is one of →I, →E, ×I, ×E, ⊕I, ⊕E, or “use h”. Recall from §14.1 that ∧ behaves like × and ∨ like ⊕, so the same moves derive proofs and programs — that identity is the whole point of the week.

[E14.1] · type-directed derivation · tier 2 · core · target modusPonens

Derive modusPonens : A → (A → B) → B (with A B : Type) — a value, and a proof, and a function application, all at once: under Curry-Howard this term is the inference rule “from A and A → B, conclude B.” Give the derivation trace (§2.6 format) then the term; name the rule closing each goal. Effort: 3 trace steps, ~1 line.

#guard modusPonens 3 (fun n => n + 1) = 4
#guard modusPonens "hi" String.length = 2
#guard modusPonens true (fun b => !b) = false

First-step hint: the goal is an arrow into an arrow, so the first two moves are forced (→I on a : A, then →I on f : A → B); the last goal B is closed by one →E (f a). Which hypothesis does the final application use, and which supplies its argument?

[E14.2] · type-directed derivation · tier 2 · stretch · target distribute

Derive distribute : A × (B ⊕ C) → (A × B) ⊕ (A × C) (with A B C : Type) — the distributivity of ∧ over ∨, read as a program. Give the derivation trace then the term. Effort: ~5 trace steps.

#guard distribute ((5, Sum.inl 1) : Nat × (Nat ⊕ Nat)) = Sum.inl (5, 1)
#guard distribute ((5, Sum.inr 2) : Nat × (Nat ⊕ Nat)) = Sum.inr (5, 2)

First-step hint: after →I on the pair p and ×E to name p.1 : A and p.2 : B ⊕ C, the output side is not yet determined — you must ⊕E (match) on p.2 before you can choose ⊕I .inl/.inr, because which side of the result you build depends on which side the input was. State, at each step, the remaining goal.

[E14.3] · type reading (free theorems) · tier 2 · core

The inverse of derivation: read a type to learn what every inhabitant must do (§7.2, and §2.6’s “inverse direction”). No code to submit.

(a) ∀ A B : Type, A × B → A — reading only the type, what must every inhabitant do, and how many inhabitants are there? (This is Prod.fst; under Curry-Howard it is the proof of P ∧ Q → P, i.e. And.left.)

(b) ∀ A B : Type, A → A ⊕ B — how many inhabitants, and why can no inhabitant produce a B? Name the Curry-Howard reading of this type as a logical implication.

(c) Contrast: does the type ∀ A : Type, A ⊕ B → A have any inhabitant when B is a type the code cannot inspect? Say why the .inr case blocks it — this is where a type fails to be inhabited, i.e. the proposition is not provable.

[E14.4] · counterexample finding · tier 1 · core

A student claims “every Term is well-typed — typecheck assigns a type to all of them.” It is wrong: an ill-typed application and an unbound variable both have no typing. Find witnesses and encode them so the checks succeed (recall (typecheck ctx e).map (·.1) : Option Ty reads off the assigned type, or none):

#guard (typecheck [] (Term.app (Term.natLit 1) (Term.natLit 2))).map (·.1) ≠ some Ty.Nat
#guard (typecheck [] (Term.var "x")).map (·.1) = none
#guard (typecheck [] (Term.app (Term.boolLit true) (Term.natLit 2))).map (·.1) = none

What is the correct characterization of when typecheck ctx e returns some _? (It is exactly when Typed ctx e τ is inhabited for some τ — read the app and var clauses of §14.5.)

[E14.5] · decidability identification · tier 1 · core

For each Curry-Howard proposition, say whether decide can close it and why (finite domain? decidable predicate? a Decidable/DecidableEq instance in scope?) before checking — the judgment is the point, not the tool-use:

(a) (Ty.Nat = Ty.Nat) ∧ (Ty.Bool ≠ Ty.Nat) (b) ∃ n ∈ ([1, 2, 3] : List Nat), n > 2 (c) ∀ n : Nat, n + 0 = n (d) Typed [] (Term.natLit 1) Ty.Nat

#guard decide ((Ty.Nat = Ty.Nat) ∧ (Ty.Bool ≠ Ty.Nat)) = true
#guard decide (∃ n ∈ ([1, 2, 3] : List Nat), n > 2) = true
-- (c) and (d) have no check on purpose: say why decide cannot close each.  For (d),
--     note that Typed is an inductive Prop with no Decidable instance — even though
--     `typecheck` effectively decides it, `decide` needs the instance, which is absent.

[E14.6] · specification writing · specification reading · tier 2 (+ tier-3 reading) · stretch · target Complete

Two parts, one about the checker’s specification.

(a) Spec writing. State typecheck’s completeness as a Prop — the converse of the soundness the return type gives for free: “whenever Typed ctx e τ holds, typecheck ctx e returns a some whose type is τ.” Write it as a single def Complete : Prop := ∀ ….

(b) Spec reading (tier 3). Read the provided proof typecheck_sound (§14.6) — do not author a proof. Explain, in one sentence each: why is soundness discharged by p.2 alone (what does the return type Option (Σ' τ, Typed ctx e τ) already guarantee)? And why can that same return type not discharge your completeness Prop from part (a) — what would a proof of completeness have to do that soundness never does?

end W14

Lean 4 beyond research

A snapshot, taken at the start of the Fall 2026 semester, of organizations using Lean 4 outside of research: what each one is doing with it, and the scale of the organization doing it. Every figure and claim is cited on the snapshot page, whose numbers link through to all thirty sources.

Market capitalizations retrieved 2 September 2026, in USD; private valuations are the most recent round, and some were still open at that date. Each claim above is cited on the snapshot page, whose figures link through to all thirty sources.

Accessibility

This document states the accessibility standard that the online materials in this repository are subject to, the conformance status of those materials, and the automated measures that keep that status from silently regressing.

It is written to be accurate rather than reassuring. Where this material does not yet conform, that is said plainly, with the specific criterion and the remediation path.

Last reviewed: 2 September 2026 · Contact: Kevin Sullivan, sullivan@virginia.edu

1. Scope

Everything published from this repository to https://kevinsullivan.github.io/Lean4CS1, which is the course book, the course page and schedule, and the standalone pages built from src/. It does not cover third-party sites linked from those pages, nor the PDFs of assigned readings, which are the publishers’ material and are not redistributed here.

2. Applicable standard

The University of Virginia is a public entity under Title II of the Americans with Disabilities Act, so course material published on the open web is governed by the Department of Justice rule on web and mobile accessibility, published 24 April 2024:

28 CFR § 35.200 — Requirements for web and mobile accessibility. “A public entity shall ensure that the following are readily accessible to and usable by individuals with disabilities: (1) Web content that a public entity provides or makes available, directly or through contractual, licensing, or other arrangements …”

The technical standard the rule adopts is WCAG 2.1, Level A and Level AA.

The compliance date that applies here is 26 April 2027. A state university takes the population of its state, not its enrolment, so UVA falls in the “50,000 or more” tier. That date is one year later than originally set: DOJ extended it by interim final rule in April 2026. Entities under 50,000 and special district governments have until 26 April 2028.

Two related obligations point at the same technical target and are satisfied by meeting it:

• Section 508 of the Rehabilitation Act, whose Revised Standards (36 CFR Part 1194, App. A, § 702.10.1, effective 18 January 2018) incorporate WCAG 2.0 Level A and AA by reference. WCAG 2.1 is a superset, so conforming to 2.1 AA conforms to 2.0 AA.
• Section 504 of the same Act, as a condition of federal financial assistance.

The rule excepts compliance that would cause a fundamental alteration of the service or an undue financial and administrative burden. No such exception is claimed for this material.

3. Conformance status

Partially conformant with WCAG 2.1 Level AA, with the exceptions in §5.

Claiming full conformance today would be false. The pages authored in this repository conform and are verified on every deploy. Pages generated by mdBook, the static site generator that builds the book, carry defects originating in its own theme, listed in §5 with their upstream tracking issues.

4. Automated measures

The assurance is a build gate, not a periodic audit, so a regression cannot reach the published site between reviews.

What runs. scripts/a11y_check.py serves the built book, drives it in headless Chromium, and runs axe-core against the rule tags wcag2a, wcag2aa, wcag21a, wcag21aa and section508.

Where it runs.

• Locally, as make a11y. The target depends on build, so it can never audit a stale book/.
• In continuous integration, as the Check accessibility step of .github/workflows/mdbook.yml, positioned between the build and the upload. A violation on a gated page fails the job, and nothing is published. The site cannot regress into non-conformance without the deploy stopping.

What it gates versus reports. A violation on a page authored here fails the build. Violations on mdBook’s generated pages are printed but do not fail it, because they originate upstream and cannot be corrected from this repository; gating on them would stop every deploy for a defect we cannot fix. They remain visible in each build log and are tracked in §5.

Verified in both directions. The gate is exercised for false negatives as well as false positives: removing the lang attribute from a page causes the build to fail, and restoring it causes it to pass. A check that cannot fail provides no assurance.

Checks performed by hand, because automated tools cannot evaluate them, and repeated when layout or type changes:

• 1.4.10 Reflow — no horizontal scrolling at 320 CSS pixels.
• 1.4.12 Text Spacing — no clipping or overlap when line height, letter spacing, word spacing and paragraph spacing are overridden to the criterion’s values.
• 1.4.4 Resize Text — no loss of content at 200%.
• 2.4.1 / 2.4.7 — the skip link is the first tab stop and becomes visible on focus; focus indicators are visible throughout.
• 1.4.3 Contrast — computed ratios for every foreground/background token pair in both light and dark themes, against the 4.5:1 threshold for body text.

The limits of this. Automated testing detects a minority of accessibility barriers — commonly estimated at a third to a half. A clean axe run is evidence of the absence of machine-detectable defects, not of usability for disabled readers. Testing with actual assistive technology, and by disabled users, is not currently part of this process and would strengthen it materially.

5. Known non-conformances

All three arise in mdBook’s generated output rather than in content authored here. Each is reported upstream; none is fixable from this repository without overriding mdBook’s templates.

Remediated, not merely absent. mdBook renders Markdown task lists (- [ ]) as <input disabled type="checkbox"> with no accessible name, failing 4.1.2 Name, Role, Value (A). The setup checklist used that syntax and carried eight instances. It is now written as a plain bulleted list, which reads the same and removes the defect from this site entirely. The underlying mdBook bug is reported upstream as #3212 and would return if task-list syntax were reintroduced, so it is recorded here rather than forgotten. The build now rejects that syntax, so the claim in this paragraph cannot quietly become false.

PR #3078 is mergeable and awaiting review; PR #2144 currently conflicts. Neither has merged, so remediation here does not depend on upstream: mdBook supports replacing theme/index.hbs, which would let the first two be fixed locally ahead of the April 2027 date. That carries its own maintenance cost, since an overridden template pins this repository to a snapshot of mdBook’s markup and can regress on upgrade.

6. Reporting a problem

If any part of this material is inaccessible to you, email sullivan@virginia.edu with the page address and what went wrong. Reports are acted on, and a barrier that blocks access to course content is treated as urgent regardless of whether it appears above.

7. Review

This statement is reviewed whenever the accessibility gate changes, when mdBook is upgraded, and at the start of each semester. The upstream issues in §5 are re-checked at each review.

In-Class Plan

The plan for today is to continue to learn about and practice with inductive type definitions. For today, pair up with a study buddy: someone to work and chat with today.

Computational types and Logical types

• Empty and False
• Unit and True
• Polymorphic types
• Sum (⊕) and Or (∨)
• Prod (×) and And (∧)
• _ → Empty and Not (¬)

Parametric Polymorphism

Suppose you’ve defined some type, α, and now you wish to define the identity function on values of this type. Here’s what that looks like with α = Nat, α = Bool, and α = List Nat. It even works for the Empty type.

def id_Empty    : Empty     → Empty     := fun n => n
def id_Bool     : Bool      → Bool      := fun n => n
def id_Nat      : Nat       → Nat       := fun n => n
def id_ListNat  : List Nat  → List Nat  := fun n => n

It should be obvious that every implementation is exactly the same except for the single type of value it consumes and returns.

Factor into Fixed Template with Variable Parameters

In such cases we can factor these programs into a single parameterized definition, with a fixed template capturing the commonalities, and parameters that can be set to any value to express the variability. This is that looks like.

#check Nat.add
#check Nat.add 3

def myAdd := Nat.add
#check myAdd
#eval myAdd 3 4

def add3 := Nat.add 3
#check add3
#eval add3 7

def sum := Nat.add 3 4
#check sum

def f' : Nat → Nat → Nat → Nat := fun a b c => 0

#check (((f' 0) 1) 2)
-- #check (f' 0 (1 2))

def id' (α : Sort u) : α → α               := fun n => n

#eval id' Nat 3
#eval id' Bool true
#eval id' (List Nat) [1,2,3]

Type (Actually Value) Inference

In each of these examples the second actual parameter is a value of the type, α, given by the first parameter. The type checker enforces this rule. Try it. This is an example of what we’ve called dependent typing. The value of α (a type), determines the type of the second argument.

Q: what does that say, in principle, about the need to give the first argument explicitly?

#eval id' _ 3
#eval id' _ true
#eval id' _ [1,2,3]

Implciit Arguments for Better Readability

Lean syntax allows for even further cleanup in the form of what Lean calls implicit arguments. Curly braces around a parameter declaration tells Lean to infer it, allowing the user not to write anything at all.

def id'' {α : Sort u} : α → α := fun n => n

#eval id'' 3
#eval id'' true
#eval id'' [1,2,3]

Disabling Implicit Arguments When Necessary

You may not provide an implicit parameter explicitly. If Lean can’t infer an implicit argument and you must give it explicitly you can turn off inference locally using @.

-- will not work
-- #eval id'' Nat 3

#eval @id'' Nat 3

Lean’s standard library includes the polymorphic identity function for you. It’s called id. Let’s look at its type and a few applications.

#check id''     -- C-style and explicit args
#check (id'')   -- → notation and meta-variables
#check @id''    -- C-style and explicit args
#check (@id'')  -- → notation, explicit args (my fav)

Parametricity

Parametric polymorphism depends on the implentation not relying on any knowledge at all of its actual argument type. Polymorphic functions must handle their arguments as entirely opaque. You cannot match on a value of a polynmorphic type argument. Interestingly polymorphic functions sometimes have a single unique implementation, one that’s literally forced. How else can you complete this function definition except with a? There is no other choice!

def id''' {α : Sort u} (a : α) : α := a

(Note the alternative function definition syntax used in this case. Rather than α → α and fun a => a, we’ve moved the first α argument to the left of the colon and gave it a name, making its scope global; then we return just a rather than fun a => a.

Binding Names to Arguments

Moving an argument to the left of the , which should look to you like ordinary, say, Python, syntax, means that a name must be bound to it right there, (unless it’s unused in the body, where _ works). Our earlier examples bound names during pattern matching. You then cannot pattern match using | function notation on a value for which a name is already bound. Use match instead.

-- This is fine
def yep : Bool → Bool
| true => true
| false => false

-- def nope (b : Bool) : Bool
-- | true => true
-- | false => false

def yep' (b : Bool) : Bool :=
match b with
| true => true
| false => false

Abstract Data/Proof Types

In practice, a mere inductive definition does not get you to a comprehensiv library in support of programming with values of that type. A complete abstract data type package will also include:

• elimination functions (e.g., Bool.elim below)
• domain-specific notations (× for Prod, ⊕ for Sum)
• domain-soecific functions (e.g., List.length for Lists)
• already proven theorems (e.g., ∀ a b, len (a ++ b) = len a + len b )
• proof automations (e.g., decision (proof- building) procedures)

Example: Bool

namespace hide

Here’s the standard definition of Bool.

inductive MyBool where
| true
| false

Suppose we want to define a function from Bool to some other type, β, where the return value of type β To define any function whose behavior depends on the actual value of the argument requires case analysis

-- elimination function: provide result for each case
def myBoolElim
  {α : Sort u}
  (b : MyBool)
  (f : MyBool → α)
  (t: MyBool → α) :=
match b with
| MyBool.true => t b
| MyBool.false => f b

-- Elimination function: case analysis, computation per case
#eval myBoolElim
  MyBool.true
  (fun b => "It's false!")    -- false branch (warns b unused)
  (fun _ => "It's true!")     -- true case: _ silences warning

-- The Boolean *and* function
def myAnd : MyBool → MyBool → MyBool
| MyBool.true, MyBool.true => MyBool.true   -- matching on two args
| _, _ => MyBool.false                  -- wildcard any other combo

-- The Boolean *or* function
def myOr : MyBool → MyBool → MyBool
| MyBool.false, MyBool.false => MyBool.false
| _, _ => MyBool.true

-- The MyBoolean *not* function
def myNot : MyBool → MyBool
| MyBool.true => MyBool.false
| MyBool.false => MyBool.true

-- Notations. Two infix operators and one prefix
-- Each with an associated precedence level
-- Each reducing to a function we just defined
infixl:35 " && " => myAnd
infixl:30 " || " => myOr
notation:max "!" b:40 => myNot b

-- Examples with and without notation
def b1 : MyBool := MyBool.true
def b2 : MyBool := MyBool.false
#eval b1 && b2
#eval myAnd b1 b2
#eval b1 || b2
#eval myOr b1 b2
#eval !b1
#eval myNot b1

-- How about a theorem? Same as def but used for logic (vs computation)
theorem trueIsIdentityForAnd : ∀ (b : MyBool), (b && MyBool.true) = b
| MyBool.true => rfl
| MyBool.false => rfl
end hide

#check Bool