how can i filter out the elements?

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)

CLICK HERE to find out more related problems solutions.

Leave a Comment

Your email address will not be published.

Scroll to Top