Skip to content

Improve performance of `set_solver`

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

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)

Merge request reports