NotMembership.agda

open import Level using (Level)
open import Function using (_$_; _∘_)
open import Data.List.Base
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Relation.Nullary using (¬_; yes; no)
open import Relation.Nullary.Negation using (contradiction)
open import Relation.Binary using (_⇒_; Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)

module _
       {a} {A : Set a}
       (_≟_ : Decidable (_≡_ {A = A}))
       where

  infix 4 _∈_ _∉_ _∉′_

  _∈_ _∉_ _∉′_ : A → List A → Set _
  x ∈ xs = Any (x ≡_) xs
  x ∉ xs = ¬ (x ∈ xs)
  x ∉′ xs = All (x ≢_) xs

  ∉⇒∉′ : _∉_ ⇒ _∉′_
  ∉⇒∉′ {x} {[]}     _ = []
  ∉⇒∉′ {x} {y ∷ xs} ¬p with x ≟ y
  ... | yes x≡y = contradiction (here x≡y) ¬p
  ... | no x≢y = x≢y ∷ ∉⇒∉′ (¬p ∘ there)

  ∉′⇒∉ : _∉′_ ⇒ _∉_
  ∉′⇒∉ {x} {y ∷ xs} (x≢y ∷ q) (here x≡y) = contradiction x≡y x≢y
  ∉′⇒∉ {x} {y ∷ xs} (x≢y ∷ q) (there p) = ∉′⇒∉ q p