Improve performance of `set_solver`

Merged Robbert Krebbers requested to merge ci/robbert/setunfold into master

This MR improves the performance of the tactic set_unfold, which is the core of set_solver. It does do this by introducing the following type class:

Class SetUnfoldElemOf `{ElemOf A C} (x : A) (X : C) (Q : Prop) :=
  { set_unfold_elem_of : x  X  Q }.

This type class is more specific than SetUnfold since it only applies to goals of the form x ∈ X. As such, type class search is much faster as it will never look through the definition of , which caused set_unfold to be very slow for the case of gset; see #29 (closed).

Note that compared to my proposal in #29 (closed) there is no need for any type class opaqueness anymore. This MR should also be fully backwards compatible, but to obtain optimal performance developments may want to change their SetUnfold (_ ∈ _) _ instances into SetUnfoldElemOf _ _ _. See iris@fdfed0e9 for an example.

Performance stats:

  • 69.61% improvement on the dreaded algebra/gset file in Iris
  • 2.23% overall improvement on Iris


This MR closes #29 (closed) and iris#232 (closed)

Merge request reports