------------------------------------------------------------------------
-- Decision procedures for finite sets and subsets of finite sets
------------------------------------------------------------------------

{-# OPTIONS --universe-polymorphism #-}

module Data.Fin.Dec where

open import Function
import Data.Bool as Bool
open import Data.Nat hiding (_<_)
open import Data.Vec hiding (_∈_)
open import Data.Vec.Equality as VecEq
  using () renaming (module HeterogeneousEquality to HetVecEq)
open import Data.Fin
open import Data.Fin.Subset
open import Data.Fin.Subset.Props
open import Data.Product as Prod
open import Data.Empty
open import Function
import Function.Equivalence as Eq
open import Relation.Binary
import Relation.Binary.HeterogeneousEquality as H
open import Relation.Nullary
import Relation.Nullary.Decidable as Dec
open import Relation.Unary using (Pred)

infix  _∈?_

_∈?_ : ∀ {n} x (p : Subset n) → Dec (x ∈ p)
zero  ∈? inside  ∷ p = yes here
zero  ∈? outside ∷ p = no  λ()
suc n ∈? s ∷ p       with n ∈? p
...                  | yes n∈p = yes (there n∈p)
...                  | no  n∉p = no  (n∉p ∘ drop-there)

private

  restrictP : ∀ {n} → (Fin (suc n) → Set) → (Fin n → Set)
  restrictP P f = P (suc f)

  restrict : ∀ {n} {P : Fin (suc n) → Set} →
             (∀ f → Dec (P f)) →
             (∀ f → Dec (restrictP P f))
  restrict dec f = dec (suc f)

any? : ∀ {n} {P : Fin n → Set} →
       ((f : Fin n) → Dec (P f)) →
       Dec (∃ P)
any? {zero}  {P} dec = no (((λ()) ∶ ¬ Fin ) ∘ proj₁)
any? {suc n} {P} dec with dec zero | any? (restrict dec)
...                  | yes p | _            = yes (_ , p)
...                  | _     | yes (_ , p') = yes (_ , p')
...                  | no ¬p | no ¬p'       = no helper
  where
  helper : ∄ P
  helper (zero  , p)  = ¬p p
  helper (suc f , p') = ¬p' (_ , p')

nonempty? : ∀ {n} (p : Subset n) → Dec (Nonempty p)
nonempty? p = any? (λ x → x ∈? p)

private

  restrict∈ : ∀ {n} P {Q : Fin (suc n) → Set} →
              (∀ {f} → Q f → Dec (P f)) →
              (∀ {f} → restrictP Q f → Dec (restrictP P f))
  restrict∈ _ dec {f} Qf = dec {suc f} Qf

decFinSubset : ∀ {n} {P Q : Fin n → Set} →
               (∀ f → Dec (Q f)) →
               (∀ {f} → Q f → Dec (P f)) →
               Dec (∀ {f} → Q f → P f)
decFinSubset {zero}          _    _    = yes λ{}
decFinSubset {suc n} {P} {Q} decQ decP = helper
  where
  helper : Dec (∀ {f} → Q f → P f)
  helper with decFinSubset (restrict decQ) (restrict∈ P decP)
  helper | no ¬q⟶p = no (λ q⟶p → ¬q⟶p (λ {f} q → q⟶p {suc f} q))
  helper | yes q⟶p with decQ zero
  helper | yes q⟶p | yes q₀ with decP q₀
  helper | yes q⟶p | yes q₀ | no ¬p₀ = no (λ q⟶p → ¬p₀ (q⟶p {zero} q₀))
  helper | yes q⟶p | yes q₀ | yes p₀ = yes (λ {_} → hlpr _)
    where
    hlpr : ∀ f → Q f → P f
    hlpr zero    _  = p₀
    hlpr (suc f) qf = q⟶p qf
  helper | yes q⟶p | no ¬q₀ = yes (λ {_} → hlpr _)
    where
    hlpr : ∀ f → Q f → P f
    hlpr zero    q₀ = ⊥-elim (¬q₀ q₀)
    hlpr (suc f) qf = q⟶p qf

all∈? : ∀ {n} {P : Fin n → Set} {q} →
        (∀ {f} → f ∈ q → Dec (P f)) →
        Dec (∀ {f} → f ∈ q → P f)
all∈? {q = q} dec = decFinSubset (λ f → f ∈? q) dec

all? : ∀ {n} {P : Fin n → Set} →
       (∀ f → Dec (P f)) →
       Dec (∀ f → P f)
all? dec with all∈? {q = ⊤} (λ {f} _ → dec f)
...      | yes ∀p = yes (λ f → ∀p ∈⊤)
...      | no ¬∀p = no  (λ ∀p → ¬∀p (λ {f} _ → ∀p f))

decLift : ∀ {n} {P : Fin n → Set} →
          (∀ x → Dec (P x)) →
          (∀ p → Dec (Lift P p))
decLift dec p = all∈? (λ {x} _ → dec x)

private

  restrictSP : ∀ {n} → Side → (Subset (suc n) → Set) → (Subset n → Set)
  restrictSP s P p = P (s ∷ p)

  restrictS : ∀ {n} {P : Subset (suc n) → Set} →
              (s : Side) →
              (∀ p → Dec (P p)) →
              (∀ p → Dec (restrictSP s P p))
  restrictS s dec p = dec (s ∷ p)

anySubset? : ∀ {n} {P : Subset n → Set} →
             (∀ s → Dec (P s)) →
             Dec (∃ P)
anySubset? {zero} {P} dec with dec []
... | yes P[] = yes (_ , P[])
... | no ¬P[] = no helper
  where
  helper : ∄ P
  helper ([] , P[]) = ¬P[] P[]
anySubset? {suc n} {P} dec with anySubset? (restrictS inside  dec)
                              | anySubset? (restrictS outside dec)
... | yes (_ , Pp) | _            = yes (_ , Pp)
... | _            | yes (_ , Pp) = yes (_ , Pp)
... | no ¬Pp       | no ¬Pp'      = no helper
    where
    helper : ∄ P
    helper (inside  ∷ p , Pp)  = ¬Pp  (_ , Pp)
    helper (outside ∷ p , Pp') = ¬Pp' (_ , Pp')

-- If a decidable predicate P over a finite set is sometimes false,
-- then we can find the smallest value for which this is the case.

¬∀⟶∃¬-smallest :
  ∀ n {p} (P : Fin n → Set p) → (∀ i → Dec (P i)) →
  ¬ (∀ i → P i) → ∃ λ i → ¬ P i × ((j : Fin′ i) → P (inject j))
¬∀⟶∃¬-smallest zero    P dec ¬∀iPi = ⊥-elim (¬∀iPi (λ()))
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi with dec zero
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | no ¬P0 = (zero , ¬P0 , λ ())
¬∀⟶∃¬-smallest (suc n) P dec ¬∀iPi | yes P0 =
  Prod.map suc (Prod.map id extend′) $
    ¬∀⟶∃¬-smallest n (λ n → P (suc n)) (dec ∘ suc) (¬∀iPi ∘ extend)
  where
  extend : (∀ i → P (suc i)) → (∀ i → P i)
  extend ∀iP[1+i] zero    = P0
  extend ∀iP[1+i] (suc i) = ∀iP[1+i] i

  extend′ : ∀ {i : Fin n} →
            ((j : Fin′ i) → P (suc (inject j))) →
            ((j : Fin′ (suc i)) → P (inject j))
  extend′ g zero    = P0
  extend′ g (suc j) = g j

-- Decision procedure for _⊆_ (obtained via the natural lattice
-- order).

infix  _⊆?_

_⊆?_ : ∀ {n} → Decidable (_⊆_ {n = n})
p₁ ⊆? p₂ =
  Dec.map (Eq.sym NaturalPoset.orders-equivalent) $
  Dec.map′ H.≅-to-≡ H.≡-to-≅ $
  Dec.map′ HetVecEq.to-≅ HetVecEq.from-≅ $
  VecEq.DecidableEquality._≟_ Bool.decSetoid p₁ (p₁ ∩ p₂)