Agda：类型在 `with` 块中没有被简化

Question

我正在尝试解决 this 教程第 23 页的奖金练习，但我无法填补这个漏洞：

lem-all-filter : {A : Set}(xs : List A)(p : A -> Bool)
              -> All (satisfies p) (filter p xs)
lem-all-filter [] p = all[]
lem-all-filter (x :: xs) p with p x
... | true = {! !} :all: lem-all-filter xs p
... | false = lem-all-filter xs p

如果我在孔中键入 C-c C-，然后我会收到此消息：

Goal: isTrue (p x)
--------------------------------
xs : List .A
p  : .A -> Bool
x  : .A
.A : Set

但我希望目标的类型为 True，因为 p x 是 true 和 isTrue true = True。我错过了什么吗？

Answer 1

当您在 p x 上进行模式匹配时，p x 会被重写为上下文中各处的模式，但重写时该漏洞不在上下文中：它出现得较晚，因此 p x 的类型不会被重写。您可以记住 p x 等于 true 使用 inspect 习语（现在已弃用，取而代之的是 inspect on steroids），但您也可以执行以下操作：

lem-all-filter : {A : Set}(xs : List A)(p : A -> Bool)
              -> All (satisfies p) (filter p xs)
lem-all-filter [] p = all[]
lem-all-filter (x :: xs) p with p x | λ (y : isTrue (p x)) -> y :all: lem-all-filter xs p
... | true  | onTrue = onTrue _
... | false | onTrue = lem-all-filter xs p

在这里，您在上下文中显式地引入了 :all: 的参数类型，因此当 p x 被重写为 true 时，onTrue 的类型减少为True -> All (satisfies p) (x :: filter p xs) 根据需要。

Agda：类型在 `with` 块中没有被简化

Agda: type isn't simplified in `with` block

agda