coq简介模式可以在最合适的机会进行分裂吗？

问题描述

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

H1: A /\ B
H2: C

我知道 intros [H1 H2]会产生

H1: A
H2: B /\ C

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

谢谢

解决方法

Coq中的_ /\ _表示法是一种右关联的 binary 运算符，因此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并使用 view 模式。从目标开始 A /\ B /\ C -> P您可以使用intros [HAB HC]%and_assoc.来获得HAB : A /\ B和HC : C：pat%and_assoc部分说and_assoc应该首先应用于最高假设，然后然后进一步pat破坏。