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。