I am working on the theorem ev_ev__ev in IndProp.v of Software Foundations (Vol 1: Logical Foundations).
Theorem ev_ev__ev : forall n m,
even (n+m) -> even n -> even m.
Proof.
intros n m Enm En. induction En as [| n' Hn' IHn'].
- (* En: ev_0 *) simpl in Enm. apply Enm.
- (* En: ev_SS n' Hn': even n'
with IHn': even (n' + m) -> even m *)
apply IHn'. simpl in Enm. inversion Enm as [| n'm H]. apply H.
Qed.
where even is defined as:
Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).
At the point of the second bullet -, the context as well as the goal is as follows:
m, n' : nat
Enm : even (S (S n') + m)
Hn' : even n'
IHn' : even (n' + m) -> even m
______________________________________(1/1)
even m
I understand how m, n', Enm, Hn' in the context are generated. However, how is IHn' generated?
Induction hypotheses are systematically created for premises of constructors that are in the same type family. So, you can look at each constructor independently.
Assume you have an inductive definition of a type that starts with:
Inductive arbitraryName : A -> B -> Prop :=
An induction principle called arbitraryName_ind will be created, which starts with a quantification over an arbitrary predicate usually called P with the same type
forall P : A -> B -> Prop,
Now, if you have a constructor of the form
arbitrary_constructor : forall x y, arbitraryName x y -> ...
The induction principle will have a sub-clause for this constructor that starts with the same quantifications over all variables in the constructor, the same hypothesis, plus an induction hypothesis for the premise that relies on arbitraryName.
forall x y, arbitraryName x y -> P x y -> ...
Finally, each constructor of the inductive definition has to finish with an application of the defined type family (in this case arbitraryName). The end of the clause for this constructor apply the function P to the same argument.
Let's go back to arbitrary_constructor and suppose it has the following full type:
arbitrary_constructor : forall x y, arbitraryName x y -> arbitraryName (g x y) (h x y)
In that case the clause in the induction principle is :
(forall x y, arbitraryName x y -> P x y -> P (g x y) (h x y))
In the case of even, there is a constructor ev_SS that has the following shape:
ev_SS : forall x, even x -> even (S (S x))
So the clause that is generated has the following shape:
(forall x, even x -> P x -> P (S (S x)))
The induction hypothesis IHn' corresponds exactly to this P in the clause.
The full induction principle has the following shape.
forall P : nat -> Prop, P 0 ->
(forall x, even x -> P x -> P (S (S x))) ->
forall n, even n -> P n
When you type induction En, this theorem is applied. The hypothesis even n, where n is universally quantified, is matched with the text of En in the goal at that moment. It turns out that the statement of that hypothesis is even n (the n here is fixed in the goal) so the universally quantified n is instantiated with the local n from the goal context. Then, the tactic tries to find all the hypotheses in the context where this n appears. In this case, there is Enm, so this hypothesis is used to define the P on which the induction principle will be instantiated. In a sense, what happens is that Enm is put back in the goal's conclusion, as if one had executed revert Enm.
We need P n to be the same thing as even (n + m) -> even m. The most natural solution is that P is equal to the function fun x => even (x + m) -> even m
So in the second case of the proof by induction, a new n' is introduced and P is applied to n' to give the contents of the induction hypothesis:
(even (n' + m) -> even m)
and P is applied to S (S n') to give the contents of the final goal.
even (S (S n') + m) -> even m
Now, at the time of calling the induction tactic, the hypothesis Enm was in the context, so the statement even (S (S n') + m), which is morally an offspring of Enm is put back in the context with the same name. Note that there was already a hypothesis named Enm in the other goal, but the statement was again different.
It is normal that you have a question on how this induction hypothesis was generated, because what happens actually involves several operations.