如何化简Coq中的cofix表达式？以super_nat为例求证等式

针对你给出的余归纳类型与余递归函数，要证明forall x, more x = S x，可以通过以下步骤完成：

1. 展开余递归函数定义：先用unfold more将目标中的more展开为原始余递归定义，此时目标变为：

   (cofix more (x0 : super_nat) : super_nat := S x0) x = S x
   

2. 执行Beta化简：使用cbv beta策略对余递归函数的应用做Beta转换，这一步会将(cofix more (x0) := S x0) x化简为S x，目标随即变为S x = S x。

3. 自反性收尾：最后用reflexivity完成证明，因为等式两边完全一致。

完整证明脚本如下：

CoInductive super_nat := S : super_nat -> super_nat.
Fact unfold_super_nat : forall (n : super_nat), n = match n with S x => S x end.
Proof. intros n. destruct n. reflexivity. Qed.

CoFixpoint more x := S x.

Goal forall x, more x = S x.
Proof.
  intros x.
  unfold more.
  cbv beta.
  reflexivity.
Qed.

你也可以用更简洁的方式，直接用compute策略一步完成化简，替代unfold more和cbv beta：

Goal forall x, more x = S x.
Proof.
  intros x.
  compute.
  reflexivity.
Qed.

原理说明：余递归函数的定义本质是余固定点，但对于直接应用的场景，Beta转换完全合法，Coq的cbv或compute策略可以处理这类化简，将余递归函数的应用展开为定义体的实例化形式，最终得到可通过自反性证明的等式。

内容的提问来源于stack exchange，提问作者radrow