QSort in Agda, Round 4

This round we externally prove that qsort returns an increasingly-sorted list. The logic is quite the same, so I'll simply post the code without explanation. A "philosophical" argument follows the code.

partition-bdd : (p : Nat)(xs : List Nat) -> {m n : Nat} ->
                  (bddAbove m ⋯ bddBelow n) xs ->
                  ((\pair -> (bddAbove p ⋯ bddBelow n) (fst pair)) ⋯
                   (\pair -> (bddAbove m ⋯ bddBelow p) (snd pair)))
                  (partition p xs)
partition-bdd p [] {m}{n} _ = (bdd-above-base {p} ‖ bdd-below-base {n}) ‖
                              (bdd-above-base {m} ‖ bdd-below-base {p})
partition-bdd p (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  with partition p xs
     | partition-bdd p xs {m}{n} (xs-bddabv ‖ xs-bddblw)
     | cmp x p
... | < ys , zs > | (ys-bddabv ‖ ys-bddblw) ‖ zs-bddpfs | \/-IL x≼p =
  (bdd-above-step ys-bddabv x≼p ‖ bdd-below-step ys-bddblw n≼x) ‖ zs-bddpfs
... | < ys , zs > | ys-bddpfs ‖ (zs-bddabv ‖ zs-bddblw) | \/-IR p≼x =
  ys-bddpfs ‖ (bdd-above-step zs-bddabv x≼m ‖ bdd-below-step zs-bddblw p≼x)

qsort-inc-sorted : ∀ (\xs -> {m n : Nat} ->(bddAbove m ⋯ bddBelow n) xs ->
                     (IncSorted ⋯ bddAbove m ⋯ bddBelow n) (qsort xs))
qsort-inc-sorted [] bddpf = inc-sorted-base ‖ bddpf
qsort-inc-sorted (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  with partition x xs | partition-bdd x xs (xs-bddabv ‖ xs-bddblw)
... | < ys , zs > | ys-bdd ‖ zs-bdd
  with qsort-inc-sorted ys ys-bdd | qsort-inc-sorted zs zs-bdd
qsort-inc-sorted (x :: xs) {m}{n}
  (bdd-above-step xs-bddabv x≼m ‖ bdd-below-step xs-bddblw n≼x)
  | < ys , zs > | ys-bdd ‖ zs-bdd | ys'-sorted ‖ ys'-bddabv ‖ ys'-bddblw
                                  | zs'-sorted ‖ zs'-bddabv ‖ zs'-bddblw =
  inc-sorted-concat
    ys'-sorted
    (inc-sorted-step zs'-sorted zs'-bddblw (≼-refl {x}))
    ys'-bddabv
    (bdd-below-step zs'-bddblw (≼-refl {x})) ‖
  bdd-above-concat (relaxUpperBound ys'-bddabv x≼m)
                   (bdd-above-step zs'-bddabv x≼m) ‖
  bdd-below-concat ys'-bddblw
    (relaxLowerBound (bdd-below-step zs'-bddblw (≼-refl {x})) n≼x)

I think it is appropriate to name this kind of proof style externalism, while the intrusive approach taken in round 1 and 2 may be named internalism. The two terms are borrowed from Epistemology, where internalism requires one to provide justification for his/her (true) belief in order to claim that belief is knowledge, while externalism doesn't impose such a requirement but instead allows a justification to be provided externally by someone else.

So far my experience shows that externalism naturally leads to modularized proofs and (at least) won't take more effort than internalism, since Agda supports externalism reasonably well (e.g., magic with), while internalist proofs are coupled with algorithms or data structures and thus hard to combine or reuse. Besides, if one really needs an internalist version, he/she can simply write something like

qsort''′ : List Nat -> List Nat ∣ IncSorted
qsort''′ xs with lemma3 xs
qsort''′ xs | ∃-I _ (xs' ⋮ xs≡xs' ‖ xs'-bdd)
  with qsort-inc-sorted xs' xs'-bdd
qsort''′ xs | ∃-I _ (xs' ⋮ xs≡xs' ‖ xs'-bdd) | xs''-sorted ‖ _ =
  qsort xs ⋮ subst (\ys -> IncSorted (qsort ys)) xs≡xs' xs''-sorted

So currently I think externalism has the advantage over internalism. (Just contrary to the position I take toward epistemic internalism and externalism!)

--
The next (and, very likely, the final) round would be proving the ultimate correctness of qsort!

---

I think I'm going to stop here since I just can't prove that the relation IsPermutation xs ys is transitive... Anyway, the primary aim of this series of exercises has been achieved, and that's good. XD