filter.idr

all' : (a -> Bool) -> List a -> Bool
all' f [] = True
all' f (x :: xs) = f x && all' f xs
  
allLemma : f x = True -> all' f xs = True -> all' f (x :: xs) = True
allLemma p1 p2 = rewrite p1 in rewrite p2 in Refl
  
allFiltered : (f : a -> Bool) -> (xs : List a) -> all' f (filter f xs) = True
allFiltered f [] = Refl
allFiltered f (x :: xs) = lemma (allFiltered f xs) (f x) Refl where
  lemma : all' f (filter f xs) = True -> (b : Bool) -> b = f x -> all' f (filter f (x :: xs)) = True
  lemma p False p2 =
    rewrite sym p2 in p
  lemma p True p2 = rewrite sym p2 in allLemma (sym p2) p

allFiltered : (f : a -> Bool) -> (xs : List a) -> all' f (filter f xs) = True
allFiltered f [] = Refl
allFiltered f (x::xs) with (f x) proof fx
  | True = rewrite sym fx in allFiltered f xs
  | False = allFiltered f xs

@clayrat Nice :)
I'm curious about the syntax in the with-rule though. What are proof and fx?
I originally thought to conduct the proof using the with-rule like this to just match on the result of f x, but this didn't appear to be refining the types. That is, f x was still appearing in types and wasn't getting replaced with True or False in the respective branches, so the ifThenElse expressions weren't reducing.

There's a section at the bottom of http://docs.idris-lang.org/en/latest/tutorial/views.html explaining this, basically fx is the name of the variable that will hold the proof that the expression being matched on equals the corresponding result for each matcher branch.

Oh my god, this is incredible! It's like Idris has the "inspect" pattern from Agda built right in! Thanks for showing me