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:
Can anyone help with this proof?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).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 .Qed.(**)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: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.Qed.(**)I've been working on a exercise from Software Foundations. It asks you to give a proof for the following theorem :Hi club!
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.
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.
- [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type), Hugo Carvalho, 11/17/2014
- Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type), Pierre-Marie Pédrot, 11/17/2014
- Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type), Kyle Stemen, 11/18/2014
- Re: [Coq-Club] Pigeonhole Principle without excluded middle (or decidable type), Kyle Stemen, 11/18/2014
Archive powered by MHonArc 2.6.18.