3. Follow an inspection

You can now explain the quantifier example and distinguish its proposition from its proof. This lesson applies those distinctions to Definograph's reader. Your goal is to keep track of the expression you are reading, the route used to reach it, and the checks that apply at that point.

Follow the mathematical order

Use the first statement again:

example : Prop := ∀ x : Nat, ∃ y : Nat, y = x

A reading of its logical structure has five conceptual stages:

1. Read the outer universal quantifier.
2. Enter its body, where x : Nat is available.
3. Read the existential quantifier inside that body.
4. Enter its condition with a candidate y : Nat also available.
5. Read y = x in that scope.

These stages describe the mathematics, not a fixed number of interface clicks or recorded checks. A single inspection can produce several outcomes. The important invariant is the order and scope of the binders.

Here is a schematic trace you can read without the editor. A, B, and C label the worksheet's expressions; they are not interface step numbers or a captured session.

At B, x comes from entering A's binder. At C, y is a candidate introduced to read B's condition. Each expression forms a proposition in its context. Checking that fact supplies no proof of the proposition; in particular, reaching C has not supplied a proof that its candidate satisfies the equality.

The entered variables are only the part of context tracked by this mathematical example. An actual captured context can also contain surrounding declarations and auxiliary entries; keep those as well.

Distinguish two ways of moving

The guided reading presents the mathematical structure in a sequence, with a logical overview. Its Previous, Next, and step selector change the part being emphasized. The full static statement remains available below it.

The editor's Source data view serves a different purpose: it lets you inspect the original expression and the records behind subsequent operations. Choosing a retained step or changing a display does not rerun Lean. An explicit inspection action requests a fresh capture.

This difference matters when asking whether a later display is new evidence. Moving your reading focus can reveal evidence that was already recorded. It does not generate another check.

From Lean source to a reader view

For each x, there is a y

example : Prop := ∀ x : Nat, ∃ y : Nat, y = x

Download QuantifierForallExists.lean

For each x, y is introduced inside x’s scope. The choice of y may depend on x.

One y for every x

example : Prop := ∃ y : Nat, ∀ x : Nat, y = x

Download QuantifierExistsForall.lean

Here y is introduced before x. The same y is required to work for every x.

Optional local activity: inspect the quantifiers

This activity assumes the matching local editor setup described in the reference. The steps below document the accepted controls; this page does not include a fresh capture of your session.

1. Open QuantifierForallExists.lean in a trusted Lean workspace. Select the complete proposition after :=, then run Definograph: Visualize Selection.
2. Open Source data, then Checker input. Select the outer constructor representing the whole prepared term and choose Check chosen occurrence. Read the returned term, context, inferred type, and recorded outcomes.
3. Choose Read logical structure of original selected term (one layer). Read the outer logical layer together with its formation evidence.
4. In the returned structure, choose the body and use Check chosen part. On that derived term, choose Read logical structure of this term (one layer).
5. Repeat the body inspection to reach the equality. Track which binder each action enters. Read the context alongside the expression.

“Choose the body” describes which part to select; it is not the name of a separate button. For these examples the universal body has the internal path tag piBody, displayed as Product body in the continuation-path choices. The existential body lies through Argument, then Lambda body (appArg, then lamBody). Use the displayed constructor tree, preserving the binder context attached to that path.

Now start a separate inspection of QuantifierExistsForall.lean. Compare the binder order with the first example. The equality can have the same printed form while the enclosing statement imposes a different requirement.

If an operation reports a refusal or unavailable result, read that result and retain the earlier evidence. A failed continuation does not justify guessing the missing structure. The reader reference covers unavailable controls and navigation limits.

The editor operates on the complete trusted buffer, including commands outside the selection. It uses the project's built imports. Editing the buffer or changing the selection invalidates its attachment; selecting text does not create an execution sandbox.

Inspect a proof's type deliberately

Suppose the selected expression is a proof. The question “What does this prove?” concerns its inferred proposition type. That type and the proof term are distinct expressions.

In source data, choosing the Inferred type display only changes what you see. To make that type the starting term of a continuation, choose Inspect type of original selected term. On a derived term, the corresponding control is Inspect type of this term. You can then choose Read logical structure of this term (one layer) on the resulting type.

This explicit step preserves the relationship: the proposition is the inferred type of the proof. Directly inspecting the logical structure of the proof term asks a different question.

Exercise 3.1. You have selected a law proof. You switch the display to Inferred type, then want to continue by reading that type's universal quantifier. What explicit operation is needed first?

Read a retained history

An attempt is a retained sequence of explicit inspections and their outcomes. Selecting a step means reading the history through that point, its prefix.

Use the section labels to separate the questions:

Section navigation and the return links move reading focus within this attempt and step. They do not select a different history or run a new check.

Exercise 3.2. Return to the schematic trace. Suppose you are reading the prefix through B, and a later step checked that C has type Prop. Should that later check be reported as evidence established by the prefix through B? Does it prove C's equality?

You now have a way to avoid a common reading mistake: collecting every visible success and treating it as support for the currently selected expression. The route and the relevant prefix are part of the evidence.

← Propositions and proofs · Tutorial contents · Next: Laws and owners →