diff --git a/CHANGELOG.md b/CHANGELOG.md index b780aa6e1f..343460e8c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -75,6 +75,13 @@ New modules Relation.Binary.Construct.Interior.Symmetric ``` +* Pointwise and equality relations over indexed containers: + ```agda + Data.Container.Indexed.Relation.Binary.Pointwise + Data.Container.Indexed.Relation.Binary.Pointwise.Properties + Data.Container.Indexed.Relation.Binary.Equality.Setoid + ``` + Additions to existing modules ----------------------------- @@ -142,6 +149,11 @@ Additions to existing modules idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x ``` +* In `Data.Container.Indexed.Core`: + ```agda + Subtrees o c = (r : Response c) → X (next c r) + ``` + * In `Data.Fin.Properties`: ```agda nonZeroIndex : Fin n → ℕ.NonZero n diff --git a/doc/README/Data.agda b/doc/README/Data.agda index e7d8a13886..c1e900e541 100644 --- a/doc/README/Data.agda +++ b/doc/README/Data.agda @@ -218,7 +218,8 @@ import README.Data.Vec.Relation.Binary.Equality.Cast -- monad, least fixed point, etc.) can be used import README.Data.Container.FreeMonad -import README.Data.Container.Indexed +import README.Data.Container.Indexed.VectorExample +import README.Data.Container.Indexed.MultiSortedAlgebraExample -- Wrapping n-ary relations into a record definition so type-inference -- remembers the things being related. diff --git a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda new file mode 100644 index 0000000000..0c466c932c --- /dev/null +++ b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda @@ -0,0 +1,431 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Example of multi-sorted algebras as indexed containers +------------------------------------------------------------------------ + +{-# OPTIONS --safe --cubical-compatible #-} + +module README.Data.Container.Indexed.MultiSortedAlgebraExample where + +------------------------------------------------------------------------ +-- Preliminaries +------------------------------------------------------------------------ +-- We import library content for indexed containers, standard types, +-- and setoids. + +open import Level + +open import Data.Container.Indexed.Core using (Container; ⟦_⟧; _◃_/_) +open import Data.Container.Indexed.FreeMonad using (_⋆C_) +open import Data.W.Indexed using (W; sup) + +open import Data.Product using (Σ; _×_; _,_; Σ-syntax) +open import Data.Sum using (_⊎_; inj₁; inj₂; [_,_]) +open import Data.Empty.Polymorphic using (⊥; ⊥-elim) + +open import Function using (_∘_) +open import Function.Bundles using (Func) + +open import Relation.Binary using (Setoid; IsEquivalence) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +import Data.Container.Indexed.Relation.Binary.Equality.Setoid as ICSetoid +import Relation.Binary.Reasoning.Setoid as SetoidReasoning + +open Setoid using (Carrier; _≈_; isEquivalence) +open Func renaming (to to apply) + +-- Letter ℓ denotes universe levels. + +variable + ℓ ℓ' ℓˢ ℓᵒ ℓᵃ ℓᵐ ℓᵉ ℓⁱ : Level + I : Set ℓⁱ + S : Set ℓˢ + +------------------------------------------------------------------------ +-- The interpretation of a container (Op ◃ Ar / sort) is +-- +-- ⟦ Op ◃ Ar / sort ⟧ X s = Σ[ o ∈ Op s ] ((i : Ar o) → X (sort o i)) +-- +-- which contains pairs consisting of an operator $o$ and its collection +-- of arguments. The least fixed point of (X ↦ ⟦ C ⟧ X) is the indexed +-- W-type given by C, and it contains closed first-order terms of the +-- multi-sorted algebra C. + +-- We need to interpret indexed containers on Setoids. +-- This definition is missing from the standard library v1.7. + +⟦_⟧s : (C : Container I S ℓᵒ ℓᵃ) (ξ : I → Setoid ℓᵐ ℓᵉ) → S → Setoid _ _ +⟦ C ⟧s ξ = ICSetoid.setoid ξ C + +------------------------------------------------------------------------ +-- Multi-sorted algebras +-------------------------------------------------------------------------- +-- A multi-sorted algebra is an indexed container. +-- +-- * Sorts are indexes. +-- +-- * Operators are commands/shapes. +-- +-- * Arities/argument are responses/positions. +-- +-- Closed terms (initial model) are given by the W type for a container, +-- renamed to μ here (for least fixed-point). + +-- We assume a fixed signature (Sort, Ops). + +module _ (Sort : Set ℓˢ) (Ops : Container Sort Sort ℓᵒ ℓᵃ) where + open Container Ops renaming + ( Command to Op + ; Response to Arity + ; next to sort + ) + +-- We let letter $s$ range over sorts and $\mathit{op}$ over operators. + + variable + s s' : Sort + op op' : Op s + +------------------------------------------------------------------------ +-- Models + + -- A model is given by an interpretation (Den $s$) for each sort $s$ + -- plus an interpretation (den $o$) for each operator $o$. + + record SetModel ℓᵐ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc ℓᵐ) where + field + Den : Sort → Set ℓᵐ + den : {s : Sort} → ⟦ Ops ⟧ Den s → Den s + + -- The setoid model requires operators to respect equality. + -- The Func record packs a function (apply) with a proof (cong) + -- that the function maps equals to equals. + + record SetoidModel ℓᵐ ℓᵉ : Set (ℓˢ ⊔ ℓᵒ ⊔ ℓᵃ ⊔ suc (ℓᵐ ⊔ ℓᵉ)) where + field + Den : Sort → Setoid ℓᵐ ℓᵉ + den : {s : Sort} → Func (⟦ Ops ⟧s Den s) (Den s) + + +------------------------------------------------------------------------ +-- Terms + + -- To obtain terms with free variables, we add additional nullary + -- operators, each representing a variable. + -- + -- These are covered in the standard library FreeMonad module, + -- albeit with the restriction that the operator and variable sets + -- have the same size. + + Cxt = Sort → Set ℓᵒ + + variable + Γ Δ : Cxt + + -- Terms with free variables in Var. + + module _ (Var : Cxt) where + + -- We keep the same sorts, but add a nullary operator for each variable. + + Ops⁺ : Container Sort Sort ℓᵒ ℓᵃ + Ops⁺ = Ops ⋆C Var + + -- Terms with variables are then given by the W-type for the extended container. + + Tm = W Ops⁺ + + -- We define nice constructors for variables and operator application + -- via pattern synonyms. + -- Note that the $f$ in constructor var' is a function from the empty set, + -- so it should be uniquely determined. However, Agda's equality is + -- more intensional and will not identify all functions from the empty set. + -- Since we do not make use of the axiom of function extensionality, + -- we sometimes have to consult the extensional equality of the + -- function setoid. + + pattern _∙_ op args = sup (inj₂ op , args) + pattern var' x f = sup (inj₁ x , f ) + pattern var x = var' x _ + + -- Letter $t$ ranges over terms, and $\mathit{ts}$ over argument vectors. + + variable + t t' t₁ t₂ t₃ : Tm Γ s + ts ts' : (i : Arity op) → Tm Γ (sort _ i) + +------------------------------------------------------------------------ +-- Parallel substitutions + + -- A substitution from Δ to Γ holds a term in Γ for each variable in Δ. + + Sub : (Γ Δ : Cxt) → Set _ + Sub Γ Δ = ∀{s} (x : Δ s) → Tm Γ s + + -- Application of a substitution. + + _[_] : (t : Tm Δ s) (σ : Sub Γ Δ) → Tm Γ s + (var x ) [ σ ] = σ x + (op ∙ ts) [ σ ] = op ∙ λ i → ts i [ σ ] + + -- Letter $σ$ ranges over substitutions. + + variable + σ σ' : Sub Γ Δ + +------------------------------------------------------------------------ +-- Interpretation of terms in a model +------------------------------------------------------------------------ + + -- Given an algebra $M$ of set-size $ℓ^m$ and equality-size $ℓ^e$, + -- we define the interpretation of an $s$-sorted term $t$ as element + -- of $M(s)$ according to an environment $ρ$ that maps each variable + -- of sort $s'$ to an element of $M(s')$. + + module _ {M : SetoidModel ℓᵐ ℓᵉ} where + open SetoidModel M + + -- Equality in $M$'s interpretation of sort $s$. + + _≃_ : Den s .Carrier → Den s .Carrier → Set _ + _≃_ {s = s} = Den s ._≈_ + + -- An environment for Γ maps each variable $x : Γ(s)$ to an element of $M(s)$. + -- Equality of environments is defined pointwise. + + Env : Cxt → Setoid _ _ + Env Γ .Carrier = {s : Sort} (x : Γ s) → Den s .Carrier + Env Γ ._≈_ ρ ρ' = {s : Sort} (x : Γ s) → ρ x ≃ ρ' x + Env Γ .isEquivalence .IsEquivalence.refl {s = s} x = Den s .Setoid.refl + Env Γ .isEquivalence .IsEquivalence.sym h {s} x = Den s .Setoid.sym (h x) + Env Γ .isEquivalence .IsEquivalence.trans g h {s} x = Den s .Setoid.trans (g x) (h x) + + -- Interpretation of terms is iteration on the W-type. + -- The standard library offers `iter' (on sets), but we need this to be a Func (on setoids). + + ⦅_⦆ : ∀{s} (t : Tm Γ s) → Func (Env Γ) (Den s) + ⦅ var x ⦆ .apply ρ = ρ x + ⦅ var x ⦆ .cong ρ=ρ' = ρ=ρ' x + ⦅ op ∙ args ⦆ .apply ρ = den .apply (op , λ i → ⦅ args i ⦆ .apply ρ) + ⦅ op ∙ args ⦆ .cong ρ=ρ' = den .cong (refl , λ i → ⦅ args i ⦆ .cong ρ=ρ') + + -- An equality between two terms holds in a model + -- if the two terms are equal under all valuations of their free variables. + + Equal : ∀ {Γ s} (t t' : Tm Γ s) → Set _ + Equal {Γ} {s} t t' = ∀ (ρ : Env Γ .Carrier) → ⦅ t ⦆ .apply ρ ≃ ⦅ t' ⦆ .apply ρ + + -- This notion is an equivalence relation. + + isEquiv : IsEquivalence (Equal {Γ = Γ} {s = s}) + isEquiv {s = s} .IsEquivalence.refl ρ = Den s .Setoid.refl + isEquiv {s = s} .IsEquivalence.sym e ρ = Den s .Setoid.sym (e ρ) + isEquiv {s = s} .IsEquivalence.trans e e' ρ = Den s .Setoid.trans (e ρ) (e' ρ) + +------------------------------------------------------------------------ +-- Substitution lemma + + -- Evaluation of a substitution gives an environment. + + ⦅_⦆s : Sub Γ Δ → Env Γ .Carrier → Env Δ .Carrier + ⦅ σ ⦆s ρ x = ⦅ σ x ⦆ .apply ρ + + -- Substitution lemma: ⦅t[σ]⦆ρ ≃ ⦅t⦆⦅σ⦆ρ + + substitution : (t : Tm Δ s) (σ : Sub Γ Δ) (ρ : Env Γ .Carrier) → + ⦅ t [ σ ] ⦆ .apply ρ ≃ ⦅ t ⦆ .apply (⦅ σ ⦆s ρ) + substitution (var x) σ ρ = Den _ .Setoid.refl + substitution (op ∙ ts) σ ρ = den .cong (refl , λ i → substitution (ts i) σ ρ) + +------------------------------------------------------------------------ +-- Equations + + -- An equation is a pair $t ≐ t'$ of terms of the same sort in the same context. + + record Eq : Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ) where + constructor _≐_ + field + {cxt} : Sort → Set ℓᵒ + {srt} : Sort + lhs : Tm cxt srt + rhs : Tm cxt srt + + -- Equation $t ≐ t'$ holding in model $M$. + + _⊧_ : (M : SetoidModel ℓᵐ ℓᵉ) (eq : Eq) → Set _ + M ⊧ (t ≐ t') = Equal {M = M} t t' + + -- Sets of equations are presented as collection E : I → Eq + -- for some index set I : Set ℓⁱ. + + -- An entailment/consequence $E ⊃ t ≐ t'$ is valid + -- if $t ≐ t'$ holds in all models that satify equations $E$. + + module _ {ℓᵐ ℓᵉ} where + + _⊃_ : (E : I → Eq) (eq : Eq) → Set _ + E ⊃ eq = ∀ (M : SetoidModel ℓᵐ ℓᵉ) → (∀ i → M ⊧ E i) → M ⊧ eq + + -- Derivations + -------------- + + -- Equalitional logic allows us to prove entailments via the + -- inference rules for the judgment $E ⊢ Γ ▹ t ≡ t'$. + -- This could be coined as equational theory over a given + -- set of equations $E$. + -- Relation $E ⊢ Γ ▹ \_ ≡ \_$ is the least congruence over the equations $E$. + + data _⊢_▹_≡_ {I : Set ℓⁱ} + (E : I → Eq) : (Γ : Cxt) (t t' : Tm Γ s) → Set (ℓˢ ⊔ suc ℓᵒ ⊔ ℓᵃ ⊔ ℓⁱ) where + + hyp : ∀ i → let t ≐ t' = E i in + E ⊢ _ ▹ t ≡ t' + + base : ∀ (x : Γ s) {f f' : (i : ⊥) → Tm _ (⊥-elim i)} → + E ⊢ Γ ▹ var' x f ≡ var' x f' + + app : (∀ i → E ⊢ Γ ▹ ts i ≡ ts' i) → + E ⊢ Γ ▹ (op ∙ ts) ≡ (op ∙ ts') + + sub : E ⊢ Δ ▹ t ≡ t' → + ∀ (σ : Sub Γ Δ) → + E ⊢ Γ ▹ (t [ σ ]) ≡ (t' [ σ ]) + + refl : ∀ (t : Tm Γ s) → + E ⊢ Γ ▹ t ≡ t + + sym : E ⊢ Γ ▹ t ≡ t' → + E ⊢ Γ ▹ t' ≡ t + + trans : E ⊢ Γ ▹ t₁ ≡ t₂ → + E ⊢ Γ ▹ t₂ ≡ t₃ → + E ⊢ Γ ▹ t₁ ≡ t₃ + +------------------------------------------------------------------------ +-- Soundness of the inference rules + + -- We assume a model $M$ that validates all equations in $E$. + + module Soundness {I : Set ℓⁱ} (E : I → Eq) (M : SetoidModel ℓᵐ ℓᵉ) + (V : ∀ i → M ⊧ E i) where + open SetoidModel M + + -- In any model $M$ that satisfies the equations $E$, + -- derived equality is actual equality. + + sound : E ⊢ Γ ▹ t ≡ t' → M ⊧ (t ≐ t') + + sound (hyp i) = V i + sound (app {op = op} es) ρ = den .cong (refl , λ i → sound (es i) ρ) + sound (sub {t = t} {t' = t'} e σ) ρ = begin + ⦅ t [ σ ] ⦆ .apply ρ ≈⟨ substitution {M = M} t σ ρ ⟩ + ⦅ t ⦆ .apply ρ' ≈⟨ sound e ρ' ⟩ + ⦅ t' ⦆ .apply ρ' ≈⟨ substitution {M = M} t' σ ρ ⟨ + ⦅ t' [ σ ] ⦆ .apply ρ ∎ + where + open SetoidReasoning (Den _) + ρ' = ⦅ σ ⦆s ρ + + sound (base x {f} {f'}) = isEquiv {M = M} .IsEquivalence.refl {var' x λ()} + + sound (refl t) = isEquiv {M = M} .IsEquivalence.refl {t} + sound (sym {t = t} {t' = t'} e) = isEquiv {M = M} .IsEquivalence.sym + {x = t} {y = t'} (sound e) + sound (trans {t₁ = t₁} {t₂ = t₂} + {t₃ = t₃} e e') = isEquiv {M = M} .IsEquivalence.trans + {i = t₁} {j = t₂} {k = t₃} (sound e) (sound e') + + +------------------------------------------------------------------------ +-- Birkhoff's completeness theorem +------------------------------------------------------------------------ + + -- Birkhoff proved that any equation $t ≐ t'$ is derivable from $E$ + -- when it is valid in all models satisfying $E$. His proof (for + -- single-sorted algebras) is a blue print for many more + -- completeness proofs. They all proceed by constructing a + -- universal model aka term model. In our case, it is terms + -- quotiented by derivable equality $E ⊢ Γ ▹ \_ ≡ \_$. It then + -- suffices to prove that this model satisfies all equations in $E$. + +------------------------------------------------------------------------ +-- Universal model + + -- A term model for $E$ and $Γ$ interprets sort $s$ by (Tm Γ s) quotiented by $E ⊢ Γ ▹ \_ ≡ \_$. + + module TermModel {I : Set ℓⁱ} (E : I → Eq) where + open SetoidModel + + -- Tm Γ s quotiented by E⊢Γ▹·≡·. + + TmSetoid : Cxt → Sort → Setoid _ _ + TmSetoid Γ s .Carrier = Tm Γ s + TmSetoid Γ s ._≈_ = E ⊢ Γ ▹_≡_ + TmSetoid Γ s .isEquivalence .IsEquivalence.refl = refl _ + TmSetoid Γ s .isEquivalence .IsEquivalence.sym = sym + TmSetoid Γ s .isEquivalence .IsEquivalence.trans = trans + + -- The interpretation of an operator is simply the operator. + -- This works because $E⊢Γ▹\_≡\_$ is a congruence. + + tmInterp : ∀ {Γ s} → Func (⟦ Ops ⟧s (TmSetoid Γ) s) (TmSetoid Γ s) + tmInterp .apply (op , ts) = op ∙ ts + tmInterp .cong (refl , h) = app h + + -- The term model per context Γ. + + M : Cxt → SetoidModel _ _ + M Γ .Den = TmSetoid Γ + M Γ .den = tmInterp + + -- The identity substitution σ₀ maps variables to themselves. + + σ₀ : {Γ : Cxt} → Sub Γ Γ + σ₀ x = var' x λ() + + -- σ₀ acts indeed as identity. + + identity : (t : Tm Γ s) → E ⊢ Γ ▹ t [ σ₀ ] ≡ t + identity (var x) = base x + identity (op ∙ ts) = app λ i → identity (ts i) + + -- Evaluation in the term model is substitution $E ⊢ Γ ▹ ⦅t⦆σ ≡ t[σ]$. + -- This would even hold "up to the nose" if we had function extensionality. + + evaluation : (t : Tm Δ s) (σ : Sub Γ Δ) → E ⊢ Γ ▹ (⦅_⦆ {M = M Γ} t .apply σ) ≡ (t [ σ ]) + evaluation (var x) σ = refl (σ x) + evaluation (op ∙ ts) σ = app (λ i → evaluation (ts i) σ) + + -- The term model satisfies all the equations it started out with. + + satisfies : ∀ i → M Γ ⊧ E i + satisfies i σ = begin + ⦅ tₗ ⦆ .apply σ ≈⟨ evaluation tₗ σ ⟩ + tₗ [ σ ] ≈⟨ sub (hyp i) σ ⟩ + tᵣ [ σ ] ≈⟨ evaluation tᵣ σ ⟨ + ⦅ tᵣ ⦆ .apply σ ∎ + where + open SetoidReasoning (TmSetoid _ _) + tₗ = E i .Eq.lhs + tᵣ = E i .Eq.rhs + +------------------------------------------------------------------------ +-- Completeness + +-- Birkhoff's completeness theorem \citeyearpar{birkhoff:1935}: +-- Any valid consequence is derivable in the equational theory. + + module Completeness {I : Set ℓⁱ} (E : I → Eq) {Γ s} {t t' : Tm Γ s} where + open TermModel E + + completeness : E ⊃ (t ≐ t') → E ⊢ Γ ▹ t ≡ t' + completeness V = begin + t ≈˘⟨ identity t ⟩ + t [ σ₀ ] ≈˘⟨ evaluation t σ₀ ⟩ + ⦅ t ⦆ .apply σ₀ ≈⟨ V (M Γ) satisfies σ₀ ⟩ + ⦅ t' ⦆ .apply σ₀ ≈⟨ evaluation t' σ₀ ⟩ + t' [ σ₀ ] ≈⟨ identity t' ⟩ + t' ∎ + where open SetoidReasoning (TmSetoid Γ s) diff --git a/doc/README/Data/Container/Indexed.agda b/doc/README/Data/Container/Indexed/VectorExample.agda similarity index 89% rename from doc/README/Data/Container/Indexed.agda rename to doc/README/Data/Container/Indexed/VectorExample.agda index adf6cbc9e5..45d45cc740 100644 --- a/doc/README/Data/Container/Indexed.agda +++ b/doc/README/Data/Container/Indexed/VectorExample.agda @@ -6,7 +6,7 @@ {-# OPTIONS --with-K --safe --guardedness #-} -module README.Data.Container.Indexed where +module README.Data.Container.Indexed.VectorExample where open import Data.Unit open import Data.Empty @@ -27,12 +27,14 @@ module _ {a} (A : Set a) where -- 2. Responses the indexed container returns to these commands -- 3. Update of the index based on the command and the response issued. --- For a vector, commands are constructors, responses are the number of subvectors --- (0 if the vector is empty, 1 otherwise) and the update corresponds to setting the --- size of the tail (if it exists). We can formalize these ideas like so: +-- For a vector, commands are constructors, responses are the number +-- of subvectors (0 if the vector is empty, 1 otherwise) and the +-- update corresponds to setting the size of the tail (if it exists). +-- We can formalize these ideas like so: --- Depending on the size of the vector, we may have reached the end already (nil) --- or we may specify what the head should be (cons). This is the type of commands. +-- Depending on the size of the vector, we may have reached the end +-- already (nil) or we may specify what the head should be (cons). +-- This is the type of commands. data VecC : ℕ → Set a where nil : VecC zero diff --git a/src/Data/Container/Indexed/Core.agda b/src/Data/Container/Indexed/Core.agda index 75d1a0d986..04175781d9 100644 --- a/src/Data/Container/Indexed/Core.agda +++ b/src/Data/Container/Indexed/Core.agda @@ -12,34 +12,46 @@ open import Level open import Data.Product.Base using (Σ; Σ-syntax; _,_; ∃) open import Relation.Unary +private variable + i o c r ℓ ℓ′ : Level + I : Set i + O : Set o + +------------------------------------------------------------------------ +-- Definition + infix 5 _◃_/_ -record Container {i o} (I : Set i) (O : Set o) (c r : Level) : - Set (i ⊔ o ⊔ suc c ⊔ suc r) where +record Container (I : Set i) (O : Set o) c r : Set (i ⊔ o ⊔ suc c ⊔ suc r) where constructor _◃_/_ field Command : (o : O) → Set c Response : ∀ {o} → Command o → Set r next : ∀ {o} (c : Command o) → Response c → I +------------------------------------------------------------------------ -- The semantics ("extension") of an indexed container. -⟦_⟧ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} → Container I O c r → - Pred I ℓ → Pred O _ -⟦ C ◃ R / n ⟧ X o = Σ[ c ∈ C o ] ((r : R c) → X (n c r)) +module _ (C : Container I O c r) (X : Pred I ℓ) where + open Container C + + Subtrees : ∀ o → Command o → Set _ + Subtrees o c = (r : Response c) → X (next c r) + + ⟦_⟧ : Pred O _ + ⟦_⟧ o = Σ (Command o) (Subtrees o) ------------------------------------------------------------------------ -- All and any -module _ {i o c r ℓ} {I : Set i} {O : Set o} - (C : Container I O c r) {X : Pred I ℓ} where +module _ (C : Container I O c r) {X : Pred I ℓ} where -- All. - □ : ∀ {ℓ′} → Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _ + □ : Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _ □ P (_ , _ , k) = ∀ r → P (_ , k r) -- Any. - ◇ : ∀ {ℓ′} → Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _ + ◇ : Pred (Σ I X) ℓ′ → Pred (Σ O (⟦ C ⟧ X)) _ ◇ P (_ , _ , k) = ∃ λ r → P (_ , k r) diff --git a/src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda b/src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda new file mode 100644 index 0000000000..8e259e90f7 --- /dev/null +++ b/src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda @@ -0,0 +1,60 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Equality over indexed container extensions parametrised by a setoid +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary using (Setoid) + +module Data.Container.Indexed.Relation.Binary.Equality.Setoid + {ℓⁱ ℓᶜ ℓᵉ} {I : Set ℓⁱ} (S : I → Setoid ℓᶜ ℓᵉ) + where + +open import Function +open import Level using (Level; _⊔_; suc) +open import Relation.Binary + +open import Data.Container.Indexed.Core +open import Data.Container.Indexed.Relation.Binary.Pointwise +import Data.Container.Indexed.Relation.Binary.Pointwise.Properties + as Pointwise + +open Setoid using (Carrier; _≈_) + +private variable + ℓˢ ℓᵖ : Level + O : Set _ + +------------------------------------------------------------------------ +-- Definition of equality + +module _ (C : Container I O ℓˢ ℓᵖ) (o : O) where + + Eq : Rel (⟦ C ⟧ (Carrier ∘ S) o) (ℓᵉ ⊔ ℓˢ ⊔ ℓᵖ) + Eq = Pointwise C (_≈_ ∘ S) o + +------------------------------------------------------------------------ +-- Relational properties + + refl : Reflexive Eq + refl = Pointwise.refl C _ (Setoid.refl ∘ S) + + sym : Symmetric Eq + sym = Pointwise.sym C _ (Setoid.sym ∘ S) + + trans : Transitive Eq + trans = Pointwise.trans C _ (Setoid.trans ∘ S) + + isEquivalence : IsEquivalence Eq + isEquivalence = record + { refl = refl + ; sym = sym + ; trans = trans + } + + setoid : Setoid (ℓˢ ⊔ ℓᵖ ⊔ ℓᶜ) (ℓˢ ⊔ ℓᵖ ⊔ ℓᵉ) + setoid = record + { isEquivalence = isEquivalence + } diff --git a/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda b/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda new file mode 100644 index 0000000000..afaba23f09 --- /dev/null +++ b/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda @@ -0,0 +1,58 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Pointwise equality for indexed containers +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Container.Indexed.Relation.Binary.Pointwise where + +open import Data.Product using (_,_; Σ-syntax) +open import Function +open import Level using (Level; _⊔_) +open import Relation.Binary using (REL; _⇒_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) + +open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧) + +private variable + ℓᵉ ℓᵉ′ ℓᵖ ℓˢ ℓˣ ℓʸ : Level + I O : Set _ + +------------------------------------------------------------------------ +-- Equality, parametrised on an underlying relation. + +-- Since ⟦_⟧ is a Σ-type, not a record, I'd say Pointwise should also be +-- a Σ-type, not a record. Maybe we need to update module +-- `Data.Container.Relation.Binary.Pointwise` accordingly... +-- +-- record Pointwise : Set (ℓˢ ⊔ ℓᵖ ⊔ ℓᵉ) where +-- constructor _,_ +-- field shape : c ≡ c' +-- position : Eqs shape xs ys + +module _ (C : Container I O ℓˢ ℓᵖ) + {X : I → Set ℓˣ} {Y : I → Set ℓʸ} (R : (i : I) → REL (X i) (Y i) ℓᵉ) + (o : O) + ((c , xs) : ⟦ C ⟧ X o) + ((c' , ys) : ⟦ C ⟧ Y o) + where + open Container C + + Eqs : c ≡ c' → Subtrees C X o c → Subtrees C Y o c' → Set _ + Eqs refl xs ys = (r : Response c) → R (next c r) (xs r) (ys r) + + Pointwise = Σ[ eq ∈ c ≡ c' ] Eqs eq xs ys + +------------------------------------------------------------------------ +-- Operations + +module _ {C : Container I O ℓˢ ℓᵖ} + {X : I → Set ℓˣ} {Y : I → Set ℓʸ} + {R : (i : I) → REL (X i) (Y i) ℓᵉ} + {R′ : (i : I) → REL (X i) (Y i) ℓᵉ′} + where + + map : (R⇒R′ : ∀ i → R i ⇒ R′ i) {o : O} → Pointwise C R o ⇒ Pointwise C R′ o + map R⇒R′ (refl , f) = refl , R⇒R′ _ ∘ f diff --git a/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda new file mode 100644 index 0000000000..58e6966154 --- /dev/null +++ b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda @@ -0,0 +1,45 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Properties of pointwise equality for indexed containers +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where + +open import Axiom.Extensionality.Propositional +open import Data.Container.Indexed.Core +open import Data.Container.Indexed.Relation.Binary.Pointwise +open import Data.Product using (_,_; Σ-syntax; -,_) +open import Level using (Level; _⊔_) +open import Relation.Binary +open import Relation.Binary.PropositionalEquality as P + using (_≡_; subst; cong) + +private variable + ℓᵉ ℓᵖ ℓˢ ℓˣ : Level + I O : Set _ + +module _ + (C : Container I O ℓˢ ℓᵖ) {X : I → Set ℓˣ} + (R : (i : I) → Rel (X i) ℓᵉ) + {o : O} + where + + refl : (∀ i → Reflexive (R i)) → Reflexive (Pointwise C R o) + refl R-refl = P.refl , λ p → R-refl _ + + sym : (∀ i → Symmetric (R i)) → Symmetric (Pointwise C R o) + sym R-sym (P.refl , f) = P.refl , λ p → R-sym _ (f p) + + trans : (∀ i → Transitive (R i)) → Transitive (Pointwise C R o) + trans R-trans (P.refl , f) (P.refl , g) = P.refl , λ p → R-trans _ (f p) (g p) + +-- If propositional equality is extensional, then `Eq _≡_` and `_≡_` coincide. +Eq⇒≡ : {C : Container I O ℓˢ ℓᵖ} {X : I → Set ℓˣ} {R : (i : I) → Rel (X i) ℓᵉ} + {o : O} {xs ys : ⟦ C ⟧ X o} → + Extensionality ℓᵖ ℓˣ → + Pointwise C (λ (i : I) → _≡_ {A = X i}) o xs ys → + xs ≡ ys +Eq⇒≡ ext (P.refl , f≈f′) = cong -,_ (ext f≈f′)