Why agda with-abstraction don't erase some clauses?

Question

I'm trying to write a theorem left as exercise in the Dependently Typed Programming in Agda tutorial written by Ulf Norell and James Chapman (page 23) and I don't understand a probably very simple thing about with.

Essentially I have these definitions

data   False : Set where
record True  : Set where

data Bool : Set where
  true  : Bool
  false : Bool

isTrue : Bool -> Set
isTrue true  = True
isTrue false = False

satisfies : {A : Set} -> (A -> Bool) -> A -> Set
satisfies p x = isTrue (p x)

data List (A : Set) : Set where
  []   : List A
  _::_ : (x : A)(xs : List A) -> List A

infixr 30 _:all:_
data All {A : Set} (P : A -> Set) : List A -> Set where
  all[]   : All P []
  _:all:_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)

filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
... | true  = x :: filter p xs
... | false = filter p xs

and I'm trying to solve this

filter-all-lem : ∀ {p xs} -> All (satisfies p) (filter p xs)
filter-all-lem {p} {[]} with filter p []
... | [] = all[]
... | f :: fs = ?
filter-all-lem {p} {x :: xs} = ?

On the second hole I haven't tried anything yet and probably that's not the better way to to this, but my question isn't this one.

filter p [] is the first case of filter. It expands to []. So why agda can't infer that the case f :: fs is not possible? Unification should solve this really easily. But if I try to remove the clause entirely or use the absurd pattern I receive errors because not all the possibilities are covered.

And if the unification rules of agda don't do this automatically, how can I force it to be aware of it? Maybe rewrite? (I don't know how to rewrite in agda by now)

Twan van Laarhoven Twan van Laarhoven · Accepted Answer · 2019-09-03T14:59:21

The with filter p [] is not needed in this case, as you say, you can already deduce that filter p [] = []. So you can just write

filter-all-lem {p} {[]} = all[]

For understanding with clauses it helps to know how Agda expands these, which is as a local function, where the thing being matched on (filter p [] in this case) is a new parameter. So you get

filter-all-lem {p} {[]} = helper {p} (filter p [])
  where
  helper :: ∀ {p} ys -> All (satisfies p) ys
  helper [] = all[]
  helper (f :: fs) = ?

And inside the helper you actually lose the knowledge that the list is empty. There is the inspect idiom in the standard library to keep this knowledge around in the form of an equality, but you don't need that here.

As a general rule for proving things about a function that uses with (such as filter (x :: xs)), you should have the exact same structure of with clauses in your proofs, or with clauses that include the things being matched on in dependent types.

Why agda with-abstraction don't erase some clauses?

1 Answers