------------------------------------------------------------------------
-- 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 Data.Unit.Base using (⊤)
open import Data.Bool.Base using (true; false)
open import Data.Empty using (⊥; ⊥-elim)
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 Level using (Level; _⊔_; Lift)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Nullary.Decidable.Core as Dec
using (Dec; yes; no; _because_; _×-dec_)
import Relation.Unary as Unary
using (Pred; Satisfiable; Universal; IUniversal)
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? _)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4