为什么 agda with-abstraction 不删除某些子句?
Why agda with-abstraction don't erase some clauses?
我正在尝试在 Ulf Norell 和 James Chapman 编写的 Dependently Typed Programming in Agda 教程(第 23 页)中写一个定理作为练习,但我不明白关于 with 的一个可能非常简单的事情。
基本上我有这些定义
data False : Set where
record True : Set where
data Bool : Set where
true : Bool
false : Bool
isTrue : Bool -> Set
isTrue true = True
isTrue false = False
satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)
data List (A : Set) : Set where
[] : List A
_::_ : (x : A)(xs : List A) -> List A
infixr 30 _:all:_
data All {A : Set} (P : A -> Set) : List A -> Set where
all[] : All P []
_:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true = x :: filter p xs
... | false = filter p xs
我正在努力解决这个问题
filter-all-lem : ∀ {p xs} -> All (satisfies p) (filter p xs)
filter-all-lem {p} {[]} with filter p []
... | [] = all[]
... | f :: fs = ?
filter-all-lem {p} {x :: xs} = ?
在第二个洞我还没有尝试过任何东西,这可能不是更好的方法,但我的问题不是这个。
filter p []
是filter的第一种情况。它扩展为 []
。那么为什么 agda 不能推断 f :: fs
这种情况是不可能的呢?统一应该很容易解决这个问题。但是,如果我尝试完全删除该子句或使用荒谬的模式,我会收到错误消息,因为并未涵盖所有可能性。
如果 agda 的统一规则不自动执行此操作,我如何强制它知道它?也许重写? (我现在不知道如何在 agda 中重写)
在这种情况下不需要with filter p []
,正如你所说,你已经可以推断出filter p [] = []
。所以你可以写
filter-all-lem {p} {[]} = all[]
为了理解子句,了解 Agda 如何扩展这些子句会有所帮助,这是一个局部函数,其中匹配的东西(在本例中为 filter p []
)是一个新参数。所以你得到
filter-all-lem {p} {[]} = helper {p} (filter p [])
where
helper :: ∀ {p} ys -> All (satisfies p) ys
helper [] = all[]
helper (f :: fs) = ?
而在帮助器内部,您实际上不知道列表是空的。标准库中有 inspect 习语以等式的形式保存这些知识,但你在这里不需要它。
作为证明有关使用 with 的函数的一般规则(例如 filter (x :: xs)
),您的证明中应该具有与子句完全相同的结构,或者包含包含以下内容的子句匹配依赖类型。
我正在尝试在 Ulf Norell 和 James Chapman 编写的 Dependently Typed Programming in Agda 教程(第 23 页)中写一个定理作为练习,但我不明白关于 with 的一个可能非常简单的事情。
基本上我有这些定义
data False : Set where
record True : Set where
data Bool : Set where
true : Bool
false : Bool
isTrue : Bool -> Set
isTrue true = True
isTrue false = False
satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)
data List (A : Set) : Set where
[] : List A
_::_ : (x : A)(xs : List A) -> List A
infixr 30 _:all:_
data All {A : Set} (P : A -> Set) : List A -> Set where
all[] : All P []
_:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true = x :: filter p xs
... | false = filter p xs
我正在努力解决这个问题
filter-all-lem : ∀ {p xs} -> All (satisfies p) (filter p xs)
filter-all-lem {p} {[]} with filter p []
... | [] = all[]
... | f :: fs = ?
filter-all-lem {p} {x :: xs} = ?
在第二个洞我还没有尝试过任何东西,这可能不是更好的方法,但我的问题不是这个。
filter p []
是filter的第一种情况。它扩展为 []
。那么为什么 agda 不能推断 f :: fs
这种情况是不可能的呢?统一应该很容易解决这个问题。但是,如果我尝试完全删除该子句或使用荒谬的模式,我会收到错误消息,因为并未涵盖所有可能性。
如果 agda 的统一规则不自动执行此操作,我如何强制它知道它?也许重写? (我现在不知道如何在 agda 中重写)
在这种情况下不需要with filter p []
,正如你所说,你已经可以推断出filter p [] = []
。所以你可以写
filter-all-lem {p} {[]} = all[]
为了理解子句,了解 Agda 如何扩展这些子句会有所帮助,这是一个局部函数,其中匹配的东西(在本例中为 filter p []
)是一个新参数。所以你得到
filter-all-lem {p} {[]} = helper {p} (filter p [])
where
helper :: ∀ {p} ys -> All (satisfies p) ys
helper [] = all[]
helper (f :: fs) = ?
而在帮助器内部,您实际上不知道列表是空的。标准库中有 inspect 习语以等式的形式保存这些知识,但你在这里不需要它。
作为证明有关使用 with 的函数的一般规则(例如 filter (x :: xs)
),您的证明中应该具有与子句完全相同的结构,或者包含包含以下内容的子句匹配依赖类型。