4. Keep a law with its owner
Mathematical structures often bundle objects, operations, and laws. Your goal is to read such a bundle without treating its field names as a mathematical definition or separating a law from the object to which it belongs.
Read the fields in order
Consider this complete source file:
structure Rotor where
Carrier : Type
turn : Carrier → Carrier
fixed : ∀ x, turn x = x
example (owner : Rotor) (unused : Nat) : Rotor := owner
structure declares a type of records. Each record of type Rotor has three fields:
| Field | What it supplies |
|---|---|
Carrier | A type of objects. |
turn | A function from that type to itself. |
fixed | A proof that applying that function to any object gives the same object. |
The arrow in Carrier → Carrier describes the function's input and output types. In the law, Lean infers that x has type Carrier from its use as the input of turn.
Read the law as an equation. Despite the name turn, it says that the function fixes every input. Nothing in this declaration supplies angles, a metric, coordinates, or a nontrivial rotation.
The final line accepts an existing record owner and returns it. It does not construct a new record or prove the law from other assumptions. The law is already one of the fields required of the supplied record.
Make ownership explicit
For this particular record, the fields have these meanings:
| Expression | Type or proposition |
|---|---|
owner.Carrier | A type. |
owner.turn | owner.Carrier → owner.Carrier |
owner.fixed | ∀ x : owner.Carrier, owner.turn x = x |
The dot means field access. Its repeated owner is doing real work: the input type, function, and law all belong to the same record.
If left and right are two records, their carrier types are not assumed to coincide. Even if printed labels look similar, you cannot automatically pass an element of left.Carrier into right.turn or use left.fixed as a law about right.turn.
Exercise 4.1. Which fact directly permits replacing left with right throughout a law about the record?
- The two records have fields with the same names.
- Their carrier types are equal.
- You have a proof that the records themselves are equal.
Hint
The replacement must account for all the fields, including the operations.
Worked answer
The third fact permits rewriting one record as the other, including its corresponding fields. Matching names do not establish identity. Equality of the carriers identifies the types, but does not by itself provide a replacement of the entire record or its operations. Further mathematical reasoning could establish other useful relationships; those would need their own justification.
Use a law at a particular input
With owner : Rotor and x : owner.Carrier, the term owner.fixed x has type owner.turn x = x. It supplies the equality proof by applying the universal law to the input.
Compare two actions:
| Action | Result |
|---|---|
| Inspect the equality inside the law's type. | Read the condition owner.turn x = x with its binder context. |
Apply the law proof to x. | Obtain a proof term owner.fixed x for that equality. |
The contained equality is useful to read, but containment alone has not constructed the application in the second row.
Exercise 4.2. After entering the universal body, can you say “the reader has separately proved this equality for the displayed x” solely because the equality is now visible?
Worked answer
No. You have reached a contained expression in the appropriate context. A separately checked proof application would be additional evidence. The universal law can supply such a proof, but the inspection path must not silently substitute one operation for the other.
Inspect the record locally
With the same local prerequisites as Lesson 3, open RotorLaw.lean, select the final owner in the example declaration, and run Definograph: Visualize Selection. Open Source data, then Checker input.
This selection is a structure value. The initial guided reader may refuse it while Source data still contains its exact expression. That is a useful boundary: source inspection and the guided mathematical presentation are separate capabilities.
In Checker input, select the whole prepared term and use Check chosen occurrence. Continue with:
- Inspect fields of original occurrence to request the field catalogue.
- Check field fixed to inspect the projected law of this owner.
- Inspect type of this term to continue from the law's proposition type.
- Read logical structure of this term (one layer) to inspect its universal layer.
- Select its body and use Check chosen part, retaining the entered binder and full context.
The catalogue lists fields; it is not itself a typing check of every field. Read the projection's own outcomes and owner identity. Then use the distinction above when reading the equality inside its type.
Keep unused : Nat in the recorded context. Its presence tells you that it was available, not that the returned term uses it. Lean's unused-variable warning for this example is a diagnostic, distinct from a rejected checking outcome.
Test the picture against the definition
Does every Rotor have an element? The declaration does not say so. A type can be empty; the universal law then has no inputs to which it must be applied.
The optional download RotorExamples.lean constructs a record with natural-number carrier and identity function, and another with empty carrier. Both meet exactly the same field requirements. It also checks the type of a law application.
Exercise 4.3. Would a diagram with one dot labelled “an element of the carrier” be justified for every Rotor?
Worked answer
No. The empty-carrier example rules out a general claim that an element exists. A schematic variable introduced under a universal binder has a different role from a displayed witness whose existence is asserted. The drawing must preserve that distinction.
← Follow an inspection · Tutorial contents · Next: Checking evidence →