double-recursive.idr

%default total

data DecreasingArg : List a -> Type where
  Base : DecreasingArg []
  Recurse : DecreasingArg xs -> ({y : List a} -> [] = y -> DecreasingArg y) -> DecreasingArg {a} (x :: xs)

toDecreasingArg : (l : List a) -> DecreasingArg l
toDecreasingArg [] = Base
toDecreasingArg (_ :: xs) =
    Recurse (toDecreasingArg xs) g
  where
    g : {y : List a} -> [] = y -> DecreasingArg y
    g Refl = Base

f : List a -> List a
f l = getWitness (f' l (toDecreasingArg l))
  where
    f' : (l : List a) -> .(DecreasingArg l) -> Subset (List a) (\x => [] = x)
    f' [] Base = Element [] Refl
    f' (x :: xs) (Recurse dxs pfn) = case (f' xs dxs) of
      (Element y p) => f' y (pfn p) -- Note that we match on 'p' here, not Refl. Refl would work but is cheating for the general case