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)
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.