我一直在反对一个问题的头几天,但我的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)} {()}
什么关于[this](https://gist.github.com/vituscze/6807d6529aed9e9f60e6)? – Vitus 2014-11-21 00:49:20
是的。你需要'with'子句将'test2'的类型确定为'Foo nil',但是输入必须是'Foo nil',所以你不能在第一个条件中使用'with'子句地点。通过为'Foo'的尾部赋一个变量值,你可以进入'with',然后等式确保只有'nil'情况在'with'内部是相关的。 – zmthy 2014-11-21 04:11:11
@Vitus是的!这就对了!你想发布它作为答案,所以我可以接受它吗?我之前尝试过这样的事情,但设法失败 - 我认为我也与'refl'相匹配,这会使事情中断,即添加“foo refl rest = 0”引发“我不确定是否应该有构造函数test2的情况“。这对我来说似乎很奇怪!我没有在证明上进行匹配的情况下尝试它!非常感谢 – dorchard 2014-11-21 11:57:17