I have two setoids and bisimilar:
Definition of lang_iff:
Definition lang := str -> Prop.
Definition lang_iff (s1 s2: lang): Prop :=
forall (s: str),
s \in s1 <-> s \in s2.
The setoid lang_setoid:
Add Parametric Relation: lang lang_iff
reflexivity proved by lang_iff_refl
symmetry proved by lang_iff_sym
transitivity proved by lang_iff_trans as lang_setoid.
Definition of bisimilar:
CoInductive bisimilar : lang -> lang -> Prop :=
| bisim : forall (P Q: lang),
...
-> bisimilar P Q.
The bisimilar_setoid:
Add Parametric Relation: lang bisimilar
reflexivity proved by bisimilar_refl
symmetry proved by bisimilar_sym
transitivity proved by bisimilar_trans as bisimilar_setoid.
These are proven to be equivalent:
Theorem bisimilar_is_equivalence:
forall (P Q: lang),
bisimilar P Q <-> lang_iff P Q.
I can manually rewrite between them with some acrobatics, but was wondering if there is a way to help Coq to see that it can rewrite between two setoids and make the following possible without Fail:
Example example_rewriting_using_lang_iff_in_bisimilar:
forall (P Q: lang)
(pq: lang_iff P Q),
bismilar Q P.
Proof.
intros.
Fail rewrite pq.
Fail reflexivity.
Abort.
The reason for this question is that it is useful to take some steps with coinduction in bisimilar and then resolve an equivalence with lang_iff.
A second part of this question is whether we need to preprove all the morphisms from lang_iff in bimisilar or if there is some command to reuse them?
You can register bisimilar as a morphism for lang_iff:
Add Parametric Morphism : bisimilar
with signature lang_iff ==> lang_iff ==> iff as bisimilar_lang_morphism.
Proof.
intros ?? H ?? H'.
apply bisimilar_is_equivalence in H, H'.
split; intro H0.
now rewrite <- H, H0.
now rewrite H, H'.
Qed.
And now rewriting works in your proof script:
Example example_rewriting_using_lang_iff_in_bisimilar:
forall (P Q: lang)
(pq: lang_iff P Q),
bisimilar Q P.
Proof.
intros.
rewrite pq.
reflexivity.
Qed.