Proving length of mapped and filtered lists in Idris

First, let’s start by implementing map' and filter' for lists:

total map' : (a -> b) -> List a -> List b
map' _ [] = []
map' f (x :: xs) = f x :: map' f xs

total filter' : (a -> Bool) -> List a -> List a
filter' p []      = []
filter' p (x::xs) with (p x)
  filter' p (x::xs) | True  = x :: filter' p xs
  filter' p (x::xs) | False = filter' p xs

Trying a few cases:

Idris> map' (\x => x + 1) [1, 2]
[2, 3] : List Integer
Idris> filter' (\x => x /= 2) [1, 2]
[1] : List Integer

Looks neat.

A valid question would be: What do we know about the length of a mapped and length of a filtered list?

Intuition says that the length of a mapped list will be the same as the length of that list, since the values of the elements might change but not the actual length (size) of the original list. Let’s prove this fact:

-- For any given list xs, and any function f, the length of xs is same as the length of xs mapped with f
total theorem_1 : (xs : List a) -> (f : a -> b) -> length xs = length (map' f xs)
theorem_1 [] _        = Refl
theorem_1 (x :: xs) f = let I_H = theorem_1 xs f in rewrite I_H in Refl

Easy peasy, just use induction.

Filtering is a bit trickier. The length of a filtered list can be less than or equal to the original list. The intuitive reasoning for this is as follows:

Maybe the filter will apply to some elements, in which case the length of the filtered list will be less than the length of the original list
Or, maybe the filter will not apply at all, in which case the length of the filtered list is the same as the length of the original list

Let’s prove it!

-- For any given list xs, and any filtering function f, the length of xs >= the length of xs filtered with f
total theorem_2 : (xs : List a) -> (f : a -> Bool) -> LTE (length (filter' f xs)) (length xs)
theorem_2 [] _        = LTEZero {right = 0}
theorem_2 (x :: xs) f with (f x)
  theorem_2 (x :: xs) f | False = let I_H = theorem_2 xs f in let LTESuccR_I_H = lteSuccRight I_H in LTESuccR_I_H
  theorem_2 (x :: xs) f | True  = let I_H = theorem_2 xs f in let LTESucc_I_H  = LTESucc I_H in LTESucc_I_H

I constructed this proof using holes. The base case was very simple, however, for the inductive step we needed to do something else. With the inductive step we consider two cases:

In the case the filter was applied (False), the I_H needs to match the target type LTE _ (S _)
In the case the filter was not applied (True), the I_H needs to match the target type LTE (S _) (S _)

Idris has built-in proofs for these, with the following types:

Idris> :t lteSuccRight
lteSuccRight : LTE n m -> LTE n (S m)
Idris> :t LTESucc
LTESucc : LTE left right -> LTE (S left) (S right)

So we just needed to use them to conclude the proof.

Bonus: The only reason I rewrote filter' was to use with which seems easier to rewrite to when proving stuff about it. The built-in filter uses ifThenElse and I haven’t found a way to rewrite goals that are using it. I rewrote map' just for consistency.

Bonus 2: Thanks to gallais@reddit for this hint. It seems that the same with (f x) used in the proof also makes the ifThenElse reduce.