The Coq mailing list

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

Dear Rene,

Because the Implicit Arguments mechanism is not strong enough in general
to infer P from forall a, exists b, P a b statements, I wrote a little 
tactic that does that
and gives the inferred predicate as an argument to deskolemise.

Best,
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.
Proof.
intros [ f H ] a.
exists (f a).
apply H.
Qed.

End Deskolemise.

Implicit Arguments deskolemise [A B P].

Ltac skolemise :=
  let a := fresh "a" in
  let w := fresh in
  (
  intro a;
  match goal with
  |- (ex ?p) =>
    pose (w := p);
    pattern a in w;
    let w' := eval cbv delta [w] in w in
    match w' with
      (?R a) => apply (deskolemise (P := R)); clear w
    end
  end
  ).

Section test.

Variable A : Type.
Variable D : A -> Prop.

Lemma sam :
  (exists f, forall a, D a /\ ~ D (f a))
  -> forall a, exists b, D a /\ ~ D b.
Proof.
intro H.

(*
here [apply deskolemise.] fails;
Coq cannot infer that the 3rd implicit argument of [deskolemise]
should be [fun a b => D a /\ ~ D b].
*)

skolemise.
exact H.
Qed.

Print sam.

(*
ofcourse, instead of applying [deskolemise] we could also choose to
prove the implication directly, as follows.
I'd proof terms referring to [deskolemise] rather than
their unfolded version though.
*)

Ltac adhoc_hack_tac H :=
  let f := fresh "F" in
  let x := fresh "a" in
  (
  intro x;
  destruct H as [ f H ];
  exists (f x);
  exact (H x)
  ).

Lemma sam2 :
  (exists f, forall a, D a /\ ~ D (f a))
  -> forall a, exists b, D a /\ ~ D b.
Proof.
intro H.
adhoc_hack_tac H.
Qed.

Print sam2.