如何检查产品内部的价值（Σ）？

Question

我正在尝试通过使用 filterVec 函数来了解 Σ 类型，类似于可用于列表的 filter 函数。请参阅下面的实现：

-- Some imports we will need later
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Data.Vec

-- The filterVec function
filterVec : {n : ℕ} -> (ℕ -> Bool) -> Vec ℕ n -> Σ ℕ (λ length → Vec ℕ length)
filterVec _ [] = 0 , []
filterVec f (x ∷ xs) with filterVec f xs
... | length , filtered = if f x then (suc length , x ∷ filtered) else (length , filtered)

对我的功能很满意，我决定测试一下

dummyVec : Vec ℕ 5
dummyVec = 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []

dummyFn : Vec ℕ 5
dummyFn with filterVec (λ _ → true) dummyVec
dummyFn | length , xs = {!!} -- I would like to return xs here, but Agda throws a type error

出于某种原因，Agda 无法分辨 length 是 5，所以它不允许我 return xs。但是，下面的代码确实有效：

open import Relation.Binary.PropositionalEquality
dummyProof : proj₁ (filterVec (λ _ → true) dummyVec) ≡ 5
dummyProof = refl

我对这种行为感到非常困惑。在 dummyFn 的情况下，Agda 无法判断长度为 5，但在 dummyProof 的情况下，Agda 可以毫无问题地证明它。

我错过了什么？我怎样才能让 dummyFn 工作？

Answer 1

with 将值绑定到名称。如果要计算，可以使用 let:

dummyFn′ : Vec ℕ 5
dummyFn′ = let length , xs = filterVec (λ _ → true) dummyVec
           in xs

让我们看下面的例子：

dummy : Set
dummy with 5
dummy | x = {!!}

洞中的x是否应该神奇地缩减为5？不，你给了 5 另一个名字 — x，这些表达式在判断上和命题上都不相等。

现在在你的例子中：

dummyFn : Vec ℕ 5
dummyFn with filterVec (λ _ → true) dummyVec
dummyFn | length , xs = {!!}

您已将 length 名称的长度设为 xs。而且它不会减少到 5。这是一个名字。如果你既想给出名字又想记住名字的用途，可以使用 inspect 成语：

dummyFn′′ : Vec ℕ 5
dummyFn′′ with filterVec (λ _ → true) dummyVec | inspect (filterVec (λ _ → true)) dummyVec
dummyFn′′ | length , xs | [ refl ] = xs

如何检查产品内部的价值（Σ）？

How to inspect the value inside a product (Σ)?

agda