Unify handling of proof mode terms

[MackieLoeffel]

This PR unifies the handling of proof mode terms following the Rocq implementation: It first introduces a tactic ispecialize to specialize a given Iris hypothesis with a proof mode term. Then it introduces an ihave tactic that allows to introduce a pure entailment into the proof mode. Tactics that use a proof mode term can then simply call the iHave function provided by ihave to parse a given proof mode term. This is then used to refactor iapply to a sequence of ihave and ispecialize following the Rocq implementation.

There are open TODOs about changing iapply to be able to introduce and instantiate mvars (see the tests). This is currently blocked on the use of type class search, see #iris-lean > Issues with typeclasses in the proof mode.

Additionally, this PR does some small refactorings:

• It makes ⊢ a definition EmpValid like in Rocq instead of just a notation. This prevents typeclass problems for IntoEmpValid.
• It introduces the ⊢@{PROP} like in Rocq to specify the bi of an entailment.
• It adds the Goals type for collecting the goals generated by a tactic and automatically putting dependent goals last.

[lzy0505]

The failing test exact_forall' actually worked before (with an extra istart), and

theorem apply_forall4 [BI PROP] (P Q : α → PROP) (a : α) : (∀ x, P x -∗ Q x) ⊢ P a -∗ Q a := by
  iintro H HP
  iapply H $! ?_ with HP

worked before, but now fails.

Seems like we did a slightly better job at instantiating mvars. But I don't know if we should make some ad-hoc fixes for these cases, or wait until we have a better general solution.

[MackieLoeffel]

Indeed. The test worked before because of the isDefEq here. This isDefEq felt a bit random and only works in the special case were we don't need to strip anything from the goal. So I removed it with the plan to have a more general solution that would make this unnecessary. But I can also add it back if we want to make this test work.

[lzy0505]

This isDefEq felt a bit random and only works in the special case were we don't need to strip anything from the goal. So I removed it with the plan to have a more general solution that would make this unnecessary. But I can also add it back if we want to make this test work.

I'm fine with not adding it. I think the other example I mentioned fails for a similar reason. The PR looks great!

[markusdemedeiros]

Yep, this looks sweet. I updated the branch, you can see in my latest commit that I updated some new proofmode code to use the new spats.

Unless you want to wait for anyone else to look it over, I can merge.

One piece of personal bikeshedding (which does not block this PR): is there any way you'd consider ditching the $! syntax from Iris-Rocq? The more I think about it the more I like the idea of prefixing pure specializations with % to match our other syntax.

[MackieLoeffel]

The changes you pushed look good to me. From my side, this MR can be merged. I have some more changes building on top of this MR, starting with #108

I agree that we should think about the proof mode specialization patterns. Let's discuss it on Zulip.