Agda의`Vec`에 안전한`length` 함수를 쓰는 방법은 무엇입니까?

Question

Data.Vec이 (가) 있으므로 Vec은 무엇인지 알고 있습니다.

Nat와 Vec이 동형임을 증명하고 싶습니다.

내가 성공적으로 냇가 VEC로 변환 할 수 있습니다 증명하는 함수를 만들었습니다 : I는 해당 vec→ℕ을 쓰기 위해 노력하고있어

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

동안, 나는 실패했습니다.

나는 이런 식으로 뭔가를 쓰고 싶어 (이 컴파일되지 않습니다 만 읽을 수의) : 첫 번째 코드에서

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을 반환하도록 지정 순서대로 평등을 도입했습니다. 그것이 당신을 돕길 바랍니다. 귀하의 형식 서명을 사용하여 구문 분석 오류가있어이를 개발했습니다.

당신은 길이 vec→ℕ이 definitionally 동일하게 만들 수

Answer 2

:

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

그건별로 의미가 없습니다. List N는 Nat와 동형이지만 Vec의 경우에는 이미 자연수를 인덱스로 넣고있는 것이 사실입니까 ???