Proving that concatenating two increasing lists produces an increasing list

Question

Let's consider a predicate showing that the elements in the list are in increasing order (and for simplicity let's only deal with non-empty lists):

mutual
  data Increasing : List a -> Type where
    SingleIncreasing  : (x : a) -> Increasing [x]
    RecIncreasing     : Ord a => (x : a) ->
                                 (rest : Increasing xs) ->
                                 (let prf = increasingIsNonEmpty rest
                                  in x <= head xs = True) ->
                                 Increasing (x :: xs)

  %name Increasing xsi, ysi, zsi

  increasingIsNonEmpty : Increasing xs -> NonEmpty xs
  increasingIsNonEmpty (SingleIncreasing y) = IsNonEmpty
  increasingIsNonEmpty (RecIncreasing x rest prf) = IsNonEmpty

Now let's try to write some useful lemmas with this predicate. Let's start with showing that concatenating two increasing lists produces an increasing list, given that the last element of the first list is not greater than the first element of the second list. The type of this lemma would be:

appendIncreasing : Ord a => {xs : List a} ->
                            (xsi : Increasing xs) ->
                            (ysi : Increasing ys) ->
                            {auto leq : let xprf = increasingIsNonEmpty xsi
                                            yprf = increasingIsNonEmpty ysi
                                        in last xs <= head ys = True} ->
                            Increasing (xs ++ ys)

Let's now try to implement it! A reasonable way seems to be case-splitting on xsi. The base case where xsi is a single element is trivial:

appendIncreasing {leq} (SingleIncreasing x) ysi = RecIncreasing x ysi leq

The other case is more complicated. Given

appendIncreasing {leq} (RecIncreasing x rest prf) ysi = ?wut

it seems reasonable to proceed by recursively proving this for the result of joining rest and ysi by relying on leq and then prepending x using the prf. At this point the leq is actually a proof of last (x :: xs) <= head ys = True, and the recursive call to appendIncreasing would need to have a proof of last xs <= head ys = True. I don't see a good way to directly prove that the former implies the latter, so let's fall back to rewriting and first write a lemma showing that the last element of a list isn't changed by prepending to the front:

lastIsLast : (x : a) -> (xs : List a) -> {auto ok : NonEmpty xs} -> last xs = last (x :: xs)
lastIsLast x' [x] = Refl
lastIsLast x' (x :: y :: xs) = lastIsLast x' (y :: xs)

Now I would expect to be able to write

appendIncreasing {xs = x :: xs} {leq} (RecIncreasing x rest prf) ysi =
  let rest' = appendIncreasing {leq = rewrite lastIsLast x xs in leq} rest ysi
  in ?wut

but I fail:

When checking right hand side of appendIncreasing with expected type
        Increasing ((x :: xs) ++ ys)

When checking argument leq to Sort.appendIncreasing:
        rewriting last xs to last (x :: xs) did not change type last xs <= head ys = True

How can I fix this?

And, perhaps, my proof design is suboptimal. Is there a way to express this predicate in a more useful manner?

xash xash · Accepted Answer · 2018-04-10T14:39:48

If rewrite doesn't find the right predicate, try to be explicit with replace.

appendIncreasing {a} {xs = x :: xs} {ys} (RecIncreasing x rest prf) ysi leq = 
  let rekPrf = replace (sym $ lastIsLast x xs) leq
               {P=\T => (T <= (head ys {ok=increasingIsNonEmpty ysi})) = True} in
  let rek = appendIncreasing rest ysi rekPrf in
  let appPrf = headIsHead xs ys {q = increasingIsNonEmpty rek} in
  let extPrf = replace appPrf prf {P=\T => x <= T = True} in
  RecIncreasing x rek extPrf

with

headIsHead : (xs : List a) -> (ys : List a) ->
             {auto p : NonEmpty xs} -> {auto q : NonEmpty (xs ++ ys)} ->
             head xs = head (xs ++ ys)
headIsHead (x :: xs) ys = Refl

Some suggestions:

Use Data.So x instead of x = True, makes run-time functions easier to write.
Lift Ord a from the constructor to the type, making it more clear which ordering is used (and you don't have to match on {a} at appendIncreasing, I guess).
Don't forget that you can match on variables in constructors, so instead of repeating that Increasing xs has NonEmpty xs, just use Increasing (x :: xs).

Leading to:

data Increasing : Ord a -> List a -> Type where
  SingleIncreasing : (x : a) -> Increasing ord [x]
  RecIncreasing    : (x : a) -> Increasing ord (y :: ys) ->
                                So (x <= y) ->
                                Increasing ord (x :: y :: ys)

appendIncreasing : {ord : Ord a} ->
                   Increasing ord (x :: xs) -> Increasing ord (y :: ys) ->
                   So (last (x :: xs) <= y) ->
                   Increasing ord ((x :: xs) ++ (y :: ys))

Should make proving things a lot easier, especially if you want to include empty lists.

Proving that concatenating two increasing lists produces an increasing list

1 Answers