证明两个函数的外延相等

Question

我想出了函数 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.

我被困在这里。我真的想不出一个有用且更容易证明的引理。在没有显式累加器的情况下，如何证明直接式和基于累加器的递归函数的相等性？

Answer 1

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

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 的策略来实现归纳成功的更一般的目标。

Answer 2

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

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

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

然后证明很容易完成

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.