Equivalence vs. Equality - Generalized Rewriting

[larsk21]

Currently, the bidirectional entailment ⊣⊢ is defined as equality in order to use Lean's rw tactic to rewrite with bidirectional entailments in proofs inside the framework (e.g. in proofs of the derived laws). https://github.com/larsk21/iris-lean/blob/bde762e5d24b2f3777b8c950dc5857b2e8f4f9c6/src/Iris/BI/DerivedConnectives.lean#L7

This requires the axiom equiv_entails, stating that equality is equal to entailments in both directions, which is used to resolve a bidirectional entailment (using an instance of AntiSymm). https://github.com/larsk21/iris-lean/blob/bde762e5d24b2f3777b8c950dc5857b2e8f4f9c6/src/Iris/BI/Interface.lean#L108-L111

The axiom is however not true for all separation logics, which is why setoids and quotient types need to be used to instantiate the separation logic interface with such logics (see readme). This is, however, not a viable solution, since Lean's Setoid type does not support parameterized equivalances, such as ={n}= from the Iris separation logic.

There are at least two possible solutions:

1. As soon as Lean supports generalized rewriting, we should change the equality = to an equivalence ≡ and rewrite with that.
2. We could instead extend the tactic rw' included in this project (currently used for rewriting with preorders, such as ⊢) to support equivalences as well. This is less prefered, since it would probably require a backtracking search and should really be part of a general solution for generalized rewriting outside of this project. Also, rw' should be replaced with Lean's generalized rewriting in the future.

see also Rewriting congruent relations