证明两个函数的扩展相等

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 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.

Answer 2

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

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 来获得更普遍的归纳成功的目标。

证明两个函数的扩展相等

Proving extentional equality of two functions

functional-programming

theorem-proving

coq