(* Today we talk about inversion, which is destruct on steroids. *)
(* We use even again today. *)
Inductive even : nat -> Prop :=
| EvenO : even 0
| EvenS : forall n, even n -> even (S (S n))
.
(* Let's prove something really simple. *)
Goal not (even 3).
Proof.
(* We have to show that even 3 -> False. We unfold not to remind ourselves. *)
red.
(* We know that it's impossible to build a proof of even 3. To build a proof
of even 3 we'ld need to build a proof of even 1. But to build a proof of
even 1, we'ld have to find some m such that 1 = S (S m) and even m holds.
This m clearly can't be found, because 1 = S O. How do we get Coq to show this? *)
(* First we need to change 3 in even 3 to a variable. *)
remember 3 as n.
intros.
(* Then, we need to put our new equality hypothesis in the conclusion. *)
generalize Heqn. clear Heqn.
(* Now we can match on our even hypothesis. *)
refine (match H in even n0 return n0 = 3 -> False with
| EvenO => _
| EvenS n1 Ev =>
(match Ev in even n1 return S (S n1) = 3 -> False with
| EvenO => _
| EvenS n2 Ev2 => _
end)
end).
discriminate.
discriminate.
discriminate.
Qed.
(* There is a function that can do some of this work for you. Unlike the
induction functions it is not generated automatically. But, you can build it. *)
Derive Dependent Inversion even_inv with (forall n, even n) Sort Prop.
Print even_inv.
(* We can solve the same goal again. *)
Goal not (even 3).
Proof.
red.
remember 3 as n.
intros.
apply (even_inv n (fun _ _ => False)); auto.
intros. subst. discriminate.
intros. subst. clear H0.
apply (even_inv n0 (fun _ _ => False)); auto.
intros. subst. discriminate.
intros. subst. discriminate.
Qed.
(* What we just used was the maximal inversion principle. The
minimal inversion principle can be constructed like this. This is
by analogy with maximal and minimal induction principles. *)
Derive Inversion even_inv' with (forall n, even n) Sort Prop.
Print even_inv'.
(* Note that P is simpler now, and doesn't take a proof of evenness as
an argument. *)
(* We prove the goal one more time. *)
Goal not (even 3).
Proof.
red.
remember 3 as n.
apply (even_inv' n (fun _ => False)); auto.
intros. subst. discriminate.
intros. subst.
apply (even_inv' n0 (fun _ => False)); auto.
intros. subst. discriminate.
intros. subst. discriminate.
Qed.
(* No surprise that there is a tactic for this, called inversion. *)
Goal not (even 3).
Proof.
red. intros.
(* We must specify the hypothesis we want to destruct. *)
info inversion_clear H.
(* inversion is a busy tactic. It not only matched against the
two constructors, it discarded the one it could get rid of using
a discriminate tactic. *)
(* We can use the same tactic again to break apart even 1. *)
inversion H0.
Show Proof.
Qed.
(* That was somewhat painful. Why not use our new knowledge to
write a decison procedure for not evenness? We'll use the "partial" approach. *)
Require Import MoreSpecif.
Open Scope partial_scope.
Definition checkUneven (n : nat) : [ not (even n) ].
refine (fix F (n : nat) : [ not (even n) ] :=
match n as n0 return [not (even n0)] with
| O => No
| 1 => Yes
| S (S n) => Reduce (F n)
end).
(* We clearly want to deploy inversion here in the even 1 case. *)
red. intros H. info inversion H using even_inv'; auto.
intros. discriminate.
intros. discriminate.
(* We want to use inversion here as well, but referring to variables, not constants.
We can always change a goal like this:
not A
---------
not B
to the goal
B
----
A
this is just the contrapositive.
*)
intros H. apply _H. clear _H.
(* Of course, now it's obvious that inversion is called for. again.
This time, we use the inversion tactic without specifying a
particular inversion principle. This turns out to be easier, and is
the default behavior. *)
inversion H; intros; subst; auto.
Defined.
(* Note that there is a difference between the way inversion principles are used
and the way induction principles are used. Unlike the induction tactic,
the inversion tactic does not use an inversion principle, but generates the
code in place. To use an inversion principle it is necessary to state it explicitly.
Most people use the inversion tactic without a principle. A reason to use a
principle is space efficiency. *)
(* Not all we need is a partialOut function and we can generate proofs of unevenness
for any uneven number. *)
Definition partialOut (P : Prop) (p : partial P) :
match p with Proved _ => P | Uncertain => True end :=
match p with
| Proved p => p
| Uncertain => I
end.
Eval compute in checkUneven 3.
Goal not (even 1025).
Proof.
apply (partialOut (not (even 1025)) (checkUneven 1025)).
Qed.
(* Exercise : Goal forall n, even n -> n <> 5. *)
(* Note: It is pretty typical to follow inversion with subst, to remove all the
substitutable equalities. *)