Agdaの `Vec`に安全な` length`関数を書く方法は？

Question

Data.Vecがあるので、私たちはVecが何であるかを知っています。

NatとVecが同型であることを証明したいと思います。

は私はNATがVecをに変換できることを証明機能正常に作成されました：

ℕ→vec : (n : ℕ) → Vec ⊤ n 
ℕ→vec zero = [] 
ℕ→vec (suc a) = tt ∷ ℕ→vec a 

私は、対応するvec→ℕを書くしようとしていたときにしばらく、私は失敗しました。

私はこのような何かを書きたい（それはコンパイルされませんが、それは読みやすいです）：最初のコードで

vec→ℕ : ∀ {n} → Vec ⊤ n → (n : ℕ) 
vec→ℕ []  = zero 
vec→ℕ (tt ∷ a) = suc (vec→ℕ a) 

は、引数、戻り値の長さが正確であることを保証しています。 しかし、最初の引数の長さが正確に戻り値であることを確認するにはどうすればよいですか？

Answer 1

私はそれが最良の解決策であるかどうかわかりませんが、私が把握したものです。代わりに、結果が正確にnあるというの

open import Data.Vec 
open import Data.Unit 
open import Data.Nat 
open import Data.Product 

open import Relation.Binary.PropositionalEquality 

vec→ℕ : ∀ {n} → Vec ⊤ n → ∃ (λ m → n ≡ m) 
vec→ℕ []  = zero , refl 
vec→ℕ (tt ∷ a) with vec→ℕ a 
vec→ℕ (tt ∷ a) | m , refl = suc m , refl 

は、私がn ≡ mような機能がmを返すことを指定順に平等を導入しました。それがあなたを助けることを願っています。あなたの型シグネチャを使用して、私は解析エラーがあり、これを開発しました。

Answer 2

あなたは長さにvec→ℕがdefinitionally等しくすることができます：

vec→ℕ : ∀ {n} → Vec ⊤ n → ℕ 
vec→ℕ {n} _ = n 

そして私は、これはどこでもあなたが得るℕが正しいものであるという特性を必要とするだろうとAgdaに十分に透明だと思う、それは自動的に（つまり削減によって）利用できるようになります。

編集を追加するには：vec→ℕのタイプは、それが返すatural ℕを強要され規定していないので、あなたは、これがunderspecifiedさだと思うかもしれません。しかし、Agdaはこの定義を見ている。あなたがそれを必要とする場合は、次の外部正しさの証明を証明することができます（私はそれが任意の値を追加しないと主張したい）：vec→ℕ xsはnにdefinitionally等しいため、我々は必要としないことを

open import Relation.Binary.PropositionalEquality 

vec→ℕ-correct : ∀ {n} {xs : Vec ⊤ n} → vec→ℕ xs ≡ n 
vec→ℕ-correct = refl 

注意を証明書にnまたはxsのいずれかを見てください。

Answer 3

これはあまり意味がありません。リストNはNatと同型ですが、Vecの場合はすでにインデックスとして自然数を入れていますか？