在 Coq 中，重写适用于 = 但不适用于 <-> (iff)

我在证明期间有以下内容，我需要替换normal_form step t with value t因为有一个已证明的定理存在等价。

H1 : t1 ==>* t1' /\ normal_form step t1'
t2' : tm
H2 : t2 ==>* t2' /\ normal_form step t2'
______________________________________(1/1)
exists t' : tm, P t1 t2 ==>* t' /\ normal_form step t'

等价定理为：

Theorem nf_same_as_value
 : forall t : tm, normal_form step t <-> value t

现在，我可以用这个定理重写normal_form假设中出现的情况，but not在目标中。那是

rewrite nf_same_as_value in H1; rewrite nf_same_as_value in H2.

对假设有效，但是rewrite nf_same_as_value.目标上给出：

Error:
Found no subterm matching "normal_form step ?4345" in the current goal.

Is the rewrite这里的目标在理论上是不可能的，还是一个实施问题？

- 编辑 -

我的困惑是，如果我们定义normal_form step = value，重写会起作用。如果我们定义forall t, normal_form step t <-> value t，那么rewrite有效，如果normal_form step不在存在主义中被引用，但如果在存在主义中则不起作用。

改编@Matt的例子，

Require Export Coq.Setoids.Setoid.
Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Requal : R1 = R2. 
Admitted. 

Theorem Requiv : forall x y, R1 x y <-> R2 x y. 
Admitted. 

Theorem test0 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requal in H. (*works*) rewrite Requal. (*works as well*) 

Theorem test2 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite <- Requiv in H. (*works*) rewrite Requiv. (*fails*) 

让我困惑的是为什么最后一步必须失败。

1 subgoal
y : Prop
H : R1 y y
______________________________________(1/1)
exists x : Prop, R1 x x

这种失败与功能外延有关吗？

错误信息特别令人困惑：

Error:
Found no subterm matching "R1 ?P ?P0" in the current goal.

仅有一个子项匹配R1 _ _，即R1 x x。

另外，根据@larsr，如果重写有效eexists is used

Theorem test1 : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. eexists. rewrite Requiv. (*works as well*) apply H. Qed.

做了什么eexists在这里添加？

重写不能属于存在量词。你需要实例化t'首先，然后才能进行重写。注意econstructor在这种情况下可能是一种有用的策略，它可以用统一变量替换存在量词。

编辑回应OP的评论

这仍然无法实现平等。举个例子，尝试：

Inductive R1 : Prop -> Prop -> Prop :=
|T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
|T2_refl : forall P, R2 P P.

Theorem Req : forall x y, R1 x y = R2 x y. 
Admitted. 

Theorem test : forall y, R2 y y -> exists x, R1 x x. 
Proof.
  intros. rewrite Req. (*rewrite still fails*)

这个问题实际上不是关于相等与 iff 的问题，这个问题与绑定（在本例中是 lambda）下的重写有关。实施情况 https://coq.inria.fr/library/Coq.Init.Logic.html of exists x : A, P实际上只是语法ex A (fun x => P x)，所以重写失败不是因为 iff，而是因为rewrite战术不想受到约束x in (fun x => P x)。似乎有一种方法可以做到这一点setoid_重写 https://coq.inria.fr/refman/Reference-Manual029.html#sec756，但是，我对此没有任何经验。