Proving `T b` when `b` is already matched on

Question

I am trying to prove something simple:

open import Data.List
open import Data.Nat
open import Data.Bool
open import Data.Bool.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Unit

repeat : ∀ {a} {A : Set a} → ℕ → A → List A
repeat zero x = []
repeat (suc n) x = x ∷ repeat n x

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x

I thought proving filter-repeat is going to be easy by pattern matching on p x:

filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x
filter-repeat p x () (suc n) | false
filter-repeat p x prf (suc n) | true  = cong (_∷_ x) (filter-repeat p x prf n)

However this complains that prf : ⊤ is not of type T (p x). So I thought, OK, this seems like a familiar problem, let's whip out inspect:

filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true  | [ eq ] rewrite eq = cong (_∷_ x) (filter-repeat p x {!!} n)

but despite the rewrite, the type of the hole is still T (p x) instead of T true. Why is that? How do I reduce its type to T true so I can fill it with tt?

Workaround

I was able to work around it by using T-≡:

open import Function.Equality using (_⟨$⟩_)
open import Function.Equivalence

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf zero = refl
filter-repeat p x prf (suc n) with p x | inspect p x
filter-repeat p x () (suc n) | false | _
filter-repeat p x tt (suc n) | true  | [ eq ] = cong (_∷_ x) (filter-repeat p x (Equivalence.from T-≡ ⟨$⟩ eq) n)

but I would still like to understand why the inspect-based solution doesn't work.

Answer 1

As András Kovács says the inductive case requires prf to be of type T (p x) while you've already changed it to just ⊤ by pattern matching on p x. One simple solution is just to call filter-repeat recursively before pattern matching on p x:

open import Data.Empty

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf  0      = refl
filter-repeat p x prf (suc n) with filter-repeat p x prf n | p x
... | r | true  = cong (x ∷_) r
... | r | false = ⊥-elim prf

It also can sometimes be useful to use the protect pattern:

data Protect {a} {A : Set a} : A → Set where
  protect : ∀ x → Protect x

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x q  0      = refl
filter-repeat p x q (suc n) with protect q | p x | inspect p x
... | _ | true  | [ _ ] = cong (x ∷_) (filter-repeat p x q n)
... | _ | false | [ r ] = ⊥-elim (subst T r q)

protect q saves the type of q from being rewritten, but it also means that in the false case the type of q is still T (p x) rather than ⊥, hence the additional inspect.

Another variant of the same idea is

module _ {a} {A : Set a} (p : A → Bool) (x : A) (prf : T (p x)) where
  filter-repeat : ∀ n → filter p (repeat n x) ≡ repeat n x
  filter-repeat  0      = refl
  filter-repeat (suc n) with p x | inspect p x
  ... | true  | [ r ] = cong (x ∷_) (filter-repeat n)
  ... | false | [ r ] = ⊥-elim (subst T r prf)

module _ ... (prf : T (p x)) where prevents the type of prf from being rewritten as well.

Answer 2

Dependent pattern matching only affects the goal and the context at the exact point of their use. Matching on p xrewrites the current context and reduces the type of prf to ⊤ in the true branch.

However, when you do the recursive filter-repeat call, you once again supply x as argument there, and T (p x) in filter-repeat depends on that x, not the old one in the outer context, even though they're definitionally equal. We could've passed something other than x, hypothetically, so no assumption can be made about it before the filter-repeat call.

x can be made invariant in the context by factoring it out from the induction:

open import Data.Empty

filter-repeat : ∀ {a} {A : Set a} → (p : A → Bool) → (x : A) → T (p x) → ∀ n →
  filter p (repeat n x) ≡ repeat n x
filter-repeat p x prf = go where
  go : ∀ n → filter p (repeat n x) ≡ repeat n x
  go zero    = refl
  go (suc n) with p x | inspect p x
  go (suc n) | true  | [ eq ] = cong (_∷_ x) (go n)
  go (suc n) | false | [ eq ] = ⊥-elim (subst T eq prf)