≡-Reasoning and 'with' patterns
agda
Solution
The trouble with `with`-clauses is that Agda forgets the information it learned from pattern match unless you arrange beforehand for this information to be preserved.
More precisely, when Agda sees a `with expression` clause, it replaces all the occurences of `expression` in the current context and goal with a fresh variable `w` and then gives you that variable with updated context and goal into the with-clause, forgetting everything about its origin.
In your case, you write `filter p (map f (x ∷ xs))` inside the with-block, so it goes into scope after Agda has performed the rewriting, so Agda has already forgotten the fact that `p (f x)` is `true` and does not reduce the term.
You can preserve the proof of equality by using one of the "Inspect"-patterns from the standard library, but I'm not sure how it can be useful in your case.
Problem
I was proving some properties of `filter` and `map`, everything went quite good until I stumbled on this property: `filter p (map f xs) ≡ map f (filter (p ∘ f) xs)`. Here's a part of the code that's relevant: ``` open import Relation.Binary.PropositionalEquality open import Data.Bool open import Data.List hiding (filter) import Level filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A filter _ [] = [] filter p (x ∷ xs) with p x ... | true = x ∷ filter p xs ... | false = filter p xs ``` Now, because I love writing proofs using the `≡-Reasoning` module, the first thing I tried was: ``` open ≡-Reasoning open import Function filter-map : ∀ {a b} {A : Set a} {B : Set b} (xs : List A) (f : A → B) (p : B → Bool) → filter p (map f xs) ≡ map f (filter (p ∘ f) xs) filter-map [] _ _ = refl filter-map (x ∷ xs) f p with p (f x) ... | true = begin filter p (map f (x ∷ xs)) ≡⟨ refl ⟩ f x ∷ filter p (map f xs) -- ... ``` But alas, that didn't work. After trying for one hour, I finally gave up and proved it in this way: ``` filter-map (x ∷ xs) f p with p (f x) ... | true = cong (λ a → f x ∷ a) (filter-map xs f p) ... | false = filter-map xs f p ``` Still curious about why going through `≡-Reasoning` didn't work, I tried something very trivial: ``` filter-map-def : ∀ {a b} {A : Set a} {B : Set b} (x : A) xs (f : A → B) (p : B → Bool) → T (p (f x)) → filter p (map f (x ∷ xs)) ≡ f x ∷ filter p (map f xs) filter-map-def x xs f p _ with p (f x) filter-map-def x xs f p () | false filter-map-def x xs f p _ | true = -- not writing refl on purpose begin filter p (map f (x ∷ xs)) ≡⟨ refl ⟩ f x ∷ filter p (map f xs) ∎ ``` But typechecker doesn't agree with me. It would seem that the current goal remains `filter p (f x ∷ map f xs) | p (f x)` and even though I pattern matched on `p (f x)`, `filter` just won't reduce to `f x ∷ filter p (map f xs)`. Is there a way to make this work with `≡-Reasoning`? Thanks!