Improve performance of `set_solver`
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
See https://coq-speed.mpi-sws.org/d/1QE_dqjiz/coq-compare?orgId=1&var-project=iris&var-branch1=master&var-commit1=3f7f9f4e0cb404aa5936255288fa8e15a3be12b6&var-config1=coq-8.9.0&var-branch2=ci%2Frobbert%2Fset_unfold&var-commit2=6d17dc6d21fa2a5bdb40aa915d2748794fe8907c&var-config2=coq-8.9.0&var-group=(.)%2F%5B%5E%2F%5D&var-metric=instructions
This MR closes #29 (closed) and iris#232 (closed)