当 simpl 或 cbn 策略无效时减少 coq

Question

我试图证明这一点：

Fixpoint max(a: nat)(b:nat): nat :=
if a <=? b then b
else a.
Example ex: forall n:nat, n = max n n.
Proof.
intros.
(...)

simpl 和 cbn 策略不会产生任何结果。 如果我调用 cbv [max]，那么我会得到一个 redex，然后我不知道如何继续证明。更准确地说，我得到：

n = (fix max (a b : nat) {struct a} : nat := if a <=? b then b else a) n n

如何摆脱这个 redex (fix max ....) n n ？

Answer 1

即使函数不是递归的，也有一个Fixpoint，这就是fix 的来源。请改用Definition。

只有当结构递减的参数（这里是n，第一个参数）以构造函数开头时，fix 才会减少。所以如果你的函数真的是递归的，你可以使用destruct n.。