coq - 如何将 rhs 从 coq 中的相等性中拉出来

Question

如果我有以下内容:

H : some complicated expression = some other complicated expression

我想捕获

u := some other complicated expression

无需将其硬编码到我的证明中(即使用pose)

在 LTac 中是否有一种干净的方法可以做到这一点？

Answer 1

我确信还有其他 ltac 方法可以做到这一点，就我而言，我更喜欢使用 SSReflect 的上下文模式语言来做到这一点。 (您需要安装插件或使用包含 SSReflect 的 Coq >= 8.7):

(* ce_i = complicated expression i *)
Lemma example T (ce_1 ce_2 : T) (H : ce_1 = ce_2) : False.
set u := (X in _ = X) in H.

最终目标:

  T : Type
  ce_1, ce_2 : T
  u := ce_2 : T
  H : ce_1 = u
  ============================
  False

通常您可以越来越细化模式，直到获得相当稳定的匹配。

请注意，这恰好是 SSReflect 手册中第 8.3 节“上下文模式”的第一个示例。