# Optimize iIntoEmpValid

This PR is the result of me trying to understand why `iPoseProof`

was very slow (taking up to 20s) in some instances in our Coq development (https://github.com/logsem/cerise). This happens in particular when: 1) the (Coq) context is large, and 2) the lemma passed to `iPoseProof`

starts with many forall quantifiers (up to ~35).

It seems then that the source of the slowness is `iIntoEmpValid`

, which is implemented as `first [ notypeclasses refine ... | notypeclasses refine | ... ]`

. The forall case is the second one, and it seems that with large contexts, the first `notypeclasses refine`

(which fails) is responsible for the majority of the time spent in the tactic. (On the example taking 20s, manually doing `do 35 notypeclasses refine (into_emp_valid_forall _ _ _ _); iIntoEmpValid`

only takes 1s.)

The optimization that I propose here is to add a "fast path" to `iIntoEmpValid`

for the `(_ -> _)`

and `(forall _, _)`

cases, where the application of the corresponding lemma is gated by an Ltac pattern matching. This avoids relying on unification to select the lemma to apply. The fix should be fully backwards compatible: if no "fast path" patterns match, we just fall back to the current implementation.

With this patch, the cumulated time for a full build of our cerise project (on a fast computer) goes from `75 min`

to `58 min`

, which I think is a good speedup.