{-# OPTIONS --cubical --safe #-}

module Data.List.Membership where

open import Data.List
open import Data.Fin
open import Data.Fin.Properties
open import Prelude
open import Relation.Nullary
open import Path.Reasoning
open import Data.List.Relation.Unary as Relation using (module Exists; module Congruence; ◇; ◇!)
import Data.Nat as ℕ
import Data.Nat.Properties as ℕ
open import Data.Maybe.Properties using (just-inj)

module _ {a} {A : Type a} {x : A} where
  open Exists (_≡ x)
    using (push; pull; push!; pull!; here!; _◇++_; _++◇_)
    renaming (◇? to _∈?_)
    public

infixr  _∈_ _∈!_ _∉_
_∈_ : A → List A → Type _
x ∈ xs = ◇ (_≡ x) xs

_∉_ : {A : Type a} → A → List A → Type a
x ∉ xs = ¬ (x ∈ xs)

_∈!_ : A → List A → Type _
x ∈! xs = ◇! (_≡ x) xs

cong-∈ : ∀ (f : A → B) {x : A} xs → x ∈ xs → f x ∈ map f xs
cong-∈ f {x} = Congruence.cong-◇ (_≡ x) (_≡ (f x)) (cong f)

fin∈tabulate :  ∀ {n}
                (f : Fin n → A)
                (i : Fin n) →
                f i ∈ tabulate n f
fin∈tabulate {n = suc _} f f0     = f0 , refl
fin∈tabulate {n = suc _} f (fs i)  =
  push (fin∈tabulate (f ∘ fs) i)

open import Function.Injective

at : ∀ {xs : List A} (n : Fin (length xs)) → (xs ! n) ∈ xs
at n = n , refl

module _ {a} {A : Set a} (_≟_ : Discrete A) where
  isSet⟨A⟩ : isSet A
  isSet⟨A⟩ = Discrete→isSet _≟_

  infixl  _\\_
  _\\_ : List A → A → List A
  xs \\ x = foldr f [] xs
    where
    f : A → List A → List A
    f y xs with x ≟ y
    ... | yes p = xs
    ... | no  p = y ∷ xs

  uniques : List A → List A
  uniques = foldr f []
    where
    f : A → List A → List A
    f x xs = x ∷ (xs \\ x)

  x∉xs\\x : ∀ x xs → x ∉ xs \\ x
  x∉xs\\x x (y ∷ xs) (n , x∈xs) with x ≟ y
  x∉xs\\x x (y ∷ xs) (n      , x∈xs)  | yes p = x∉xs\\x x xs (n , x∈xs)
  x∉xs\\x x (y ∷ xs) (f0   , y≡x)   | no ¬p = ¬p (sym y≡x)
  x∉xs\\x x (y ∷ xs) (fs n  , x∈xs)  | no ¬p = x∉xs\\x x xs (n , x∈xs)

  x∈!x∷xs\\x : ∀ x xs → x ∈! x ∷ xs \\ x
  x∈!x∷xs\\x x xs = here! (refl , isSet⟨A⟩ _ _ refl) (x∉xs\\x x xs)

  x∉xs⇒x∉xs\\y : ∀ (x : A) y xs → x ∉ xs → x ∉ xs \\ y
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs x∈xs\\y with y ≟ z
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs x∈xs\\y | yes p =
    x∉xs⇒x∉xs\\y x y xs (x∉xs ∘ push) x∈xs\\y
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs (f0  , x∈xs\\y) | no ¬p =
    x∉xs (f0 , x∈xs\\y)
  x∉xs⇒x∉xs\\y x y (z ∷ xs) x∉xs (fs n , x∈xs\\y) | no ¬p =
    x∉xs⇒x∉xs\\y x y xs (x∉xs ∘ push) (n , x∈xs\\y)

  x∈!xs⇒x∈!xs\\y : ∀ (x : A) y xs → y ≢ x → x ∈! xs → x ∈! xs \\ y
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x x∈!xs with y ≟ z
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x x∈!xs | yes p =
    x∈!xs⇒x∈!xs\\y x y xs y≢x (pull! (y≢x ∘ p ;_) x∈!xs)
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x ((f0  , x∈xs) , uniq) | no ¬p =
    here! (x∈xs , isSet⟨A⟩ _ _ _) (x∉xs⇒x∉xs\\y x y xs (ℕ.znots ∘ cong FinToℕ ∘ cong fst ∘ uniq ∘ push))
  x∈!xs⇒x∈!xs\\y x y (z ∷ xs) y≢x ((fs n , x∈xs) , uniq) | no ¬p =
    push! z≢x (x∈!xs⇒x∈!xs\\y x y xs y≢x (pull! z≢x ((fs n , x∈xs) , uniq)))
    where z≢x = ℕ.snotz ∘ cong FinToℕ ∘ cong fst ∘ uniq ∘ (f0 ,_)

  ∈⇒∈! : (x : A) (xs : List A) → x ∈ xs → x ∈! uniques xs
  ∈⇒∈! x (y ∷ xs) (f0  , x∈xs) =
    subst (_∈! (y ∷ uniques xs \\ y)) x∈xs (x∈!x∷xs\\x y (uniques xs))
  ∈⇒∈! x (y ∷ xs) (fs n , x∈xs) with y ≟ x
  ... | yes p = subst (_∈! (y ∷ uniques xs \\ y)) p (x∈!x∷xs\\x y (uniques xs))
  ... | no ¬p = push! ¬p (x∈!xs⇒x∈!xs\\y x y (uniques xs) ¬p (∈⇒∈! x xs (n , x∈xs)))

infixr  _∈²_
_∈²_ : A → List (List A) → Type _
x ∈² xs = ◇ (x ∈_) xs

∈²→∈ : ∀ {x : A} xs → x ∈² xs → x ∈ concat xs
∈²→∈ = Relation.◇-concat (_≡ _)