QuickSortが停止する事をあぐだくんに教えてあげたい

けれども、分かりません・・・。

module QSort where
  
open import Data.List
open import Data.Bool
open import Data.Product

data Nat : Set0 where
  zero : Nat
  succ : Nat -> Nat

Length : {A : Set0} -> List A -> Nat
Length [] = zero
Length (x ∷ xs) = succ (Length xs) 

_<_ : Nat -> Nat -> Bool
_ < zero = false    
zero < _ = true
(succ a) < (succ b) = a < b

filter1 : (Nat -> Bool) -> List Nat -> List Nat
filter1 p [] = []
filter1 p (x &#8759; xs) with p x | filter1 p xs
... | true  | ys = (x &#8759; ys)
... | false | ys = ys

sort : List Nat -> List Nat
sort [] = []
sort (x &#8759; xs) = (sort first) ++ [ x ] ++ (sort last)
  where
    first : List Nat
    first = filter1 (λ v -> v < x) xs
    last  : List Nat
    last  = filter1 (λ v -> not (v < x)) xs

filter1は停止性が勝手に確認されるらしくて良いんですけれども、sortは一方そうは行かない感じです。

このプログラムを書く人間からしてみると

first = filter1 (λ v -> v < x) xs 'は' (x &#8759; xs) 'よりも短い'

という事が分かっていて、lastも同様で、sortは元のリストより短いリストを作りそれに繰り返し適用していくので、いつかは再帰が止まるという事が分かります。

が、あぐだくんは何考えているのか知らないんですけれども、少なくともfilter1した結果が、filter1を適用したリストよりも小さくなる

filter1 (λ v -> v < x) xs <= xs

という事が分かって無いんじゃないかと思います。これが分からないと

filter1 (λ v -> v < x) xs <= xs かつ xs <= x &#8759; xs したがって
first = filter1 (λ v -> v < x) xs 'は' (x &#8759; xs) 'よりも短い'

という事が言えません。

さて、そうしたらどうやって教えれば良いのかとかいう感じなんですけれども・・・。

色々

data NatPair : Nat -> Nat -> Set0 where
  nat_pair : (a : Nat) -> (b : Nat) -> NatPair a b

LE : (a : Nat) -> (b : Nat) -> NatPair b b
LE n m = ∃(x : Nat) . nat_pair (x + n) m

みたいなん出来ないかなー。

このLEが定義出来ると、LE (succ zero) zeroみたいな事は取りあえず出来なくなるので、それは制約につながってどうにかなってくれるかなーみたいな。