Can I tell Coq to do induction from n to n + 2?
Question
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:
forall n : nat, evenb n = true -> exists k : nat, n = double kforall n : nat, evenb n = true -> exists k : nat, n = double kn: nat
H: evenb n = trueexists k : nat, n = double kH: evenb 0 = trueexists k : nat, 0 = double kn': nat
H: evenb (S n') = true
IHn': evenb n' = true -> exists k : nat, n' = double kexists k : nat, S n' = double kH: evenb 0 = trueexists k : nat, 0 = double kreflexivity.H: evenb 0 = true0 = double 0n': nat
H: evenb (S n') = true
IHn': evenb n' = true -> exists k : nat, n' = double kexists k : nat, S n' = double k
But apparently induction works one natural number at a time, and exists k : nat, S n' = double k is clearly not provable.
Is there a way to have induction go from n to n + 2?
Answer (Li-yao Xia)
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.)
forall n : nat, evenb n = true -> exists k : nat, n = double kforall n : nat, evenb n = true -> exists k : nat, n = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double kforall 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. EDIT: You can also use the command Guarded at any time to check this.
apply self. (* seems fine, all goals done. *)
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'.
forall n : nat, evenb n = true -> exists k : nat, n = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double kforall n : nat, evenb n = true -> exists k : nat, n = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n: natevenb n = true -> exists k : nat, n = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double kevenb 0 = true -> exists k : nat, 0 = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double kevenb 1 = true -> exists k : nat, 1 = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n': natevenb (S (S n')) = true -> exists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double kevenb 0 = true -> exists k : nat, 0 = double kreflexivity.self: forall n : nat, evenb n = true -> exists k : nat, n = double k
H: evenb 0 = true0 = double 0discriminate.self: forall n : nat, evenb n = true -> exists k : nat, n = double kevenb 1 = true -> exists k : nat, 1 = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n': natevenb (S (S n')) = true -> exists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n': natevenb n' = true -> exists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n': nat
H: evenb n' = trueexists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n': nat
H: exists k : nat, n' = double kexists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n', k: nat
Hk: n' = double kexists k : nat, S (S n') = double kself: forall n : nat, evenb n = true -> exists k : nat, n = double k
n', k: nat
Hk: n' = double kS (S n') = double (S k)reflexivity. Qed.self: forall n : nat, evenb n = true -> exists k : nat, n = double k
n', k: nat
Hk: n' = double kS (S (double k)) = double (S k)
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.
forall P : nat -> Prop,
P 0 ->
(forall n : nat, evenb n = true -> P n -> P (S (S n))) ->
forall n : nat, 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.
forall P : nat -> Prop, P 0 -> (forall n : nat, evenb n = true -> P n -> P (S (S n))) -> forall n : nat, evenb n = true -> 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.
forall P : nat -> Prop, P 0 -> (forall n : nat, evenb n = true -> P n -> P (S (S n))) -> forall n : nat, evenb n = true -> P nP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))forall n : nat, evenb n = true -> P nP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P nforall n : nat, evenb n = true -> P nP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n: natevenb n = true -> P nP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P nevenb 0 = true -> P 0P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P nevenb 1 = true -> P 1P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': natevenb (S (S n')) = true -> P (S (S n'))P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P nevenb 0 = true -> P 0apply HO.P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
H: evenb 0 = trueP 0discriminate.P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P nevenb 1 = true -> P 1P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': natevenb (S (S n')) = true -> P (S (S n'))P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueP (S (S n'))P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueevenb n' = trueP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueP n'apply H.P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueevenb n' = trueP: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueP n'apply H. Qed.P: nat -> Prop
HO: P 0
HSS: forall n : nat, evenb n = true -> P n -> P (S (S n))
self: forall n : nat, evenb n = true -> P n
n': nat
H: evenb (S (S n')) = trueevenb n' = true
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.
forall n : nat, evenb n = true -> exists k : nat, n = double kforall n : nat, evenb n = true -> exists k : nat, n = double kexists k : nat, 0 = double kforall n : nat, evenb n = true -> (exists k : nat, n = double k) -> exists k : nat, S (S n) = double kexists k : nat, 0 = double kreflexivity.0 = double 0forall n : nat, evenb n = true -> (exists k : nat, n = double k) -> exists k : nat, S (S n) = double kn: nat
H: evenb n = true
k: nat
Hk: n = double kexists k : nat, S (S n) = double kn: nat
H: evenb n = true
k: nat
Hk: n = double kS (S n) = double (S k)reflexivity. Qed.n: nat
H: evenb n = true
k: nat
Hk: n = double kS (S (double k)) = double (S k)
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.
Answer (Anton Trunov)
Yes, absolutely! Let's use the induction principle from this answer.
From Coq Require Import Arith.P: nat -> PropP 0 -> P 1 -> (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P nP: nat -> PropP 0 -> P 1 -> (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P nP: nat -> Prop
H0: P 0
H1: P 1
Hstep: forall n : nat, P n -> P (S n) -> P (S (S n))
n: natP ninduction n; intuition. Qed.P: nat -> Prop
H0: P 0
H1: P 1
Hstep: forall n : nat, P n -> P (S n) -> P (S (S n))
n: natP n /\ P (S n)
Now we can use the new principle like so (I switched the non-standard functions with their stdlib counterparts so that everything compiles):
forall n : nat, Nat.even n = true -> exists k : nat, n = Nat.double kforall n : nat, Nat.even n = true -> exists k : nat, n = Nat.double kn: nat
Ev: Nat.even n = trueexists k : nat, n = Nat.double k(* the rest of the proof has been removed to not spoil the fun *)Ev: Nat.even 0 = trueexists k : nat, 0 = Nat.double kEv: Nat.even 1 = trueexists k : nat, 1 = Nat.double kn: nat
Ev: Nat.even (S (S n)) = true
IHn: Nat.even n = true -> exists k : nat, n = Nat.double kexists k : nat, S (S n) = Nat.double k