Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.
A typing judgment is a ternary relation between two terms t and T, and a context Γ, which is itself a list of pairs, variable-type :
$$\Gamma ⊢\ t\ :\ T$$
Typing rules provide an inductive definition of well-formed typing judgments. For instance, a context provides a type to every variable it stores:
$$\Gamma ⊢\ x\ :\ T \quad (x, T) \in Γ$$
A type is a term T which occurs on the right of a colon, in a well-formed typing judgment.
Here is an example of context, and of judgment checking using the Check command:
Contexts also log the current hypotheses:
The fact that the command for stating lemma also involves a colon is no coincidence.
In fact, statements are types, proofs are terms (of a prescribed type) and typing rules encode rules for verifying the well-formedness of proofs.
A type is a term, and therefore it can also be typed in a typing judgment. A sort s is the type of a type:
$$\Gamma ⊢\ t\ :\ T \quad \quad \Gamma ⊢\ T\ :\ s $$
The sort Prop is the type of statements:
Warning: well-typed statements are not necessarily provable.
Types used as data structures live in a different sort, called Set.
Of course, a sort also has a type:
And there is in fact a tour of sorts, for consistency reasons which are beyond the scope of today's lecture:
Non atomic types are types of functions: the source of the arrow prescribes the type of the argument, and the codomain gives the type of the application of the function to its argument.
Reminder: Lesson 2 introduced polymorphic data types, e.g. list:
Polymorphic type are types of functions with a Type source:
A dependent type is a function whose co-domain is Type, and which takes at least one of its arguments in a data type, like nat or bool.
Here is for instance a type which could represent matrices (for a fixed type of coefficients), with size presecribed by its arguments:
And here is a function which uses this type as co-domain:
The typing rule for application prescribes the type of arguments:
Note that our arrow -> is just a notation for the type of functions with a non-dependent codomain:
What is an arrow type bewteen two types in Prop, i.e., between two statements?
It is an implication statement: the proof of an implication maps
any proof
of the premise to a proof of the conclusion.
The tactic move=> is used to prove an implication, by introducing its premise, i.e. adding it to the current context:
The tactic apply: allows to make use of an implication hypothesis in a proof. Its variant exact: fails if this proof step does not close the current goal.
The apply: tactic is also used to specialize a lemma:
Note how Coq did conveniently compute the appropriate instance by matching the statement against the current formula to be proved.
So far, we have only (almost) rigorously explained types Type, Prop, and forall x : A, B. But we have also casually used other constants like bool or nat.
The following declaration:
Inductive bool : Set := true : bool | false : bool
in fact introduces new constants in the language:
$$\vdash \textsf{bool} : \textsf{Set} \quad \vdash \textsf{true} : \textsf{bool} \quad \vdash \textsf{false} : \textsf{bool} $$
Term bool is a type, and the terms true and false are called constructors.
The closed (i.e. variable-free) terms of type bool are freely generated by true and false, i.e. they are exactly true and false.
This is the intuition behind the definition by (exhaustive) pattern matching used in Lesson 2:
The following declaration:
Inductive nat : Set := O : nat | S (n : nat)
in fact introduces new constants in the language:
$$\vdash \textsf{nat} : \textsf{Set} \quad \vdash \textsf{O} : \textsf{nat} \quad \vdash \textsf{S} : \textsf{nat} \rightarrow \textsf{nat} $$
Term nat is a type, and the terms O and S are called constructors.
The closed (i.e. variable-free) terms of type bool are freely generated by O and S, i.e. they are exactly O and terms S (S ... (S O)).
This is the intuition behind the definition by induction used in Lesson 2:
More precisely, an induction scheme is attached to the definition of an inductive type:
Quiz: what is this type used for:
Let us now review the three natures of proofs that involve a term of an inductive type:
Equality is a polymorphic, binary relation on terms:
It comes with an introduction rule, to build proofs of equalities, and with an elimination rule, to use equality statements.
The eq_ind principle states that an equality statement can be used to perform right to left substitutions.
It is in fact sufficient to justify the symmetry and transitivity properties of equalities.
Note how restoring the coercion from bool to Prop helps with readability.
But this is quite inconvenient: the rewrite tactic offers support for applying eq_ind conveniently.
Digression: eq being polymorphic, nothing prevents us from stating equalities on equality types:
See the Coq cheat sheet for more connectives: