特殊构造函数上的模式匹配

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