open import 1Lab.Prelude

open import Data.List.Membership
open import Data.List.Base
open import Data.Dec.Base
open import Data.Sum.Base

module Data.List.Quantifiers where

Quantifiers over listsπŸ”—

data Some {β„“ β„“'} {A : Type β„“} (P : A β†’ Type β„“') : List A β†’ Type (β„“ βŠ” β„“') where
  here  : βˆ€ {x xs} β†’ P x       β†’ Some P (x ∷ xs)
  there : βˆ€ {x xs} β†’ Some P xs β†’ Some P (x ∷ xs)

data All {β„“ β„“'} {A : Type β„“} (P : A β†’ Type β„“') : List A β†’ Type (β„“ βŠ” β„“') where
  []  :                             All P []
  _∷_ : βˆ€ {x xs} β†’ P x β†’ All P xs β†’ All P (x ∷ xs)

private variable
  β„“ β„“' : Level
  A B : Type β„“
  P Q : A β†’ Type β„“'
  x y : A
  xs ys : List A

Some-elim
  : βˆ€ {P : A β†’ Type β„“} (R : (xs : List A) β†’ Some P xs β†’ Type β„“')
  β†’ (βˆ€ {x} {xs} β†’ (p : P x) β†’ R (x ∷ xs) (here p))
  β†’ (βˆ€ {x} {xs} β†’ (p : Some P xs) β†’ R xs p β†’ R (x ∷ xs) (there p))
  β†’ βˆ€ {xs : List A} (s : Some P xs) β†’ R xs s
Some-elim R h t (here p) = h p
Some-elim R h t (there p) = t p (Some-elim R h t p)

Some-rec
  : βˆ€ {P : A β†’ Type β„“} {X : Type β„“'}
  β†’ (βˆ€ {x} β†’ P x β†’ X)
  β†’ (X β†’ X)
  β†’ βˆ€ {xs : List A} β†’ Some P xs β†’ X
Some-rec h t (here p) = h p
Some-rec h t (there p) = t (Some-rec h t p)

All-elim
  : βˆ€ {P : A β†’ Type β„“} (R : (xs : List A) β†’ All P xs β†’ Type β„“')
  β†’ R [] []
  β†’ ( βˆ€ {x} {xs} (px : P x) (pxs : All P xs)
    β†’ R xs pxs
    β†’ R (x ∷ xs) (px ∷ pxs))
  β†’ βˆ€ {xs : List A} (a : All P xs) β†’ R xs a
All-elim R n e [] = n
All-elim R n e (x ∷ a) = e x a (All-elim R n e a)

All-rec
  : βˆ€ {P : A β†’ Type β„“} {X : Type β„“'}
  β†’ X
  β†’ (βˆ€ {x} β†’ P x β†’ X β†’ X)
  β†’ βˆ€ {xs : List A} β†’ All P xs β†’ X
All-rec n e [] = n
All-rec n e (p ∷ a) = e p (e p n)

∷-all-head : All P (x ∷ xs) β†’ P x
∷-all-head (px ∷ _) = px

∷-all-tail : All P (x ∷ xs) β†’ All P xs
∷-all-tail (_ ∷ pxs) = pxs

∷-all-Γ— : All P (x ∷ xs) β†’ P x Γ— All P xs
∷-all-Γ— (px ∷ pxs) = px , pxs

Β¬some-[] : Β¬ Some P []
Β¬some-[] ()

∷-some-⊎ : Some P (x ∷ xs) β†’ P x ⊎ Some P xs
∷-some-⊎ (here px) = inl px
∷-some-⊎ (there pxs) = inr pxs

∷-Β¬some-head : Β¬ (Some P (x ∷ xs)) β†’ Β¬ (P x)
∷-¬some-head ¬some px = ¬some (here px)

∷-Β¬some-tail : Β¬ (Some P (x ∷ xs)) β†’ Β¬ (Some P xs)
∷-¬some-tail ¬some px = ¬some (there px)

some-map : (βˆ€ {x} β†’ P x β†’ Q x) β†’ Some P xs β†’ Some Q xs
some-map f (here px) = here (f px)
some-map f (there pxs) = there (some-map f pxs)

all-map : (βˆ€ {x} β†’ P x β†’ Q x) β†’ All P xs β†’ All Q xs
all-map f [] = []
all-map f (px ∷ pxs) = f px ∷ all-map f pxs

not-some→all-not
  : Β¬ (Some P xs)
  β†’ All (Ξ» x β†’ Β¬ (P x)) xs
not-some→all-not {xs = []} ¬some = []
not-someβ†’all-not {xs = x ∷ xs} Β¬some =
  ∷-Β¬some-head Β¬some ∷ not-someβ†’all-not (∷-Β¬some-tail Β¬some)

all-not→not-some
  : All (Ξ» x β†’ Β¬ P x) xs
  β†’ Β¬ (Some P xs)
all-notβ†’not-some (Β¬P ∷ ps) (here p)  = Β¬P p
all-notβ†’not-some (Β¬P ∷ ps) (there x) = all-notβ†’not-some ps x

some?
  : βˆ€ {P : A β†’ Type β„“}
  β†’ (βˆ€ x β†’ Dec (P x))
  β†’ (xs : List A) β†’ Dec (Some P xs)
some? P? [] = no Β¬some-[]
some? P? (x ∷ xs) with P? x
... | yes px = yes (here px)
... | no Β¬px with some? P? xs
... | yes pxs = yes (there pxs)
... | no ¬pxs = no ([ ¬px , ¬pxs ] ∘ ∷-some-⊎)

all?
  : βˆ€ {P : A β†’ Type β„“}
  β†’ (βˆ€ x β†’ Dec (P x))
  β†’ (xs : List A) β†’ Dec (All P xs)
all? P? [] = yes []
all? P? (x ∷ xs) with P? x | all? P? xs
... | yes p | yes ps = yes (p ∷ ps)
... | yes p | no ¬ps = no (¬ps ∘ ∷-all-tail)
... | no ¬p | q = no (¬p ∘ ∷-all-head)

instance
  Dec-Some : βˆ€ {P : A β†’ Type β„“} β†’ ⦃ βˆ€ {x} β†’ Dec (P x) ⦄ β†’ {xs : List A} β†’ Dec (Some P xs)
  Dec-Some {P = P} = some? (Ξ» x β†’ holds? (P x)) _

  Dec-All : βˆ€ {P : A β†’ Type β„“} β†’ ⦃ βˆ€ {x} β†’ Dec (P x) ⦄ β†’ {xs : List A} β†’ Dec (All P xs)
  Dec-All {P = P} = all? (Ξ» x β†’ holds? (P x)) _

all-∈ : All P xs β†’ x ∈ xs β†’ P x
all-∈ {P = P} (px ∷ pxs) (here p) = subst P (sym p) px
all-∈ (px ∷ pxs) (there x∈xs) = all-∈ pxs x∈xs

to-all : (βˆ€ x β†’ x ∈ xs β†’ P x) β†’ All P xs
to-all {xs = []} p = []
to-all {xs = x ∷ xs} p = p x (here refl) ∷ to-all (Ξ» i w β†’ p i (there w))

instance
  H-Level-All : βˆ€ {β„“ β„“'} {A : Type β„“} {P : A β†’ Type β„“'} {n} ⦃ _ : βˆ€ {x} β†’ H-Level (P x) n ⦄ {xs} β†’ H-Level (All P xs) n
  H-Level-All {P = P} {xs = xs} = hlevel-instance
    (retractβ†’is-hlevel {A = βˆ€ x β†’ x βˆˆβ‚— xs β†’ P x} _ to-all (Ξ» a _ β†’ all-∈ a) inv (hlevel _))
    where
      inv : βˆ€ {xs} β†’ is-left-inverse (to-all {xs = xs} {P = P}) (Ξ» a z β†’ all-∈ a)
      inv {xs} [] = refl
      inv {x ∷ xs} (y ∷ ys) i = coe1β†’i (Ξ» _ β†’ P x) i y ∷ inv ys i