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]是做一個簡單的方法這，也適用於粘結劑。）