18

_+_-Operation forは通常、Nat最初の引数で再帰的に定義されるため、型チェッカーがそれを知ることは明らかに自明ではありませんi + 0 == i。ただし、固定サイズのベクトルに関数を記述すると、この問題に頻繁に遭遇します。

一例: アグダ関数を定義するにはどうすればよいですか

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)

nベクトルの最後に最初の値を置くのはどれですか?

Haskellでの簡単な解決策は

swap 0 xs     = xs
swap n (x:xs) = swap (n-1) (xs ++ [x])

私は次のようにAgdaで同様に試しました：

swap : {A : Set}{m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {_} {zero} xs          = xs 
swap {_} {_} {suc i} (x :: xs)  = swap {_} {_} {i} (xs ++ (x :: []))

ただし、タイプ チェッカーは次のメッセージで失敗します (これ{zero}は、上記のswap-Definition のケースに関連しています)。

.m != .m + zero of type Nat
when checking that the expression xs has type Vec .A (.m + zero)

それで、私の質問: アグダにどのように教えm == m + zeroますか? swapそして、そのような関数をAgdaでどのように書くのですか?

4

1 に答える 1

15

m == m + zero難しすぎないことをアグダに教えること。たとえば、等値証明に標準型を使用すると、次の証明を書くことができます。

rightIdentity : (n : Nat) -> n + 0 == n
rightIdentity zero = refl
rightIdentity (suc n) = cong suc (rightIdentity n)

rewrite次に、キーワードを使用してこの証明を使用するよう Agda に指示できます。

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)    
swap {_} {m} {zero} xs rewrite rightIdentity m = xs 
swap {_} {_} {suc i} (x :: xs) = ?

ただし、2 番目の方程式に必要な証明を提供することは、はるかに困難です。一般に、計算の構造を型の構造と一致させようとする方がはるかに良い考えです。そうすれば、定理の証明を大幅に減らすことができます (この場合は何もしません)。

たとえば、

drop : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A m
take : {A : Set} {m : Nat} -> (n : Nat) -> Vec A (n + m) -> Vec A n

(どちらも定理の証明なしで定義できます)、Agda は大騒ぎせずにこの定義を喜んで受け入れます。

swap : {A : Set} {m n : Nat} -> Vec A (n + m) -> Vec A (m + n)
swap {_} {_} {n} xs = drop n xs ++ take n xs
于 2012-10-18T16:00:57.370 に答える