如何复制Coq中的假设？

Question

在证明期间,我遇到了一个假设H.我有lemmas: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',虽然通常可以采取更直接的方式为得到你想要的东西.