Fix setoid rewriting for function application in Iris
Some of you (me included) might have struggled rewriting into f a using H : f ≡ g. Today, a user called Yannick Zakowski discovered a fix by reading rewrite's error message, and I adapted this to Iris:
From iris.algebra Require Import ofe.
Instance equiv_ext_discrete_fun {A B} :
subrelation (≡@{A -d> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance equiv_ext_ofe_mor {A B} :
subrelation (≡@{A -n> B}) (pointwise_relation A (≡)).
Proof. done. Qed.
Instance dist_ext_discrete_fun {A B n} :
subrelation (dist n (A := A -d> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
Instance dist_ext_ofe_mor {A B n} :
subrelation (dist n (A := A -n> B)) (pointwise_relation A (dist n)).
Proof. done. Qed.
I'm going to test this in my project first, to verify the performance implication and robustness, and to find again good testcases, but I thought I'd record this here in an issue.