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.