coq - 如何在 Coq 中复制假设？

Question

在证明过程中，我遇到了一个假设 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

Answer 1

如果你绝对需要按照你的建议多次使用一个假设，你可以使用前向推理策略，例如 assert这样做而不从上下文中清除它，例如

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

你也可以做类似 assert (H' := H). 的事情显式复制 H进入 H' ，虽然你通常可以采取更直接的方式来获得你想要的东西。