3

我在证明期间有以下内容，我需要替换为normal_form step t，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假设中的出现，但不能重写目标中的出现。那是

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.

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

- 编辑 -

我在这里的困惑是，如果我们定义normal_form step = value，重写就会起作用。如果我们定义forall t, normal_form step t <-> value t，则rewrite作品 ifnormal_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使用重写工作

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

这里eexists添加了什么？

4

1 回答 1

4

重写不能在存在量词下进行。您需要先实例化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）有关。 的实现exists x : A, P实际上只是 for 的语法，ex A (fun x => P x)因此重写失败不是因为 iff，而是因为该rewrite策略不想进入 for xin的绑定(fun x => P x)。似乎有一种方法可以用setoid_rewrite做到这一点，但是，我对此没有任何经验。

于 2015-12-12T16:36:07.180 回答