coq - 如何从 coq 中的等式中拉出 rhs

如果我有以下几点:

H : some complicated expression = some other complicated expression

我想捕获

u := some other complicated expression

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

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

最佳答案

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

(* 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 节“上下文模式”的第一个示例。

关于coq - 如何从 coq 中的等式中拉出 rhs，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/44338252/