Compute Simple Membership Proofs; Source of Idea: Agda Standard Library

InstMagic.agda

{-# OPTIONS --without-K --safe #-}
{- Works with Agda 2.6.2 -}

module InstMagic where

open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl)
open import Data.List using (List ; [] ; _∷_)
open import Data.Unit using (⊤ ; tt)
open import Data.Nat using (ℕ ; zero ; suc ; _≟_)
open import Data.List.Relation.Unary.Any using (Any ; any? ; here ; there)
open import Relation.Nullary.Decidable using (True ; toWitness)

elem : ∀ (x : ℕ) (xs : List ℕ) →
  {{True (any? (_≟_ x) xs)}} →
  Any (_≡_ x) xs
elem _ _ {{x∈xs-true}} = (toWitness x∈xs-true)

test : Any (_≡_ 5) (2 ∷ 5 ∷ 1 ∷ [])
test = elem 5 (2 ∷ 5 ∷ 1 ∷ [])

over-there : test ≡ there (here refl)
over-there = refl