Meet Lean

Most of this course, you say what must be true. Dafny or TLC goes looking for the reason.

Sometimes they stop. The thing you said is still waiting. That waiting thing is an obligation. Nobody has shown why it is true yet.

A proof is the steps you write, and Lean saying yes to them. Those steps are a checked argument. Checked means Lean looked. Argument means the steps.

This part of the course comes last on purpose. It is the odd case, when the other tools get stuck. It is not the skill the course is teaching.

Lean is the tool for that leftover step.

If Lean is not done, it shows you the claim it still needs. That claim is the goal. The goal is the obligation, sitting in front of you.

A goal still sitting there means "not finished." It does not mean Lean found a broken example, like balance = -1. There is usually no list of bad inputs.

sorry is a blank. Lean lets the file through and leaves the goal sitting there. A blank is not a proof.

The small part of Lean that checks each step is called the kernel. You will see that word in the results.

The file on the right is one claim and its proof. Here it is one line at a time.

theorem add_zero (n : Nat) : n + 0 = n := by is the claim. theorem means “here is a claim”. add_zero is its name. (n : Nat) means “for any counting number n”. n + 0 = n is what Lean has to be convinced of. := by means “the steps start here”.

Before any step, that claim is the goal Lean is waiting on.

rfl is the one step. Lean's definition of + says n + 0 is n. While Lean checks rfl, it looks that up and swaps n in for n + 0. The claim becomes n = n, which is true because both sides are the same. You do not write that swap. After rfl, nothing is left waiting.

Hit Verify. If every step is accepted and no goal is left waiting, you get a green result.

If the steps do not finish the claim, Lean reports an unsolved goal and shows the claim it is still waiting on. That is not a broken example. It means nobody has shown why the claim is true yet.

If you write sorry in place of the steps, Lean lets the file through but leaves the goal waiting. This course rejects it, because a blank is not a proof.

A theorem is two parts. First the claim. Then the steps.

You will meet three steps. rfl finishes a goal that is true just because of how something is defined. rw uses a fact you already have, “this equals that”, and swaps one side for the other. induction splits a counting number into zero, and “one more than a smaller number.”

Each one gets its own mission with a small example. sorry is a blank. It is not allowed here.

The theorem on the right is already done. Hit Verify (or ⌘↩ / Ctrl+Enter). The green check is the whole exercise. You are not solving a word puzzle.

Then start the first mission. There, you will fill in a sorry yourself.