8.4 Inversion
Generalities about inversion
When working with (co)inductive predicates, we are very often faced to some of these situations:- we have an inconsistent instance of an inductive predicate in the local context of hypotheses. Thus, the current goal can be trivially proved by absurdity.
- we have a hypothesis that is an instance of an inductive predicate, and the instance has some variables whose constraints we would like to derive.
The inversion tactics are very useful to simplify the work in these cases. Inversion tools can be classified in three groups:
- tactics for inverting an instance without stocking the inversion lemma in the context; this includes the tactics (Dependent) Inversion and (Dependent) Inversion_clear.
- commands for generating and stocking in the context the inversion lemma corresponding to an instance; this includes Derive (Dependent) Inversion and Derive (Dependent) Inversion_clear.
- tactics for inverting an instance using an already defined inversion lemma; this includes the tactic Inversion ...using.
As inversion proofs may be large in size, we recommend the user to stock the lemmas whenever the same instance needs to be inverted several times.
Example 1: Non-dependant inversion
Let's consider the relation Le over natural numbers and the following variables:
Coq < Inductive Le : nat->nat->Set :=Coq < LeO : (n:nat)(Le O n) | LeS : (n,m:nat) (Le n m)-> (Le (S n) (S m)).Coq < Variable P:nat->nat->Prop.Coq < Variable Q:(n,m:nat)(Le n m)->Prop.For example, consider the goal:
Coq < Show.1 subgoal
n : nat
m : nat
H : (Le (S n) m)
============================
(P n m)
To prove the goal we may need to reason by cases on H and to derive that m is necessarily of the form (S m0) for certain m0 and that (Le n m0). Deriving these conditions corresponds to prove that the only possible constructor of (Le (S n) m) is LeS and that we can invert the -> in the type of LeS. This inversion is possible because Le is the smallest set closed by the constructors LeO and LeS.
Coq < Inversion_clear H.1 subgoal
n : nat
m : nat
m0 : nat
H0 : (Le n m0)
============================
(P n (S m0))
Note that m has been substituted in the goal for (S m0) and that the hypothesis (Le n m0) has been added to the context.
Sometimes it is interesting to have the equality m=(S m0) in the context to use it after. In that case we can use Inversion that does not clear the equalities:
Coq < Undo.Coq < Inversion H.1 subgoal
n : nat
m : nat
H : (Le (S n) m)
n0 : nat
m0 : nat
H0 : n0=n
H2 : (S m0)=m
H1 : (Le n m0)
============================
(P n (S m0))
Example 2: Dependant Inversion
Let us consider the following goal:
Coq < Show.1 subgoal
n : nat
m : nat
H : (Le (S n) m)
============================
(Q (S n) m H)
As H occurs in the goal, we may want to reason by cases on its structure and so, we would like inversion tactics to substitute H by the corresponding term in constructor form. Neither Inversion nor Inversion_clear make such a substitution. To have such a behavior we use the dependent inversion tactics:
Coq < Dependent Inversion_clear H.1 subgoal
n : nat
m : nat
m0 : nat
l : (Le n m0)
============================
(Q (S n) (S m0) (LeS n m0 l))
Note that H has been substituted by (LeS n m0 l) and m by (S m0).
Example 3: using already defined inversion lemmas
For example, to generate the inversion lemma for the instance (Le (S n) m) and the sort Prop we do:
Coq < Derive Inversion_clear leminv with (n,m:nat)(Le (S n) m) Sort Prop.Coq < Check leminv.leminv
: (P:nat->nat->Prop)
(n,m:nat)
((m0:nat)(Le n m0)->(P n (S m0)))->(Le (S n) m)->(P n m)
Then we can use the proven inversion lemma:
Coq < Show.1 subgoal
n : nat
m : nat
H : (Le (S n) m)
============================
(P n m)
Coq < Inversion H using leminv.1 subgoal
n : nat
m : nat
H : (Le (S n) m)
============================
(m0:nat)(Le n m0)->(P n (S m0))