专业构造函数的模式匹配
几天来，我一直在面对一个问题，但我的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但是Agda抱怨说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)} {()} 回答 2
Stack Overflow用户
发布于 2014-11-21 17:23:44
通过设置数据类型的方式，您无法以任何有意义的方式对具有非平凡索引的值进行模式匹配。当然，问题是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 memStack Overflow用户
发布于 2014-11-20 23:26:44
为什么不定义foo
foo : Foo nil -> ℕ
foo _ = 0注意:使用当前开发版本的Agda (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 = 0https://stackoverflow.com/questions/27045886
复制相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号