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

module Data.List.Relation.Unary where

open import Prelude
open import Data.List.Base
open import Data.Fin
open import Relation.Nullary
open import Data.Sum
open import Data.List.Indexing

private
  variable p : Level

module Inductive◇ where
 data ◇ {A : Type a} (P : A → Type p) : List A → Type (a ℓ⊔ p) where
   here   : ∀ {x xs} → P x      → ◇ P (x ∷ xs)
   there  : ∀ {x xs} → ◇ P xs   → ◇ P (x ∷ xs)

◇ : (P : A → Type p) → List A → Type _
◇ P xs = ∃ i × P (xs ! i)

◇! : (P : A → Type p) → List A → Type _
◇! P xs = isContr (◇ P xs)

module Exists {a} {A : Type a} {p} (P : A → Type p) where
  push : ∀ {x xs} → ◇ P xs → ◇ P (x ∷ xs)
  push (n , p) = fs n , p

  pull : ∀ {x xs} → ¬ P x → ◇ P (x ∷ xs) → ◇ P xs
  pull ¬Px (f0   , p) = ⊥-elim (¬Px p)
  pull ¬Px (fs n , p) = n , p

  uncons : ∀ {x xs} → ◇ P (x ∷ xs) → P x ⊎ ◇ P xs
  uncons (f0 , p) = inl p
  uncons (fs x , p) = inr (x , p)

  infixr  _++◇_ _◇++_
  _++◇_ : ∀ {xs} ys → ◇ P xs → ◇ P (ys ++ xs)
  [] ++◇ ys = ys
  (x ∷ xs) ++◇ ys = push (xs ++◇ ys)

  _◇++_ : ∀ xs → ◇ P xs → ∀ {ys} → ◇ P (xs ++ ys)
  _◇++_ (x ∷ xs) (f0  , ∃Pxs) = f0 , ∃Pxs
  _◇++_ (x ∷ xs) (fs n , ∃Pxs) = push (xs ◇++ (n , ∃Pxs))

  push! : ∀ {x xs} → ¬ P x → ◇! P xs → ◇! P (x ∷ xs)
  push! ¬Px x∈!xs .fst = push (x∈!xs .fst)
  push! ¬Px x∈!xs .snd (f0   , px) = ⊥-elim (¬Px px)
  push! ¬Px x∈!xs .snd (fs n  , y∈xs) i = push (x∈!xs .snd (n , y∈xs) i)

  pull! : ∀ {x xs} → ¬ P x → ◇! P (x ∷ xs) → ◇! P xs
  pull! ¬Px ((f0   , px    ) , uniq) = ⊥-elim (¬Px px)
  pull! ¬Px ((fs n  , x∈xs  ) , uniq) .fst = (n , x∈xs)
  pull! ¬Px ((fs n  , x∈xs  ) , uniq) .snd (m , x∈xs′) i =
    pull ¬Px (uniq (fs m , x∈xs′ ) i)

  here! : ∀ {x xs} → isContr (P x) → ¬ ◇ P xs → ◇! P (x ∷ xs)
  here! Px p∉xs .fst = f0 , Px .fst
  here! Px p∉xs .snd (f0  , p∈xs) i .fst = f0
  here! Px p∉xs .snd (f0  , p∈xs) i .snd = Px .snd p∈xs i
  here! Px p∉xs .snd (fs n , p∈xs) = ⊥-elim (p∉xs (n , p∈xs))

  module _ (P? : ∀ x → Dec (P x)) where
    open import Relation.Nullary.Decidable.Logic

    ◇? : ∀ xs → Dec (◇ P xs)
    ◇? [] = no λ ()
    ◇? (x ∷ xs) =  iff-dec (⟦l f0 ,_ ,r push ⟧ iff uncons) (P? x || ◇? xs)

◻ : (P : A → Type p) → List A → Type _
◻ P xs = ∀ i → P (xs ! i)

