agda - 不相关的隐式 : Why doesn't agda infer this proof?

Question

最近我在 Agda 中为有限集创建了一个类型，实现如下:

open import Relation.Nullary
open import Relation.Nullary.Negation
open import Data.Empty
open import Data.Unit
open import Relation.Binary.PropositionalEquality
open import Data.Nat

suc-inj : (n m : ℕ) → (suc n) ≡ (suc m) → n ≡ m
suc-inj n .n refl = refl

record Eq (A : Set) : Set₁ where
  constructor mkEqInst
  field
    _decide≡_ : (a b : A) → Dec (a ≡ b)
open Eq {{...}}

mutual
  data FinSet (A : Set) {{_ : Eq A }} : Set where
    ε   : FinSet A
    _&_ : (a : A) → (X : FinSet A) → .{ p : ¬ (a ∈ X)} → FinSet A

  _∈_ : {A : Set} → {{p : Eq A}} → (a : A) → FinSet A → Set
  a ∈ ε = ⊥
  a ∈ (b & B) with (a decide≡ b)
  ...            | yes _     = ⊤
  ...            | no _    = a ∈ B

  _∉_ : {A : Set} → {{p : Eq A}} → (a : A) → FinSet A → Set
  _∉_ a X = ¬ (a ∈ X)

decide∈ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∈ X)
decide∈ a ε = no (λ z → z)
decide∈ a (b & X) with (a decide≡ b)
decide∈ a (b & X)    | yes _ = yes tt
...                  | no _  = decide∈ a X

decide∉ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∉ X)
decide∉ a X = ¬? (decide∈ a X)

instance
  eqℕ : Eq ℕ
  eqℕ = mkEqInst decide
    where decide : (a b : ℕ) → Dec (a ≡ b)
          decide zero zero = yes refl
          decide zero (suc b) = no (λ ())
          decide (suc a) zero = no (λ ())
          decide (suc a) (suc b) with (decide a b)
          ...                       | yes p = yes (cong suc p)
          ...                       | no  p = no (λ x → p ((suc-inj a b) x))

但是，当我使用以下内容测试此类型时:

test : FinSet ℕ
test = _&_ zero ε

由于某种原因，Agda 无法推断 ¬ ⊥ 类型的隐式参数。 !然而， auto 当然找到了这个微不足道的命题的证明: λ x → x : ¬ ⊥ .

我的问题是:既然我已经将隐式证明标记为不相关，为什么 Agda 不能简单地运行 auto找到 ¬ ⊥的证明在类型检查期间？据推测，每当填写其他隐式参数时，Agda finda 的确切证据可能很重要，因此它不应该只是运行 auto ，但是如果证明被标记为不相关，就像我的情况一样，为什么 Agda 找不到证明？

注意:我有一个更好的实现，我在这里实现了 ∉直接，Agda 可以找到相关的证明，但我想大致了解为什么 Agda 不能自动为隐式参数找到这些类型的证明。在 Agda 的当前实现中有什么方法可以像我在这里想要的那样获得这些“自动隐式”？或者是否有一些理论上的原因为什么这会是一个坏主意？

Answer 1

证明搜索无法解决不相关的论点没有根本原因，但是担心在许多情况下它会很慢和/或找不到解决方案。

一个更面向用户的事情是允许用户指定应该使用特定策略推断某个参数，但也没有实现。在您的情况下，您将提供一种尝试使用 (\x -> x) 解决目标的策略。