variadic-functions - 如何证明这个关于 eta 展开的引理？

Question

(here 是我目前工作的要点。)

Coq 带有一个关于 eta 减少的规则，允许我们证明如下内容:

Variables X Y Z : Type.
Variable f : X -> Y -> Z.

Lemma eta1 : (fun x => f x) = f.
Proof.
  auto.
Qed.

eta 规则不仅仅是一个等式重写，所以我们也可以在 Binder 下面使用它:

Lemma eta2 : (fun x y => f x y) = f.
Proof.
  auto.
Qed.

当然，人们会期望您可以将其概括为任意元数的 f。这是我天真的尝试:

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint toType(ts : list Type)(t : Type) : Type :=
  match ts with
  |[]    => t
  |u::vs => u -> (toType vs t)
  end.

Compute toType [X;Y] Z.

(*
     = X -> Y -> Z
     : Type
*)

Fixpoint etaexpand(ts : list Type) : forall t : Type, toType ts t -> toType ts t :=
  match ts as ts return forall t, toType ts t -> toType ts t with
  |[]    => fun t x => x
  |u::vs => fun t f (x:u) => etaexpand vs t (f x)
  end.

Compute etaexpand [X;Y] Z f.
(*
     = fun (x : X) (x0 : Y) => f x x0
     : toType [X; Y] Z
*)

Lemma etaexpand_id : forall ts t f, etaexpand ts t f = f.
Proof.
  induction ts; intros.
  auto.
  simpl.
  (*stuck here*)

我卡在了上述引理的归纳步骤上。自然地，我想使用归纳假设重写，但我不能，因为相关的子项出现在 Binder 下面。当然，我自己知道归纳假设应该可以在 Binder 下使用，因为它只是一个 eta 重写链。那么我想知道是否有一种聪明的方法来陈述并说服 Coq 相信这一事实。

Answer 1

如果有人好奇，here's我经过深思熟虑后提出的解决方案。

关键是要同时证明etaexpand ts t的以下“niceness”属性:

Definition nice{X Y}(F : Y -> Y) := (forall y, F y = y) -> forall f : X -> Y, 
  (fun x => F (f x)) = f.