专用构造函数上的模式匹配 [英] Pattern match on specialised constructors

问题描述

几天来我一直在努力解决一个问题，但我的 Agda 技能不是很强大.

I've been banging my head against a problem for a few days, but my Agda skills are not very strong.

我正在尝试针对仅在特定索引处定义的索引数据类型编写函数.这仅适用于数据构造器的某些专业化.我不知道如何定义这样的函数.我试图将我的问题减少到一个较小的例子.

I am trying to write a function over an indexed data type which is defined only at a particular index. This is only possible for certain specialisations of the data constructors. I can't figure out how to define such a function. I've tried to reduce my problem to a smaller example.

设置涉及自然数列表，具有用于见证列表成员的类型和用于删除列表成员的函数.

The setup involves lists of natural numbers, with a type for witnessing members of the list, and a function for deleting list members.

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)

快速检查一下，删除单例列表的头元素是空列表:

Just a quick check that removing the head element of a singleton list is the empty list:

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

现在我有一些由列表索引的包装数据类型

Now I have some wrapper data type that is indexed by lists

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

test2 构造函数接受一个列表和一个成员资格值，并通过从列表中删除元素的结果来索引数据类型.

The test2 constructor takes a list and a membership value and indexes the data type by the result of deleting the element from the list.

现在我遇到的问题是我想要一个具有以下签名的函数:

Now the bit where I am stuck is I want a function of the following signature:

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

即，取一个 Foo 值，其索引专门用于 nil.这适用于 test 案例

i.e., taking a Foo value with its index specialised to nil. This is fine for the test case

foo test = 0

第二种情况很棘手.我最初的想象是这样的:

The second case is tricky. I initially imagined something like:

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

但是 Agda 在检查模式 test2 .(_ :: nil) .here 的类型为 Foo nil 时会抱怨 xs \\ mem != nil 类型为 List.所以我尝试使用 with 子句:

But Agda complains that xs \\ mem != nil of type List when checking that the pattern test2 .(_ :: nil) .here has type Foo nil. So I tried using a with-clause:

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

这会产生相同的错误.我已经尝试了各种排列，但是我不太清楚如何使用 n \\ m = nil 回到模式中的信息.我尝试了各种其他类型的谓词，但无法弄清楚如何告诉 Agda 它需要知道什么.非常感谢一些帮助！谢谢.

This yields the same error. I have experimented with various permutations, but alas I can't quite figure out how to use the information that n \\ m = nil back in the pattern. I've tried various other kinds of predicates but can't quite figure out how to tell Agda what it needs to know. Would very much appreciate some help! Thanks.

附加:我在 Agda 中写了一个证明，给出任何 xs : List 和 m : x \in xs (xs \\ m = nil) 暗示 xs = x :: nil 和 m = here ，这似乎对赋予类型很有用检查器，但我不知道如何做到这一点.我必须在 pi 类型上引入逐点相等，以尊重使问题复杂化的依赖关系:

Additional: I wrote a proof in Agda that given any xs : List and m : x \in xs that (xs \\ m = nil) implies that xs = x :: nil and m = here, which seems like it could be useful to give to the type checker, but I'm not sure how to do this. I had to introduce a pointwise equality on pi types that respects the dependency which complicates matters:

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)} {()} 

推荐答案

根据您设置数据类型的方式，您无法真正以任何有意义的方式对具有非平凡索引的值进行模式匹配.问题当然是Agda不能(一般)解决xs \\ mem和nil的统一.

With the way you set up your data type, you cannot really pattern match on values with non-trivial index in any meaningful way. The problem is of course that Agda cannot (in general) solve the unification of xs \\ mem and nil.

模式匹配的设置方式，你不能真正提供任何证据来帮助统一算法.但是，您可以通过不限制索引并使用另一个参数和描述实际限制的证明来确保模式匹配有效.这样，您可以进行模式匹配，然后使用证明来消除不可能的情况.

The way pattern matching is set up, you cannot really provide any proof to help the unification algorithm. However, you can ensure that the pattern matching works by leaving the index unrestricted and using another parameter with a proof that describes the actual restriction. This way, you can do a pattern match and then use the proof to eliminate impossible cases.

所以，不是只有 foo，我们将有另一个带有额外参数的函数(比如 foo-helper):

So, instead of having only foo, we'll have another function (say foo-helper) with extra parameter:

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来恢复原始函数:

You can then recover the original function by simply providing a proof that nil ≡ nil:

foo : Foo nil → ℕ
foo = foo refl

<小时>

如果您希望经常进行这种模式匹配，那么更改数据类型的定义可能会有所帮助:

---

If you anticipate doing this kind of pattern matching often, it might be beneficial to instead change the definition of the data type:

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

通过这种方式，您始终可以进行模式匹配，因为您没有复杂的索引，并且由于包含的证明，仍然可以消除任何不可能的情况.如果我们想用这个定义写foo，我们甚至不需要辅助函数:

This way, you can always pattern match because you do not have complicated indices and still eliminate any impossible cases thanks to the included proof. If we want to write foo with this definition, we do not even need a helper function:

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

<小时>

并证明这两种数据类型(逻辑上)等价:

---

And to show that these two data types are (logically) equivalent:

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

这篇关于专用构造函数上的模式匹配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！