Coq 中的 `context` 表达式

Question

我试图理解'context' 表达式（相对于context 模式）。在手册中描述为：

context ident [ expr ]

ident must denote a context variable bound by a context pattern of a match expression. This expression evaluates replaces the hole of the value of ident by the value of expr.

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

Answer 1

这是一个示例，将 fst (a, _) 替换为 a，将 snd (_, b) 替换为 b，但不涉及 fst 和 snd 应用于除对以外的任何事物：

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] 是一种更简单的方法，它也适用于活页夹。）

Coq 中的 `context` 表达式

`context` expression in Coq

coq

ltac