重写适用于=，但不适用于<->。 （iff）在Coq中 [英] rewrite works for = but not for <-> (iff) in Coq

问题描述

在证明过程中，我需要满足以下条件，其中我需要将 value t 替换为 normal_form步骤t

I have the following during a proof, in which I need to replace normal_form step t with value t as there is a proven theorem that there are equivalent.

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 出现，目标中的 但不是 。

Now, I can use this theorem to rewrite normal_form occurrences in the hypotheses, but not in the goal. That is

rewrite nf_same_as_value in H1; rewrite nf_same_as_value in H2.

在该假设下有效，但重写nf_same_as_value。在目标上给出：

works on the hypothesis, but rewrite nf_same_as_value. on the goal gives:

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

在这里目标的重写是否可行从理论上讲，还是一个实现问题？

Is the rewrite on the goal here impossible theoretically, or is it an implementation issue?

-编辑-

我的困惑是，如果我们定义 normal_form step = value ，重写就可以了。如果我们为全部t定义，则normal_form步骤t<->值t ，则如果 normal_form步骤没有用引号引起来，则重写有效，但如果存在，则不起作用。

My confusion here is that if we define normal_form step = value, the rewrite would have worked. If we define forall t, normal_form step t <-> value t, then the rewrite works if normal_form step is not quoted in an existential, but does not work if it is in an existential.

适应@Matt的示例，

Adapting @Matt 's example,

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*) 

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

What confuses me is why the last step has to fail.

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

此故障与功能扩展有关吗？

Is this failure related to functional extensionality?

错误消息特别令人困惑：

The error message is particularly confusing:

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

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

There is exactly one subterm matching R1 _ _, namely R1 x x.

此外，如果使用了 ，则每个@larsr都可以进行重写

Also, per @larsr, the rewrite works if 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.

在这里添加的东西是什么 p>


What did eexists add here?

推荐答案

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

The rewrite cannot go under the existential quantifier. You'll need to instantiate t' first before you can do the rewrite. Note that econstructor may be a useful tactic in this case, which can replace the existential quantifier with a unification variable.

编辑以回应OP的评论

对于平等，这仍然行不通。例如，尝试：

This will still not work for equality. As an example, try:

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）下重写。 的实现存在x：A，P 实际上只是 ex A（fun x => P x）的语法，所以重写失败不是因为iff，而是因为 rewrite 策略不想进入中 x 的约束下（fun x = > P x）。似乎可以使用 setoid_rewrite 来做到这一点，但是，我对此没有任何经验。

The issue is not actually about equality vs. iff, the issue relates to rewriting under a binding (in this case a lambda). The implementation of exists x : A, P is really just syntax for ex A (fun x => P x), so the rewrite is failing not because of the iff, but because the rewrite tactic does not want to go under the binding for x in (fun x => P x). It seems as though there might be a way to do this with setoid_rewrite, however, I don't have any experience with this.

这篇关于重写适用于=，但不适用于<->。 （iff）在Coq中的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！