The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Here's a first attempt at a skolemizing tactic.  I think it will only 
work for non-dependent hypotheses, though.  Coming up with one that will 
work in all cases is turning out to be quite difficult.

[the following was only tested in the trunk version, not in 8.4]

Ltac name_evars id :=
  repeat match goal with |- context[?V] => is_evar V; let H := fresh id 
in set (H:=V) in * end.

Ltac skolemize_evars :=
  repeat
    match goal with
        H := ?V : ?T, H' : ?T' |- _ =>
             match goal with
               | H2 := ?V2 : _ |- _ => has_evar V2; match H2 with H' => 
fail 2 end
               | _ => idtac
             end;
             match V with
                 context[?eV] =>
                 is_evar eV;
                   match V with
                     | context[H'] => fail 1
                     | _ => idtac
                   end;
                   match type of H' with
                       (?W') =>
                       match type of eV with
                           ?VT =>
                           let f:=fresh in
                           evar (f:W'->VT); unify eV (f H'); subst f
                       end
                   end
             end
    end.

Goal forall (n : nat)(b : bool)(f : nat->bool)(P: bool->bool->Prop),
       exists b' n', P (f n') b <-> P b' (f n).
intros i j f P.
do 2 eexists.
name_evars e.
skolemize_evars.
Abort.

-- Jonathan