The goal of this lecture note is to recapitulate the essentials of induction, from its principles to its practice, up to and including lists, which are the topic of the midterm project.
The type unit is predeclared but let us declare an isomorphic version of it:
Inductive unit' : Type :=
tt' : unit'.
Henceforth a value of type unit' can be tt'.
So when we destructure a value of type unit', e.g., with:
intros [ ].
or with:
destruct u as [ ].
or again with:
case u as [ ].
there is only one case: the unit' case with no argument.
To illustrate, let us present three proofs that Leibniz equality is reflexive for values of type unit'. The first one lets u denote the unit value and uses the reflexivity tactic:
Proposition unit'_identity :
forall u : unit',
u = u.
Proof.
intro u.
reflexivity.
The second proof is by cases. It first lets u denote the unit value, and then destructures it, naming the corresponding Leibniz equality as H_u:
Restart.
intro u.
case u as [ ] eqn:H_u.
The *goals* window then reads:
u : unit'
H_u : u = tt'
============================
tt' = tt'
We prove this subgoal using the reflexivity tactic.
The third proof is also by cases. It first destructures any given unit value, and then uses the reflexivity tactic:
Restart.
intros [ ].
reflexivity.
The type bool is predeclared but let us declare an isomorphic version of it:
Inductive bool' : Type :=
true' : bool'
| false' : bool'.
Henceforth a value of type bool' can be either true' or false'.
So when we destructure a value of type bool', e.g., with:
intros [ | ].
or with:
destruct b as [ | ].
or again with:
case b as [ | ].
there are two cases: the true' case with no argument, and the false' case, also with no argument.
To illustrate, let us present three proofs that Leibniz equality is reflexive for values of type bool'. The first one lets b denote any given Boolean and uses the reflexivity tactic:
Proposition bool'_identity :
forall b : bool',
b = b.
Proof.
intro b.
reflexivity.
The second proof is by cases. It first lets b denote any given Boolean, and then destructures it, naming the corresponding Leibniz equality as H_b:
Restart.
intro b.
case b as [ | ] eqn:H_b.
-
The *goals* window then reads:
b : bool'
H_b : b = true'
============================
true' = true'
where H_b makes it clear that we are in the true' case. Let us prove this subgoal using the reflexivity tactic, and focus on the other subgoal:
reflexivity.
-
The *goals* window then reads:
b : bool'
H_b : b = false'
============================
false' = false'
where H_b makes it clear that we are in the false' case. This second proof is completed using the reflexivity tactic:
reflexivity.
The third proof is also by cases. It first destructures any given Boolean, and then uses the reflexivity tactic in each case:
Restart.
intros [ | ].
- reflexivity.
- reflexivity.
The type nat is predeclared but let us declare an isomorphic version of it:
Inductive nat' : Type :=
O' : nat'
| S' : nat' -> nat'.
Henceforth a value of type nat' can be either O' (no argument) or the result of applying S' to one argument.
So when we destructure a value of type nat', e.g., with:
intros [ | n'].
or with:
destruct n as [ | n'].
or again with:
case n as [ | n'].
there are two cases: the O' case with no argument, i.e., the base case, and the S' case naming the argument (here: n'), i.e., the induction step.
Declaring nat' does not only have the effect of declaring this type and its constructors O' and S', it has the effect of declaring its induction principle, namely nat'_ind. And indeed after typing:
Check nat'_ind.
the *response* window reads, after renaming and re-indentation for clarity:
nat'_ind :
forall P : nat' -> Prop,
P O' ->
(forall n' : nat',
P n' ->
P (S' n')) ->
forall n : nat',
P n
In words: to prove that a property P holds for any n of type nat', we need to prove that it holds in the base case (i.e., that P O' holds), and that in the induction step, for any n' of type nat', if P n' holds (which is the induction hypothesis), then P (S' n') also holds.
Writing it as an inference rule:
| IND | P(O') | forall n' : nat', P(n') -> P(S' n') | |
| forall n : nat', P(n) | |||
So likewise, when proving something by induction over a variable of type nat', we write:
induction n as [ | n' IHn'].
to manifest that in the base case (namely O'), there is no argument, and in the induction step (namely S'), there is one argument (n') and its associated induction hypothesis (IHn').
To illustrate, let us present 4 proofs that Leibniz equality is reflexive for values of type nat'. The first one lets n denote any given Peano number and uses the reflexivity tactic:
Proposition nat'_identity :
forall n : nat',
n = n.
Proof.
intro n.
reflexivity.
The second proof is by cases. It first lets n denote any given Peano number and then destructures it, naming the corresponding Leibniz equality as H_n:
Restart.
intro n.
case n as [ | n'] eqn:H_n.
-
The *goals* window then reads:
n : nat'
H_n : n = O'
============================
O' = O'
where H_n makes it clear that we are in the base case. Let us prove this subgoal using the reflexivity tactic, and focus on the other subgoal:
reflexivity.
-
The *goals* window then reads:
n, n' : nat'
H_n : n = S' n'
============================
S' n' = S' n'
where H_n makes it clear that we are in the induction step. This second proof is completed using the reflexivity tactic:
reflexivity.
The third proof is also by cases. It first destructures any given Peano number, and then uses the reflexivity tactic in each case:
Restart.
intros [ | n'].
- reflexivity.
- reflexivity.
The fourth proof is by induction:
Restart.
intro n.
induction n as [ | n' IHn'].
-
The *goals* window displays the base case:
============================
O' = O'
Let us complete the base case and move to the induction step:
reflexivity.
-
The *goals* window reads:
n' : nat
IHn' : n' = n'
============================
S' n' = S' n'
Let us undo what tCPA helpfully did for us:
revert n' IHn'.
The *goals* window now displays the induction step:
============================
forall n' : nat', n' = n' -> S' n' = S' n'
So all the induction tactic does is activating nat'_ind.
The accompanying .v file contains a similar narrative for nat and it associated induction principle, nat_ind.
The polymorphic type of binary trees with payloads in the leaves (abbreviated “wpl”) is declared as follows:
Inductive binary_tree_wpl (V : Type) : Type :=
Leaf_wpl : V -> binary_tree_wpl V
| Node_wpl : binary_tree_wpl V -> binary_tree_wpl V -> binary_tree_wpl V.
Henceforth a value of type binary_tree_wpl V, for some given V, can be either the result of applying Leaf_wpl to V and to some value of type V (the payload) or the result of applying Node_wpl to V and to two values of type binary_tree_wpl V (the left subtree and the right subtree).
So when we destructure a value of type binary_tree_wpl V, e.g., with:
intros [v | t1 t2].
or with:
destruct t as [v | t1 t2].
or with:
case t as [v | t1 t2].
there are two cases: the Leaf_wpl case naming the arguments (namely v), and the Node_wpl case naming the two arguments (namely t1 and t2).
Declaring binary_tree_wpl does not only have the effect of declaring this type and its constructors Leaf_wpl and Node_wpl, it has the effect of declaring its induction principle, namely binary_tree_wpl_ind. And indeed after typing:
Check binary_tree_wpl_ind.
the *response* window reads, after renaming and re-indentation for clarity:
binary_tree_wpl_ind :
forall (V : Type)
(P : binary_tree_wpl V -> Prop),
(forall v : V,
P (Leaf_wpl V v)) ->
(forall t1 : binary_tree_wpl V,
P t1 ->
forall t2 : binary_tree_wpl V,
P t2 ->
P (Node_wpl V t1 t2)) ->
forall t : binary_tree_wpl V,
P t
In words: to prove that a property P holds for any t of type binary_tree_wpl V, for a given type V, we need to prove that it holds in the base case (i.e., that P (Leaf_wpl V v) holds, for any given payload v of type V), and that in the induction step, for any t1 of type binary_tree_wpl V such that P t1 holds (which is the first induction hypothesis), and for any t2 of type binary_tree_wpl V such that P t2 holds (which is the second induction hypothesis), then P (Node_wpl V t1 t2) also holds.
Writing it as an inference rule:
| IND(V) | forall v : V, P (Leaf_wpl V v) | forall t1 : binary_tree_wpl V, P t1 -> forall t2 : binary_tree_wpl V, P t2 -> P (Node_wpl V t1 t2) | |
| forall t : binary_tree_wpl V, P t | |||
So likewise, when proving something by induction over a variable of type binary_tree_wpl V, we write:
induction t as [v | t1 IHt1 t2 IHt2].
to manifest that in the Leaf case, there is an argument (v) and in the Node case, there are two arguments (t1 and t2), each of them with their associated induction hypothesis (IHt1 and IHt2).
To illustrate, let us present 4 proofs that Leibniz equality is reflexive for values of type binary_tree_wpl V, for any given V. The first one lets V denote any given type and t denote any given binary tree, and uses the reflexivity tactic:
Proposition binary_tree_wpl_identity :
forall (V : Type)
(t : binary_tree_wpl V),
t = t.
Proof.
intros V t.
reflexivity.
The second proof is by cases. It first lets V denote any given type and t denote any given binary tree, and then destructures this tree, naming the corresponding Leibniz equality as H_t:
Restart.
intros V t.
case t as [v | t1 t2] eqn:H_t.
-
The *goals* window then reads:
V : Type
t : binary_tree_wpl V
v : V
H_t : t = Leaf_wpl V v
============================
Leaf_wpl V v = Leaf_wpl V v
where H_t makes it clear that we are in the Leaf case. Let us prove this subgoal using the reflexivity tactic, and focus on the other subgoal:
reflexivity.
-
The *goals* window then reads:
V : Type
t, t1, t2 : binary_tree_wpl V
H_t : t = Node_wpl V t1 t2
============================
Node_wpl V t1 t2 = Node_wpl V t1 t2
where H_t makes it clear that we are in the Node case. This second proof is completed using the reflexivity tactic:
reflexivity.
The third proof is also by cases. It first names the given type and destructures the given binary tree, and then uses the reflexivity tactic in each case:
Restart.
intros V [v | t1 t2].
- reflexivity.
- reflexivity.
The fourth proof is by induction:
Restart.
induction t as [v | t1 IHt1 t2 IHt2].
-
The *goals* window reads as follows:
V : Type
v : V
============================
Leaf_wpl V v = Leaf_wpl V v
Let us undo what tCPA helpfully did for us:
revert v.
The *goals* window displays the base case:
V : Type
============================
forall v : V, Leaf_wpl V v = Leaf_wpl V v
Let us complete the base case and move to the induction step:
intro v.
reflexivity.
-
The *goals* window reads:
V : Type
t1, t2 : binary_tree_wpl V
IHt1 : t1 = t1
IHt2 : t2 = t2
============================
Node_wpl V t1 t2 = Node_wpl V t1 t2
Let us undo what tCPA helpfully did for us:
revert t1 IHt1 t2 IHt2.
The *goals* window now displays the induction step:
V : Type
============================
forall t1 : binary_tree_wpl V, t1 = t1 -> forall t2 : binary_tree_wpl V, t2 = t2 -> Node_wpl V t1 t2 = Node_wpl V t1 t2
So all the induction tactic does is activating binary_tree_wpl_ind.
The polymorphic type of binary trees with payloads in the nodes (abbreviated “wpn”) is declared as follows:
Inductive binary_tree_wpn (V : Type) : Type :=
Leaf_wpn : binary_tree_wpn V
| Node_wpn : binary_tree_wpn V -> V -> binary_tree_wpn V -> binary_tree_wpn V.
Henceforth a value of type binary_tree_wpn V, for some given V, can be either the result of applying Leaf_wpl to V or the result of applying Node_wpl to V, a value of type binary_tree_wpl V (the left subtree), a value of type V (the payload), and a value of type binary_tree_wpl V (the right subtree).
So when we destructure a value of type binary_tree_wpn V, e.g., with:
intros [ | t1 v t2].
or with:
destruct t as [ | t1 v t2].
or with:
case t as [ | t1 v t2].
there are two cases: the Leaf_wpn case, and the Node_wpl case naming the three arguments (namely t1, v, and t2).
Declaring binary_tree_wpn does not only have the effect of declaring this type and its constructors Leaf_wpn and Node_wpn, it has the effect of declaring its induction principle, namely binary_tree_wpn_ind. And indeed after typing:
Check binary_tree_wpn_ind.
the *response* window reads, after renaming and re-indentation for clarity:
binary_tree_wpn_ind :
forall (V : Type)
(P : binary_tree_wpn V -> Prop),
P (Leaf_wpn V) ->
(forall t1 : binary_tree_wpn V,
P t1 ->
forall (v : V)
(t2 : binary_tree_wpn V_,
P t2 ->
P (Node_wpn V t1 v t2)) ->
forall t : binary_tree_wpn V,
P t
In words: to prove that a property P holds for any t of type binary_tree_wpn V, for a given type V, we need to prove that it holds in the base case (i.e., that P (Leaf_wpn V) holds), and that in the induction step, for any t1 of type binary_tree_wpn V such that P t1 holds (which is the first induction hypothesis), for any given payload v of type V), and for any t2 of type binary_tree_wpn V such that P t2 holds (which is the second induction hypothesis), then P (Node_wpn V t1 t2) also holds.
Writing it as an inference rule:
| IND(V) | P (Leaf_wpn V) | forall t1 : binary_tree_wpn V, P t1 -> forall v : V, forall t2 : binary_tree_wpl V, P t2 -> P (Node_wpn V t1 v t2) | |
| forall t : binary_tree_wpn V, P t | |||
So likewise, when proving something by induction over a variable of type binary_tree_wpn V, we write:
induction t as [ | t1 IHt1 v t2 IHt2].
to manifest that in the Leaf case, there are no arguments and in the Node case, there are three arguments (t1, v, and t2), the first and the last of them with their associated induction hypothesis (IHt1 and IHt2).
To illustrate, let us present 4 proofs that Leibniz equality is reflexive for values of type binary_tree_wpn V, for any given V. The first one lets V denote any given type and and t denote any given binary tree, and then uses the reflexivity tactic:
Proposition binary_tree_wpn_identity :
forall (V : Type)
(t : binary_tree_wpn V),
t = t.
Proof.
intros V t.
reflexivity.
The second proof is by cases. It first lets V denote any given type and and t denote any given binary tree, and then destructures this given tree, naming the corresponding Leibniz equality as H_t:
Restart.
intros V t.
case t as [ | t1 v t2] eqn:H_t.
-
The *goals* window then reads:
V : Type
t : binary_tree_wpn V
H_t : t = Leaf_wpn V
============================
Leaf_wpn V = Leaf_wpn V
where H_t makes it clear that we are in the Leaf case. Let us prove this subgoal using the reflexivity tactic, and focus on the other subgoal:
reflexivity.
-
The *goals* window then reads:
V : Type
t, t1 : binary_tree_wpn V
v : V
t2 : binary_tree_wpn V
H_t : t = Node_wpn V t1 v t2
============================
Node_wpn V t1 v t2 = Node_wpn V t1 v t2
where H_t makes it clear that we are in the Node case. This second proof is completed using the reflexivity tactic:
reflexivity.
The third proof is also by cases. It first lets V denote any given type and destructures any given binary tree, and then uses the reflexivity tactic in each case:
Restart.
intros V [ | t1 v t2].
- reflexivity.
- reflexivity.
The fourth proof is by induction:
Restart.
intros V t.
induction t as [| t1 IHt1 v t2 IHt2].
-
The *goals* window displays the base case:
V : Type
============================
Leaf_wpn V = Leaf_wpn V
Let us complete the base case and move to the induction step:
reflexivity.
-
The *goals* window reads as follows:
V : Type
t1 : binary_tree_wpn V
v : V
t2 : binary_tree_wpn V
IHt1 : t1 = t1
IHt2 : t2 = t2
============================
Node_wpn V t1 v t2 = Node_wpn V t1 v t2
Let us undo what tCPA helpfully did for us:
revert t1 IHt1 v t2 IHt2.
The *goals* window now displays the induction step:
V : Type
============================
forall t1 : binary_tree_wpn V,
t1 = t1 -> forall (v : V) (t2 : binary_tree_wpn V), t2 = t2 -> Node_wpn V t1 v t2 = Node_wpn V t1 v t2
So all the induction tactic does is activating binary_tree_wpn_ind.
As a hopefully telling and otherwise gratuitous generalization, consider the following polymorphic type of trees:
Inductive tree3 (V : Type) : Type :=
Node0 : V -> tree3 V
| Node1 : tree3 V -> tree3 V
| Node2 : tree3 V -> tree3 V -> tree3 V
| Node3 : tree3 V -> tree3 V -> tree3 V -> tree3 V.
These funky trees have:
Henceforth a value of type tree3 V, for some given V, can be either the result of applying Node0 to a value of type V, the result of applying Node1 to V and a value of type tree3 V (1 subtree), the result of applying Node2 to V and two values of type tree3 V (2 subtrees), or the result of applying Node3 to V and three values of type tree3 V (3 subtrees).
So when we destructure a value of type tree3 V, e.g., with:
intros [v | t1 | t1 t2 | t1 t2 t3].
or with:
destruct t as [v | t1 | t1 t2 | t1 t2 t3].
or with:
case t as [v | t1 | t1 t2 | t1 t2 t3].
there are 4 cases, one for each constructor, and each one names the argument of each constructor.
Briefly (the reader is invited to step through this proof in the accompanying .v file), here are 4 proofs that Leibniz equality is reflexive for values of type tree3 V, for any given V:
Proposition tree3_identity :
forall (V : Type)
(t : tree3 V),
t = t.
Proof.
intros V t.
reflexivity.
Restart.
intros V t.
case t as [v | t1 | t1 t2 | t1 t2 t3] eqn:H_t.
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Restart.
intros V [v | t1 | t1 t2 | t1 t2 t3].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Restart.
intros V t.
induction t as [v | t1 IHt1 | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 t3 IHt3].
- reflexivity.
- reflexivity.
- reflexivity.
- reflexivity.
Qed.
Observe how for the induction proof, each subtree is accompanied by its induction hypothesis.
Anton: No induction principle for these variadic trees?Alfrothul: ‘fraid the proof rule is too large to fit within these margins.Pierre de Fermat: A common problem.Mimer: Monsieur de Fermat! Thanks for stopping by!
The type of lists is defined with nil (no argument) and :: (2 arguments, in infix form), as in OCaml, and the type argument is implicit. So when we destructure a value of type list V, for any given V, e.g., with:
intros [ | v vs'].
or with:
destruct vs as [ | v vs'].
or with:
case vs as [ | v vs'].
there are two cases: the nil case with no argument, and the cons case naming the two arguments (namely v and vs').
Applying the induction tactic here activates list_ind, the induction principle associated with lists:
list_ind :
forall (V : Type)
(P : list V -> Prop),
P nil ->
(forall (v : V)
(vs' : list V),
P vs' ->
P (v :: vs)%list) ->
forall vs : list V,
P vs
In words: to prove that a property P holds for any vs of type list V, for a given type V, we need to prove that it holds in the base case (i.e., that P nil holds), and that in the induction step, for any v of type V and for any value vs' of type list V such that P vs' holds (which is the induction hypothesis), then P (v :: vs') also holds.
Writing it as an inference rule:
| IND(V) | P (nil) | forall v : V, forall vs' : list V, P vs' -> P (v :: vs') | |
| forall vs : list V, P vs | |||
So when proving something by induction, we write:
induction vs as [ | v vs' IHvs'].
to manifest that in the nil case, there is no argument, and in the cons case, there are two arguments (v and vs'), the 2nd one with its associated induction hypothesis (IHvs').
To illustrate, let us present 4 proofs that Leibniz equality is reflexive for values of type list V, for any given V. The first one uses the reflexivity tactic, the second one is by cases and destructures any given list with a named equation among the assumptions to witness whether we are in the base case or in the induction step, the third one is also by cases, and the last one is by induction:
Proposition list_identity :
forall (V : Type)
(vs : list V),
vs = vs.
Proof.
intros V vs.
reflexivity.
Restart.
intros V vs.
case vs as [ | v vs'] eqn:H_vs.
- reflexivity.
- reflexivity.
Restart.
intros V [ | v vs'].
- reflexivity.
- reflexivity.
Restart.
intros V vs.
induction vs as [ | v vs' IHvs'].
-
The *goals* window displays the base case:
V : Type
============================
nil = nil
Let us complete the base case and move to the induction step:
reflexivity.
-
The *goals* window reads as follows:
V : Type
v : V
vs' : list V
IHvs' : vs' = vs'
============================
(v :: vs')%list = (v :: vs')%list
where tCPA unparser makes it manifest that the infix operator :: is used for lists, using the % annotation.
Let us undo what tCPA helpfully did for us:
revert v vs' IHvs'.
The *goals* window now displays the induction step:
V : Type
============================
forall (v : V) (vs' : list V), vs' = vs' -> (v :: vs')%list = (v :: vs')%list
So all the induction tactic does is activating list_ind, as can also be seen using Show Proof. at the end of the proof.
Halcyon: I think that all these identity propositions can be generalized into one identity theorem, which can be proved once and for all.
Pablito: Pray tell.
Halcyon: Sure:
Theorem identity :
forall (V : Type)
(v : V),
v = v.
Proof.
intros V v.
reflexivity.
Qed.
Pablito: Yup, that did it.
Halcyon: Thank you. Not just that, but all these identity procedures can now be proved as corollaries. Take the last one, for example:
Corollary list_identity_revisited :
forall (V : Type)
(vs : list V),
vs = vs.
Proof.
intro V.
exact (identity (list V)).
Qed.
Pablito: That did it too. Polymorphism is so cool.
Halcyon: So they are all the same, and that is why I named my theorem “identity”. Who knows, maybe one day, it will be known as “Halcyon’s identity” and listed in Wikipedia.
Pablito: Way to go, Halcyon. Way to go.
Anton: Isomorphic?
Alfrothul: Yes, that’s what it says above. The type bool and the type bool' are isomorphic.
Anton: So if we write two conversion functions from either to the other...
Alfrothul: ...these two functions should be inverses of each other, yes.
Anton: Let me try. First, a conversion function from bool to bool':
Definition bool_to_bool' (b : bool) : bool' :=
match b with
true =>
true'
| false =>
false'
end.
Alfrothul: Yes. And then, a conversion function from bool' to bool:
Definition bool'_to_bool (b : bool') : bool :=
match b with
true' =>
true
| false' =>
false
end.
Anton: Your conversion function is a left inverse of mine:
Proposition bool'_to_bool_is_a_left_inverse_of_bool_to_bool' :
forall b : bool,
bool'_to_bool (bool_to_bool' b) = b.
Alfrothul: Yes. And your conversion function is a left inverse of mine:
Proposition bool_to_bool'_is_a_left_inverse_of_bool'_to_bool :
forall b' : bool',
bool_to_bool' (bool'_to_bool b') = b'.
Pablito: The proof of these two propositions is by cases.
Mimer: And as we shall see in the chapter about isometries in the equilateral triangle, these proofs by cases can be written very concisely in tCPA.
Consider right-to-left (instead of the usual left-to-right) linked lists:
Inductive tsil' (V : Type) : Type :=
lin' : tsil' V
| snoc' : tsil' V -> V -> tsil' V.
Prove that list' and tsil' are isomorphic types.
The solution involves two routine induction proofs and is in the resource file for the present lecture note.
Verify that nat and nat' are isomorphic types.
On the occasion, a data type has only one summand. For example, consider the abstract syntax of the target language in the term project:
Inductive byte_code_instruction : Type :=
PUSH : nat -> byte_code_instruction
| ADD : byte_code_instruction
| SUB : byte_code_instruction.
Inductive target_program : Type :=
Target_program : list byte_code_instruction -> target_program.
Whereas byte_code_instruction has three data constructors, target_program has only one.
To illustrate, let us present three proofs that Leibniz equality is reflexive for values of type target_program. The first one lets sp denote any given source program:
Proposition target_program_identity :
forall sp : target_program,
sp = sp.
Proof.
intro sp.
The *goals* window then reads:
sp : target_program
============================
sp = sp
And the proof is completed using the reflexivity tactic:
reflexivity.
The second proof is by cases, even though there is only one case. It first destructures any given target program, letting bcis denote the list of byte-code instructions in any given source program:
Restart.
intros [bcis].
The *goals* window then reads:
bcis : list byte_code_instruction
============================
Target_program bcis = Target_program bcis
And the proof is completed using the reflexivity tactic:
reflexivity.
The third proof is by also cases, distinguishing whether the list of byte-code instructions in any given source program is empty or nonempty:
Restart.
intros [[ | bci bcis']].
The *goals* window then reads:
============================
Target_program nil = Target_program nil
subgoal 2 (ID 36) is:
Target_program (bci :: bcis') = Target_program (bci :: bcis')
Halcyon (modestly): Another instance of my identity.Pablito: And the destructuring notation can be nested too.
We can also define the empty data type, i.e., a data type with no summand:
Inductive empty : Type.
The destructuring notation for the intros tactic scales:
Proposition empty_identity :
forall e : empty,
e = e.
Proof.
intros [ ].
Mimer (reflectively): Full of emptiness...Loki: I didn’t have you as a Donna Summer fan, Mimer.Mimer: Harrumph.