为什么无法在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.

如果我使用simpl之后intro x,什么都不会改变.Coq不会尝试使用抽象值x来评估fix-function.但是如果我对x进行归纳分析,Coq将自动评估等式的左侧并将其减少为0和S x.

为什么Coq禁止我用抽象值x来评估修复函数？

Answer 1

simpl(以及所有其他计算策略)应用转换规则.由于您的目标是平等的,因此reflexivity如果您的条款可以兑换,您可以直接使用.但是(fix f (n : nat) : nat := n) x并且x不可兑换.

减少的规则fix是iota转换.它在手册中描述(第4章"归纳结构的微积分",§4.5.5"定点定义",在"缩减规则"下).缩减规则要求参数以构造函数开头.通常,这需要确保终止.手册中的示例与您的类似:

以下不是转换,但可以在案例分析后证明.

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.