Take a conjunction of two hypotheses and create a new hypothesis in Coq

Question

I'm wondering as destruct H as (H1 & H2). on hypothesis H : p /\ q creates two hypotheses H1 : p and H2 : q, if there is any tactic that does the other way around. That is, taking two hypotheses and creating one with conjunction of those.

Answer 1

Here are two possibilities, using the assert tactic:

Goal forall A B : Prop, A -> B -> A /\ B.
Proof.
intros A B HA HB.
assert (H1 : A /\ B). { now split. }
assert (H2 := conj HA HB).
Abort.