为什么不能在 Coq 中评估具有抽象值的固定定义表达式？

Question

我需要证明一个定理：

Theorem t : forall x, (fix f (n : nat) : nat := n) x = x.

非正式证明会像

一样简单

f is an identity function. So the result is the same as the input.

如果我在 intro x 之后使用 simpl，什么都不会改变。 Coq 不会尝试用抽象值 x 来计算 fix-function。然而，如果我对 x 进行归纳分析，Coq 会自动计算方程的左侧并将其简化为 0 和 S x.

为什么 Coq 禁止我用抽象值 x 计算 fix-function？

Answer 1

simpl（以及所有其他计算策略）应用转换规则。由于您的目标是平等，如果您的条件是可转换的，您可以直接使用 reflexivity。但是 (fix f (n : nat) : nat := n) x 和 x 是不可转换的。

减少fix的规则是iota转换。 manual（第 4 章“归纳构造的微积分”，§4.5.5“定点定义”，“归约规则”下）对其进行了描述。缩减规则要求参数以构造函数开头。通常，这是确保终止所必需的。手册中有一个与您的类似的示例：

The following is not a conversion but can be proved after a case analysis.

Coq < Goal forall t:tree, sizet t = S (sizef (sont t)).
Coq < Coq < 1 subgoal

  ============================
   forall t : tree, sizet t = S (sizef (sont t))

Coq < reflexivity. (** this one fails **)
Toplevel input, characters 0-11:
> reflexivity.
> ^^^^^^^^^^^
Error: Impossible to unify "S (sizef (sont t))" with "sizet t".

Coq < destruct t.
1 subgoal

  f : forest
  ============================
   sizet (node f) = S (sizef (sont (node f)))

Coq < reflexivity.
No more subgoals.

你要证明的等式实际上是某种形式的外延性。 Coq 没有作为原始规则的可扩展性，它可以在类型明确时派生。破坏显式 nat 论证正是这样做的：让你证明这种外延性属性。证明这种外延引理在 Coq 开发中相当普遍。

Theorem t : forall x, (fix f (n : nat) : nat := n) x = x.
Proof.
  destruct x; reflexivity.
Qed.

为什么不能在 Coq 中评估具有抽象值的固定定义表达式？

Why cannot evaluate a fix-defined expression with an abstract value in Coq?

coq