是否有一个策略,我可以在下面的示例中使用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.
...
您可能正在寻找以下行:
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将抱怨"无界" h
。