The Coq mailing list

[Rene Vestergaard <vester AT jaist.ac.jp>]

Dear Jevgenijs,

Your proposal only eliminates the use of P (inside its scope), right? My 
interest lies outside the section and is not really related to P (as a 
local/global parameter).

In case it isn't clear, the idea is to use Theorem deskolemise to 
conclude forall-exists results from previously proved exists-forall 
results. I would like to do this without wrapping the(!) body of two 
considered predicates up as a function and pass to deskolemise in 
addition to the exists-forall proof. Doing so is not troublesome, of 
course, but it is not elegant, either, and it raises the entry level for 
parsing the proof.

Cheers,
RV

Jevgenijs Sallinens wrote:
>  > Rene Vestergaard wrote:
>  > When invoking it, the specific P needs to be listed in addition to the
>  > formula being deskolemised. Is there a nice/standard alternative whose
>  > uses are implicit about the P?
> Dear Rene,
>  
> I hope the following could help by hiding P with coercion.
> If nothing depends on specific structure of P, probably better to  
> declare it as global parameter.  
> Regards,
> Jevgenijs.
>  
>  
> Section Deskolemise.
>  
> Variable A : Type.
> Variable B : Type.
> Variable P : A -> B -> Prop.
> Coercion P: A >->  Funclass.
>  
> Theorem deskolemise : (exists F : A -> B, forall a : A , a (F a))
>                        -> forall a : A , exists b : B , a b.
> intro skolemised. elim skolemised.
> intros F gConcl arg. exists (F arg). apply gConcl.
> Qed.
>  
> End Deskolemise.
>
>