2007/11/13

Transitivity Reprise

我證不出 permutation 的 transitivity!也就是說,如果 xs 和 ys 是彼此的 permutation,ys 和 zs 又是彼此的 permutation,那麼 xs 和 zs 也是彼此的 permutation(xs, ys, zs 都是 lists)。我用的「互為 permutation」的定義是

data IsPermutation {A : Set} : List A -> List A -> Set where
  perm-base : IsPermutation [] []
  perm-step : {x : A}{xs : List A}(ys zs : List A) ->
                IsPermutation xs (ys ++ zs) ->
                IsPermutation (x :: xs) (ys ++ x :: zs)

憑直覺照著 Agda 給的 context, goal type 那些互動資訊走的話,很容易導致 infinite recursion。只要這一步寫完,qsort 的正確性就完全證明了。

--
怎麼都是 transitivity…頭好痛 XD。

Labels: