特殊構造函數上的模式匹配

Question

我一直在反對一個問題的頭幾天，但我的Agda技能不是很強。

我想寫一個函數，只在一個索引的數據類型，只在一個特定的索引定義。這隻適用於數據構造函數的某些特殊化。我無法弄清楚如何定義這樣的功能。我試圖將我的問題減少到一個更小的例子。

該設置涉及到自然數列表，列表中有目擊成員的類型以及刪除列表成員的函數。

open import Data.Nat 
open import Relation.Binary.Core 

data List : Set where 
    nil : List 
    _::_ : (x : ℕ) -> (xs : List) -> List 

-- membership within a list 
data _∈_ (x : ℕ) : List -> Set where 
    here : forall {xs} -> x ∈ (x :: xs) 
    there : forall {xs y} -> (mem : x ∈ xs) -> x ∈ (y :: xs) 

-- delete 
_\\_ : forall {x} (xs : List) -> (mem : x ∈ xs) -> List 
_\\_ nil() 
_\\_ (_ :: xs) here = xs 
_\\_ (_ :: nil) (there()) 
_\\_ (x :: xs) (there p) = x :: (xs \\ p) 

只是一個快速檢查，取消一個單鏈表的頭元素是空列表：

check : forall {x} -> nil ≡ ((x :: nil) \\ here) 
check = refl 

現在我有一個是通過列表索引的一些包裝數據類型

-- Our test data type 
data Foo : List -> Set where 
    test : Foo nil 
    test2 : forall {x} (xs : List) -> (mem : x ∈ xs) -> Foo (xs \\ mem) 

構造函數test2獲取列表和成員資格值，並根據從列表中刪除元素的結果爲數據類型編制索引。

現在我在哪裏卡住了位我想以下簽名的函數：

foo : Foo nil -> ℕ 
foo = {!!} 

即採取Foo價值與它的索引專門用於nil。這對test案件很好

foo test = 0 

第二種情況很棘手。我最初想象的是這樣的：

foo : Foo nil -> ℕ 
foo test = 0 
foo (test2 .(_ :: nil) .here) = 1 

但阿格達抱怨xs \\ mem != nil of type List when checking that the pattern test2 .(_ :: nil) .here has type Foo nil。所以我嘗試使用with-clause：

foo : Foo nil -> ℕ 
foo test = 0 
foo (test2 xs m) with xs \\ m 
... | nil = 1 
... |() 

這會產生相同的錯誤。我已經嘗試了各種排列，但唉，我不能完全弄清楚如何使用n \\ m = nil回到模式中的信息。我已經嘗試了各種其他類型的謂詞，但不知道如何告訴Agda它需要知道什麼。非常感謝一些幫助！謝謝。

---

附加：我在阿格達寫了一個證明，給予任何xs : List和m : x \in xs那（xs \\ m = nil）意味着xs = x :: nil和m = here，這似乎是它可以是給類型檢查是有用的，但我米不知道如何做到這一點。我已經向大家介紹的是尊重其問題複雜化的依賴於PI類型逐點平等：

data PiEq {A : Set} {B : A -> Set} : (a : A) -> (b : A) -> (c : B a) -> (d : B b) -> Set where 
    pirefl : forall {x : A} {y : B x} -> PiEq {A} {B} x x y y 

check' : forall {x xs m} {eq : xs \\ m ≡ nil} -> (PiEq {List} {\xs -> x ∈ xs} xs (x :: nil) m here) 
check' {xs = nil} {()} 
-- The only case that works 
check' {xs = ._ :: nil} {here} = pirefl 
-- Everything else is refuted 
check' {xs = ._ :: (_ :: xs)} {here} {()} 
check' {xs = ._ :: nil} {there()} 
check' {xs = ._} {there here} {()} 
check' {xs = ._} {there (there m)} {()} 

Answer 1

與你建立你的數據類型的方式，你不能真正模式與任何有意義的方式匹配非重要索引值。問題當然是Agda不能（通常）解決xs \\ mem和nil的統一。

模式匹配設置的方式，你不能真正提供任何證明來幫助統一算法。但是，您可以通過保持索引不受限制並使用另一個帶有描述實際限制的證明的參數來確保模式匹配工作正常。這樣，您可以進行模式匹配，然後使用證明來消除不可能的情況。

因此，而不是隻有foo，我們將有另一個功能（比如foo-helper）與額外的參數：

foo-helper : ∀ {xs} → xs ≡ nil → Foo xs → ℕ 
foo-helper p test = 0 
foo-helper p (test2 ys mem) with ys \\ mem 
foo-helper p (test2 _ _) | nil = 1 
foo-helper () (test2 _ _) | _ :: _ 

然後，您可以通過簡單地提供一個證明恢復原來的功能nil ≡ nil：

foo : Foo nil → ℕ 
foo = foo refl 

---

如果您預計以後這種模式往往匹配的，它可能是改變，而不是有益數據類型的定義：

data Foo′ : List → Set where 
    test′ : Foo′ nil 
    test2′ : ∀ {x} xs ys → (mem : x ∈ xs) → ys ≡ xs \\ mem → Foo′ ys 

這樣，您就可以隨時模式匹配，因爲你沒有複雜的指標，仍然消除任何不可能的情況下由於所包含的證明。如果我們想寫foo這個定義，我們甚至不需要一個輔助函數：

foo′ : Foo′ nil → ℕ 
foo′ test′ = 0 
foo′ (test2′ xs .nil mem _) with xs \\ mem 
foo′ (test2′ _ ._ _ _) | nil = 1 
foo′ (test2′ _ ._ _()) | _ :: _ 

---

，並表明這兩種數據類型（邏輯）等價：

to : ∀ {xs} → Foo xs → Foo′ xs 
to test = test′ 
to (test2 xs mem) = test2′ xs (xs \\ mem) mem refl 

from : ∀ {xs} → Foo′ xs → Foo xs 
from test′ = test 
from (test2′ xs .(xs \\ mem) mem refl) = test2 xs mem 

Answer 2

爲什麼不定義由

foo : Foo nil -> ℕ 
foo _ = 0 

foo？

注意：使用阿格達的開發版本（https://github.com/agda/agda/commit/06fe137dc7d7464b7f8f746d969250bbd5011489）我得到了錯誤

I'm not sure if there should be a case for the constructor test2, 
because I get stuck when trying to solve the following unification 
problems (inferred index ≟ expected index): 
    xs \\ mem ≟ nil 
when checking the definition of foo 

當我寫

foo test = 0