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

Question

我的目标是foo在比赛分支中包含对某些引理的调用.该调用使用R分支的本地变量作为其参数之一:

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

我想执行beta扩展,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.

这是没有记录的,我已将其报告为GitHub上的一个问题.