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
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.)
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"
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 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
S n, whereas the induction step for
even_ind goes from
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
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
induction. We now get only the two meaningful cases,
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.