Proofs in Lean

Now we'll translate all the concepts we've seen so far—goals, contexts, proof rules—into Lean.

When you open a Lean file, you'll see two main areas in your window: a panel on the left containing your Lean code and a panel on the right (called the Infoview) containing your current proof state. Initially, the right-hand panel will be empty. However, if you move your cursor to within a proof block (the area between by and done in a theorem declaration), you'll see the Infoview update to display your current proof state:

Each proof rule is represented by a tactic in Lean: a command you can write inside your proof block that applies the corresponding rule to your proof state. Proofs in English are a sequence of sentences that we can think of as implicitly applying proof rules to an implicit proof state; proofs in Lean are a sequence of tactics that apply proof rules to an explicit proof state shown in the Infoview.

For instance, in the example above, the first rule I'll want to apply is implication introduction, which is accomplished by the tactic assume. Some tactics, like assume, add an entry to your context; since Lean requires that everything in your context have a name, such tactics take an argument specifying what you'd like the new entry to be called. In this example, I'll choose hpq to represent the hypothesis p ∧ q:

After I enter this tactic, my proof state immediately updates to reflect the result of applying the corresponding proof rule. I continue entering tactics, one on each line, to apply appropriate proof rules and work toward discharging my goal. After I apply conjunction elimination via eliminate and conjunction introduction with split_goal, I find myself with two goals (given by conjunction introduction). Notice that Lean automatically shows the context for each above the corresponding goal:

However, our proof rules only allow us to "work on" one goal at a time. It's good practice, therefore, to use the { } notation—demonstrated below—to "focus" the topmost goal. As shown below, this causes Lean to only display the goal you're actively working on:

Once I finish working on a goal, my tactic state updates to show "No goals":

Notice that this doesn't mean I don't have any goal remaining for my overall proof—it just means I've finished working on the current goal. (The wording is a little misleading.) A good way to tell that the overall proof still has some remaining goals is that there's still a red error message displaying on the done line—this will go away once the entire proof is complete.

Once I've completed the entire proof, the Infoview updates to show "No goals" even on the done line, and the error message on that line disappears: