Searching over a list with a decidable equality

.gitignore

*.agdai
*.vim

Decdeck.agda

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

open import Search
open import Deck

module Decdeck (A : Set)(_==_ : A → A → Bool) where
open import Declist A _==_

data AllExcept (P : A → Set) : List A → Deck A → Set where
  empty   : ∀{ys}      → AllExcept P ys ∅
  holds   : ∀{x ys xs} → P x → AllExcept P ys xs → AllExcept P ys (x ∷ xs)
  removed : ∀{x ys xs} → x ∈ ys → AllExcept P ys xs → AllExcept P ys (x ∷ xs)
  delete  : ∀{y ys xs} → AllExcept P (y ∷ ys) xs → AllExcept P ys (y ~ xs)
  both    : ∀{ys a b}  → AllExcept P ys a → AllExcept P ys b → AllExcept P ys (a ∪ b)

data AnyExcept (P : A → Set) : List A → Deck A → Set where
  here   : ∀{x ys xs} → P x → x ∉ ys → AnyExcept P ys (x ∷ xs)
  there  : ∀{x ys xs} → AnyExcept P ys xs → AnyExcept P ys (x ∷ xs)
  delete : ∀{y ys xs} → AnyExcept P (y ∷ ys) xs → AnyExcept P ys (y ~ xs)
  left   : ∀{ys xs d} → AnyExcept P ys xs → AnyExcept P ys (xs ∪ d)
  right  : ∀{ys xs d} → AnyExcept P ys xs → AnyExcept P ys (d ∪ xs)

data FindExcept (P : A → Bool)(ys : List A)(xs : Deck A) : Set where
  missing : AllExcept (isFalse ∘ P) ys xs → FindExcept P ys xs
  found   : AnyExcept (isTrue  ∘ P) ys xs → FindExcept P ys xs

AllDeck : (P : A → Set) → Deck A → Set
AllDeck P xs = AllExcept P [] xs

AnyDeck : (P : A → Set) → Deck A → Set
AnyDeck P xs = AnyExcept P [] xs

FindDeck : (A → Bool) → Deck A → Set
FindDeck P xs = FindExcept P [] xs


-- We use a couple of lemmae → shorten line length
private findexcept∷false : ∀ P x ys xs → P x ≡ false → FindExcept P ys (x ∷ xs)
private findexcept∷true  : ∀ P x ys xs → P x ≡ true  → FindExcept P ys (x ∷ xs)

findexcept : (P : A → Bool) → (ys : List A) → (xs : Deck A) → FindExcept P ys xs
findexcept P ys ∅         = missing empty
findexcept P ys (x ∷ xs)  with inspect (P x)
findexcept P ys (x ∷ xs)  | false with≡ eq = findexcept∷false P x ys xs eq
findexcept P ys (x ∷ xs)  | true  with≡ eq = findexcept∷true  P x ys xs eq
findexcept P ys (x ~ xs)  with findexcept P (x ∷ ys) xs
...                       | missing allfalse = missing (delete allfalse)
...                       | found   anytrue  = found (delete anytrue)
findexcept P ys (ls ∪ rs) with findexcept P ys ls
...                       | found   fl = found (left fl)
...                       | missing ml with findexcept P ys rs
...                                         | missing mr = missing (both ml mr)
...                                         | found   fr  = found (right fr)

findexcept∷false P x ys xs eq with findexcept P ys xs
...  | missing pf = missing (holds (falseIsFalse eq) pf)
...  | found pf   = found (there pf)

findexcept∷true P x ys xs eq with x ∈? ys
...  | missing pf      = found (here (trueIsTrue eq) (missing∉ pf))
...  | found vs w ws b with findexcept P ys xs
...                    | missing pf = missing (removed (found∈ vs w ws b) pf)
...                    | found   pf = found (there pf)


finddeck : (P : A → Bool) → (xs : Deck A) → FindDeck P xs
finddeck P xs = findexcept P [] xs

