Coq中函数参数能否自动完成作用域解析以适配nat与Z混用场景？

常规函数调用场景的解决方案 #

报错本质是全局打开Z_scope后，数字字面量默认解析为Z类型，导致列表字面量类型为list Z与函数要求的list nat不匹配。无需每次手动加%nat标记，最常用的方案是通过Arguments指令给函数参数绑定默认作用域提示：

Require Import List ZArith.
Import ListNotations.
Open Scope Z_scope.

Definition f (l : list nat) := l.
(* 给f的第一个参数l指定默认解析用nat_scope *)
Arguments f l%nat_scope.

Compute f [1;3]. (* 正常执行，返回 = [1; 3] : list nat *)

这个指令会告诉Coq解析器，在处理f的参数时，优先使用nat_scope解析参数内的符号（包括数字、列表记法等），完全替代手动加%nat的操作。
如果是局部场景需要统一用nat解析，也可以用局部作用域块：

Section UseNatForAll.
  Open Scope nat_scope.
  (* 这个Section内的所有数字默认解析为nat *)
  Compute f [1;3].
End UseNatForAll.

自定义记法场景的解决方案 #

有两种方案可以避免记法使用时手动加作用域：

1. 直接在记法定义时给参数绑定作用域：

(* 定义记法时指定l参数用nat_scope解析 *)
Notation "\\\ l ///" := (f l%nat_scope) (at level 0).

Compute \\\[1;3]///. (* 正常执行，无报错 *)

2. 如果已经通过Arguments给对应函数加了作用域提示，记法定义不需要额外修改，会自动继承函数的作用域提示：

Arguments f l%nat_scope.
Notation "\\\ l ///" := (f l) (at level 0).

Compute \\\[1;3]///. (* 同样正常执行 *)

补充说明 #

如果需要更灵活的跨作用域数字解析，可以开启Coq的Set Type Inference for Numerals选项（Coq 8.14+版本支持），开启后数字会优先根据上下文期望的类型自动选择解析为nat或Z，适合大量混用两种数字类型的场景。

内容的提问来源于stack exchange，提问作者woolly-minded