Lesson 07
Why a proof can be a term
How can a proof checker treat logic as a form of typed programming?
In dependent type theory, propositions can be types and proofs can be terms. Checking a proof becomes the precise task of checking that a term has its declared type.
After this lesson, you should be able to
- Explain propositions as types for implication and conjunction.
- Distinguish a proof term from the tactic or elaborator that produced it.
- Describe dependent types, inductive types, recursors, and universes at an introductory level.
7.1
A proof of an implication is a function
To prove P → Q, assume a proof of P and construct a proof of Q. Type theory represents that argument as a function from terms of type P to terms of type Q. Applying the function to evidence for P returns evidence for Q.
A proof of P and Q contains both parts. A proof of P or Q identifies a side and carries a proof of that side. These data shapes give logical connectives computational meaning.
7.2
Types can depend on values
A dependent type can mention a value, such as the length in Vector α n. The index rules out length mismatches during type checking instead of leaving them as later runtime tests.
Propositions also depend on values. The statement n + 0 = n forms a different proposition for each natural number n, and a universal proof supplies evidence for every n.
7.3
Inductive declarations support recursion and induction
Natural numbers can be generated by zero and successor. A recursor states how to produce a result for zero and how to extend a result from n to successor n. When the result is a proposition depending on n, this becomes mathematical induction.
Universes organize types into levels and prevent inconsistent self-reference. A polymorphic theorem can use a universe variable instead of being copied at each level.
7.4
Source syntax is not the final proof object
An elaborator resolves notation, omitted arguments, and overloaded names. A tactic searches for proof steps or divides a goal into smaller goals. Both may be complex, but their result can remain outside the trusted base when the kernel checks the final explicit term.
The proof term is authoritative for kernel acceptance. A clear human proof remains valuable because it explains why the term should work and which mathematical idea it records.
Worked example
Read a proof of P and Q implies P
Construct a proof of P ∧ Q → P.
- Assume the input
Let h be a proof of P ∧ Q.
- Inspect its type
A proof of a conjunction contains a proof of P and a proof of Q.
- Select the first field
Return the P component of h.
- Read it as a function
The complete proof maps any h : P ∧ Q to h.left : P.
Result. The function has type P ∧ Q → P, so it is a proof of the implication.
7.5
Check your understanding
Answer each question before opening the explanation.
1 Why can a tactic remain outside the trusted computing base?
The kernel checks the explicit proof term produced by the tactic and rejects it if the term has the wrong type.
2 What does Vector α n record that List α does not?
The vector type records its length n as part of the type.
Concept wiki
Terms in this lesson
- Formal proof A proof expressed in a language whose steps can be checked mechanically.
- Proof term A term whose type is the proposition it proves.
- Type theory A formal foundation in which terms have types and propositions can be types.
- Dependent type A type that can mention a value.
- Elaborator A program that turns convenient source syntax into explicit terms for a kernel.
- Tactic A procedure that constructs or refines a proof.
- Inductive type A type generated by a declared set of constructors.
- Recursor The elimination rule used to define functions or proofs by cases on an inductive value.
- Universe A level used to organize types without placing every type inside itself.