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.