The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-10-02T12:54:53+02:00, Jason Gross wrote:

> You might have used some axioms accidentally via tactics in,
> e.g., pigeonhole_principle_exmid_eq.  Try [Print
> Assumptions pigeonhole_principle_exmid_eq.]
> (replacing pigeonhole_principle_exmid_eq with whatever theorem you
> want to check) to see if it depends on axioms.  (I'm
> suggesting pigeonhole_principle_exmid_eq because I don't see how that
> is possible without classical axioms.)

Thanks for pointing it out.

Print Assumptions pigeonhole_principle_exmid_eq.

=>

Axioms:
appears_in_dec : forall (X : Type) (x : X) (l : list X),
                 {appears_in x l} + {~ appears_in x l}

I had introduced a

Parameter appears_in_dec :
  forall {X : Type} (x : X) (l : list X),
    {appears_in x l} + {~ appears_in x l}.

to define a function used in the proof of pigeonhole_principle_exmid_eq.
I was going around in circles!

Best regards,
Raghu.

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