Coq自定义小于等于记号报Illegal application错误如何解决？

问题原因 #

报错的核心是记号定义中括号使用错误导致的语法解析异常：
你写的(bnot (beq A B) bnot(less A B))会被Coq解析为：将bnot (beq A B)这个Cond类型的项作为函数，传入bnot和less A B两个参数，而Cond本身不是函数类型，因此抛出非法应用错误。
同时你对band的参数包裹逻辑存在错误：band接收两个Cond类型的参数，需要分别为两个参数套上独立的括号。

解决方法 #

首先修正小于等于逻辑对应的表达式：A ≤ B等价于¬(¬(A = B) ∧ ¬(A < B))，对应到你的Cond构造子写法应该是：
bnot (band (bnot (beq A B)) (bnot (less A B)))
将正确的表达式替换到记号定义中即可，完整修正后的代码如下：

From Coq Require Import String.

Inductive Exp :=
| num : nat -> Exp
| var : string -> Exp
| add : Exp -> Exp -> Exp
| sub : Exp -> Exp -> Exp
| div : Exp-> Exp -> Exp.

Inductive Cond :=
| base : bool -> Cond
| bnot : Cond -> Cond
| beq  : Exp -> Exp -> Cond 
| less : Exp -> Exp -> Cond
| band : Cond -> Cond -> Cond.

Notation "A <=' B" := (bnot (band (bnot (beq A B)) (bnot (less A B)))) (at level 10).

验证效果 #

执行类型检查语句不会再报错：

Check var "x" <=' var "y".
(* 输出：var "x" <=' var "y"
     : Cond *)

注意：你测试用的"x"为string类型，不是Exp类型的var构造子实例，直接执行Check "x" <=' "y"仍然会报参数类型不匹配错误，需要替换为var "x" <=' var "y"，或者额外定义字符串到var的coercion自动转换。

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