coq - coq intros 模式可以在最合适的连接机会处拆分吗？

Question

我想知道是否有一些介绍模式可以介绍 A /\ B /\ C为

H1: A /\ B
H2: C

我知道这 intros [H1 H2]会产生

H1: A
H2: B /\ C

但无法弄清楚如何为另一个方向配置支架。这是一个简单的例子；但我有一个更复杂的连词和析取组合，我更喜欢从右到左破坏。

谢谢，

标签： coq

Answer 1

Coq 中的_ /\ _符号是右结合二元运算符，所以A /\ B /\ C真的代表A /\ (B /\ C). 如果您想构建一些A /\ B，您应该首先完全分解/\( intros [HA [HB HC]].，您可以任意嵌套模式)，然后构建A /\ B假设（例如使用assert (A /\ B) as HAB by (split ; [exact HA| exact HB]).或您喜欢添加假设的任何其他方式）。

在更复杂的设置中，您可能想要编写引理and_assoc : forall A B C, A /\ B /\ C -> (A /\ B) /\ C并使用视图模式。从一个目标开始， A /\ B /\ C -> P您可以使用intros [HAB HC]%and_assoc.获取HAB : A /\ Band HC : C：该pat%and_assoc部分说and_assoc应该首先应用于顶级假设，然后进一步破坏 with pat。