The Coq mailing list

[Ilya Sergey <ilya.sergey AT imdea.org>]

Dear John.

 

The second is "pigeonhole_principle".  With or without LEM I run into the same
problem: a goal of n < m in a context of n < S m, which is clearly unprovable.
If induction on l1 is the right way to start this proof, what is the next
creative step?  So far I have:

    Theorem pigeonhole_principle: forall (X:Type) (l1 l2:list X),
      (forall x, appears_in x l1 -> appears_in x l2)
        -> length l2 < length l1
        -> repeats l1.
    Proof.
      move=> X.
      elim=> [|x xs IHxs] l2 Happ Hlen.
        inversion Hlen.
      apply repeats_tail.
      apply: IHxs => // [z ?|].
      apply: Happ. by constructor.
    Admitted.

Since you're using SSReflect anyway, I'd recommend you to take a look on some of the functions from the seq module, in particular, those that have to do with filtering (assuming the equality is decidable).

Essentially, if you build your induction on the "long" list, in the constructor case you need to consider two options: whether the head element 'x' does occur in the tail of the long list, or it doesn't. The first case is easy to prove. 

In the second case, you need to remove 'x' from the second, shorter list before using the induction hypothesis. The function filter would be useful here. Then you apply the induction hypothesis to the new shorter list xs'. Here is the proof up to this point.

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

Require Import ssreflect ssrbool ssrnat eqtype ssrfun seq.

Variable A : eqType.

Fixpoint has_repeats (xs : seq A) :=

  if xs is x :: xs' then (x \in xs') || has_repeats xs' else false.

Theorem pigeonhole xs1 xs2 :

        size xs2 < size xs1 -> {subset xs1 <= xs2} -> has_repeats xs1.

Proof.

elim: xs1 xs2=>[|x xs1 IH] xs2 //= H1 H2. 

case H3: (x \in xs1) => //=. 

pose xs2' := filter (predC (pred1 x)) xs2.

apply: (IH xs2').

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The rest of the proof is essentially by a number of rewritings using lemmas from seq (inE, mem_filter, count_filter, count_predC etc.).

Cheers,

Ilya