------------------------------------------------------------------------
-- The Agda standard library
--
-- Heterogeneous N-ary Relations
------------------------------------------------------------------------

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

module Relation.Nary where

------------------------------------------------------------------------
-- Concrete examples can be found in README.Nary. This file's comments
-- are more focused on the implementation details and the motivations
-- behind the design decisions.
------------------------------------------------------------------------

open import Level using (Level; _⊔_; Lift)
open import Data.Unit.Base
open import Data.Bool.Base using (true; false)
open import Data.Empty
open import Data.Nat.Base using (zero; suc)
open import Data.Product.Base as Product using (_×_; _,_)
open import Data.Product.Nary.NonDependent
open import Data.Sum.Base using (_⊎_)
open import Function.Base using (_$_; _∘′_)
open import Function.Nary.NonDependent
open import Relation.Nullary.Negation using (¬_)
open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _because_; _×-dec_)
import Relation.Unary as Unary
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)

private
  variable
    r : Level
    R : Set r

------------------------------------------------------------------------
-- Generic type constructors

-- `Relation.Unary` provides users with a wealth of combinators to work
-- with indexed sets. We can generalise these to n-ary relations.

-- The crucial thing to notice here is that because we are explicitly
-- considering that the input function should be a `Set`-ended `Arrows`,
-- all the other parameters are inferrable. This allows us to make the
-- number arguments (`n`) implicit.
------------------------------------------------------------------------

------------------------------------------------------------------------
-- Quantifiers

-- If we already know how to quantify over one variable, we can easily
-- describe how to quantify over `n` variables by induction over said `n`.

quantₙ : (∀ {i l} {I : Set i}  (I  Set l)  Set (i  l)) 
          n {ls} {as : Sets n ls} 
         Arrows n as (Set r)  Set (r  ( n ls))
quantₙ Q zero     f = f
quantₙ Q (suc n)  f = Q  x  quantₙ Q n (f x))

infix 5 ∃⟨_⟩ Π[_] ∀[_]

-- existential quantifier

∃⟨_⟩ :  {n ls r} {as : Sets n ls}  as  Set r  Set (r  ( n ls))
∃⟨_⟩ = quantₙ Unary.Satisfiable _

-- explicit universal quantifiers

Π[_] :  {n ls r} {as : Sets n ls}  as  Set r  Set (r  ( n ls))
Π[_] = quantₙ Unary.Universal _

-- implicit universal quantifiers

∀[_] :  {n ls r} {as : Sets n ls}  as  Set r  Set (r  ( n ls))
∀[_] = quantₙ Unary.IUniversal _

-- ≟-mapₙ : ∀ n. (con : A₁ → ⋯ → Aₙ → R) →
--               Injectiveₙ n con →
--               ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--               Dec (a₁₁ ≡ a₁₂) → ⋯ → Dec (aₙ₁ ≡ aₙ₂) →
--               Dec (con a₁₁ ⋯ aₙ₁ ≡ con a₁₂ ⋯ aₙ₂)

≟-mapₙ :  n {ls} {as : Sets n ls} (con : Arrows n as R)  Injectiveₙ n con 
          {l r}  Arrows n (Dec <$> Equalₙ n l r) (Dec (uncurryₙ n con l  uncurryₙ n con r))
≟-mapₙ n con con-inj =
  curryₙ n λ a?s  let as? = Product-dec n a?s in
  Dec.map′ (cong (uncurryₙ n con) ∘′ fromEqualₙ n) con-inj as?

------------------------------------------------------------------------
-- Substitution

module _ {n r ls} {as : Sets n ls} (P : as  Set r) where

-- Substitutionₙ : ∀ n. ∀ a₁₁ a₁₂ ⋯ aₙ₁ aₙ₂ →
--                      a₁₁ ≡ a₁₂ → ⋯ → aₙ₁ ≡ aₙ₂ →
--                      P a₁₁ ⋯ aₙ₁ → P a₁₂ ⋯ aₙ₂

  Substitutionₙ : Set (r  ( n ls))
  Substitutionₙ =  {l r}  Equalₙ n l r  (uncurryₙ n P l  uncurryₙ n P r)

  substₙ : Substitutionₙ
  substₙ = curryₙ n (subst (uncurryₙ n P) ∘′ fromEqualₙ n)

------------------------------------------------------------------------
-- Pointwise liftings of k-ary operators

-- Rather than having multiple ad-hoc lifting functions for various
-- arities we have a fully generic liftₙ functional which lifts a k-ary
-- operator to work with k n-ary functions whose respective codomains
-- match the domains of the operator.
-- The type of liftₙ is fairly unreadable. Here it is written with ellipsis:

