Coq中的上下文表达式

Question

我想了解'上下文'表达式（与context模式相反）。在手动它被描述为：

上下文IDENT [EXPR]

IDENT必须表示由 匹配表达式的上下文图案结合的上下文变量。这个表达式的计算结果用expr的值替换了ident的 值的空洞。

有人可以共享一个例子说明这种构造的用法吗？我想它必须涉及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]是做一个简单的方法这，也适用于粘结剂。）