6. Read an unfamiliar structure
This final lesson combines the earlier skills. Try to read the declaration before opening the worked explanation. The objective is to justify your interpretation from the fields and their types.
Start with the source
structure ReturnMap where
Source : Type
Target : Type
send : Source → Target
back : Target → Source
returns : ∀ x, back (send x) = x
example (system : ReturnMap) (unused : Nat) :
∀ x : system.Source, system.back (system.send x) = x :=
system.returns
Exercise 6.1. Read the record in ordinary language. What are the types of send and back? Which round trip does the law describe? Does the final declaration construct a new record or use an existing one?
Hint
Start with x and follow each function application from the inside out. Keep system attached to its fields.
Worked answer
The record contains two types, a function from Source to Target, a function back from Target to Source, and a proof that the composite back (send x) returns each input x.
The final declaration takes an existing system. Its proof is the stored law system.returns. It does not construct a record or prove the law independently of that supplied record. The additional natural-number parameter is available but unused.
Follow one input
The law describes this sequence of expressions:
| Stage | Expression | Type |
|---|---|---|
| Start | x | system.Source |
| Send | system.send x | system.Target |
| Return | system.back (system.send x) | system.Source |
The final expression can be compared with the initial one because they have the same type. The law asserts their equality for every source input.
The declaration says nothing about the visual appearance of either type. A diagram may show two labelled regions and arrows as a schematic account of the typed functions, but it must not add distances, coordinates, or elements whose existence has not been established.
Check the direction of the law
Exercise 6.2. Does returns also state that send (back y) = y for every y : Target?
Hint
The quantified variable in the declared law belongs to Source. The proposed new statement quantifies over Target.
Worked answer
No. It states only the round trip starting in Source. A map can return every sent input correctly while some target objects are never sent to.
For a concrete counterexample, take Source to be Unit, a type with one value, and Target to be Bool, with values false and true. Let send always return false, and let back always return the single unit value. Then back (send x) = x for every source input. But starting from true gives send (back true) = false, so the other round trip fails.
The download ReturnMap.lean constructs this record and checks both the required law and the failure at true.
Derive a consequence, then distinguish it from inspection
Exercise 6.3. Suppose a and b are source inputs and system.send a = system.send b. Must a = b? Try an equality argument before reading the answer.
Hint
Apply system.back to the given equality, then use the return law at each input.
Worked answer
Yes. Applying back preserves equality, so back (send a) = back (send b). The return law identifies the left side with a and the right side with b. Therefore a = b.
This property is called injectivity: equal outputs force equal inputs. It follows from the law, but it is not merely another field read directly from the record.
The Lean proof in ReturnMap.lean makes the reasoning explicit. Between propositions, → reads “implies”: here an equality of outputs implies an equality of inputs.
theorem send_injective (system : ReturnMap) :
∀ a b : system.Source, system.send a = system.send b → a = b := by
intro a b same
calc
a = system.back (system.send a) := (system.returns a).symm
_ = system.back (system.send b) := congrArg system.back same
_ = b := system.returns b
This block uses the ReturnMap declaration at the start of the lesson. In the middle line, congrArg applies the same function to both sides of an equality. The _ on the left continues from the previous right-hand side.
The proof establishes a mathematical consequence. A field catalogue or a drawing of the original law alone should not be described as having performed this proof.
Plan an inspection before opening the reader
Exercise 6.4. Starting from the owner system, you want to inspect its stored proof system.returns, then read the equality inside that proof's proposition. Write down the relationships you must preserve. What should remain visible when you reach the equality?
Worked answer
The route begins with a particular owner, then projects that owner's returns field. A type inspection relates the projected proof to its inferred proposition type. Reading the universal layer and entering its body reaches the equality in the context of its source input.
Preserve the owner, entered binder, full recorded context, ordered inspection relations, and relevant outcomes and audits. The context may include unused; displaying it does not claim the proof uses it. A check outside the selected prefix cannot become evidence for that prefix. Reaching the contained equality does not silently construct a specialized equality proof.
This is an inspection plan for a new example. The source and mathematical proofs were checked with Lean; no new Definograph capture of this record is supplied here. Any local refusal or unavailable operation should be reported as such.
Explain the result to another reader
Try writing a short explanation without looking back. It should identify the types and functions, state the law in the correct direction, and say where its proof comes from.
A complete answer could be:
An existing
systemprovides two types and functions between them. Its stored law proves that sending a source input and then applyingbackreturns that input. The law belongs to this record. It does not assert the opposite round trip for every target value. Reading a contained equality, checking a proof application, and proving a further consequence are distinct operations.
You have used the same method on a familiar equality, a record with one type, and an unfamiliar record with two types. In each case, the interpretation came from the expression's structure and the evidence attached to it.