COQ中如何在同一引理中对Z和R类型同时使用<=运算符？

报错原因 #

该报错是因为Coq的比较运算符<=是类型敏感的，会优先匹配当前打开的类型作用域（scope）规则：如果你当前默认启用了实数R的作用域，<=会被识别为实数上的小于等于关系，要求两侧参数都为R类型。你写的结论n <= (floor x)里n和floor x都是Z类型，自然会触发类型不匹配的报错。

正确的引理写法 #

你只需要显式标注结论里的<=是整数Z上的比较关系即可，有两种常用写法：

1. 用作用域后缀%Z标注整个比较表达式：

Lemma l: forall (n:Z) (x:R), (IZR n) <= x -> (n <= floor x)%Z.

2. 直接调用整数比较的定义Z.le：

Lemma l: forall (n:Z) (x:R), IZR n <= x -> Z.le n (floor x).

能不能同时在Z和R类型上用<=运算符？ #

可以，Coq支持运算符重载，只需要通过作用域标注明确运算符对应的类型即可：

• 实数比较可以加%R后缀，例如(IZR n <= x)%R
• 整数比较可以加%Z后缀，例如(n <= floor x)%Z

如果不希望每次都加后缀，也可以通过Open Scope Z_scope.或者Open Scope R_scope.切换当前默认的作用域，但混合使用两种类型的比较时，还是建议显式加后缀避免解析歧义。

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