模式匹配专门的构造函数

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)

只需快速检查删除单例列表的head元素是空列表:

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它需要知道什么.非常感谢一些帮助!谢谢.

---

附加:我在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

通过设置数据类型的方式,您无法以任何有意义的方式对具有非平凡索引的值进行实际模式匹配.问题当然是阿格达不能(一般)解决的统一的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