The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 07/29/2014 05:10 PM, Jonathan wrote:
> Coming up with one that will work in all cases is turning out to be 
> quite difficult.

It wasn't that difficult - skolemize_evars just needed some slight 
modifications:

Ltac dep_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
                           let x:=(eval pattern H' in VT) in
                           match x with
                               ?x' _ =>
                               evar (f:forall (a:W'), x' a); unify eV 
(f H'); subst f
                           end
                       end
                   end
             end
    end.

This seems to work at least in the very few cases I've tried so far.  
The Ltac is ugly, and probably highly inefficient in goals with many 
hypotheses, but most of that is due to not being able to use certain 
Ltac idioms (like reverting hypotheses while iterating over them) that 
due to Coq's conservative ways would alter the instantiatability of the 
very evars we're trying to "save".

It also certainly does produce redundant proofs, as one ends up needing 
to instantiate the skolem function with things like match expressions 
that recapitulate some of the proof steps between skolemization and 
eventual instantiation.  At least you no longer need to know what the 
correct instantiation is a-priori.

After using it a bit, it just makes me wonder what it would take to get 
Coq to be less conservative with its evar instantiation rules - because 
skolemization is doing so little to accomplish a workaround to these 
rules, but that workaround ends up having a price.

-- Jonathan