The Coq mailing list

[gallais <guillaume.allais AT ens-lyon.org>]

If you are willing to have membership / repeat predicates living
in Type (it is needed to write the `remove` function) then there
is a fairly simple constructive solution:
https://github.com/gallais/potpourri/blob/master/agda/poc/PigeonHole.agda

Now, it should not be too hard to move from a Prop-based formulation
to a Type-based one if you can decide equality of elements: you can
recover a membership predicate in Type by searching the list for an
element (decidable equality!) with the guarantee to find one (Prop-
based membership predicate!).

On 15/01/15 18:15, Ben wrote:
> here are some useful links:
>
> https://sympa.inria.fr/sympa/arc/coq-club/2014-11/msg00124.html
> https://gist.github.com/anonymous/e9493ce195219c4c2b18
>
> i tried to do it myself i failed -- i'm just a beginner.  at some point i 
> convinced myself that the right way to do it is
>
> - prove pigeonhole for lists of nats (using decidable equality)
>
> - convert the general problem into a problem about lists of nats by using 
> indices
>
> but i got bogged down in details.  also there's a Prop vs Type issue with 
> appears_in, i think.
>
> best, ben
>
> > On Jan 15, 2015, at 12:14 AM, Jiten Pathy 
> > <jpathy AT fssrv.net>
> >  wrote:
> >
> > Hello,
> > Trying to prove pigeon hole from SF using excluded_middle. Stuck while
> > doig the following. A hint on what i am doing wrong?
> >
> > https://gist.github.com/anonymous/548325557388612bd60e