Coq证明代码运行报Not the right number of missing arguments错误如何解决

你编写的exists bool [true] [false]不符合Coq战术语法规则：Coq中空格代表函数应用，该写法会被解析为尝试将bool作为函数传入[true]、[false]两个参数后，再传递给exists战术，和exists单次接收1个实例参数的要求不匹配，因此抛出参数数量错误。

有两种可直接运行的修正方式：

• 方案1：拆分exists调用，每次实例化一层存在量词，完整代码如下：

Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1 ++ l2 <> l2 ++ l1.
Proof.
  exists bool.
  exists [true].
  exists [false].
  simpl.
  discriminate.
Qed.

• 方案2：Coq 8.12及以上版本支持单次exists传入多个实例参数，参数之间用逗号分隔即可，完整代码如下：

Require Import Coq.Lists.List.
Import ListNotations.

Theorem con_not_com :
  exists A (l1 l2 : list A), l1 ++ l2 <> l2 ++ l1.
Proof.
  exists bool, [true], [false].
  simpl.
  discriminate.
Qed.

内容的提问来源于stack exchange，提问作者Serene M