阿格達如何確定一個類型是不可能

Question

所以我試圖理解爲什麼這個代碼給周圍的（）

data sometype : List ℕ → Set where 
    constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (l1 ++ (n ∷ l2)) 

somef : sometype [] → ⊥ 
somef() 

黃色高亮但這並不

data sometype : List ℕ → Set where 
    constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (n ∷ (l1 ++ l2)) 

somef : sometype [] → ⊥ 
somef() 

似乎都這樣sometype []是空的，但Agda無法找出第一個？爲什麼？這樣做的代碼是什麼？我能否以某種方式定義somef以使第一個定義有效？

Answer 1

Agda不能假設任何關於任意功能的東西，如++。假設我們定義++方式如下：

_++_ : {A : Set} → List A → List A → List A 
xs ++ ys = [] 

在這種情況下，sometype [] → ⊥是不可證明，並接受()荒謬的模式將是一個錯誤。

在第二個示例中，sometype的索引必須是n ∷ (l1 ++ l2)的格式，這是一個構造函數表達式，因爲_∷_是一個列表構造函數。 Agda可以安全地推斷出_∷_構建的列表永遠不會等於[]。一般來說，不同的構造函數可能被認爲是不可能統一的。

Agda對功能應用程序的功能是儘可能減少它們。在某些情況下，減少產生構造函數表達式，在其他情況下則不會，並且我們需要編寫額外的證明。

爲了證明sometype [] → ⊥，我們應該先做一些概括。我們無法對sometype []（因爲類型索引中的++）的值進行模式匹配，但我們可以在sometype xs上匹配一些抽象的xs。所以，我們的引理如下：

someF' : ∀ xs → sometype xs → xs ≡ [] → ⊥ 
someF' .(n ∷ l2)   (constr [] l2 n)() 
someF' .(n' ∷ l1 ++ n ∷ l2) (constr (n' ∷ l1) l2 n)() 

換句話說，∀ xs → sometype xs → xs ≢ []。我們可以從中得出所需的證據：

someF : sometype [] → ⊥ 
someF p = someF' [] p refl