[ re #432 #460 ] Heterogeneous version of Sublist

Author: gallais

CHANGELOG.md

@@ -248,6 +248,8 @@ Other major changes
 
 * Added new modules `Data.List.Relation.Prefix.Heterogeneous(.Properties)`
 
+* Added new modules `Data.List.Sublist.Heterogeneous(.Properties)`
+
 * Added new modules `Data.List.First` and `Data.List.First.Properties` for a
   generalization of the notion of "first element in the list to satisfy a
   predicate".
@@ -667,9 +669,12 @@ Other minor additions
   wlog : Total _R_ → Symmetric Q → (∀ a b → a R b → Q a b) → ∀ a b → Q a b
   ```
 
-* Added new definition to `Relation.Binary.Core`:
+* Added new definitions to `Relation.Binary.Core`:
   ```agda
   Antisym R S E = ∀ {i j} → R i j → S j i → E i j
+
+  Max : REL A B ℓ → B → Set _
+  Min : REL A B ℓ → A → Set _
   ```
 
 * Added new proofs to `Relation.Binary.Lattice`:

src/Data/List/Relation/Sublist/Heterogeneous.agda

@@ -0,0 +1,40 @@
+------------------------------------------------------------------------
+-- 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 --without-K --safe #-}
+
+module Data.List.Relation.Sublist.Heterogeneous where
+
+open import Level using (_⊔_)
+open import Data.List.Base using (List; []; _∷_)
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+------------------------------------------------------------------------
+-- Type and basic combinators
+
+module _ {a b r} {A : Set a} {B : Set b} (R : REL A B r) where
+
+  data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
+    []   : Sublist [] []
+    _∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
+    _∷_  : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)
+
+module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {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
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  minimum : Min (Sublist R) []
+  minimum []       = []
+  minimum (x ∷ xs) = x ∷ʳ minimum xs

src/Data/List/Relation/Sublist/Heterogeneous/Properties.agda

@@ -0,0 +1,112 @@
+-----------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the heterogeneous sublist relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Relation.Sublist.Heterogeneous.Properties where
+
+open import Data.Empty
+open import Data.List.Any using (Any; here; there)
+open import Data.List.Base as List using (List; []; _∷_; _++_; [_]; length)
+open import Data.List.Relation.Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Sublist.Heterogeneous
+open import Data.Nat using (ℕ; _≤_); open ℕ; open _≤_
+open import Data.Nat.Properties
+  using (suc-injective; ≤-step; n≤1+n; <-irrefl; module ≤-Reasoning)
+open import Function
+open import Relation.Binary
+open import Relation.Binary.PropositionalEquality as P using (_≡_)
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  fromAny : ∀ {a bs} → Any (R a) bs → Sublist R [ a ] bs
+  fromAny (here r)  = r ∷ minimum _
+  fromAny (there p) = _ ∷ʳ fromAny p
+
+  toAny : ∀ {a bs} → Sublist R [ a ] bs → Any (R a) bs
+  toAny (y ∷ʳ rs) = there (toAny rs)
+  toAny (r ∷ rs)  = here r
+
+  length-mono-Sublist-≤ : ∀ {as bs} → Sublist R as bs → length as ≤ length bs
+  length-mono-Sublist-≤ []        = z≤n
+  length-mono-Sublist-≤ (y ∷ʳ rs) = ≤-step (length-mono-Sublist-≤ rs)
+  length-mono-Sublist-≤ (r ∷ rs)  = s≤s (length-mono-Sublist-≤ rs)
+
+  fromPointwise : Pointwise R ⇒ Sublist R
+  fromPointwise []       = []
+  fromPointwise (r ∷ rs) = r ∷ fromPointwise rs
+
+  toPointwise : ∀ {as bs} → length as ≡ length bs →
+                Sublist R as bs → Pointwise R as bs
+  toPointwise {bs = []}     eq []         = []
+  toPointwise {bs = b ∷ bs} eq (r ∷ rs)   = r ∷ toPointwise (suc-injective eq) rs
+  toPointwise {bs = b ∷ bs} eq (.b ∷ʳ rs) =
+    ⊥-elim $ <-irrefl eq (s≤s (length-mono-Sublist-≤ rs))
+
+module _ {a b c r s t} {A : Set a} {B : Set b} {C : Set c}
+         {R : REL A B r} {S : REL B C s} {T : REL A C t} where
+
+  trans : Trans R S T → Trans (Sublist R) (Sublist S) (Sublist T)
+  trans rs⇒t []        []        = []
+  trans rs⇒t rs        (y ∷ʳ ss) = y ∷ʳ trans rs⇒t rs ss
+  trans rs⇒t (y ∷ʳ rs) (s ∷ ss)  = _ ∷ʳ trans rs⇒t rs ss
+  trans rs⇒t (r ∷ rs)  (s ∷ ss)  = rs⇒t r s ∷ trans rs⇒t rs ss
+
+module _ {a b r s e} {A : Set a} {B : Set b}
+         {R : REL A B r} {S : REL B A s} {E : REL A B e} where
+
+  antisym : Antisym R S E → Antisym (Sublist R) (Sublist S) (Pointwise E)
+  antisym rs⇒e []        []        = []
+  antisym rs⇒e (r ∷ rs)  (s ∷ ss)  = rs⇒e r s ∷ antisym rs⇒e rs ss
+  -- impossible cases
+  antisym rs⇒e (_∷ʳ_ {xs} {ys₁} y rs) (_∷ʳ_ {ys₂} {zs} z ss) =
+    ⊥-elim $ <-irrefl P.refl $ begin
+    length (y ∷ ys₁) ≤⟨ length-mono-Sublist-≤ ss ⟩
+    length zs        ≤⟨ n≤1+n (length zs) ⟩
+    length (z ∷ zs)  ≤⟨ length-mono-Sublist-≤ rs ⟩
+    length ys₁       ∎ where open ≤-Reasoning
+  antisym rs⇒e (_∷ʳ_ {xs} {ys₁} y rs) (_∷_ {y} {ys₂} {z} {zs} s ss)  =
+    ⊥-elim $ <-irrefl P.refl $ begin
+    length (z ∷ zs) ≤⟨ length-mono-Sublist-≤ rs ⟩
+    length ys₁      ≤⟨ length-mono-Sublist-≤ ss ⟩
+    length zs       ∎ where open ≤-Reasoning
+  antisym rs⇒e (_∷_ {x} {xs} {y} {ys₁} r rs)  (_∷ʳ_ {ys₂} {zs} z ss) =
+    ⊥-elim $ <-irrefl P.refl $ begin
+    length (y ∷ ys₁) ≤⟨ length-mono-Sublist-≤ ss ⟩
+    length xs        ≤⟨ length-mono-Sublist-≤ rs ⟩
+    length ys₁       ∎ where open ≤-Reasoning
+
+------------------------------------------------------------------------
+-- _++_
+
+module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
+
+  ++⁺ : ∀ {as bs cs ds} → Sublist R as bs → Sublist R cs ds →
+        Sublist R (as ++ cs) (bs ++ ds)
+  ++⁺ []         cds = cds
+  ++⁺ (y ∷ʳ abs) cds = y ∷ʳ ++⁺ abs cds
+  ++⁺ (ab ∷ abs) cds = ab ∷ ++⁺ abs cds
+
+------------------------------------------------------------------------
+-- map
+
+module _ {a b c d r} {A : Set a} {B : Set b} {C : Set c} {D : Set d}
+         {R : REL C D r} where
+
+  map⁺ : ∀ {as bs} (f : A → C) (g : B → D) →
+         Sublist (λ a b → R (f a) (g b)) as bs →
+         Sublist R (List.map f as) (List.map g bs)
+  map⁺ f g []        = []
+  map⁺ f g (y ∷ʳ rs) = g y ∷ʳ map⁺ f g rs
+  map⁺ f g (r ∷ rs)  = r ∷ map⁺ f g rs
+
+  map⁻ : ∀ {as bs} (f : A → C) (g : B → D) →
+         Sublist R (List.map f as) (List.map g bs) →
+         Sublist (λ a b → R (f a) (g b)) as bs
+  map⁻ {[]}     {bs}     f g rs        = minimum _
+  map⁻ {a ∷ as} {[]}     f g ()
+  map⁻ {a ∷ as} {b ∷ bs} f g (_ ∷ʳ rs) = b ∷ʳ map⁻ f g rs
+  map⁻ {a ∷ as} {b ∷ bs} f g (r ∷ rs)  = r ∷ map⁻ f g rs

src/Relation/Binary/Core.agda

@@ -122,11 +122,18 @@ Trichotomous : ∀ {a ℓ₁ ℓ₂} {A : Set a} → Rel A ℓ₁ → Rel A ℓ
 Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
   where _>_ = flip _<_
 
+
+Max : ∀ {a ℓ} {A : Set a} {b} {B : Set b} → REL A B ℓ → B → Set _
+Max _≤_ T = ∀ x → x ≤ T
+
 Maximum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
-Maximum _≤_ ⊤ = ∀ x → x ≤ ⊤
+Maximum = Max
+
+Min : ∀ {a ℓ} {A : Set a} {b} {B : Set b} → REL A B ℓ → A → Set _
+Min R = Max (flip R)
 
 Minimum : ∀ {a ℓ} {A : Set a} → Rel A ℓ → A → Set _
-Minimum _≤_ = Maximum (flip _≤_)
+Minimum = Min
 
 _Respects_ : ∀ {a ℓ₁ ℓ₂} {A : Set a} → (A → Set ℓ₁) → Rel A ℓ₂ → Set _
 P Respects _∼_ = ∀ {x y} → x ∼ y → P x → P y