Нерелевантные имплициты: почему agda не делает этого доказательства?

Недавно я сделал тип для конечных множеств в 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 получить эти "автоматические имплициты", как я хочу здесь? Или есть какая-то теоретическая причина, по которой это было бы плохой идеей?


agda
person Nathan BeDell    schedule 02.04.2017    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Нет фундаментальной причины, по которой нерелевантные аргументы не могут быть разрешены с помощью поиска доказательств, однако есть опасения, что во многих случаях это будет медленным и / или не найдет решения.

Более ориентированным на пользователя способом было бы позволить пользователю указать, что определенный аргумент должен быть выведен с использованием определенной тактики, но это также не было реализовано. В вашем случае вы бы предложили тактику, которая пытается решить цель с помощью (\ x -> x).

person Saizan    schedule 05.04.2017
comment
Интересно, можно подумать, что это, по крайней мере, вариант компилятора. Возможно, я добавлю запрос функции на Github. - person Nathan BeDell; 05.04.2017

arrow_upward
1
arrow_downward

Если вы дадите более прямое определение ∉, то неявный аргумент получит тип ⊤ вместо ¬ ⊥. Agda может автоматически подставлять аргументы типа ⊤ с помощью расширения eta, поэтому ваш код просто работает:

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 ε
person Jesper    schedule 11.04.2017