The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

Hi club!

I've been working on a exercise from Software Foundations. It asks you to give a proof for the following theorem :

Require ClassicalFacts.

Inductive appears_in {X:Type} (a:X) : list X -> Prop :=
| ai_here : forall l, appears_in a (a::l)
| ai_later : forall b l, appears_in a l -> appears_in a (b::l).

Inductive repeats {X:Type} : list X -> Prop :=
| rep_base : forall l x, appears_in x l -> repeats (x::l)
| rep_step : forall l x, repeats l -> repeats (x::l).

Theorem pigeonhole_principle: forall (X:Type) (l1 l2:list X),
   ClassicalFacts.excluded_middle ->
   (forall x, appears_in x l1 -> appears_in x l2) ->
   length l2 < length l1 ->
   repeats l1.
Proof.

 (**)

Qed.

Now, the comments on the exercise mention that it's possible to prove the theorem without the excluded middle hypothesis. Searching around on the internet, i've easily found solutions that replace the excluded middle by the hypothesis that the type X has decidable equality.

The way the comments were worded led me to believe that this should be possible without any sort of extra hypothesis whatsoever. Below is the strongest statement i've managed to prove:

Inductive member {X:Type} (a:X) : list X -> Type :=
  | HFirst : forall l, member a (a::l)
  | HNext : forall b l, member a l -> member a (b::l).

Theorem pigeonhole_principle: forall (X:Type) (l1 l2:list X),
   (forall x, member x l1 -> member x l2) ->
   length l2 < length l1 ->
   repeats l1.
Proof.

 (**)

Qed.

That is, i've proven the principle using the Type-analogue of "appears_in". For the curious (although i must warn you that it isn't by any means a pretty script), here's a link to the development : https://gist.github.com/anonymous/e9493ce195219c4c2b18 .

At this point i haven't been able to make any further progress. It seems like, since "repeats" is a Prop (and therefore the whole proof happens in a Prop context), it should be possible to switch the "member" in the hypothesis for "appears_in", but alas, my current strategy seems to depend on the Type-ness of the hypothesis, that is, simply switching "sig"s for "exists" doesn't work (crucially, i have a lemma whose statement has projections in it).

Can anyone help with this proof?