不相干的暗示：爲什麼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 ε

阿格達出於某種原因不能推斷類型爲¬ ⊥的隱含參數！然而，汽車當然會找到這個無足輕重的命題的證明：λ x → x : ¬ ⊥。

我的問題是這樣的：自從我標誌着隱含證明爲不相關的，爲什麼不能簡單地阿格達運行auto找到¬ ⊥類型檢查期間的證明？據推測，每當填寫其他隱含的論點時，它可能與阿格達發現的確切證據有關，所以它不應該僅僅運行auto，但如果證明被標記爲不相關，就像我的情況一樣，爲什麼阿格達不能找到證據？

注意：我有一個更好的實現，我直接實現了∉，Agda可以找到相關證明，但我想了解一般Agda爲什麼不能自動爲隱式參數找到這些類型的證明。在目前Agda的實施中，有沒有辦法像我想要的那樣獲得這些「自動隱含」？還是有一些理論上的原因，爲什麼這是一個壞主意？

來源

2017-04-02 Nathan BeDell

沒有根本原因爲什麼無關的論證不能通過證明搜索來解決，但是恐懼是在很多情況下它會很慢和/或找不到解決方案。

更多用戶指導的事情是允許用戶指定應該使用特定策略推斷某個參數，但該參數尚未實現。在你的情況下，你會提供一個策略，試圖用（\ x - > x）來解決目標。

來源

2017-04-05 08:53:16 Saizan

有趣的是，你會認爲這將至少是一個編譯器選項。也許我會在Github上發佈一個功能請求。 –

如果你給的∉更直接的定義，則隱含參數得到鍵入⊤代替¬ ⊥。阿格達可以通過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 ε

來源

2017-04-11 12:00:44 Jesper

不相干的暗示：爲什麼agda沒有推斷出這個證明？

回答

相關問題