- A+

I'm trying to see if it's possible to prove `evenb n = true <-> exists k, n = double k`

from https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html without involving odd numbers at all. I tried something like the following:

`Theorem evenb_double_k : forall n, evenb n = true -> exists k, n = double k. Proof. intros n H. induction n as [|n' IHn']. - exists 0. reflexivity. - (* stuck *) `

But apparently induction works one natural number at a time, and `exists k : nat, S n' = double k`

is clearly not provable.

`n' : nat H : evenb (S n') = true IHn' : evenb n' = true -> exists k : nat, n' = double k ______________________________________(1/1) exists k : nat, S n' = double k `

Is there a way to have induction go from n to n+2?

There is a tactic called `fix`

. I will try to explain what is happening at a high level, because I think it is a cool hack, but be warned that `fix`

is a double-edged sword, generally ill advised to use: it depends on really low-level details of Coq, that make proofs quite fragile, and when they break, the error messages are difficult to understand.

`fix foo i`

, where `foo`

is a fresh variable, and `i`

is an integer, is a tactic which applies to a goal with at least `i`

arguments (for example, `forall n, evenb n = true -> ...`

has two: `n`

and a proof of `evenb n = true`

), and **assumes the goal that you are trying to prove**, naming that new hypothesis `foo`

. (Yes, you read that right.)

`Theorem evenb_double_k : forall n, evenb n = true -> exists k, n = double k. Proof. fix self 1. (* 1 subgoal (ID 17) self : forall n : nat, evenb n = true -> exists k : nat, n = double k ============================ forall n : nat, evenb n = true -> exists k : nat, n = double k *) `

Of course, there is a catch: **that hypothesis must be applied to a proper subterm of n** (which is the

*first*argument of the goal, that's what the number parameter of

`fix self 1`

means, we say that the first argument is the *decreasing argument*). What is a proper subterm of

`n`

? It is a value that you can get only by destructing `n`

, at least once.Note that Coq won't immediately complain if you still decide to apply the hypothesis `self`

directly (`n`

is not a proper subterm of itself). Coq only checks the "subterm" requirement on `Qed`

.

` apply self. (* seems fine, all goals done. *) Qed. (* ERROR! *) `

You can approximatively imagine `fix`

as a form of strong induction, where the induction hypothesis (`self`

) is given for all terms smaller than the current one, not only immediate predecessors. However this "subterm" relation does not actually appear in the statement of `self`

. (This peculiarity is what makes `fix`

a low-level, dangerous tactic.)

After a `fix`

you generally want to `destruct`

the decreasing argument. This is where `fix`

allows your proof to follow the structure of `evenb`

. Below, we destruct again immediately in the `S`

case. So we get three cases: `n = O`

, `n = S O`

, `n = S (S n')`

for some `n' : nat`

.

The first case is easy, the second one is vacuous, and the third one is where you need the "induction hypothesis" `self`

at `n'`

.

`Proof. fix self 1. intros n. destruct n as [| [| n']]. - exists 0; reflexivity. - discriminate. - simpl. intro H. apply self in H. destruct H as [k Hk]. exists (S k). rewrite Hk; reflexivity. Qed. `

Some of the reasoning there is fairly generic, and it can be pulled out into a custom *induction principle for even nats*, which is concretely another

`Theorem`

.`Theorem even_ind : forall (P : nat -> Prop), P O -> (forall n, evenb n = true -> P n -> P (S (S n))) -> forall n, evenb n = true -> P n. `

Compare it to the standard induction principle for `nat`

, which is in fact also a theorem, named `nat_ind`

. This is what the `induction`

tactic uses under the hood.

`About nat_ind. (* nat_ind : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *) `

The induction step in `nat_ind`

goes from `n`

to `S n`

, whereas the induction step for `even_ind`

goes from `n`

to `S (S n)`

, and has an extra hypothesis saying that our numbers are even.

The proof of `even_ind`

follows a similar structure to `evenb_double_k`

, although it is more abstract because it generalizes over all predicates `P`

on `nat`

.

`Proof. intros P HO HSS. fix self 1. intros n. destruct n as [| [| n']]. - intro; apply HO. - discriminate. - intros H. apply HSS. + apply H. + apply self. apply H. Qed. `

Another approach here is to not use `fix`

at all (since it should be avoided), but keep `induction`

as a primitive to prove the alternative `even_ind`

principle. That is fine for `nat`

, but for some complex inductive types, the default induction principle is too weak and a handwritten `fix`

is the only way.

Finally, going back to `evenb_double_k`

, we can use the new induction principle with `apply even_ind`

, as opposed to `fix`

or `induction`

. We now get only the two meaningful cases, `O`

and `S (S n')`

where `n'`

is even.

`Theorem evenb_double_k' : forall n, evenb n = true -> exists k, n = double k. Proof. apply even_ind. - exists 0. reflexivity. - intros n H [k Hk]. exists (S k). rewrite Hk. reflexivity. Qed. `

Definitions used in this answer:

`Fixpoint evenb n := match n with | S (S n') => evenb n' | S O => false | O => true end. Fixpoint double k := match k with | O => O | S k' => S (S (double k')) end. `