{-# OPTIONS --safe  #-}

open import Level
open import Function.Base
open import Data.Maybe using (Maybe; Is-just; Is-nothing; nothing)
open import Data.Empty
open import Data.Unit
open import Data.List
import Data.List as L
open import Data.Fin
open import Data.Product hiding (map)
open import Data.Sum hiding (map)
open import Agda.Builtin.Equality
open import Data.Nat using (ℕ)
open import Data.List.Membership.Propositional
open import Data.List.Membership.Propositional.Properties
-- open import Data.List.Membership.Setoid.Properties
-- open import Data.List.Relation.Unary.Any.Properties as Any
open import Data.List.Relation.Unary.Any hiding (map)
open import Data.List.Relation.Unary.All hiding (map)
import Data.List.Relation.Unary.AllPairs as AllPairs
open import Relation.Nullary
import Data.Maybe.Relation.Unary.Any as Maybe-Any
import Data.Maybe.Relation.Unary.All as Maybe-All
import Data.List.Relation.Unary.Any as Any
open import Relation.Unary using (Pred)
import Relation.Unary as Pred
open import Relation.Binary.PropositionalEquality.Core
open import Relation.Binary.Definitions

open import Finite

module Auxiliary-Definitions where


infix -6 _↔_
_↔_ : ∀ {a} {b} (A : Set a) (B : Set b) → Set (a ⊔ b)
_↔_ A B = (A → B) × (B → A)


Injective : ∀ {a} {b} {A : Set a} {B : Set b} (f : A → B) → Set _
Injective f = ∀ {x} {y} → f x ≡ f y → x ≡ y

-- a bit like fold of Relation.Binary.Construction.Closure.Symmetric
∇-sym : ∀ {a} {r} {A : Set a} {R : A → A → Set r} → Symmetric R → ∀ {x} {y} → R x y ⊎ R y x → R x y
∇-sym _ (inj₁ Rxy) = Rxy
∇-sym sym (inj₂ Ryx) = sym Ryx

module SetM where
  _>>=_ : ∀ {a b c : Level} {A : Set c} → ((A → Set a) → Set b) → (A → Set a) → Set b
  _>>=_ f x = f x

Is-just-dec : ∀ {a} {A : Set a} {m : Maybe A} → Dec (Is-just m)
Is-just-dec {m = Maybe.just x} = yes (Maybe-Any.just tt)
Is-just-dec {m = nothing} = no (λ ())

dec²-Maybe : ∀ {a} {A : Set a} (m : Maybe A) → Is-just m ⊎ Is-nothing m
dec²-Maybe (Maybe.just x) = inj₁ (Maybe-Any.just tt)
dec²-Maybe nothing = inj₂ Maybe-All.nothing

¬Is-just : ∀ {a} {A : Set a} {m : Maybe A} → ¬ (Is-just m) → Is-nothing m
¬Is-just {m = Maybe.just x} ¬is-just = ⊥-elim (¬is-just (Maybe-Any.just tt))
¬Is-just {m = nothing} _ = Maybe-All.nothing

Is-just¬nothing : ∀ {a} {A : Set a} {m : Maybe A} → (Is-just m) → ¬ Is-nothing m
Is-just¬nothing {m = Maybe.just x} j (Maybe-All.just ())

is-just-⇒-ret-just : ∀ {a} {A : Set a} {j : Maybe A} → Is-just j → ∃[ x ] j ≡ Maybe.just x
is-just-⇒-ret-just {a} {A} {Maybe.just x} (Maybe-Any.just tt) = x , refl

ret-just-⇒-is-just : ∀ {a} {A : Set a} {x : A} {j : Maybe A} → j ≡ Maybe.just x → Is-just j
ret-just-⇒-is-just {a} {A} {j} eq rewrite eq = Maybe-Any.just tt

from-Is-just : ∀ {a} {A : Set a} {m : Maybe A} → (Is-just m) → A
from-Is-just {m = Maybe.just x} _ = x


¬¬-dec : ∀ {p} {P : Set p} → Dec P → ¬ ¬ P → P
¬¬-dec (yes w) _ = w
¬¬-dec (no w) ¬¬P = ⊥-elim (¬¬P w)

-- richer decision combinators:
dec² : ∀ {p} {P : Set p} → Dec P → P ⊎ ¬ P
dec² (yes p) = inj₁ p
dec² (no ¬p) = inj₂ ¬p

→-dec² : ∀ {a} {b} {A : Set a} {B nB : Set b} → Dec A → (B ⊎ nB) → (A → B) ⊎ (A × nB)
→-dec² (no ¬a) _ = inj₁ (λ a → ⊥-elim (¬a a))
→-dec² _ (inj₁ b) = inj₁ (λ _ → b)
→-dec² (yes a) (inj₂ ¬b) = inj₂ (a , ¬b)

dec²-∀⊎ : ∀ {a b p q : Level} {A : Set a} {B : Set b} {P : A ⊎ B → Set p} {Q : A ⊎ B → Set q}
          → (∀ x → P (inj₁ x)) ⊎ (∃[ x ] Q (inj₁ x))
          → (∀ x → P (inj₂ x)) ⊎ (∃[ x ] Q (inj₂ x))
          → (∀ x → P x) ⊎ (∃[ x ] Q x)
dec²-∀⊎ (inj₁ on-A) (inj₁ on-B) = inj₁ (λ { (inj₁ x) → on-A x ; (inj₂ x) → on-B x })
dec²-∀⊎ (inj₂ (x , Qx)) _ = inj₂ ((inj₁ x) , Qx)
dec²-∀⊎ _ (inj₂ (x , Qx)) = inj₂ ((inj₂ x) , Qx)

dec²-∀× : ∀ {a b p q : Level} {A : Set a} {B : Set b} {P : A × B → Set p} {Q : A × B → Set q}
          → (∀ x → ∀ y → P (x , y)) ⊎ (∃[ x ] ∃[ y ] Q (x , y))
          → (∀ xy → P xy) ⊎ (∃[ xy ] Q xy)
dec²-∀× (inj₁ curried) = inj₁ (λ (x , y) → curried x y)
dec²-∀× (inj₂ (x , y , Qxy)) = inj₂ ((x , y) , Qxy)

module dec²M where
  -- do-notation for decision procedures
  _>>=_ : ∀ {a ¬a b ¬b ℓ : Level}
            {X : Set ℓ}
            {A : X → Set a} {¬A : X → Set ¬a}
            {B : Set b} {¬B : Set ¬b}
            → ((∀ x → A x ⊎ ¬A x) → B ⊎ ¬B)
            → ((∀ x → A x ⊎ ¬A x) → B ⊎ ¬B)
  _>>=_ f x = f x
  _>>_ : ∀ {a ¬a b ¬b : Level}
            {A : Set a} {¬A : Set ¬a}
            {B : Set b} {¬B : Set ¬b}
            → (A ⊎ ¬A → B ⊎ ¬B)
            → (A ⊎ ¬A → B ⊎ ¬B)
  _>>_ f x = f x

module _ {a b} {A : Set a} {B : Set b} where

  data Is-inj₁ : A ⊎ B → Set (a ⊔ b) where
    inj₁ : ∀ x → Is-inj₁ (inj₁ x)

  data Is-inj₂ {a b} {A : Set a} {B : Set b} : A ⊎ B → Set (a ⊔ b) where
    inj₂ : ∀ x → Is-inj₂ (inj₂ x)

  elim-Is-inj₁ : ∀ {x : A ⊎ B} → Is-inj₁ x → A
  elim-Is-inj₁ .{inj₁ x} (inj₁ x) = x

  elim-Is-inj₂ : ∀ {x : A ⊎ B} → Is-inj₂ x → B
  elim-Is-inj₂ .{inj₂ x} (inj₂ x) = x

  dec-inj : ∀ (x : A ⊎ B) → Is-inj₁ x ⊎ Is-inj₂ x
  dec-inj (inj₁ x) = inj₁ (inj₁ x)
  dec-inj (inj₂ y) = inj₂ (inj₂ y)

  Is-inj₁? : ∀ (x : A ⊎ B) → Dec (Is-inj₁ x)
  Is-inj₁? (inj₁ x) = yes (inj₁ x)
  Is-inj₁? (inj₂ _) = no (λ ())

  Is-inj₂? : ∀ (x : A ⊎ B) → Dec (Is-inj₂ x)
  Is-inj₂? (inj₁ _) = no (λ ())
  Is-inj₂? (inj₂ x) = yes (inj₂ x)


module _ {a p : Level} {A : Set a} {P : A → Set p} where
  list-Any⇒∃ : {l : List A} → Any P l → ∃[ x ] (x ∈ l × P x)
  list-Any⇒∃ (here {x} px) = x , ((here refl) , px)
  list-Any⇒∃ (there later) with (x , x∈l , px ) ← list-Any⇒∃ later = x , there x∈l , px

  list-∃⇒Any : {l : List A} → ∃[ x ] (x ∈ l × P x) → Any P l
  list-∃⇒Any (x , here refl , px) = here px
  list-∃⇒Any (x , there el , px) = there (list-∃⇒Any (x , el , px))

  list-All⇒∀ : {l : List A} → All P l → ∀ e → e ∈ l → P e
  list-All⇒∀ (px ∷ _) e (here e-hd) rewrite e-hd = px
  list-All⇒∀ (_ ∷ all-p-l) e (there e∈l) = list-All⇒∀ all-p-l e e∈l

  list-∀⇒All : {l : List A} → (∀ e → e ∈ l → P e) → All P l
  list-∀⇒All {l = []} prop = []
  list-∀⇒All {l = x ∷ l} prop = (prop x (here refl)) ∷ (list-∀⇒All {l = l} λ e e∈l → prop e (there e∈l))

  ∀Element⇒All : {l : List A} → (∀ ((e ∈'): Element l) → P e) → All P l
  ∀Element⇒All all-P = list-∀⇒All (λ e e∈l → all-P (e ∈⊣ e∈l))
  All⇒∀Element : {l : List A} → All P l → (∀ ((e ∈') : Element l) → P e)
  All⇒∀Element all-P (e ∈⊣ elem) = list-All⇒∀ all-P e elem

  ∃Element⇒Any : {l : List A} → (Σ[ e ∈ Element l ] P (Element.val e)) → Any P l
  ∃Element⇒Any ((x ∈⊣ y) , z) = list-∃⇒Any (x , y , z)

  Any⇒∃Element : {l : List A} → Any P l → (Σ[ e ∈ Element l ] P (Element.val e))
  Any⇒∃Element anyPl with (x , y , z) ← list-Any⇒∃ anyPl = (x ∈⊣ y) , z

module _ {a r : Level} {A : Set a} {R : A → A → Set r} where
  AllPairs⇒∀≢ : {l : List A} → AllPairs.AllPairs R l → ∀ {x} {y} → x ∈ l → y ∈ l → x ≢ y → R x y ⊎ R y x
  AllPairs⇒∀≢ {[]} AllPairs.[] () ()
  AllPairs⇒∀≢ {(_ ∷ _)} (x AllPairs.∷ allp) (here refl) (here refl) neq = ⊥-elim (neq refl)
  AllPairs⇒∀≢ {(_ ∷ l)} (Rx AllPairs.∷ allp) (here refl) (there y∈l) _ = inj₁ (list-All⇒∀ Rx _ y∈l)
  AllPairs⇒∀≢ {(_ ∷ l)} (Ry AllPairs.∷ allp) (there x∈l) (here refl) _ = inj₂ (list-All⇒∀ Ry _ x∈l)
  AllPairs⇒∀≢ {(_ ∷ _)} (_ AllPairs.∷ allp) (there x∈l) (there y∈l) neq = AllPairs⇒∀≢ allp x∈l y∈l neq


-- If all elements of the list l are distinct, then the containment-proofs are unique, and so e1 e2 : Element l
-- are identical iff their val fields are identical:
val-injective : ∀ {a} {A : Set a} {l : List A} → AllPairs.AllPairs _≢_ l → Injective (Element.val {l = l})
val-injective {l = .(v ∷ _)} _ {v ∈⊣ here refl} {w ∈⊣ here refl} refl = refl
val-injective {l = .(v ∷ _)} (v≢tail AllPairs.∷ _) {v ∈⊣ here refl} {w ∈⊣ there d} v≡w = ⊥-elim (list-All⇒∀ v≢tail w d v≡w)
val-injective {l = .(_ ∷ _)} (w≢tail AllPairs.∷ _) {v ∈⊣ there c} {w ∈⊣ here refl} v≡w = ⊥-elim (list-All⇒∀ w≢tail v c (sym v≡w))
val-injective {l = .(_ ∷ _)} (_ AllPairs.∷ tail-distinct) {v ∈⊣ there c} {w ∈⊣ there d} v≡w
  with (val-injective tail-distinct {v ∈⊣ c} {w ∈⊣ d} v≡w)
... | refl = refl

module _ {a p : Level} {A : Set a} {l : List A} {P : Element l → Set p} where
  ∃Element-assocr : ∃[ e ] P e → ∃[ x ] (∃[ w ] P (x ∈⊣ w))
  ∃Element-assocr ((x ∈⊣ w) , p) = x , w , p
  ∃Element-assocl : ∃[ x ] (∃[ w ] P (x ∈⊣ w)) → ∃[ e ] P e
  ∃Element-assocl (x , w , p) = ((x ∈⊣ w) , p)

module _ {a : Level} {A : Set a} where
  AnyElement⇒∃ : ∀ (l : List A) {p} → {P : Element l → Set p} → Any P (list-elements l) → ∃[ e ] P e
  AnyElement⇒∃ l an = Data.Product.map₂ proj₂ (list-Any⇒∃ an)

  ∃⇒AnyElement : ∀ (l : List A) {p} {P : Element l → Set p} → (∃[ e ] P e) → Any P (list-elements l)
  ∃⇒AnyElement l (e , Pe) = list-∃⇒Any (e , double-elem l e , Pe)

  dec-∃∈ : ∀ (l : List A) {p} {P : Element l → Set p} → Pred.Decidable P → Dec (∃[ e ] P e)
  dec-∃∈ l dec-P = map′ (AnyElement⇒∃ l) (∃⇒AnyElement l) (any? dec-P (list-elements l))

  dec²-Element : ∀ {l : List A} {p} {P Q : Element l → Set p}
             → (∀ x → P x ⊎ Q x)
             → (∀ x → P x) ⊎ (∃[ x ] Q x)
  dec²-Element {l} {p} {P} {Q} dec = goal
    where
      goal : (∀ x → P x) ⊎ (∃[ x ] Q x)
      goal with (dec-∃∈ l λ - → Is-inj₂? (dec -))
      goal | no no-Q = inj₁ (λ x →
        case (dec-inj (dec x)) of λ
        { (inj₁ Px) → elim-Is-inj₁ Px
        ; (inj₂ Qx) → ⊥-elim (no-Q (x , Qx))
        })
      goal | yes (x , Qx) = inj₂ (x , elim-Is-inj₂ Qx)

  -- Special case for finite types A for non-dependent P, Q:
  dec²-finite : ∀ {p} {P Q : A → Set p}
              → {l : List A}
              → (∀ (x : A) → x ∈ l)
              → (∀ x → P x ⊎ Q x)
              → (∀ x → P x) ⊎ (∃[ x ] Q x)
  dec²-finite {p} {P} {Q} {l} full dec =
    Data.Sum.map P'⇒P Q'⇒Q nested
    where
      P' = λ {(x ∈') → P x}
      Q' = λ {(x ∈') → Q x}
      dec' : ∀ (x : Element l) → P' x ⊎ Q' x
      dec' (x ∈') = dec x
      nested = dec²-Element {l} {P = P'} {Q = Q'} dec'
      P'⇒P : (∀ x → P' x) → (∀ x → P x)
      P'⇒P all-P' x = all-P' (x ∈⊣ (full x))
      Q'⇒Q : (∃[ x ] Q' x) → ∃[ x ] Q x
      Q'⇒Q ((x ∈⊣ _), Qx) = x , Qx

  ¬∀Elements⇒∃ : ∀ (l : List A) {p} {P : Element l → Set p} → Pred.Decidable P → (¬ ∀ e → P e) → ∃[ e ] (¬ P e)
  ¬∀Elements⇒∃ l {P = P} dec-P ¬all with (dec-∃∈ l {P = λ - → ¬ (P -)} (λ e → ¬? (dec-P e)))
  ... | yes ∃e = ∃e
  ... | no ¬∃e = ⊥-elim (¬all λ e → ¬¬-dec (dec-P e) λ ¬Pe → ¬∃e (e , ¬Pe))


record Enumerable {a} (A : Set a) : Set a where
  field
    by-index : ℕ → A
    index-of : A → ℕ
    split-epi : ∀ (x : A) → (x ≡ by-index (index-of x))


list-fin : (n : ℕ) → List (Fin n)
list-fin ℕ.zero = []
list-fin (ℕ.suc n) = Fin.zero ∷ map Fin.suc (list-fin n)

list-fin-any : ∀ (n : ℕ) (k : Fin n) → k ∈ list-fin n
list-fin-any (ℕ.suc n) Fin.zero = here refl
list-fin-any (ℕ.suc n) (Fin.suc k) = there ( ∈-map⁺ Fin.suc (list-fin-any n k) )

dec-to-sum : ∀ {p} {P : Set p} → Dec P → P ⊎ (¬ P)
dec-to-sum (yes P) = inj₁ P
dec-to-sum (no P) = inj₂ P

_contains_ : {a p : Level} → {A : Set a} → (List A) → (P : A → Set p) → Set (a ⊔ p)
_contains_ l pred = Any pred l