结合两个假设并在Coq中创建新的假设

问题描述

我想知道假设destruct H as (H1 & H2).上的H : p /\ q会创建两个假设H1 : p和H2 : q，如果有任何策略可以反过来。也就是说，采用两个假设，并与它们结合起来。

解决方法

使用assert策略有两种可能：

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.