製品内の値（Σ）を調べる方法は？

Question

関数で再生することで、Σタイプの周りを頭で囲んでいます。これは、リストで利用できる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であることを伝えることができないので、それは私を許可していません返信する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を与えています。これらの表現は、判決的にも命題的にも同等ではありません。あなたの例では今

：あなたはxsの長さにlength名前を与えてくれた

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

。そしてそれは5に縮小されません。それは名前です。名前をつけて名前を覚えておきたい場合は、

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

という名前のイディオムがあります。