------------------------------------------------------------------------ -- The Agda standard library -- -- An inductive definition of the heterogeneous sublist relation -- This is a generalisation of what is commonly known as Order -- Preserving Embeddings (OPE). ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} open import Data.List.Base using (List; []; _∷_; [_]) open import Data.List.Relation.Unary.Any using (Any; here; there) open import Level using (_⊔_) open import Relation.Binary.Core using (REL; _⇒_) open import Relation.Binary.Definitions using (_⟶_Respects_; Min) open import Relation.Unary using (Pred) module Data.List.Relation.Binary.Sublist.Heterogeneous {a b r} {A : Set a} {B : Set b} {R : REL A B r} where ------------------------------------------------------------------------ -- Re-export core definitions open import Data.List.Relation.Binary.Sublist.Heterogeneous.Core public ------------------------------------------------------------------------ -- Type and basic combinators module _ {s} {S : REL A B s} where map : R ⇒ S → Sublist R ⇒ Sublist S map f [] = [] map f (y ∷ʳ rs) = y ∷ʳ map f rs map f (r ∷ rs) = f r ∷ map f rs minimum : Min (Sublist R) [] minimum [] = [] minimum (x ∷ xs) = x ∷ʳ minimum xs ------------------------------------------------------------------------ -- Conversion to and from Any -- Special case: Sublist R [ a ] bs → Any (R a) bs toAny : ∀ {a as bs} → Sublist R (a ∷ as) bs → Any (R a) bs toAny (y ∷ʳ rs) = there (toAny rs) toAny (r ∷ rs) = here r fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs fromAny (here r) = r ∷ minimum _ fromAny (there p) = _ ∷ʳ fromAny p ------------------------------------------------------------------------ -- Generalised lookup based on a proof of Any module _ {p q} {P : Pred A p} {Q : Pred B q} (resp : P ⟶ Q Respects R) where lookup : ∀ {xs ys} → Sublist R xs ys → Any P xs → Any Q ys lookup (y ∷ʳ p) k = there (lookup p k) lookup (rxy ∷ p) (here px) = here (resp rxy px) lookup (rxy ∷ p) (there k) = there (lookup p k) ------------------------------------------------------------------------ -- Disjoint sublists xs,ys ⊆ zs -- -- NB: This does not imply that xs and ys partition zs; -- zs may have additional elements. private infix 4 _⊆_ _⊆_ = Sublist R infixr 5 _∷ₙ_ _∷ₗ_ _∷ᵣ_ data Disjoint : ∀ {xs ys zs} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) → Set (a ⊔ b ⊔ r) where [] : Disjoint [] [] -- Element y of zs is neither in xs nor in ys: _∷ₙ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} → (y : B) → Disjoint τ₁ τ₂ → Disjoint (y ∷ʳ τ₁) (y ∷ʳ τ₂) -- Element y of zs is in xs as x with x≈y: _∷ₗ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {x y} → (x≈y : R x y) → Disjoint τ₁ τ₂ → Disjoint (x≈y ∷ τ₁) (y ∷ʳ τ₂) -- Element y of zs is in ys as x with x≈y: _∷ᵣ_ : ∀ {xs ys zs} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {x y} → (x≈y : R x y) → Disjoint τ₁ τ₂ → Disjoint (y ∷ʳ τ₁) (x≈y ∷ τ₂) ------------------------------------------------------------------------ -- Disjoint union of two sublists xs,ys ⊆ zs -- -- This is the Cover relation without overlap of Section 6 of -- Conor McBride, Everybody's Got To Be Somewhere, -- MSFP@FSCD 2018: 53-69. data DisjointUnion : ∀ {xs ys zs us} (τ₁ : xs ⊆ zs) (τ₂ : ys ⊆ zs) (τ : us ⊆ zs) → Set (a ⊔ b ⊔ r) where [] : DisjointUnion [] [] [] -- Element y of zs is neither in xs nor in ys: skip. _∷ₙ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} → (y : B) → DisjointUnion τ₁ τ₂ τ → DisjointUnion (y ∷ʳ τ₁) (y ∷ʳ τ₂) (y ∷ʳ τ) -- Element y of zs is in xs as x with x≈y: add to us. _∷ₗ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} {x y} → (x≈y : R x y) → DisjointUnion τ₁ τ₂ τ → DisjointUnion (x≈y ∷ τ₁) (y ∷ʳ τ₂) (x≈y ∷ τ) -- Element y of zs is in ys as x with x≈y: add to us. _∷ᵣ_ : ∀ {xs ys zs us} {τ₁ : xs ⊆ zs} {τ₂ : ys ⊆ zs} {τ : us ⊆ zs} {x y} → (x≈y : R x y) → DisjointUnion τ₁ τ₂ τ → DisjointUnion (y ∷ʳ τ₁) (x≈y ∷ τ₂) (x≈y ∷ τ)