用等价的及物性重写目标

Question

我想证明以下定理:

Theorem T5:
forall s t, (forall u, OoS s u <-> OoS t u) -> s = t.

我当前的背景和目标是:

1 subgoal
s, t : Entity
H : forall u : Entity, OoS s u <-> OoS t u
______________________________________(1/1)
(forall v : Entity, OoS s v <-> OoS s v / OoS t v) /
(forall v : Entity, OoS t v <-> OoS s v / OoS t v)

我想知道是否有可能使用隐含的等价将目标重写为forall v : Entity, OoS s v <-> OoS t v，因为两个等价的右侧部分是相同的。然后我会用假设的方法来完成我的证明。但我不知道这是否可能，以及如何做到这一点。

Answer 1

您可以在充分一致的上下文中使用setoid重写rewrite与任何等价关系，参见此文档页。

在您的特定情况下，它应该是这样的:

From Coq Require Import Setoid.
Context (Entity : Type) (OoS : Entity -> Entity -> Prop)
(s t : Entity) (H : forall v, OoS s v <-> OoS t v).
enter code here
Goal (forall v : Entity, OoS s v <-> OoS s v / OoS t v) /
(forall v : Entity, OoS t v <-> OoS s v / OoS t v).
Proof.
split; intros v; rewrite H; intuition.
Qed.

我将连接分开并引入v，以便rewrite H正确地统一OoS s ?x(可能有一种方法可以做到不使用绑定器下的setoid重写，但我对这些技术并不熟练)。