如何解决Coq:在两个等效的 setoid 之间重写
我有两个 setoids 和双相似:
lang_iff 的定义:
Definition lang := str -> Prop.
Definition lang_iff (s1 s2: lang): Prop :=
forall (s: str),s \in s1 <-> s \in s2.
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.
bisimilar 的定义:
CoInductive bisimilar : lang -> lang -> Prop :=
| bisim : forall (P Q: lang),...
-> bisimilar P Q.
Add Parametric Relation: lang bisimilar
reflexivity proved by bisimilar_refl
symmetry proved by bisimilar_sym
transitivity proved by bisimilar_trans as bisimilar_setoid.
Theorem bisimilar_is_equivalence:
forall (P Q: lang),bisimilar P Q <-> lang_iff P Q.
我可以用一些杂技在它们之间手动重写,但想知道是否有办法帮助 Coq 看到它可以在两个 setoid 之间重写并在没有 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.
这个问题的原因是在双相似中采取一些联合归纳的步骤,然后用 lang_iff 解决等价是有用的。
这个问题的第二部分是我们是否需要在 bimisilar 中预先证明来自 lang_iff 的所有态射,或者是否有一些命令可以重用它们?
解决方法
您可以将 bisimilar
注册为 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.
现在在你的证明脚本中重写作品:
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.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。