The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hello,

 If you work with the Development version of Coq , you may load the 
Logic.ClassicalEpsilon module,
which  asserts classical logic for Prop (by requiring Logic.Classical) 
and declares an axiom (the one called lift_ex
in Benjamin's message).


Axiom constructive_indefinite_description :
 forall (A : Type) (P : A->Prop),
 (exists x, P x) -> { x : A | P x }.

Then EM and lift_or can be derived as lemmas.


Pierre

Benjamin Werner wrote:

> Hello,
>
> In addition to Hugo's answer, note also that if you happen to be  
> working in classical logic
> (which then would be classical logic for Type) you can always lift  
> your hypotheses from
> Prop to Type, when you need to.
>
> For instance:
>
> Parameter EM : forall T : Type, T + (T->False).
>
> Lemma lift_ex : forall A P, (exists x, P x) -> {x:A| P x}.
> intros A P e; elim (EM {x:A| P x}); trivial; intro neg.
> assert (f:False).
> elim e; intros x p; apply neg; exists x; trivial.
> elim f.
> Qed.
>
> Lemma lift_or : forall A B, A\/B -> {A}+{B}.
> intros A B o; elim (EM ({A}+{B})) ; trivial; intros neg.
> assert (f:False); try elim f.
> elim o; auto.
> Qed.
>
>
> Cheers,
>
>
> Benjamin
>
>
> Le 3 sept. 06 à 15:01, Eric Jaeger (SGDN) a écrit :
>
> > Hi,
> >
> > After some time working with Coq, I've chosen for one of my  projects 
> > (in which I don't care about impredicativity or proof  irrelevance, 
> > but have difficulties to "eliminate" Prop hypothesis  with a Set 
> > goal) to work without using the Prop sort, but Set  instead... It's 
> > of course fine for my definitions, etc. and I was  happy to discover 
> > that tactics such as rewrite can use identity as  well as equality. 
> > However, I still have difficulties to get rid of  Prop - in 
> > particular as far as equality is concerned.
> >
> > As an example, if for "S:Set" I define "Inductive ind_id:S->S- 
> > >Set:=ii_intro:forall (a:S), ind_id a a", then the inversion tactic  
> > applied to an hypothesis "ind_id a b" will return "a=b", while I  
> > would prefer "identity a b".
> >
> > Is there a solution to work with Coq without using Prop at all ?  Or, 
> > at least, to have Coq generate indentity results instead of  equality 
> > results ?
> >
> > Thanks for any help, Eric Jaeger
> > --------------------------------------------------------
> > Bug reports: http://coq.inria.fr/bin/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >          http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club