How to duplicate a hypothesis in Coq?

Question

During a proof, I encountered an hypothesis H. I have lemmas: H -> A and H -> B.

How can I duplicate H in order to deduce two hypotheses A and B ?

edited: More precisely, I have:

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

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

But, I want to get:

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

Fissionable

Answer 1

If you absolutely need to use an assumption multiple times as you suggested, you can use forward-reasoning tactics such as assert to do so without clearing it from the context, e.g.

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

You can also do something like assert (H' := H). to explicitly copy H into H', although you can usually resort to a more direct way for getting what you want.

Gerek

Answer 2

Why do you think that you need to duplicate the hypothesis? If you are using it in a proof, it won't become unavailable. See this example:

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.

Origan

I need both hypotheses A and B to prove a single goal. I can not split it. And when I do apply lemma1 in H H indeed gets unavailable and is replaced by A. – Fissionable

I extended my question with a sketch of the required transformation. As I said apply l1 in H replaces X to A inplace, so after it I can not apply l2 in H – Fissionable

Answer 3

If you want to duplicate hypothesis H, you can pose proof H as G. G is the name you choose for the generated hypothesis. as G can be omitted, in this way you let coq choose the name.

Trinitrophenol