coq - 在包含局部变量的调用上与 Ltac 匹配

Question

我有一个包含对一些引理的调用的目标 foo在比赛的分支内。该调用使用变量 R 作为其参数之一。分行本地:

| SomeConstr => fun R => .... (foo a b c R) ....

我想在 foo 上执行测试版扩展使调用变为:

| SomeConstr => fun R => .... ((fun d => foo a b c d) R) ....

这将使我能够进一步概括 (fun d => foo a b c d) ，这将不再依赖于分支的局部变量。由于我正在处理非常大的证明，因此我想使用 Ltac 来编写它。这是一个尝试:

match goal with
| [ |- context[(foo ?A ?B ?C ?R)] ] =>
  let d := fresh "d" in
  replace (foo A B C R) with ((fun d => foo A B C d) R)
end.

然而，“没有匹配的匹配子句”失败了。如果我更换 match 的主体分支与 idtac它仍然失败，所以问题显然是由于未能匹配给定的表达式造成的。但是，如果我少匹配一个参数，则匹配成功。例如:

match goal with
| [ |- context[(foo ?A ?B ?C)] ] =>
  idtac A; idtac B; idtac C
end.

在连续行中打印“a”、“b”和“c”。我也可以说:

match goal with
| [ |- context[(foo ?A ?B ?C)] ] =>
  let d := fresh "d" in
  replace (foo A B C) with (fun d => foo A B C d) by auto
end.

这成功了，但有趣的是目标仍然没有改变，即。电话仍然是形式 (foo a b c R)而不是 ((fun d => foo a b c d) R) .我在这里做错了什么？

Answer 1

replace战术执行β减少。你可以通过写作看到这一点

Goal True.
  replace True with ((fun x => x) True) by auto.

如果您改为使用 change策略(仅当 replace 的附带条件可以通过 reflexivity 解决时才有效)，那么它应该可以工作。例如，

Goal True.
  change True with ((fun x => x) True).

将目标更改为 (fun x : Prop => x) True .

这是未记录的，我已将其报告为 an issue on GitHub .