为什么这个 Agda 程序不会在 `with` 子句下规范化表达式？

Question

在以下 Agda 程序中：

module Hello where

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} -> (p : A -> Bool) -> (x : A) -> Set
satisfies p x = isTrue (p x)

data List (a : Set) : Set where
  []   : List a
  _::_ : a -> List a -> List a

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

data All {A : Set}(P : A -> Set) : List A -> Set where
  vacuo : All P [] 
  holds : (x : A) -> (xs : List A) -> P x -> All P xs -> All P (x :: xs)

filter-lem-b : {A : Set} -> (p : A -> Bool) -> (xs : List A) -> All (satisfies p) (filter p xs)
filter-lem-b p []        = vacuo
filter-lem-b p (x :: xs) with p x
filter-lem-b p (x :: xs) | true  = let u = holds {P = satisfies p} x xs in ?
filter-lem-b p (x :: xs) | false = filter-lem-b p xs

洞的上下文说：

u  : isTrue (p x) →
     All (λ x₁ → isTrue (p x₁)) xs →
     All (λ x₁ → isTrue (p x₁)) (x :: xs)

为什么isTrue (p x)不缩减为True，因为在匹配的分支上，已经确定了p x是true？

Answer 1

模式匹配不会导致任何等式被记住。匹配更新事物的值和类型：

右边的类型。
在左侧的其他参数中。

这种更新发生在匹配点，没有进一步携带信息。在您的情况下，目标类型或其他参数中没有任何内容取决于 p x，因此当您匹配它时不会更新任何内容。

一种解决方案是使用 inspect，它会记住一个证明，证明受检者等于模式：

open import Relation.Binary.PropositionalEquality

filter-lem-b : {A : Set} -> (p : A -> Bool) -> (xs : List A) -> All (satisfies p) (filter p xs)
filter-lem-b p []        = vacuo
filter-lem-b p (x :: xs) with p x | inspect p x
... | true  | [ eq ] = holds _ _ (subst isTrue (sym eq) _) (filter-lem-b p xs)
... | false | [ eq ] = filter-lem-b p xs

为什么这个 Agda 程序不会在 `with` 子句下规范化表达式？

Why this Agda program won't normalize an expression under a `with` clause?

agda