Eta转换策略？

Question

在下面的例子中，我可以使用一种策略来代替 replace 来简化这个表达式吗？

Require Import Vector.

Goal forall (n b:nat) (x:t nat n), (map (fun a => plus b a) x) = x.
Proof.
  intros n b x.
  replace (fun a => plus b a) with (plus b) by auto.
  ...

Answer 1

您可能正在寻找以下内容：

repeat change (fun x => ?h x) with h.

它允许您减少任意 arity 的函数。此解决方案使用 change 处理模式的能力（上述代码段中的 ?h）。

让我们给这个策略起一个更有启发性的名字，比如：

(* h is a dummy argument to make Coq happy, it gets shadowed with `?h` *)
Ltac eta_reduce_all_private h := repeat change (fun x => ?h x) with h.

Ltac eta_reduce_all := eta_reduce_all_private idtac.

如果我们尝试定义eta_reduce_all如下

Ltac eta_reduce_all := repeat change (fun x => ?h x) with h.

Coq 会抱怨 "unbounded" h.

Eta转换策略？

Eta conversion tactics?

coq

coq-tactic