coq - Coq 中的 `context` 表达式

Question

我正在尝试理解“上下文”表达式（与context 模式相反）。在手册中是这样描述的：

上下文标识 [ expr ]

ident 必须表示由匹配表达式的上下文模式绑定的上下文变量。此表达式求值用 expr 的值替换 ident 值的空洞。

有人可以分享一个例子来说明这个结构的用法吗？我想它必须涉及match使用context模式，然后使用上述形式来使用匹配的上下文。

Answer 1

这是一个替换fst (a, _)witha和snd (_, b)with的示例b，但不涉及fst并snd应用于除了 pair 之外的任何东西：

Ltac unfold_proj_pair :=
    repeat match goal with
           | [ |- context G[fst (?a, _)] ]
             => let G' := context G[a] in change G'
           | [ |- context G[snd (_, ?b)] ]
             => let G' := context G[b] in change G'
           end.

（请注意，这cbn [fst snd]是一种更简单的方法，也适用于活页夹。）