Agda Vec how to filter out elements

Question

Hi I think I don't understand well how to use Vec.filter from Data/Vec.agda.

I know how to "filter in" (keep) elements in the vector

filterProof : v.filter (λ e → e ≟ 2) (2 v.∷ v.[]) ≡ (2 vb.∷ vb.[])
filterProof = refl

however I'm not sure how to "filter out" elements.

filterProof : v.filter (λ e → e ? 2) (2 v.∷ v.[]) ≡ vb.[]
filterProof = refl

I'm not sure what goes where ? is. I know the type needs to be Relation.Nullary.Dec but not sure how to express e ≠ 2 using what's available in Relation.Nullary.Dec.

Also I would like to know why Vec.filter doesn't filter using a Bool instead of Relation.Nullary.Dec like List.filter does.

Thanks!

Cactus Cactus · Accepted Answer · 2020-11-03T11:45:24

You can turn a decision procedure for a predicate into a decision procedure for its negation:

open import Relation.Nullary

dec-¬ : ∀ {a} {P : Set a} → Dec P → Dec (¬ P)
dec-¬ (yes p) = no λ prf → prf p
dec-¬ (no ¬p) = yes ¬p

which of course means you can negate decidable relations as well:

open import Relation.Binary

module _ {a} {A B : Set a} {ℓ} where
  neg : REL A B ℓ → REL A B ℓ
  neg R x y = ¬ (R x y)

  decidable-neg : ∀ {R : REL A B ℓ} → Decidable R → Decidable (neg R)
  decidable-neg dec x y = dec-¬ (dec x y)

Agda Vec how to filter out elements

1 Answers