Agda: std-lib: List: check that a filtered list is empty

Question

I have a function filter':

filter' : {A : Set} → (A → Bool) → List A → List A
filter' p []               = l.[]
filter' p (x ∷ xs) with (p x)
...                | true  = x l.∷ filter' p xs
...                | false = filter' p xs

and a function DeleteNat:

DeleteNat : (List ℕ) → ℕ → (List ℕ)
DeleteNat nats id = filter' (λ n → not (n ≡ᵇ id)) nats

where _≡ᵇ_ is:

open import Agda.Builtin.Nat public
  using () renaming (_==_ to _≡ᵇ_)

and would like to show that after applying DeleteNat, there remains no natural number equal to the id in the List:

DeleteNatRemoveNatWithId :
  (nats : List ℕ) (id : ℕ) →
    filter' (λ n → n ≡ᵇ id) (DeleteNat nats id) ≡ l.[]
DeleteNatRemoveNatWithId []       id         = refl
DeleteNatRemoveNatWithId (x ∷ xs) id with x ≡ᵇ id
...                                  | true  = DeleteNatRemoveNatWithId xs id
...                                  | false = {!  !}

I'm unsure how to continue at {! !}. I get a hunch that it should be done using cong.

Using C-c C-. I see that I need to satisfy this type:

(filter' (λ n → n ≡ᵇ id) (x List.∷ filter' (λ n → not (n ≡ᵇ id)) xs) | x ≡ᵇ id) ≡ List.[]

I guess I need a way to somehow get the x List.∷ into the second argument of the first filter'.

Could I get a hint as to how to advance here? Is my assumption about using cong wrong?

Answer 1

filter' ... (x ∷ filter' ... xs) | x ≡ᵇ id) means that the evaluation of this function is stuck on the test x ≡ᵇ id.

To have it reduce, you would typically use with x ≡ᵇ id. But you've already done that! Yes, but the with you used targeted the inner filter that was stuck at the time. Once it got unstuck, it computed enough to emit x ∷ _ and that got the outer filter stuck on the second test (that happens to be equal to the first one).

The idiomatic way to deal with this is via the inspect idiom that will allow you to, in a single with, get your hands on not only the result of x ≡ᵇ id but also a proof that the result was computed from this expression. Once you reach the point where the outer filter is stuck, you can simply rewrite by this equation and you should then be able to see the function compute just enough that it will be possible to call the induction hypothesis.