介绍模式示例 (p1 & ... & pn) 不起作用

Question

我正在阅读 Coq (8.5p1) 参考手册，

introduction via (p1 & ... & pn) is a shortcut for introduction via (p1,(...,(...,pn)...)); it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as conj or ex_intro; for instance, an hypothesis with type A/(exists x, B/\C/\D) can be introduced via pattern (a & x & b & c & d);

为了对此进行测试，我做了：

Goal forall A B C D: Prop, A/\(exists x:nat, B/\C/\D) -> D.
intros (a & x & b & c & d).

但是 Coq 告诉我：

Error: Not an inductive product.

我在其他一些变体中遇到了同样的错误，例如没有 -> D.

的变体

有人可以解释一下正确的用法吗（在一个很有用的例子中）？

Answer 1

由于您的目标以forall A B C D: Prop,开头，您需要先介绍A B C D：

intros A B C D (a & x & b & c & d).

我认为引入这个语法是为了摆脱嵌套的方括号，它可以在引入阶段用于解构。比较以下两个证明：

Goal forall A B C D: Prop,
    A /\ (exists x:nat, B /\ C /\ D) -> D.
intros A B C D (_ & _ & _ & _ & d). assumption. Qed.

Goal forall A B C D: Prop,
    A /\ (exists x:nat, B /\ C /\ D) -> D.
intros A B C D [_ [_ [_ [_ d]]]]. assumption. Qed.

我觉得第一个比较顺眼

介绍模式示例 (p1 & ... & pn) 不起作用

example for introduction pattern (p1 & ... & pn) does not work

coq