Matthieu Sozeau

Inductive types with parameters.

The most basic example is that of pairs, i.e. cartesian products:

Pairs

Using only pattern-matching, we can define their projections:

A common recursive type with parameters: lists.

The induction principle is derived as for nat, just parameterizing over the type [A].
Regular recursive functions can also be directly defined using fix+match, e.g:
The [{struct l}] annotation can be inferred by Coq, trying each argument in turn.

Infinite trees

More elaborate types can be defined inductively, e.g. with infinite branching.
Note how the recursive call to [map_tree] is on [ts x]: as [ts] is a subterm of [t], all calls to [ts] are as well.
Sigma types. The theory of Coq does not have a primitive notion of sigma-types or dependent pairs. They are rather derived using an inductive scheme. A dependent pair is like a cartesian product, except the second component's type might depend on the first component.
We can again define the projections using pattern-matching:
The second projection is special as it involves a dependent elimination, as we have seen in the example of the induction principle for natural numbers.
Let's walk through the type-checking of this term. We set the [return] clause of the pattern-matching to [λ p', B (projT1 p')], so when typechecking the first and only branch [existT a b => b], we expect the right-hand-side to have type [(λ p', B (projT1 p')) (existT a b) ≡ B (projT1 (existT a b)) ≡ B a]. This is exactly the type of [b] in this branch. This phenomenon of dependent elimination allowing the type of branches to vary is crucial for logical reasoning. Recall the elimination principle for natural numbers. Suppose we want to prove [P n] for some natural number [n]. By dependent pattern-matching, we can split this problem in two cases, one for [P 0] and one for [P (S n')]. The proofs of both cases will fit in the two branches of a dependent pattern-matching on [n] with return clause [λ n', P n'].
It is also at the basis of the representation of structures in type theory, e.g.: a type with a binary operation that is associative could be modeled as:
We can then extract the various components using iterated projections (exercise!)
Dependent elimination can also be used independently of induction principles. For example we can define the following type [unit_or_nat b] which is [unit] when the boolean [b] is [true], and [nat] otherwise:
Using dependent elimination, we can then depend a value of type [unit_or_nat b] for any [b]:
This type allows us to construct a meaningful example of a dependent pair:
These two objects pack a boolean value and depending on it being [true] or [false], the second projection will either be a value of type [unit] or [nat]. Applying the second projection hence makes this dependency apparent:
We will come back to the use of dependent elimination throughout this lecture, but first we will focus on the notion of propositions in Coq, represented by the sort [Prop].

Logical connectives The logical connectives of the [Prop] sort can be defined inductively.

The trivial proposition. The equivalent to the [unit] type in [Type]
The empty/void proposition
The elimnator of [False] allows to inhabit any type: ex falso quodlibet
Indeed, there is no case to consider as [False] has no constructors. Conjunction has a single constructor with two arguments:
It is simply a propositional version of the cartesian product type. Projections can be defined just as easily in the proof mode (usually preferred for witnessing propositions):
Under the hood, the proof is still using the primitive [match] construct:
Disjunction is an inductive with two constructors.
The [eq] inductive models propositional equality: - it includes convertibility, e.g.
- equalities can also be proven by induction, contrary to "convertibility", which cannot even be stated in the theory (there are no type and proof terms for ≡)
Equality is reflexive, symmetric and transitive (exercise!), so it is an equivalence relation.
The eliminator for equality allows do derive the Leibniz substitution principle:
This means that we can transport values from one type to another if we can show they are equal. This is at the core of the [rewrite] tactic. Computationally, we can see that [leibniz] does not do much: apart from matching on the equality proof [e], it just returns an identity function. The interesting part is only happening at the level of types.

Simple indexed inductive types.

Dependent elimination can be understood more easily on indexed inductive types. Here we define a new inductive type [is_true : bool -> Type] with a single constructor of type [is_true true]. This means that there is no way to build a value of [is_true false] (in a consistent context).
The eliminator:
The elimator tells us that to prove a property on arbitrary [b] and [is_true b] values, we only need to provide one branch [f : P true is_true_intro]. So we can actually prove the property that given an object of type [is_true b] for any [b], we can derive that [b = true].
We can also define inductive relations using indexed inductive types: here the list membership predicate [In] which tells if some element appears in a list.
The proof terms are derivation trees for this inductive relation:
We will study how they can be how to dependently eliminate them in the last part of the lecture. For now we can assume:

Two new sigma-types / dependent pairs

Subset types:

Subset types have their first component a computational object (some t : T, where T : Type) and second component a proof about this object (some (p : P t : Prop)..
We can also project these components using [proj1_sig] and [proj2_sig] defined in the standard library.

Existential types in [Prop]

Mimick the definition from the standard library
This is a special form of sigma-types where the first component is computational (e.g. a [nat]) and the second is a proof, but the whole existential is also a proposition (in [Prop]). As we will see, we cannot project from it to get back the witness, indeed:
The eliminator for [or]: Note that the elimination sort is restricted here, [P] has to be in [Prop]. We will come back to this in a minute!