coq 中的应用程序相等性证明

Question

我有一个这样的应用程序序列 (f (f (f x)))，f 是一个任意函数和任何应用程序编号序列。我想证明 f(x y) 和 (x (f y)), x = (f f f ...) 和 y = 任意值，它们是相等的。我需要以下代码中的证明：

Fixpoint r_nat {A : Type} (a : nat) : A -> (A -> A) -> A :=
  match a with
    |S n => fun (x0 : A) (a0 : A -> A) => r_nat n (a0 x0) a0
    |0 => fun (x0 : A) (_ : A -> A) => x0
  end. 


Theorem homomo_nat : forall {T} (f : T -> T) (h : T) (x : nat), (r_nat x (f h) f) = f ((r_nat x) h f) .
compute.
??.
Qed.

我尝试展开和细化但不起作用。

Answer 1

这应该可以通过对 x 的归纳来解决，应用的次数 f。

Answer 2

我将参数 (x:nat) 移到了 (h:T) 之前。这使得归纳假设更强——它适用于 all h。那么证明就是：

Theorem homomo_nat : forall {T} (f : T -> T) (x:nat) (h : T), (r_nat x (f h) f) = f ((r_nat x) h f) .
Proof.
  induction x.
  reflexivity.
  intros. apply IHx.
Qed.

如果您愿意，您也可以 "move the arguments around" 使用策略来保留您的原始定理...从 intros; generalize dependent h.

开始

coq 中的应用程序相等性证明

Proof of application equality in coq

functional-programming

coq

proof