如何在ssreflect中使用整数加法、一元减法等熟悉算术符号？

AI 小北

2026-6-18

在MathComp ssrint中启用完整整数算术符号

1. 正确的库加载与作用域设置

你当前仅打开distn_scope，这个作用域只覆盖减法操作。要启用加法、一元负号等完整整数算术符号，需要打开int_scope（整数专属作用域）。修改后的代码如下：

From mathcomp Require Import all_ssreflect ssrint.
Open Scope int_scope.
Parameter x y : int.

Check x - y : int.       (* 减法正常工作 *)
Check x + y : int.       (* 加法现在可用 *)
Check -x : int.          (* 一元负号正常工作 *)
Check oppzD : - (x + y) = -x + -y.  (* 这条命令可正常生效 *)

如果需要保留distn_scope的其他符号，也可以同时打开两个作用域：

Open Scope distn_scope.
Open Scope int_scope.

2. 解决此类符号问题的查询方法

定位符号绑定：用Locate命令查询符号对应的定义和所属作用域，比如查询加法符号：
```
Locate "+".
```
输出会显示该符号在哪些作用域中被定义，以及对应的底层操作符（比如整数加法对应addz）。
查看作用域内容：用Print Scope命令查看指定作用域包含的所有符号，比如查看整数作用域：
```
Print Scope int_scope.
```
会列出int_scope下绑定的所有算术符号，包括+、二元-、一元-等。
搜索相关定理：用Search命令查询目标定理或操作符，比如查找整数负号分配律相关内容：
```
Search oppzD.
```
或者搜索整数加法相关定理：
```
Search addz.
```