证明两个函数的扩展相等

问题描述

我想出了函数 applyN 的两个等效定义，它将给定的函数 f 应用于参数 x n 次：

Variable A : Type.

Fixpoint applyN1 (n : nat) (f : A -> A) (x : A) :=
  match n with
    | 0 => x
    | S n0 => applyN1 n0 f (f x)
  end.

Fixpoint applyN2 (n : nat) (f : A -> A) (x : A) :=
  match n with
    | 0 => x
    | S n0 => f (applyN2 n0 f x)
  end.

我想证明这些函数在 Coq 中是外延相等的：

Theorem applyEq : forall n f x,applyN1 n f x = applyN2 n f x.
Proof.
intros.
induction n.
reflexivity.  (* base case *)
simpl.
rewrite <- IHn.

然后我就卡在这里了。我真的想不出一个有帮助且更容易证明的引理。在没有显式累加器的情况下，您如何证明直接式递归函数和基于累加器的递归函数的等式？

解决方法

例如，你可以证明一个辅助引理

Lemma apply1rec n : forall k f x,k <= S n -> f (applyN1 k f x) = applyN1 k f (f x).

（我唯一需要证明的外部引理是 le_S_n : forall n m,S n <= S m -> n <= m 来自 Coq.PeanoNat）

然后证明很容易完成

Theorem applyEq : forall n f x,applyN1 n f x = applyN2 n f x.
Proof.
  intros n ? ? ; induction n as [|n IHn].
  - reflexivity.  (* base case *)
  - simpl.
    rewrite <- IHn,(apply1rec n n).
    * reflexivity.
    * apply Nat.le_succ_diag_r.
Qed.

我能够首先使用引理证明它

Lemma applyN1_lr : forall k f x,f (applyN1 k f x) = applyN1 k f (f x).

通过归纳证明，然后对 applyEq 再次使用归纳。

请注意，我在证明我的 applyN1_lr 时遇到的事情（并且可能阻止了您的证明尝试）是您需要具有 forall x : A,… 形式的一般归纳假设。事实上，你想用 f x 而不是 x 来应用这个假设，所以在固定的 x 上进行归纳将无济于事。要做到这一点，您可以完全避免引入 x，或者使用策略 revert x 或 generalize x 来实现归纳成功的更一般目标。

coq functional-programming theorem-proving