我在证明期间有以下内容,我需要替换为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
添加了什么?