Bi-entailment and generalized rewriting

Stream: iris-lean

[Zongyuan Liu]

The Lean implementation defines OFE equivalence (≡) on BI propositions as definitionally equal to bi-entailment (⊣⊢): Equiv P Q := P ⊣⊢ Q. The Rocq implementation takes a different approach: ≡ comes from the OFE structure, ⊣⊢ is defined separately, and bi_mixin_equiv_entails connects the two.

1. I think both enforce the same constraint, but what was the rationale for defining Equiv P Q := P ⊣⊢ Q rather than following Rocq's approach?

I'm porting big_ops, but the Rocq proofs extensively use generalized rewriting which is currently missing in Lean.

2. Was the rw' tactic intended to support ⊣⊢ rewriting? If so, what's the path forward — extend rw' or a different approach?
3. In the meantime, what's the recommended approach for porting proofs that rely on generalized rewriting?

[Markus de Medeiros]

1: I'm not sure why exactly it is like this but it is equivalent.
2: There was some discussion of this in Lars König's original development which we have moved to proofmode.md. rw' is pretty limited. If you search in this channel there was some experiments with supporting generalized rewriting (search the Zulip for various attempts). You're free to pick this up if you want.
3: Generalized rewriting just searches for appropriate NonExpansive lemmas to apply around the your rewrite. We have been doing this by hand, and so far it has not been too hard. How bad is it in big_ops?

[Markus de Medeiros]

To rewrite R under a nonexpansive function f the pattern is generally something like refine .trans (f_ne.ne R) ?_). Generalized rewriting just automates the search for f_ne.ne.

[Joe Watt]

I'm far from an expert on this matter, but I thought I'd mention that mathlib has had a generalised rewriting tactic grw for a while now, see here for the implementation and documentation.

Unlike Rocq's generalised rewriting, grw (as with rw) doesn't support rewriting under binders. I'm not sure how big of a limitation this is as I'm not an expert here. I also wonder if Iris could benefit from using this instead of rw', though I imagine this tactic (along with its dependencies) would need to be moved out of mathlib for that.