Rocq 隐式参数（Implicit Arguments）完全指南：声明、自动推断与实战控制

形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载隐式参数Implicit Arguments是 Rocq ProverCoq中一类可以由上下文自动推断、无需显式书写的函数参数是多态定义、类型类与可读证明脚本得以简洁书写的基础机制。本文以 doc/sphinx/language/extensions/implicit-arguments.rst 为骨架结合 interp/impargs.ml 等核心源码与 test-suite/success/implicit.v 测试用例系统讲解隐式参数的各类形态、声明语法、自动推断开关、显式实例化方法、打印控制与隐式泛化帮助你从会用{}和[]进阶到完全掌控隐式参数的推断与插入行为。隐式参数的不同种类文档将隐式参数划分为两大类一类可以从函数其他参数的类型或周围上下文类型中推断出来另一类则依靠类型结构解析。理解这些分类是正确使用各 flag 的前提。可从其他参数类型推断的隐式参数这类参数对应于函数类型中被其他参数所依赖的形参典型代表是多态函数中的类型参数。它们进一步细分为三种形态。Strict Implicit Arguments严格隐式参数一个隐式参数被称为strict是指无论函数其他参数如何它仍能从某个其他参数的类型中推断出来。技术上讲strict 隐式参数对应这样的形参它没有被应用到函数自身的另一个形参变量上因为该形参可能抹除它的参数、不出现在 match 的 body 中、其自身也不被应用或与模式匹配因为归约可能丢失其原始形式。例如List.v模块中cons: forall A:Set, A - list A - list A其第一个参数A是 strict 的因为list是归纳类型A总是能从第三个参数的类型list A中推断出来A相对于第二个参数也是 strict 的因为它恰好是第二个参数的类型。反例类型为forall P:nat-Prop, forall n:nat, P n - ex nat P的项第二个参数n是隐式但非 strict因为它只能从第三个参数的类型P n中推断而若P是例如fun _ True该项归约后n不再出现。第一个参数P同样隐式但非 strictP无法从任意n与P n的范式规范地推断——考虑n为0、第三个参数类型为True的情形任意形如fun n match n with 0 True | _ anything end的P都是该推断问题的解。Contextual Implicit Arguments上下文隐式参数一个隐式参数被称为contextual是指它只能从当前表达式所处上下文的类型中推断。例如nil : forall A:Set, list A的唯一参数是 contextual 的。类似地类型为forall P:nat-Prop, forall n:nat, P n \/ n 0的项的两个参数都是 contextual 的此外n是 strict 而P不是。Reversible-Pattern Implicit Arguments可逆模式隐式参数还有一类隐式参数当其余所有参数的类型都已知时可以无歧义地重新推断出来。它们出现在另一个参数类型的可逆模式位置——即位于一个应用的头部但只应用于未实例化的互不相同变量。典型的例子是nat_rec的参数Pnat_rec : forall P : nat - Set, P 0 - (forall n : nat, P n - P (S n)) - forall x : nat, P xP可以通过在类型P n中对n抽象而重新推断得到。关于可逆模式隐式参数的自动声明参见下文 Controlling reversible-pattern implicit arguments 一节。通过解析可推断的隐式参数这是指一类非依赖的隐式参数仅依据其自身的类型结构即可求解即下文 Implicit types of variables 所对应的一类绑定变量类型机制以及依赖统一求解的非依赖隐式参数。隐式参数的最大/非最大插入当函数被部分应用、且下一个待应用参数是隐式参数时应用有两种解读方式若该参数被声明为maximally inserted最大插入部分应用会包含该参数否则为non-maximally inserted非最大插入部分应用不包含该参数。在 Rocq 中最大插入的隐式参数书写在花括号{ }中非最大插入的书写在方括号[ ]中相关总开关见 Maximal Implicit Insertion 小节。在源码 interp/impargs.mli 中type maximal_insertion bool直接以布尔值记录这一属性binding_kind_of_status见 interp/impargs.ml则将其映射为MaxImplicit/NonMaxImplicit/Explicit三种语法绑定形态。Trailing Implicit Arguments尾部隐式参数当一个隐式参数之后的所有参数都是隐式参数时称它为trailing。尾部隐式参数必须声明为最大插入否则它们永远不会被插入Argument name is a trailing implicit, so it cant be declared non maximal. Please use { } instead of [ ].例如下面这条命令会直接报错Fail Definition double [n] : n n.这一约束在源码层有直接对应set_maximality在发现尾部非最大隐式参数时会以Error模式抛出上述用户错误见 interp/impargs.ml 中on_trailing_implicit Error | Info | Silent与msg_trailing_implicit的实现。隐式参数的日常使用如果函数应用的某个参数可以从其他参数的类型推断出来用户可以通过把该参数替换为_来强制推断Cannot infer a term for this placeholder.当 Rocq 无法为一个_推导出实例化时就会报出上述错误。隐式参数的声明隐式参数可以在函数声明时或之后通过Arguments命令详见 doc/sphinx/language/extensions/arguments-command.rst来声明。隐式参数绑定符Implicit Argument Binders在函数定义的上下文中以下语法形式指明name是隐式参数implicit_binders :: { { name } {? : type } } | [ { name } {? : type } ]第一种形式花括号将name设为最大插入隐式参数第二种形式方括号将name设为非最大插入隐式参数。例如Definition id {A : Type} (x : A) : A : x.把id的参数A声明为最大插入隐式参数。A在id的应用中可以省略但需要时也可显式给出Definition compose {A B C} (g : B - C) (f : A - B) : fun x g (f x). Goal forall A, compose id id id (A:A).非最大插入隐式参数使用方括号Fixpoint map [A B : Type] (f : A - B) (l : list A) : list B : match l with | nil nil | cons a t cons (f a) (map f t) end. Print Implicit map.对于余归纳数据类型声明语义如下被声明为隐式参数的归纳参数无需在归纳定义中重复出现并且会同时对该归纳类型及其构造子变为隐式。例如Inductive list {A : Type} : Type : | nil : list | cons : A - list - list. Print list.若该参数不是 uniform 参数仍可使用通常的隐式参数消歧语法显式指定它。该语法也支持在内部绑定符中使用。例如在以下各类表达式中{* binder }中每个声明自身的类型可以被括号括起来以标记为隐式fun (ident:forall {* binder }, type) termforall (ident:forall {* binder }, type), typelet ident {* binder } : term in termfix ident {* binder } : term in termcofix ident {* binder } : term in term示例Axiom Ax : forall (f:forall {A} (a:A), A * A), let g {A} (x y:A) : (x,y) in f 0 g 0 0.以下两种警告需要注意Ignoring implicit binder declaration in unexpected position当一个隐式绑定符声明出现在不对应于假设类型或定义体body的表达式中时触发。示例Definition f : forall {y}, y 0.Making shadowed name of implicit argument accessible by position当同一绑定符块中两个同名变量被设为隐式时触发此时第一次出现被视为无名。示例Check let g {x:nat} (H:xx) {x} (H:xx) : x in 0.隐式参数的自动声明模式flag:: Implicit Arguments该 flag默认关闭允许系统性地把可检测为隐式的参数自动声明为隐式。自动检测由若干 flag 控制决定是否考虑 strict 与 contextual 隐式参数。在 interp/impargs.ml 中所有相关开关被统一记录在type implicits_flags { auto; strict; strongly_strict; reversible_pattern; contextual; maximal }结构里各 flag 的读写经由make_*/is_*函数完成而 vernac/vernacentries.ml 通过declare_bool_option将Implicit Arguments、Strict Implicit、Strongly Strict Implicit、Contextual Implicit、Reversible Pattern Implicit、Maximal Implicit Insertion这六个选项逐一注册进全局选项表这正对应文档中的六个 flag。控制 strict 隐式参数Controlling strict implicit argumentsflag:: Strict Implicit当自动声明模式开启时默认只自动设置 strict 隐式参数加上出于历史原因一小部分非 strict 隐式参数。若想放宽此约束、默认将所有非 strict 隐式参数也设为隐式可以关闭该 flag。flag:: Strongly Strict Implicit使用该 flag默认关闭可以精确捕获 strict 隐式参数不多不少。控制 contextual 隐式参数Controlling contextual implicit argumentsflag:: Contextual Implicit默认情况下 Rocq 不会自动把 contextual 隐式参数设为隐式。打开该 flag 可让 Rocq 也推断 contextual 隐式参数。控制可逆模式隐式参数Controlling reversible-pattern implicit argumentsflag:: Reversible Pattern Implicit默认情况下 Rocq 不会自动把 reversible-pattern 隐式参数设为隐式。打开该 flag 可让 Rocq 也推断 reversible-pattern 隐式参数。控制非显式参数后的插入Controlling the insertion of implicit arguments not followed by explicit argumentsflag:: Maximal Implicit Insertion假设隐式参数模式已开启该 flag默认关闭声明当函数被部分应用、且函数的下一个参数是隐式参数时自动插入该隐式参数。手动声明与自动声明的组合当定义中部分参数通过绑定符手动指定为隐式、且自动声明模式开启时手动隐式参数会追加到自动声明的隐式参数之上。在这种情况下若Maximal Implicit Insertionflag 处于关闭状态一些尾部隐式参数会被推断为非最大插入此时它们会被转换为最大插入形式。示例Set Implicit Arguments. Axiom eq0_le0 : forall (n : nat) (x : n 0), n 0. Print Implicit eq0_le0. Axiom eq0_le0 : forall (n : nat) {x : n 0}, n 0. Print Implicit eq0_le0.其中eq0_le0的x : n 0是自动声明的隐式参数eq0_le0则是手动 自动混合声明通过Print Implicit可以观察到两者隐式状态含最大/非最大插入的差异。从源码看interp/impargs.ml 的set_manual_implicits在合并手动与自动列表时会为手动参数标注impl_expl Manual并通过set_maximality处理最大插入性。显式应用Explicit applications在存在非 strict 或 contextual 参数、或存在部分应用的情况下隐式参数的综合可能失败此时需要显式给出应用中的某些隐式参数。实例化依赖隐式参数使用(ident : term)形式的arg其中ident是隐式参数的名称term是对应的显式项实例化非依赖隐式参数使用(natural : term)形式的arg其中natural是该参数在所有非依赖参数不论隐式与否中的序号从 1 开始计数或者可以使用qualid_annotated { term1 }形式的term_application为单次函数应用停用隐式参数的隐藏。示例显式给出隐式参数的语法Parameter X : Type. Definition Relation : X - X - Prop. Definition Transitivity (R:Relation) : forall x y:X, R x y - forall z:X, R y z - R x z. Parameters (R : Relation) (p : Transitivity R). Arguments p : default implicits. Print Implicit p. Parameters (a b c : X) (r1 : R a b) (r2 : R b c). Check (p r1 (z:c)). Check (p (x:a) (y:b) r1 (z:c) r2).这里p的隐式参数通过Arguments p : default implicits恢复为默认隐式集合之后既可以用名字(x:a)、(y:b)、(z:c)实例化也可以混合位置参数使用。使用不当时可能触发以下错误文档中未详细展开均与显式应用相关Wrong argument name Wrong argument position Argument at position natural is mentioned more than once Arguments given by name or position not supported in explicit mode Not enough non implicit arguments to accept the argument bound to ident Not enough non implicit arguments to accept the argument bound to natural显示隐式参数Print Implicit 命令cmd:: Print Implicit reference显示与某个对象关联的隐式参数并标明哪些参数是最大插入应用的。打印时的隐式参数显示flag:: Printing Implicit默认情况下基础 pretty-printing 规则会隐藏应用中可推断的隐式参数。打开该 flag 可强制打印所有隐式参数。flag:: Printing Implicit Defensive默认情况下基础打印规则会显示未被识别为 strict的隐式参数。这种防御性模式可能很快让显示变得冗长可通过关闭该 flag 来停用。相关 flag 还有Printing All。从源码看Print Implicit在 vernac/g_vernac.mlg 中解析为PrintImplicit qid其背后的隐式信息来源于implicits_table一个Summary.ref GlobRefMap.empty见 interp/impargs.ml并按需应用Arguments_renaming.arguments_names恢复参数名。与子类型subtyping的交互当一个隐式参数能从不止一个其他参数的类型推断时只有第一个这样的参数类型会被考虑而不是取所有参数类型的一个上界。因此的隐式参数推断在Fail Check nat Prop.中失败而在Check Prop nat.中成功——因为后者的第一个参数类型足以确定两侧的类型。解析时停用隐式参数以下语法可以在单个函数上禁用隐式参数term_explicit :: qualid_annotated例如函数id有一个隐式参数和一个显式参数Check (id 0). Definition id : id.id不再有隐式参数Check (id nat 0).flag:: Parsing Explicit打开该 flag默认关闭会停用隐式参数的使用。此时常量、归纳类型、构造子等的所有参数包括声明为隐式的都必须当作没有隐式参数一样给出。对称地这也影响打印。可以使用Parsing Explicitflag 重现上面的例子Set Parsing Explicit. Definition id : id. Unset Parsing Explicit. Check (id 1). Check (id nat 1).变量的隐式类型Implicit types of variables可以把变量名绑定到给定类型。例如在涉及算术的开发中可以把名字n或m绑定到自然数类型natcmd:: Implicit {| Type | Types } reserv_list语法为reserv_list :: { ( simple_reserv ) } | simple_reserv simple_reserv :: { ident } : type该命令把以ident开头即ident本身或ident后跟一个或多个单引号、下划线或数字的绑定变量的类型设为type——除非该绑定变量已声明了显式类型此时使用显式类型。示例Require Import ListDef. Implicit Types m n : nat. Lemma cons_inj_nat : forall m n l, n :: l m :: l - n m. Proof. intros m n. Abort. Lemma cons_inj_bool : forall (m n:bool) l, n :: l m :: l - n m. Abort.flag:: Printing Use Implicit Types默认情况下当变量名关联的隐式类型与该变量的实际类型一致时绑定变量的类型不会被打印。可通过关闭该 flag 停用此特性。隐式泛化Implicit generalization隐式泛化是把带自由变量的陈述自动精化elaborate为封闭陈述的机制这些自由变量被显式量化。使用Generalizable命令指定哪些变量应被泛化。语法涉及前缀generalizing_binder :: ( {, typeclass_constraint } ) | { {, typeclass_constraint } } | [ {, typeclass_constraint } ] typeclass_constraint :: {? ! } term | { name } : {? ! } term | name : {? ! } term term_generalizing :: { term } | ( term )泛化在绑定符内通过前缀激活在项中通过用{ }、[ ]或( )包围来激活用{ }包围的项其自由变量作为最大插入隐式参数引入用[ ]包围的项其自由变量作为非最大插入隐式参数引入用( )包围的项其自由变量作为显式参数引入。泛化绑定符总是把自由变量作为最大插入隐式参数引入绑定符自身照常引入其参数。在下面的陈述中A和y被自动泛化A是隐式的而x、y和匿名的相等参数是显式的Generalizable All Variables. Definition sym (x:A) : (x y - y x) : fun _ p eq_sym p. Print sym.与普通绑定符对偶地泛化绑定符中名字可选但类型必需Check (forall {x y : A}, y x).当泛化一个类型为类型类的绑定符时其自身的类参数从语法中省略并使用自动名字进行泛化不做实例搜索除非已提供否则其他参数也被泛化。这产生完全一般的陈述。可以通过给类型加!前缀或用强制类型类名为显式应用来禁用该行为注意后者会忽略隐式参数信息Class Op (A:Type) : op : A - A - A. Class Commutative (A:Type) (Op A) : commutative : forall x y, op x y op y x. Instance nat_op : Op nat : plus. Set Printing Implicit. Check (forall {Commutative }, True). Check (forall {Commutative nat}, True). Fail Check (forall {Commutative nat _}, True). Fail Check (forall {!Commutative nat}, True). Arguments Commutative _ {_}. Check (forall {!Commutative nat}, True). Check (forall {Commutative nat plus}, True).多个绑定符可以用,作为分隔符合并Check (forall {Commutative A, Hnat : !Commutative nat}, True).Generalizable 命令cmd:: Generalizable {| {| Variable | Variables } { ident } | All Variables | No Variables }控制可泛化标识符的集合。默认情况下没有变量是可泛化的。Variable/Variables ident形式只允许泛化给定的标识符多次使用该命令会累积允许的标识符其他形式会清空标识符列表All Variables形式泛化上下文中出现在泛化定界符下的所有自由变量。这可能在拼写错误时导致令人困惑的错误——此时上下文中很可能出现一些意外的泛化变量No Variables形式完全禁用隐式泛化这是默认行为在输入任何Generalizable命令之前。该命令支持global属性。从实现看泛化变量的收集与声明在 interp/implicit_quantifiers.ml 及其接口 interp/implicit_quantifiers.mli 中完成declare_generalizable、generalizable_vars_of_glob_constrGeneralizable命令的语法入口则在 vernac/g_vernac.mlg。小结与实战建议日常书写用{A}声明最大插入隐式参数如类型参数用[A]声明非最大插入隐式参数尾部隐式参数必须用{ }否则报错。自动推断开启Set Implicit Arguments后按需组合Unset Strict Implicit、Set Contextual Implicit、Set Reversible Pattern Implicit、Set Maximal Implicit Insertion它们对应 interp/impargs.ml 中implicits_flags的六个字段。排错当隐式综合失败时用(x:v)、(1:v)或f显式给出参数用Print Implicit f检查当前隐式集合用Set Printing Implicit观察被隐藏的参数。语句泛化使用前缀与Generalizable命令将自由变量自动量化为隐式/显式参数减少样板代码。仓库中 test-suite/success/implicit.v 与 test-suite/output/Implicit.v 覆盖了本节几乎所有机制的自动化回归测试读者可结合运行rocq或coqtop逐条验证本文示例。赞分享形式化验证编程语言【免费下载链接】coqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.项目地址https://gitcode.com/gh_mirrors/co/coq点击查看免费下载相关推荐Rocq 隐式强制Implicit Coercions机制详解Coercion 类、继承图与可逆强制实战Rocq 隐式强制Implicit Coercions机制详解Coercion 类、继承图与可逆强制实战 导读 隐式强制Implicit Coercio形式化验证编程语言Ruffty隐式 super() 参数缺失检测unavailable-implicit-super-arguments 规则详解Ruffty隐式 super 参数缺失检测unavailable implicit super arguments 规则详解 本篇技术指南围绕 Ruff开发工具Lint格式化静态分析CLIMojo 语言 implicit 装饰器完全指南隐式转换、deprecated 参数与标准库实战Mojo 语言 implicit 装饰器完全指南隐式转换、deprecated 参数与标准库实战 导读 本文围绕 Mojo 编译器源码仓库Modular人工智能大模型编程语言编译器标准库算子库模型推理服务模型量化创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考