--_∈′?_ : (x : A) → (xs : Deck A) → FindDeck (x ==_) xs
--x ∈′? xs = finddeck (x ==_) xs



data ReductExcept : List A → Deck A → List A → Set where
  reduct∅  : ∀{ys} → ReductExcept ys ∅ []
  reduct∉∷ : ∀{ys xs xs' x} → x ∉ ys → ReductExcept ys xs xs' → ReductExcept ys (x ∷ xs) (x ∷ xs')
  reduct∈∷ : ∀{ys xs xs' x} → x ∈ ys → ReductExcept ys xs xs' → ReductExcept ys (x ∷ xs) xs'
  reduct~  : ∀{ys xs xs' y} → ReductExcept (y ∷ ys) xs xs' → ReductExcept ys (y ~ xs) xs'
  reduct∪  : ∀{ys xsl xsr xsl' xsr'} → ReductExcept ys xsl xsl' → ReductExcept ys xsr xsr' → ReductExcept ys (xsl ∪ xsr) (xsl' ++ xsr')


Reduct : Deck A → List A → Set
Reduct xs xs' = ReductExcept [] xs xs'


reductexcept : (ys : List A) → (xs : Deck A) → Σ (List A) (ReductExcept ys xs)
reductexcept ys ∅ = [] , reduct∅
Σ.fst (reductexcept ys (x ∷ xs)) with x ∈? ys
Σ.fst (reductexcept ys (x ∷ xs)) | missing x₁ = x ∷ Σ.fst (reductexcept ys xs)
Σ.fst (reductexcept ys (x ∷ xs)) | found xs₁ y ys₁ x₁ = Σ.fst (reductexcept ys xs)
Σ.snd (reductexcept ys (x ∷ xs)) with x ∈? ys
Σ.snd (reductexcept ys (x ∷ xs)) | missing x₁ = reduct∉∷ (missing∉ x₁) (Σ.snd (reductexcept ys xs))
Σ.snd (reductexcept ys (x ∷ xs)) | found xs₁ y ys₁ x₁ = reduct∈∷ (found∈ xs₁ y ys₁ x₁) (Σ.snd (reductexcept ys xs))
Σ.fst (reductexcept ys (x ~ xs)) = Σ.fst (reductexcept (x ∷ ys) xs)
Σ.snd (reductexcept ys (x ~ xs)) = reduct~ (Σ.snd (reductexcept (x ∷ ys) xs))
Σ.fst (reductexcept ys (xs₁ ∪ xs₂)) = Σ.fst (reductexcept ys xs₁) ++ Σ.fst (reductexcept ys xs₂)
Σ.snd (reductexcept ys (xs₁ ∪ xs₂)) = reduct∪ (Σ.snd (reductexcept ys xs₁)) (Σ.snd (reductexcept ys xs₂))

reduct : (xs : Deck A) → Σ (List A) (Reduct xs)
reduct xs = reductexcept [] xs

reduce : Deck A → List A
reduce xs = Σ.fst (reduct xs)

-- If a predicate is functional with respect to _==_, then it can be found in
-- the reduct iff it can be found in the deck

--founddeck? : ∀{P xs} → FindDeck P xs → Bool
--founddeck? (missing x) = false
--founddeck? (found x)   = true
--
extensional : ∀{b} → {B : Set b} → (A → B) → Set b
extensional P = ∀ x y → isTrue (x == y) → (P x) ≡ (P y)
--
--reductext : (P : A → Bool)  → (xs : Deck A) → (xs' : List A)
--            → extensional P
--            → Reduct xs xs'
--            → (founddeck? (finddeck P xs)) ≡ (found? (find P xs'))
--reductext P xs xs' ext red = ?


allreductexcept : ∀{ys xs'} → (P : A → Set) → extensional P → (xs : Deck A) → ReductExcept ys xs xs' → AllExcept P ys xs → All P xs'
allreductexcept P ext .∅ reduct∅ alldeck = []
allreductexcept P ext (x ∷ xs) (reduct∉∷ x₁ red) (holds x₂ alldeck) = x₂ ∷ allreductexcept P ext xs red alldeck
allreductexcept {ys} P ext (x ∷ xs) (reduct∉∷ x∉ys red) (removed x∈ys alldeck) with consistent x ys x∈ys x∉ys
allreductexcept {ys} P ext (x ∷ xs) (reduct∉∷ x∉ys red) (removed x∈ys alldeck) | ()
allreductexcept P ext (x ∷ xs) (reduct∈∷ x₁ red) (holds x₂ alldeck) = allreductexcept P ext xs red alldeck
allreductexcept P ext (x ∷ xs) (reduct∈∷ x₁ red) (removed x₂ alldeck) = allreductexcept P ext xs red alldeck
allreductexcept {ys} P ext (y ~ xs) (reduct~ red) (delete alldeck) = allreductexcept {y ∷ ys} P ext xs red alldeck
allreductexcept P ext (xsl ∪ xsr) (reduct∪ redl redr) (both pfl pfr) = all++ (allreductexcept P ext xsl redl pfl) (allreductexcept P ext xsr redr pfr)

allreduct : ∀{xs'} → (P : A → Set) → extensional P → (xs : Deck A) → Reduct xs xs' → AllDeck P xs → All P xs'
allreduct P ext xs red alldeck = allreductexcept P ext xs red alldeck


reductallexcept : ∀{ys xs'} → (P : A → Set) → extensional P → (xs : Deck A) → ReductExcept ys xs xs' → All P xs' → AllExcept P ys xs
reductallexcept P ext .∅ reduct∅ all = empty
reductallexcept P ext (x ∷ xs) (reduct∉∷ x₁ red) (x₂ ∷ all) = holds x₂ (reductallexcept P ext xs red all)
reductallexcept P ext (x ∷ xs) (reduct∈∷ x₁ red) all = removed x₁ (reductallexcept P ext xs red all)
reductallexcept P ext (x ~ xs) (reduct~ red) all = delete (reductallexcept P ext xs red all)
reductallexcept P ext (xsl ∪ xsr) (reduct∪ {_} {_} {_} {xsl'} {ysl'} redl redr) all = both (reductallexcept P ext xsl redl (all++l all)) (reductallexcept P ext xsr redr (all++r all))

Deck.agda

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

open import Search

module Deck where

data Deck (A : Set) : Set where
  ∅   : Deck A
  _∷_ : A → Deck A → Deck A
  _~_ : A → Deck A → Deck A
  _∪_ : Deck A → Deck A → Deck A

data IsNormal {A : Set} : Deck A → Set where
  ∅   : IsNormal ∅
  _∷_ : ∀{xs} → (x : A) → IsNormal xs → IsNormal (x ∷ xs)

fromlist : {A : Set} → List A → Deck A
fromlist {A} [] = ∅
fromlist {A} (x ∷ xs) = x ∷ fromlist xs

normal : {A : Set} → ∀{xs} → IsNormal xs → Deck A
normal {_} {xs} _ = xs

normalIsNormal : {A : Set} → ∀{xs} → ∀ pf → IsNormal (normal {A} {xs} pf)
normalIsNormal ∅        = ∅
normalIsNormal (x ∷ pf) = x ∷ pf

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)(_==_ : A → A → Bool) where

--_∈?_ : (x : A) → (xs : List A) → Find (_== x) xs
--x ∈? xs = find (_== x) xs
--
--_∈_ : A → List A → Set
--x ∈ xs with x ∈? xs
--(x ∈ xs)              | missing x₁       = False
--(x ∈ .(xs ++ y ∷ ys)) | found xs y ys x₁ = True
--
--_∉_ : A → List A → Set
--x ∈̷ xs with x ∈? xs
--(x ∈̷ xs)              | missing x₁       = True
--(x ∈̷ .(xs ++ y ∷ ys)) | found xs y ys x₁ = False

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

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

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

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   False : Set where
record True  : Set where
  constructor ⊤

isTrue : Bool → Set
isTrue false = False
isTrue true  = True

isFalse : Bool → Set
isFalse b = isTrue (not b)

trueIsTrue : ∀{x} → x ≡ true → isTrue x
trueIsTrue refl = _

falseIsFalse : ∀{x} → x ≡ false → isFalse x
falseIsFalse refl = _

notTrueAndFalse : ∀{x} → isTrue x → isFalse x → False
notTrueAndFalse {false} () pfFalse
notTrueAndFalse {true} pfTrue ()

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


AllTrue : {A : Set} → (A → Bool) → (List A → Set)
AllTrue P = All (isTrue ∘ P)

AllFalse : {A : Set} → (A → Bool) → (List A → Set)
AllFalse P = All (isFalse ∘ P)

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

data Find {A : Set}(P : A → Bool) : List A → Set where
  missing : ∀{xs}     → AllFalse P xs → Find P xs
  found   : ∀ xs y ys → isTrue (P y)         → Find P (xs ++ y ∷ ys)

find : {A : Set} → (P : A → Bool) → (xs : List A) → Find P xs
find P [] = missing []
find P (x ∷ xs) with inspect (P x)
...             | true  with≡ eq = found [] x xs (trueIsTrue eq)
...             | false with≡ eq with find P xs
...                              | missing pf = missing (falseIsFalse eq ∷ pf)
...                              | found pre y ys pf = found (x ∷ pre) y ys pf

found? : {A : Set} → {P : A → Bool} → {xs : List A} → Find P xs → Bool
found? (missing x) = false
found? (found xs y ys x) = true

test.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ)

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

open import Search
open import Deck
open import Declist ℕ _==_
open import Decdeck ℕ _==_


x = AllExcept
md : Deck ℕ
md = (1 ~ (1 ∷ 0 ∷ ∅)) ∪ (2 ~ (3 ∷ 2 ∷ ∅))

bg : List ℕ
bg = 0 ∷ 3 ∷ []

pf : AllDeck (_∈ bg) md
pf = both (delete (removed (head ⊤) (holds (head ⊤) empty))) (delete (holds (tail (head ⊤)) (removed (head ⊤) empty)))


rd : Reduct md bg
rd = reduct∪ (reduct~ (reduct∈∷ (head ⊤) (reduct∉∷ (noteq ⊤ empty) reduct∅))) (reduct~ (reduct∉∷ (noteq ⊤ empty) (reduct∈∷ (head ⊤) reduct∅)))


rde : reduce md ≡ bg
rde = refl

small : Reduct (3 ~ (2 ~ (1 ~ (((3 ∷ ∅) ∪ (1 ∷ ∅)) ∪ (2 ∷ ∅))))) []
small = reduct~ (reduct~  (reduct~   (reduct∪ (reduct∪ (reduct∈∷ (tail (tail (head ⊤))) reduct∅) (reduct∈∷ (head ⊤) reduct∅)) (reduct∈∷ (tail (head ⊤)) reduct∅))))

==refl : ∀ n → isTrue (n == n)
==refl zero = ⊤
==refl (suc n) = ==refl n

consist : ∀ n → n ≡ (suc n) → False
consist n ()


big : (p q r p⇒q⇒r : ℕ) → Reduct ((p⇒q⇒r) ~ (q ~ (p ~ ((((p⇒q⇒r) ∷ ∅) ∪ (p ∷ ∅)) ∪ (q ∷ ∅))))) []
big p q r p⇒q⇒r = reduct~ (reduct~ (reduct~ (reduct∪ (reduct∪ (reduct∈∷ (tail (tail (head (==refl p⇒q⇒r)))) {!   !}) {!   !}) {!   !})))