在Agda中如何通过已证明引理自动填充隐式参数

解决方案 #

方案一：使用实例参数（推荐） #

这是Agda中处理这类自动填充参数的标准惯用方案，完全匹配你的需求：

1. 首先将你的全局证明obvious注册为Agda的全局实例，只需在定义前加instance关键字：

instance
  obvious : ∀ {A : Type} → Solvable A
  obvious = one-proof

2. 将trivial的p参数从普通隐式参数（单大括号{}）修改为实例参数（双大括号{{}}）：

trivial : ∀ {A : Type} {{p : Solvable A}} → A <: Top
trivial = another-proof

修改完成后，你调用trivial时不需要手动传入任何隐式参数，Agda会自动在全局实例库中匹配到obvious完成填充。同时因为p仍然是函数的入参而非函数内部生成的项，你对p做归纳、递归传入子结构的逻辑完全不受影响，也不会触发终止检查报错。如果遇到特殊场景需要手动传入自定义的p，也可以用trivial {{p = custom-p}}的语法显式指定。

方案二：使用@tactic注解 #

如果你不想注册全局实例避免冲突，也可以用tactic注解实现参数自动填充：

1. 首先导入反射相关的基础库，定义自动填充的tactic：

open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit

fill-obvious : Term → TC ⊤
fill-obvious hole = unify hole (def (quote obvious) [])

2. 给trivial的p参数加上tactic注解：

trivial : ∀ {A : Type} {p : Solvable A @(tactic fill-obvious)} → A <: Top
trivial = another-proof

该方案的调用效果和实例参数一致，也不会影响你的归纳递归逻辑，只是不需要注册全局实例。

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