如何複製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'，雖然通常可以採取更直接的方式爲得到你想要的東西。

Answer 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.