不相关的暗示：为什么 agda 不推断这个证明？

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 找到 ¬ ⊥ [=28 的证明=]在类型检查期间？据推测，每当填写其他隐式参数时，Agda finda 的证明到底是什么可能很重要，所以它不应该只是运行 auto，但如果证明已被标记为无关紧要，就像我的情况一样，为什么Agda 不能找到证明吗？

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

Answer 1

不相关的论点无法通过证据搜索解决的根本原因是，但担心在许多情况下它会很慢and/or找不到解决方案。

一个更以用户为导向的事情是允许用户指定应该使用特定策略推断某个参数，但这也没有实现。在您的情况下，您将提供一种策略，试图通过 (\ x -> x).

解决目标

Answer 2

如果您给出 ∉ 的更直接定义，则隐式参数的类型为 ⊤ 而不是 ¬ ⊥。 Agda 可以通过 eta-expansion 自动填充 ⊤ 类型的参数，因此您的代码可以正常工作：

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 & X) with (a decide≡ b)
  ...            | yes _ = ⊥
  ...            | no  _ = a ∉ X

decide∉ : {A : Set} → {{_ : Eq A}} → (a : A) → (X : FinSet A) → Dec (a ∉ X)
decide∉ a ε = yes tt
decide∉ a (b & X) with (a decide≡ b)
...                  | yes _ = no (λ z → z)
...                  | no  _ = 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 不推断这个证明？

Irrelevant implicits: Why doesn't agda infer this proof?

agda