Searching with intensional equality, maybe

Declist.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Equality

-- See http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

open import Search

module Declist (A : Set)(_=dec=_ : BiDecidable _≡_) where

Search : (x : A) → (xs : List A) → Set
Search x xs = Find (x =dec=_) xs

_∈?_ : (x : A) → (xs : List A) → Search x xs
x ∈? xs = find (x =dec=_) xs

data _∈_ (x : A) : List A → Set where
  head : ∀{y ys} → isYes (x =dec= y) → x ∈ (y ∷ ys)
  tail : ∀{y ys} → x ∈ ys            → x ∈ (y ∷ ys)

data _∉_ (x : A) : List A → Set where
  empty : x ∉ []
  noteq : ∀{y ys} → isNo (x =dec= y) → x ∉ ys → x ∉ (y ∷ ys)

nono : ∀ x xs → x ∉ xs → ¬(x ∈ xs)
nono x .[] empty = λ ()
nono x (y ∷ ys) (noteq isneq nin) (head iseq) = consistent iseq isneq
nono x (y ∷ ys) (noteq isneq nin) (tail ins) = nono x ys nin ins

--notnot : ∀ x xs → ¬(x ∈ xs) → x ∉ xs
--notnot x [] notin = empty
--notnot x (y ∷ ys) notin = noteq {!   !} (notnot x ys (λ z → notin (tail z)))

dec∈ : BiDecidable _∈_
dec∈ x [] = no (λ ())
dec∈ x (y ∷ xs) with x =dec= y

--data _∉_ (x : A) : List A → Set where
--  empty : x ∉ []
--  noteq : ∀{y ys} → isFalse (x == y) → x ∉ ys → x ∉ (y ∷ ys)
--
--missing∉ : ∀{xs x} → AllFalse (x ==_) xs → x ∉ xs
--missing∉ {[]} allpf = empty
--missing∉ {x ∷ xs} (x₂ ∷ allpf) = noteq x₂ (missing∉ allpf)
--
--found∈ : ∀{x} → ∀ xs y ys → isTrue (x == y) → x ∈ (xs ++ y ∷ ys)
--found∈ [] y ys pf = head pf
--found∈ (x ∷ xs) y ys pf = tail (found∈ xs y ys pf)
--
--decide : ∀{x xs} → Search x xs → (x ∈ xs) ⊎ (x ∉ xs)
--decide (missing pf)        = inr (missing∉ pf)
--decide (found xs' y ys pf) = inl (found∈ xs' y ys pf)
--
--
--consistent : (x : A) → (xs : List A) → x ∈ xs → x ∉ xs → False
--consistent x (y ∷ xs) (head x₁) (noteq x₂ pf∉) with x == y
--consistent x (y ∷ xs) (head ()) (noteq x₂ pf∉) | false
--consistent x (y ∷ xs) (head x₁) (noteq () pf∉) | true
--consistent x (y ∷ xs) (tail pf∈) (noteq x₁ pf∉) = consistent x xs pf∈ pf∉

Search.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.List
open import Agda.Builtin.Equality

-- See http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf

module Search where

_++_ : {A : Set} → List A → List A → List A
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
infixr 4 _++_

not : Bool → Bool
not false = true
not true  = false

_∘_ : ∀{k n m}{A : Set k}{B : A → Set n}{C : (x : A) → B x → Set m}
      → (f : {x : A} → (y : B x) → C x y)
      → (g : (x : A) → B x)
      → ((x : A) → C x (g x))
(f ∘ g) x = f (g x)

record Σ (S : Set)(T : S → Set) : Set where
  constructor _,_
  field
    fst : S
    snd : T fst
open Σ

_×_ : (A : Set) → (B : Set) → Set
A × B = Σ A λ _ → B

_⇔_ : (A : Set) → (B : Set) → Set
A ⇔ B = (A → B) × (B → A)

data ⊥ : Set where
¬_ : (A : Set) → Set
¬ A = A → ⊥

data Inspect {A : Set}(x : A) : Set where
  _with≡_ : (y : A) → x ≡ y → Inspect x

inspect : {A : Set} → (x : A) → Inspect x
inspect x = x with≡ refl


data All {A : Set}(P : A → Set) : List A → Set where
  []  : All P []
  _∷_ : ∀{x xs} → P x → All P xs → All P (x ∷ xs)

all++ : {A : Set} → ∀{xs ys} → {P : A → Set} → All P xs → All P ys → All P (xs ++ ys)
all++ [] ys = ys
all++ (x ∷ xs) ys = x ∷ all++ xs ys

all++l : {A : Set} → ∀{xs ys} → {P : A → Set} → All P (xs ++ ys) → All P xs
all++l {_} {[]} _ = []
all++l {_} {_ ∷ _} (pfx ∷ pfrst) = pfx ∷ all++l pfrst

all++r : {A : Set} → ∀{xs ys} → {P : A → Set} → All P (xs ++ ys) → All P ys
all++r {_} {_} {[]} pf = []
all++r {_} {[]} {y ∷ ys} pf = pf
all++r {_} {x ∷ xs} {y ∷ ys} (pfx ∷ pfrst) = all++r pfrst


data _⊎_ (A B : Set) : Set where
  inl : A → A ⊎ B
  inr : B → A ⊎ B

data Dec (A : Set) : Set where
  yes :   A → Dec A
  no  : ¬ A → Dec A

Decidable : {A : Set} → (A → Set) → Set
Decidable P = ∀ x → Dec (P x)

BiDecidable : {A B : Set} → (A → B → Set) → Set
BiDecidable P = ∀ x y → Dec (P x y)

data isYes {A : Set} : Dec A → Set where
  since : (x : A) → isYes (yes x)

data isNo {A : Set} : Dec A → Set where
  since : (x : ¬ A) → isNo (no x)

consistent : {A : Set} → {x : Dec A} → isYes x → isNo x → ⊥
consistent (since x) ()

yesIsYes : {A : Set}{a : A}{x : Dec A} → x ≡ (yes a) → isYes x
yesIsYes {_} {a} refl = since a

noIsNo : {A : Set}{a : ¬ A}{x : Dec A} → x ≡ (no a) → isNo x
noIsNo {_} {a} refl = since a

AllNo : {A : Set}{P : A → Set} → Decidable P → List A → Set
AllNo P xs = All (isNo ∘ P) xs

data Find {A : Set}{f : A → Set}(P : Decidable f) : List A → Set where
  missing : ∀{xs}     → AllNo P xs → Find P xs
  found   : ∀ xs y ys → isYes (P y)     → Find P (xs ++ y ∷ ys)

find : {A : Set}{f : A → Set} → (P : Decidable f) → (xs : List A) → Find P xs
find P [] = missing []
find P (x ∷ xs) with inspect (P x)
find P (x ∷ xs) | yes a with≡ eq = found [] x xs (yesIsYes eq)
find P (x ∷ xs) | no ¬a with≡ eq with find P xs
...                              | missing pf        = missing (noIsNo eq ∷ pf)
...                              | found pre y ys pf = found (x ∷ pre) y ys pf