Skip to content

Use `notypeclasses refine` in `iPoseProof*` helpers for `iDestruct`.

This MR ensures compatiblity with https://github.com/coq/coq/pull/10762 by using notypeclasses refine for the following:

  1. Applying the various helper lemmas for iPoseProof, i.e. tac_pose_proof_hyp and tac_pose_proof
  2. The base case of iAssumption, i.e. it now uses a Hint Extern with notypeclasses refine for from_assumption_exact : FromAssumption p P P. This also affects the unification with premises in iApply.

In addition, I have rewritten iIntoEmpValid to use a series of lemmas in a notypeclasses refine loops instead of the old fragile Ltac code. The advantage is that matching now happens up to unification, and we no longer need the eval zeta/hnf hacks that were present in this code.

An advantage of using notypeclasses refine in these pieces of code is that type class search is no longer triggered randomly. It basically avoids to https://github.com/coq/coq/issues/6583. Another advantage is that we now use the new unification algorithm in more places, which is often better behaved.

A disadvantage is that this MR breaks some code. Naturally, since type search search is no longer called randomly (it is basically delayed until the end of the iPoseProof), unification is often presented with more complicated goals because fewer TC arguments are resolved (over eagerly). As such, some proof mode tactics that used to succeed, will now fail. By using the new unification algorithm for iAssumption (item 2, above), I managed to reduce the number of cases where this problem appeared. However, some tactics will of course behave differently because the new unification algorithm is used.

Although breakage is inevitable, the number of changes to the reverse dependencies are limited: Rustbelt (2 lines changed), gpfls (12 lines changed), Rustbelt-relaxed (12 lines changed), Iron (35 lines changed; this includes some code cleanup).

Edited by Robbert Krebbers

Merge request reports