通过 Agda 中的函数自动解决隐式参数？

Question

假设我有一个已证明的引理“显而易见”，它说明每个类型也是可解的。

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

我有一个引理“微不足道”，不知何故需要类型 A 和可解 p（取决于 A），

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

每次我想使用这个“琐碎的”引理时，我可能需要明确地写出参数 A 和 p

trivial {A} {obvious A}

写那些证明很无聊，因为A可以推断，但是p不能，因为类型检查器不知道我的“明显”引理，所以我需要一遍又一遍地写。

如何避免这种情况？

事实上我已经尝试了两次：

尝试 1

删除参数 p 并使用 with-abstraction 创建直接参数。

trivial : ∀ {A : Type} → A <: Top
trivial {A} with obvious A 
... | branch = another-proof

它没有解决我的问题，因为实际上我需要对 p 进行一些归纳，然后使用 p 的子结构递归调用“平凡”函数。 Agda 终止检查器会抱怨它。

尝试 2

根据 Agda 文档的建议，使用 @tactic。但是我找不到更多关于它的用法的信息，有人可以解释一下吗？

Answer 1

啊哈，函数组合的答案提示了我

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

那么我们总是可以使用“trivial”而不显式地写参数。

通过 Agda 中的函数自动解决隐式参数？

Auto solve implicit arguments by a function in Agda?

agda