Induction with other base case in Coq

Question

I am trying to proof the pigeonhole problem in Coq. Therefore I have the following lemma that I want to proof:

Lemma pigeon_hole :
forall m n, m < n ->
forall f, (forall i, i < n -> f i < m) ->
exists i, i < n /\
exists j, j < n /\ i <> j /\ f i = f j.

From my teacher I have got the hint that a useful tactic to automatically prove equalities and inequalities between natural numbers is

omega.

But I doubt if that is relevant here.

I thought that it could be done with induction as in https://math.stackexchange.com/questions/910741/constructive-proof-of-pigeonhole-principle.

If I try to do induction on n, I get the base case with n=0. Here I first do 'intros.' and then 'induction n.'.

But I want the base case n=2. Is there a possibility in Coq do get that or am I on the wrong track?

Answer 1

The answer to the question you linked to contains this off-hand comment:

The case n=1 is impossible

This is good enough for a human mathematician, but not for Coq. You can tell Coq that you only want to prove cases where n >= 2 by adding that to the premises of the lemma:

Lemma pigeon_hole :
  forall m n,
  n >= 2 ->    (* added this *)
  m < n ->
  forall f,
  (forall i, i < n -> f i < m) ->
  exists i, i < n /\
  exists j, j < n /\ i <> j /\ f i = f j.

Now this statement should be provable. To get to a state where your induction starts at n = 2, you could argue like this on paper:

By cases on n.

• n = 0: impossible by the precondition n >= 2.
• n = 1: impossible by the precondition n >= 2.
• n >= 2: by induction...

You can do the same in Coq by using destruct on n twice:

Proof.
  intros.
  destruct n.

We made a case distinction between n = 0 and n >= 0 (i.e., n = S n' for some n'). We are in a proof state with:

H : 0 >= 2

This false hypothesis is exactly the kind of thing that omega can discharge for you:

  - omega.

In the other case we know that n >= 1. This is closer to n >= 2 but still not enough, so we can again do a case distinction on n to get rid of the n = 1 case:

  - destruct n.
    + omega.
    +

The proof state is now:

1 subgoal
m, n : nat
H : S (S n) >= 2
H0 : m < S (S n)
f : nat -> nat
H1 : forall i : nat, i < S (S n) -> f i < m
______________________________________(1/1)
exists i : nat,
  i < S (S n) /\ (exists j : nat, j < S (S n) /\ i <> j /\ f i = f j)

So all original uses of n have been replaced by S (S n), i.e., a value that is >= 2.

You should be able to continue from here using induction n.

Answer 2

The base is n = 0, but you can get rid of this. Then you have an inductive case where you are looking at the formula with S n every where. If you do destruct n as [ | n], then have two cases, the first on is for 1, and can probably get rid of that one again, then if do destruct n as [ | n] again, you will have to take care of the case 2. So this will play the role of your base case. Now, the remaining case will be about the same formula but where the initial n is replace by S (S (S n)) and the induction hypothesis is about the formula is already true for S (S n). That will give you an induction proof starting with base case n = 2.

But still the statement is true for n = 0 and n = 1 and you need to prove these cases on the side.

Second possibility (which would work for a base case at a higher constant)

Alternatively, you can get of the base case by showing that n is 0 is not possible, then when looking at the inductive case, you can start the proof by

destruct (le_lt_dec 2 n).

This will give you two cases: one where 2 <= n and you have to prove the property for S n, and one where n < 2. For the latter, you should be able that this is not possible (I did not check whether you should 2 or 1 as the testing bound).