module Forall {a} {A : Type a} {p} (P : A → Type p) where
  push : ∀ {x xs} → P x → ◻ P xs → ◻ P (x ∷ xs)
  push Px Pxs f0 = Px
  push Px Pxs (fs n) = Pxs n

  uncons : ∀ {x xs} → ◻ P (x ∷ xs) → P x × ◻ P xs
  uncons Pxs = Pxs f0 , Pxs ∘ fs

  pull : ∀ {x xs} → ◻ P (x ∷ xs) → ◻ P xs
  pull = snd ∘ uncons

  _++◇_ : ∀ xs {ys} → ◻ P (xs ++ ys) → ◻ P ys
  [] ++◇ xs⊆P = xs⊆P
  (x ∷ xs) ++◇ xs⊆P = xs ++◇ (xs⊆P ∘ fs)

  _◇++_ : ∀ xs {ys} → ◻ P (xs ++ ys) → ◻ P xs
  ([] ◇++ xs⊆P) ()
  ((x ∷ xs) ◇++ xs⊆P) f0 = xs⊆P f0
  ((x ∷ xs) ◇++ xs⊆P) (fs n) = (xs ◇++ pull xs⊆P) n

  both : ∀ xs {ys} → ◻ P xs → ◻ P ys → ◻ P (xs ++ ys)
  both [] xs⊆P ys⊆P = ys⊆P
  both (x ∷ xs) xs⊆P ys⊆P f0 = xs⊆P f0
  both (x ∷ xs) xs⊆P ys⊆P (fs i) = both xs (pull xs⊆P) ys⊆P i

  empty : ◻ P []
  empty ()

  module _ where
    open import Relation.Nullary.Decidable.Logic
    ◻? : (∀ x → Dec (P x)) → ∀ xs → Dec (◻ P xs)
    ◻? P? [] = yes λ ()
    ◻? P? (x ∷ xs) =  iff-dec (uncurry push iff uncons) (P? x && ◻? P? xs)

module Forall-NotExists {a} {A : Type a} {p} (P : A → Type p) where
  open import Relation.Nullary.Stable
  open import Data.Empty.Properties

  open Forall P
  ¬P = ¬_ ∘ P
  module ∃¬ = Exists ¬P

  ∀⇒¬∃¬ : ∀ xs → ◻ P xs → ¬ (◇ ¬P xs)
  ∀⇒¬∃¬ (x ∷ xs) xs⊆P (f0 , ∃¬P∈xs) = ∃¬P∈xs(xs⊆P f0)
  ∀⇒¬∃¬ (x ∷ xs) xs⊆P (fs n , ∃¬P∈xs) = ∀⇒¬∃¬ xs (xs⊆P ∘ fs) (n , ∃¬P∈xs)

  module _ (stable : ∀ {x} → Stable (P x)) where
    ¬∃¬⇒∀ : ∀ xs → ¬ (◇ ¬P xs) → ◻ P xs
    ¬∃¬⇒∀ (x ∷ xs) ¬∃¬P∈xs f0 = stable (¬∃¬P∈xs ∘ (f0 ,_))
    ¬∃¬⇒∀ (x ∷ xs) ¬∃¬P∈xs (fs n) = ¬∃¬⇒∀ xs (¬∃¬P∈xs ∘ ∃¬.push) n

    leftInv′ : ∀ (prop : ∀ {x} → isProp (P x)) xs → (x : ◻ P xs) → ¬∃¬⇒∀ xs (∀⇒¬∃¬ xs x) ≡ x
    leftInv′ prop [] x i ()
    leftInv′ prop (x ∷ xs) xs⊆P i f0 = prop (stable λ ¬p → ¬p (xs⊆P f0)) (xs⊆P f0) i
    leftInv′ prop (x ∷ xs) xs⊆P i (fs n) = leftInv′ prop xs (pull xs⊆P) i n

    ∀⇔¬∃¬ : ∀ (prop : ∀ {x} → isProp (P x)) xs → ◻ P xs ⇔ (¬ ◇ ¬P xs)
    ∀⇔¬∃¬ _ xs .fun = ∀⇒¬∃¬ xs
    ∀⇔¬∃¬ _ xs .inv = ¬∃¬⇒∀ xs
    ∀⇔¬∃¬ p xs .leftInv  = leftInv′ p xs
    ∀⇔¬∃¬ _ xs .rightInv x = isProp¬ _ _ x

