logic - 如何在 Coq 中使用 apply 来“提取”一个含义

Question

我将用一个例子来说明。

H : R -> P -> Q

H0 : R

子目标：

(Q -> P) \ / (P -> Q)

所以我的问题是如何提取（P-> Q）。我已经有了 R，但是当我“在 H0 中应用 H”时，它会评估所有内容并给我 Q。

Answer 1

您可以执行以下任何操作：

specialize (H H0).

将 H 替换为H: P -> Q, 或：

pose proof (H H0) as H1

介绍H1: P -> Q

你也可以往前走：

right. exact (H H0).