Proving theorems about functions with cases

Question

Let's say we have a function merge that, well, just merges two lists:

Order : Type -> Type
Order a = a -> a -> Bool

merge : (f : Order a) -> (xs : List a) -> (ys : List a) -> List a
merge f xs [] = xs
merge f [] ys = ys
merge f (x :: xs) (y :: ys) = case x `f` y of
                                   True  => x :: merge f xs (y :: ys)
                                   False => y :: merge f (x :: xs) ys

and we'd like to prove something clever about it, for instance, that merging two non-empty lists produces a non-empty list:

mergePreservesNonEmpty : (f : Order a) ->
                         (xs : List a) -> (ys : List a) ->
                         {auto xsok : NonEmpty xs} -> {auto ysok : NonEmpty ys} ->
                         NonEmpty (merge f xs ys)
mergePreservesNonEmpty f (x :: xs) (y :: ys) = ?wut

Inspecting the type of the hole wut gives us

wut : NonEmpty (case f x y of   True => x :: merge f xs (y :: ys) False => y :: merge f (x :: xs) ys)

Makes sense so far! So let's proceed and case-split as this type suggests:

mergePreservesNonEmpty f (x :: xs) (y :: ys) = case x `f` y of
                                                    True => ?wut_1
                                                    False => ?wut_2

It seems reasonable to hope that the types of wut_1 and wut_2 would match the corresponding branches of merge's case expression (so wut_1 would be something like NonEmpty (x :: merge f xs (y :: ys)), which can be instantly satisfied), but our hopes fail: the types are the same as for the original wut.

Indeed, the only way seems to be to use a with-clause:

mergePreservesNonEmpty f (x :: xs) (y :: ys) with (x `f` y)
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | True = ?wut_1
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | False = ?wut_2

In this case the types would be as expected, but this leads to repeating the function arguments for every with branch (and things get worse once with gets nested), plus with doesn't seem to play nice with implicit arguments (but that's probably worth a question on its own).

So, why doesn't case help here, are there any reasons besides purely implementation-wise behind not matching its behaviour with that of with, and are there any other ways to write this proof?

HTNW HTNW · Accepted Answer · 2018-05-01T21:35:00

The stuff to the left of the | is only necessary if the new information somehow propagates backwards to the arguments.

mergePreservesNonEmpty : (f : Order a) ->
                         (xs : List a) -> (ys : List a) ->
                         {auto xsok : NonEmpty xs} -> {auto ysok : NonEmpty ys} ->
                         NonEmpty (merge f xs ys)
mergePreservesNonEmpty f (x :: xs) (y :: ys) with (x `f` y)
  | True = IsNonEmpty
  | False = IsNonEmpty

-- for contrast
sym' : (() -> x = y) -> y = x
sym' {x} {y} prf with (prf ())
-- matching against Refl needs x and y to be the same
-- now we need to write out the full form
  sym' {x} {y=x} prf | Refl = Refl

As for why this is the case, I do believe it's just the implementation, but someone who knows better may dispute that.

Proving theorems about functions with cases

2 Answers