List where items can be removed

remove.agda

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)


_++_ : {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)

data   False : Set where
record True  : Set where

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 = _

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)

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 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


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

isFound? : (x : ℕ)(xs : List ℕ) → Set
isFound? x xs = Find (_==_ x) xs

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

data _∉_ (x : ℕ) : List ℕ → 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} → isFound? x xs → (x ∈ xs) ⊎ (x ∉ xs)
decide (missing pf)        = inr (missing∉ pf)
decide (found xs' y ys pf) = inl (found∈ xs' y ys pf)

singleton : (n : ℕ) → ∀ x → x ∈ (n ∷ []) → isTrue (x == n)
singleton n x (head x₁) = x₁
singleton n x (tail ())

data Free : List ℕ → Set where
  start     : Free []
  assume    : ∀{xs} → (x : ℕ) → Free xs → Free (x ∷ xs)
  discharge : ∀{xs ys} → Free (xs ++ ys) → (x : ℕ) → {_ : ∀ y → y ∈ ys → isTrue (y == x)} → Free xs

simple : Free (5 ∷ []) → Free []
simple p = discharge p 5 {singleton 5}

general : (n : ℕ) →  Free (n ∷ []) → Free []
general n p = discharge p n {singleton n}