The Coq mailing list

[Dimitri Hendriks <hendriks AT cs.ru.nl>]

On Dec 14, 2004, at 16:12, Rene Vestergaard wrote:

> Please find below an example development of deskolemisation. 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?


I'm not sure if this is what you are asking for,
but to explicitly set the arguments A, B and P
of deskolemise implicit, you do:

Implicit Arguments deskolemise [A B P].

Section test.

Variables A B : Type.

Variable P : A -> B -> Prop.

Hypothesis H : exists F : A -> B, forall a : A , P a (F a).

Check (deskolemise H).

End test.

Dimitri

> Section Deskolemise.
>
> Variable A : Type.
> Variable B : Type.
> Variable P : A -> B -> Prop.
>
> Theorem deskolemise : (exists F : A -> B, forall a : A , P a (F a))
>                       -> forall a : A , exists b : B , P a b.
> intro skolemised. elim skolemised.
> intros F gConcl arg. exists (F arg). apply gConcl.
> Qed.
>
> End Deskolemise.