Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type)


Chronological Thread 
  • From: "Kyle Stemen" <ncyms8r3x2 AT snkmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type)
  • Date: Mon, 17 Nov 2014 23:10:51 -0800

Did you manage to solve this with your inductive member technique?

I solved it by proving that since every item in l1 appears in l2, l1 can be converted into a list of indexes in l2 of where the l1 items are. It can be proved that the index list repeats since the indexes are nats, and nat has decidable equality.

Once you know which item in l1 is repeated and where the repeated items are, you can instantiate the repeats type.

On Sun, Nov 16, 2014 at 9:12 PM, Hugo Carvalho hugoccomp-at-gmail.com |coq-club/Example Allow| <mesvfd3x8t AT sneakemail.com> wrote:
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?




Archive powered by MHonArc 2.6.18.

Top of Page