如何在 Coq 中复制假设？

Posted 2023-03-28

【中文标题】如何在 Coq 中复制假设？

【英文标题】：How to duplicate a hypothesis in Coq?

【发布时间】：2014-12-07 15:34:32

【问题描述】：

在证明过程中，我遇到了一个假设H。我有引理：H -> A 和 H -> B。

我如何复制H 以推导出A 和B 的两个假设？

已编辑： 更准确地说，我有：

lemma l1: X -> A.
lemma l2: X -> B.

1 subgoals, subgoal 1 (ID: 42)
H: X
=========
Y

但是，我想得到：

1 subgoals, subgoal 1 (ID: 42)
H1: A
H2: B
=========
Y

【参考方案1】：

如果您绝对需要按照您的建议多次使用一个假设，您可以使用诸如assert 之类的前向推理策略来执行此操作，而无需从上下文中清除它，例如

assert (HA := l1 H).
assert (HB := l2 H).

您还可以执行assert (H' := H). 之类的操作，将H 显式复制到H'，尽管您通常可以采用更直接的方式来获得所需的内容。

【参考方案2】：

为什么你认为你需要复制假设？如果您在证明中使用它，它不会变得不可用。看这个例子：

Parameter A B H : Type.
Parameter lemma1 : H -> A.
Parameter lemma2 : H -> B.

Goal H -> A * B.
intro; split; [apply lemma1 | apply lemma2]; assumption.
Qed.

【讨论】：

我需要假设 A 和 B 来证明一个目标。我不能拆分它。当我这样做时，apply lemma1 in H H 确实不可用并被 A 取代。

我用所需转换的草图扩展了我的问题。正如我所说的apply l1 in H 将 X 替换为 A 就地，所以在它之后我不能apply l2 in H