-- liftₙ : ∀ k n. (B₁ → ⋯ → Bₖ → R) →
--                (A₁ → ⋯ → Aₙ → B₁) →
--                       ⋮
--                (A₁ → ⋯ → Aₙ → B₁) →
--                (A₁ → ⋯ → Aₙ → R)

liftₙ :  k n {ls rs} {as : Sets n ls} {bs : Sets k rs} 
        Arrows k bs R  Arrows k (smap _ (Arrows n as) k bs) (Arrows n as R)
liftₙ k n op = curry⊤ₙ k λ fs 
               curry⊤ₙ n λ vs 
               uncurry⊤ₙ k op $
               palg _ _ k  f  uncurry⊤ₙ n f vs) fs where

  -- The bulk of the work happens in this auxiliary definition:
  palg :  f (F :  {l}  Set l  Set (f l)) n {ls} {as : Sets n ls} 
         (∀ {l} {r : Set l}  F r  r)  Product⊤ n (smap f F n as)  Product⊤ n as
  palg f F zero    alg ps       = _
  palg f F (suc n) alg (p , ps) = alg p , palg f F n alg ps


-- implication

infixr 6 _⇒_
_⇒_ :  {n} {ls r s} {as : Sets n ls} 
      as  Set r  as  Set s  as  Set (r  s)
_⇒_ = liftₙ 2 _  A B  A  B)

-- conjunction

infixr 7 _∩_
_∩_ :  {n} {ls r s} {as : Sets n ls} 
      as  Set r  as  Set s  as  Set (r  s)
_∩_ = liftₙ 2 _ _×_

-- disjunction

infixr 8 _∪_
_∪_ :  {n} {ls r s} {as : Sets n ls} 
      as  Set r  as  Set s  as  Set (r  s)
_∪_ = liftₙ 2 _ _⊎_

-- negation

 :  {n ls r} {as : Sets n ls}  as  Set r  as  Set r
 = liftₙ 1 _ ¬_


apply⊤ₙ :  {n ls r} {as : Sets n ls} {R : as  Set r} 
          Π[ R ]  (vs : Product⊤ n as)  uncurry⊤ₙ n R vs
apply⊤ₙ {zero}  prf vs       = prf
apply⊤ₙ {suc n} prf (v , vs) = apply⊤ₙ (prf v) vs

applyₙ :  {n ls r} {as : Sets n ls} {R : as  Set r} 
         Π[ R ]  (vs : Product n as)  uncurry⊤ₙ n R (toProduct⊤ n vs)
applyₙ {n} prf vs = apply⊤ₙ prf (toProduct⊤ n vs)

iapply⊤ₙ :  {n ls r} {as : Sets n ls} {R : as  Set r} 
           ∀[ R ]  {vs : Product⊤ n as}  uncurry⊤ₙ n R vs
iapply⊤ₙ {zero}  prf = prf
iapply⊤ₙ {suc n} prf = iapply⊤ₙ {n} prf

iapplyₙ :  {n ls r} {as : Sets n ls} {R : as  Set r} 
          ∀[ R ]  {vs : Product n as}  uncurry⊤ₙ n R (toProduct⊤ n vs)
iapplyₙ {n} prf = iapply⊤ₙ {n} prf

------------------------------------------------------------------------
-- Properties of N-ary relations

-- Decidability

Decidable :  {n ls r} {as : Sets n ls}  as  Set r  Set (r   n ls)
Decidable R = Π[ mapₙ _ Dec R ]

-- erasure

⌊_⌋ :  {n ls r} {as : Sets n ls} {R : as  Set r}  Decidable R  as  Set r
⌊_⌋ {zero}  R? = Lift _ (Dec.True R?)
⌊_⌋ {suc n} R? a =  R? a 

-- equivalence between R and its erasure

fromWitness :  {n ls r} {as : Sets n ls} (R : as  Set r) (R? : Decidable R) 
              ∀[  R?   R ]
fromWitness {zero} R R? with R?
... | yes           r = λ _  r
... | false because _ = λ ()
fromWitness {suc n} R R? = fromWitness (R _) (R? _)

toWitness :  {n ls r} {as : Sets n ls} (R : as  Set r) (R? : Decidable R) 
              ∀[ R   R?  ]
toWitness {zero} R R? with R?
... | true because _ = _
... | no          ¬r = ⊥-elim ∘′ ¬r
toWitness {suc n} R R? = toWitness (R _) (R? _)