1

我试图展开Fixpoint定义并获得定义的主体。但是 Coq 不会从字面上给出定义的主体。相反，它给了我一些以 开头的东西(fix ...)，我无法使用。

例如，从Coq.Init.Wf证明以下内容

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 方法更感兴趣。

4

0 回答 0