even_Sn_not_even_n - apply 1 hypothesis in another

Link:: https://stackoverflow.com/q/56354064

Display all goals and responses

Question

Unfortunately I got stuck again:

Inductive even : nat -> Prop :=
| ev_0 : even 0
| ev_SS (n : nat) (H : even n) : even (S (S n)).

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).forall n : nat, even (S n) <-> ~ even n
Proof.forall n : nat, even (S n) <-> ~ even n
  intros n.n: nat
even (S n) <-> ~ even n split.n: nat
even (S n) -> ~ even n
n: nat
~ even n -> even (S n)
  -n: nat
even (S n) -> ~ even n intros H.n: nat
H: even (S n)
~ even n unfold not.n: nat
H: even (S n)
even n -> False intros H1.n: nat
H: even (S n)
H1: even n
False induction H1 as [|n' E' IHn].H: even 1
False
n': nat
H: even (S (S (S n')))
E': even n'
IHn: even (S n') -> False
False
    +H: even 1
False inversion H.
    +n': nat
H: even (S (S (S n')))
E': even n'
IHn: even (S n') -> False
False inversion_clear H.n': nat
E': even n'
IHn: even (S n') -> False
H0: even (S n')
False apply IHn in H0.n': nat
E': even n'
IHn: even (S n') -> False
H0: False
False apply H0.
  -n: nat
~ even n -> even (S n) intros H.n: nat
H: ~ even n
even (S n) induction n as [|n' IHn].H: ~ even 0
even 1
n': nat
H: ~ even (S n')
IHn: ~ even n' -> even (S n')
even (S (S n'))
    +H: ~ even 0
even 1 exfalso.H: ~ even 0
False apply H.H: ~ even 0
even 0 apply ev_0.
    +n': nat
H: ~ even (S n')
IHn: ~ even n' -> even (S n')
even (S (S n')) apply ev_SS.n': nat
H: ~ even (S n')
IHn: ~ even n' -> even (S n')
even n'

Here is the result:

1 subgoal

  n' : nat
  H : ~ even (S n')
  IHn : ~ even n' -> even (S n')
  ============================
  even n'

As far I could prove it in words:

(n' + 1) is not even according to H. Therefore according to IHn, it is not true that n' is not even (double negation):

IHn : ~ ~ even n'

Unfolding double negation, we conclude that n' is even.

But how to write it in coq?

Answer

The usual way to strip double negation is to introduce the "excluded middle" axiom, which is defined under the name classic in Coq.Logic.Classical_Prop, and apply the lemma NNPP.

However, in this particular case, you can use the technique called reflection by showing that the Prop is consistent with a boolean function (you might remember the evenb function introduced earlier in the book).

(Assuming you're at the beginning of IndProp) You'll soon see the following definition later in that chapter:

Inductive reflect (P : Prop) : bool -> Prop :=
| ReflectT (H : P) : reflect P true
| ReflectF (H : ~ P) : reflect P false.

You can prove the statement

Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).forall n : nat, reflect (even n) (evenb n)

and then use it to move between a Prop and a boolean (which contain the same information i.e. the (non-)evenness of n) at the same time. This also means that you can do classical reasoning on that particular property without using the classic axiom.

I suggest to complete the exercises under Reflection section in IndProp, and then try the following exercises. (Edit: I uploaded the full answer here.)

(* Since ``evenb`` has a nontrivial recursion structure, you need the
   following lemma: *)
Lemma nat_ind2 :
  forall P : nat -> Prop,
    P 0 -> P 1 -> (forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n.forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
Proof.forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
  fix IH 5.IH: forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n intros.IH: forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
P: nat -> Prop
H: P 0
H0: P 1
H1: forall n : nat, P n -> P (S (S n))
n: nat
P n destruct n as [| [| ]]; auto.IH: forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
P: nat -> Prop
H: P 0
H0: P 1
H1: forall n : nat, P n -> P (S (S n))
n: nat
P (S (S n))
  apply H1.IH: forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) ->
forall n : nat, P n
P: nat -> Prop
H: P 0
H0: P 1
H1: forall n : nat, P n -> P (S (S n))
n: nat
P n apply IH; auto.
Qed.

(* This is covered in an earlier chapter *)
Lemma negb_involutive : forall x : bool, negb (negb x) = x.forall x : bool, negb (negb x) = x
Proof.forall x : bool, negb (negb x) = x intros []; auto. Qed.

(* This one too. *)
Lemma evenb_S : forall n : nat, evenb (S n) = negb (evenb n).forall n : nat, evenb (S n) = negb (evenb n)
Proof.forall n : nat, evenb (S n) = negb (evenb n)
  induction n.evenb 1 = negb (evenb 0)
n: nat
IHn: evenb (S n) = negb (evenb n)
evenb (S (S n)) = negb (evenb (S n))
  -evenb 1 = negb (evenb 0) auto.
  -n: nat
IHn: evenb (S n) = negb (evenb n)
evenb (S (S n)) = negb (evenb (S n)) rewrite IHn.n: nat
IHn: evenb (S n) = negb (evenb n)
evenb (S (S n)) = negb (negb (evenb n)) simpl.n: nat
IHn: evenb (S n) = negb (evenb n)
evenb n = negb (negb (evenb n)) destruct (evenb n); auto.
Qed.

(* Exercises. *)
Lemma evenb_even : forall n : nat, evenb n = true -> even n.forall n : nat, evenb n = true -> even n
Proof.forall n : nat, evenb n = true -> even n induction n using nat_ind2.evenb 0 = true -> even 0
evenb 1 = true -> even 1
n: nat
IHn: evenb n = true -> even n
evenb (S (S n)) = true -> even (S (S n))
(* Fill in here *) Admitted.

Lemma evenb_odd : forall n : nat, evenb n = false -> ~ (even n).forall n : nat, evenb n = false -> ~ even n
Proof.forall n : nat, evenb n = false -> ~ even n induction n using nat_ind2.evenb 0 = false -> ~ even 0
evenb 1 = false -> ~ even 1
n: nat
IHn: evenb n = false -> ~ even n
evenb (S (S n)) = false -> ~ even (S (S n))
(* Fill in here *) Admitted.

Lemma even_reflect : forall n : nat, reflect (even n) (evenb n).forall n : nat, reflect (even n) (evenb n)
Proof. (* Fill in here. Hint: You don't need induction. *)forall n : nat, reflect (even n) (evenb n) Admitted.

Lemma even_iff_evenb : forall n, even n <-> evenb n = true.forall n : nat, even n <-> evenb n = true
Proof. (* Fill in here. Hint: use ``reflect_iff`` from IndProp. *)forall n : nat, even n <-> evenb n = true Admitted.

Theorem reflect_iff_false : forall P b, reflect P b -> (~ P <-> b = false).forall (P : Prop) (b : bool),
reflect P b -> ~ P <-> b = false
Proof. (* Fill in here. *)forall (P : Prop) (b : bool),
reflect P b -> ~ P <-> b = false Admitted.

Lemma n_even_iff_evenb : forall n, ~ (even n) <-> evenb n = false.forall n : nat, ~ even n <-> evenb n = false
Proof. (* Fill in here. *)forall n : nat, ~ even n <-> evenb n = false Admitted.

Lemma even_Sn_not_even_n : forall n,
    even (S n) <-> not (even n).forall n : nat, even (S n) <-> ~ even n
Proof.forall n : nat, even (S n) <-> ~ even n (* Fill in here.
          Hint: Now you can convert all the (non-)evenness properties
          to booleans, and then work with boolean logic! *) Admitted.