为啥带有抽象的 agda 不删除某些子句?

Posted

技术标签:

【中文标题】为啥带有抽象的 agda 不删除某些子句?【英文标题】:Why agda with-abstraction don't erase some clauses?为什么带有抽象的 agda 不删除某些子句? 【发布时间】:2019-12-29 23:35:12 【问题描述】:

我正在尝试在 Ulf Norell 和 James Chapman 编写的 Dependently Typed Programming in Agda 教程(第 23 页)中写一个作为练习留下的定理,但我不明白一个可能非常简单的事情。

基本上我有这些定义

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 [] 是过滤器的第一种情况。它扩展到[]。那么为什么agda 不能推断出f :: fs 的情况是不可能的呢?统一应该很容易解决这个问题。但是,如果我尝试完全删除该子句或使用荒谬的模式,我会收到错误,因为并未涵盖所有可能性。

如果agda的统一规则不能自动做到这一点,我怎么能强迫它知道呢?也许重写? (我现在还不知道怎么用agda重写)

【问题讨论】:

【参考方案1】:

在这种情况下不需要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) = ?

在助手内部,您实际上失去了列表为空的知识。标准库中有检查习语以等式的形式保存这些知识,但这里不需要。

作为证明使用 with(例如 filter (x :: xs))的函数的一般规则,您应该在证明中具有与 with 子句完全相同的结构,或者 with 包含独立匹配事物的子句类型。

【讨论】:

以上是关于为啥带有抽象的 agda 不删除某些子句?的主要内容,如果未能解决你的问题,请参考以下文章

使用带有某些基类、抽象类或特征的列表参数化的类型类的最佳方法

为啥不抽象字段?

为啥不能在 Redshift 的 CTE 的某些子句中调用不可变的 UDF?

为啥不抽象政策?

为啥套接字连接的基本抽象并不常见?

不明白为啥这个类被认为是抽象类