module Exists-NotForall {a} {A : Type a} {p} (P : A → Type p) where
  open Exists P
  ¬P = ¬_ ∘ P
  module ∀¬ = Forall ¬P

  ∃⇒¬∀¬ : ∀ xs → ◇ P xs → ¬ ◻ ¬P xs
  ∃⇒¬∀¬ (x ∷ xs) (f0  , P∈xs) xs⊆P = xs⊆P f0 P∈xs
  ∃⇒¬∀¬ (x ∷ xs) (fs n , P∈xs) xs⊆P = ∃⇒¬∀¬ xs (n , P∈xs) (xs⊆P ∘ fs)

  module _ (P? : ∀ x → Dec (P x)) where
    ¬∀¬⇒∃ : ∀ xs → ¬ ◻ ¬P xs → ◇ P xs
    ¬∀¬⇒∃ [] ¬xs⊆¬P = ⊥-elim (¬xs⊆¬P λ ())
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P with P? x
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P | yes p = f0 , p
    ¬∀¬⇒∃ (x ∷ xs) ¬xs⊆¬P | no ¬p = push (¬∀¬⇒∃ xs (¬xs⊆¬P ∘ ∀¬.push ¬p))

module Congruence {p q} (P : A → Type p) (Q : B → Type q)
                  {f : A → B} (f↑ : ∀ {x} → P x → Q (f x)) where
  cong-◇ : ∀ xs → ◇ P xs → ◇ Q (map f xs)
  cong-◇ (x ∷ xs) (f0 , P∈xs) = f0 , f↑ P∈xs
  cong-◇ (x ∷ xs) (fs n , P∈xs) = Exists.push Q (cong-◇ xs (n , P∈xs))

◇-concat : ∀ (P : A → Type p) xs → ◇ (◇ P) xs → ◇ P (concat xs)
◇-concat P (x ∷ xs) (f0 , ps) = Exists._◇++_ P x ps
◇-concat P (x ∷ xs) (fs n , ps) = Exists._++◇_ P x (◇-concat P xs (n , ps))

◻-concat : ∀ (P : A → Type p) xs → ◻ (◻ P) xs → ◻ P (concat xs)
◻-concat P [] xs⊆P ()
◻-concat P (x ∷ xs) xs⊆P = Forall.both P x (xs⊆P f0) (◻-concat P xs (xs⊆P ∘ fs))

module Search {A : Type a} where
  data Result {p} (P : A → Type p) (xs : List A) : Bool → Type (a ℓ⊔ p) where
    all′ : ◻ P xs → Result P xs true
    except′ : ◇ (¬_ ∘ P) xs → Result P xs false

  record Found {p} (P : A → Type p) (xs : List A) : Type (a ℓ⊔ p) where
    field
      found? : Bool
      result : Result P xs found?
  open Found public

  pattern all    ps = record { found? = true ; result = all′ ps }
  pattern except ¬p = record { found? = false ; result = except′ ¬p }

  module _ {p} {P : A → Type p} (P? : ∀ x → Dec (P x)) where
    search : ∀ xs → Found P xs
    search [] = all λ ()
    search (x ∷ xs) = search′ x xs (P? x) (search xs)
      where
      search′ : ∀ x xs → Dec (P x) → Found P xs → Found P (x ∷ xs)
      search′ x xs Px Pxs .found? = Px .does and Pxs .found?
      search′ x xs (no ¬p) Pxs .result = except′ (f0 , ¬p)
      search′ x xs (yes p) (except ¬p) .result = except′ (Exists.push (¬_ ∘ P) ¬p)
      search′ x xs (yes p) (all ps) .result = all′ (Forall.push P p ps)