我试图展开Fixpoint
定义并获得定义的主体。但是 Coq 不会从字面上给出定义的主体。相反,它给了我一些以 开头的东西(fix ...)
,我无法使用。
Lemma Fix_F_eq :
forall (x:A) (r:Acc x),
F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
Proof. intros.
状态是:
...
______________________________________(1/1)
F x
(fun (y : A) (p : R y x) =>
Fix_F y (Acc_inv x r y p)) =
Fix_F x r
现在,Fix_F
在 RHS 上的定义与 LHS 完全相同:
Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
我试图通过以下方式使其trivial
平等:
unfold Fix_F at 2.
然而,我(fix Fix_F ... )
在 RHS 上得到了类似的东西,我不能再沿着这条线继续前进:
______________________________________(1/1)
F x
(fun (y : A) (p : R y x) =>
Fix_F y (Acc_inv x r y p)) =
(fix
Fix_F (x0 : A) (r0 : Acc x0) {struct r0} :
P x0 :=
F x0
(fun (y : A) (p : R y x0) =>
Fix_F y (Acc_inv x0 r0 y p))) x r
问题是:
有没有办法将上面的内容展开Fixpoint
到它的功能体上?
注意:我知道有一种解决方法可以证明这个例子。
Proof. intros. destruct r. simpl. trivial.
Defined.
但如果它是有效的,我对unfold
-ing 方法更感兴趣。