coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Excluded middle and decidable equality

From: "N. Raghavendra" <raghu AT hri.res.in>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Excluded middle and decidable equality
Date: Fri, 04 Oct 2013 10:30:55 +0530
Cancel-lock: sha1:xKp1jbZKxLtqA8ctPpKCJdZQvkI=

At 2013-10-02T02:02:12-07:00, Daniel Schepler wrote:

> Lemma pigeonhole_principle_helper (X:Type) :
> forall hd l1 l2 : list X,
> (forall x:X, appears_in x l1 -> appears_in x (hd ++ l2)) ->
> length l2 < length l1 -> repeats (hd ++ l1).

Thanks for the nice proof. I wouldn't have come up with the way you use
the auxiliary list hd to carry out the induction.

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
- Re: [Coq-Club] Excluded middle and decidable equality, Daniel Schepler, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Jason Gross, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
    - Re: [Coq-Club] Excluded middle and decidable equality, Alan Schmitt, 10/02/2013
      - Re: [Coq-Club] Excluded middle and decidable equality, Cedric Auger, 10/02/2013
        
        Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/02/2013
  - Re: [Coq-Club] Excluded middle and decidable equality, N. Raghavendra, 10/04/2013