[ fix #432 #460 ] Heterogeneous version of Sublist

CHANGELOG.md

@@ -307,6 +307,9 @@ Non-backwards compatible changes
 * The proofs `toList⁺` and `toList⁻` in `Data.Vec.Relation.Unary.All.Properties` have been swapped
   as they were the opposite way round to similar properties in the rest of the library.
 
+* `Data.List.Relation.Binary.Sublist.Propositional.Solver` has been removed and replaced by
+  `Data.List.Relation.Binary.Sublist.DecPropositional.Solver`.
+
 * The functions `_∷=_` and `_─_` have been removed from `Data.List.Membership.Setoid` as they are subsumed by the more general versions now part of `Data.List.Any`.
 
 * Changed the type of `≡-≟-identity` to make use of the fact that equality
@@ -350,10 +353,27 @@ List of new modules
 
   Data.List.Relation.Unary.First
   Data.List.Relation.Unary.First.Properties
+
   Data.List.Relation.Binary.Prefix.Heterogeneous
   Data.List.Relation.Binary.Prefix.Heterogeneous.Properties
   Data.List.Relation.Binary.Suffix.Heterogeneous
   Data.List.Relation.Binary.Suffix.Heterogeneous.Properties
+
+  Data.List.Relation.Binary.Sublist.Heterogeneous
+  Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
+  Data.List.Relation.Binary.Sublist.Homogeneous.Properties
+  Data.List.Relation.Binary.Sublist.Homogeneous.Solver
+  Data.List.Relation.Binary.Sublist.Setoid
+  Data.List.Relation.Binary.Sublist.Setoid.Properties
+  Data.List.Relation.Binary.Sublist.DecSetoid
+  Data.List.Relation.Binary.Sublist.DecSetoid.Properties
+  Data.List.Relation.Binary.Sublist.DecSetoid.Solver
+  Data.List.Relation.Binary.Sublist.Propositional
+  Data.List.Relation.Binary.Sublist.Propositional.Properties
+  Data.List.Relation.Binary.Sublist.DecPropositional
+  Data.List.Relation.Binary.Sublist.DecPropositional.Properties
+  Data.List.Relation.Binary.Sublist.DecPropositional.Solver
+
   Data.List.Relation.Ternary.Interleaving.Setoid
   Data.List.Relation.Ternary.Interleaving.Setoid.Properties
   Data.List.Relation.Ternary.Interleaving.Propositional
@@ -1063,6 +1083,9 @@ Other minor additions
 
 * Added new definitions to `Relation.Binary.PropositionalEquality`:
   ```agda
+  trans-injectiveˡ : trans p₁ q ≡ trans p₂ q → p₁ ≡ p₂
+  trans-injectiveʳ : trans p q₁ ≡ trans p q₂ → q₁ ≡ q₂
+  subst-injective  : subst P x≡y p ≡ subst P x≡y q → p ≡ q
   module Constant⇒UIP
   module Decidable⇒UIP
   ```
@@ -1075,7 +1098,13 @@ Other minor additions
 * Added new definitions to `Relation.Binary.Core`:
   ```agda
   Antisym R S E = ∀ {i j} → R i j → S j i → E i j
-  Conn P Q      = ∀ x y → P x y ⊎ Q y x
+
+  Max : REL A B ℓ → B → Set _
+  Min : REL A B ℓ → A → Set _
+
+  Conn P Q = ∀ x y → P x y ⊎ Q y x
+
+  P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y
   ```
 
 * Added new proofs to `Relation.Binary.Lattice`:

src/Data/List/Relation/Binary/Sublist/DecPropositional.agda

@@ -0,0 +1,22 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An inductive definition of the sublist relation for types which have a
+-- decidable equality. This is commonly known as Order Preserving Embeddings (OPE).
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Decidable)
+open import Agda.Builtin.Equality using (_≡_)
+
+module Data.List.Relation.Binary.Sublist.DecPropositional
+       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+       where
+
+import Relation.Binary.PropositionalEquality as P
+
+open import Data.List.Relation.Binary.Sublist.DecSetoid (P.decSetoid _≟_)
+  hiding (lookup) public
+open import Data.List.Relation.Binary.Sublist.Propositional {A = A}
+  using (lookup) public

src/Data/List/Relation/Binary/Sublist/DecPropositional/Properties.agda

@@ -0,0 +1,21 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Sublist-related properties for types with a decidable equality
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Decidable)
+open import Agda.Builtin.Equality using (_≡_)
+
+module Data.List.Relation.Binary.Sublist.DecPropositional.Properties
+       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+       where
+
+import Relation.Binary.PropositionalEquality as P
+
+open import Data.List.Relation.Binary.Sublist.DecSetoid.Properties
+  (P.decSetoid _≟_) public
+open import Data.List.Relation.Binary.Sublist.Propositional.Properties {A = A}
+  using (lookup-injective) public

src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda

@@ -0,0 +1,19 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for proving that one list is a sublist of the other for types
+-- which enjoy decidable equalities.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Decidable)
+open import Agda.Builtin.Equality using (_≡_)
+
+module Data.List.Relation.Binary.Sublist.DecPropositional.Solver
+       {a} {A : Set a} (_≟_ : Decidable {A = A} _≡_)
+       where
+
+import Relation.Binary.PropositionalEquality as P
+
+open import Data.List.Relation.Binary.Sublist.DecSetoid.Solver (P.decSetoid _≟_) public

src/Data/List/Relation/Binary/Sublist/DecSetoid.agda

@@ -0,0 +1,18 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- An inductive definition of the sublist relation with respect to a setoid
+-- which is decidable. This is a generalisation of what is commonly known as
+-- Order Preserving Embeddings (OPE).
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (DecSetoid)
+
+module Data.List.Relation.Binary.Sublist.DecSetoid {c ℓ} (S : DecSetoid c ℓ) where
+
+private
+  module S = DecSetoid S
+
+open import Data.List.Relation.Binary.Sublist.Setoid S.setoid public

src/Data/List/Relation/Binary/Sublist/DecSetoid/Properties.agda

@@ -0,0 +1,35 @@
+-----------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Properties of the decidable setoid sublist relation
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (DecSetoid)
+
+module Data.List.Relation.Binary.Sublist.DecSetoid.Properties
+       {c ℓ} (S : DecSetoid c ℓ)
+       where
+
+open import Data.List.Base using (length)
+open import Data.List.Relation.Binary.Sublist.DecSetoid S
+open import Relation.Binary using (Decidable)
+
+private
+  module S = DecSetoid S
+
+------------------------------------------------------------------------
+-- Properties common to the setoid version
+
+import Data.List.Relation.Binary.Sublist.Setoid.Properties S.setoid as SubProp
+open SubProp
+  hiding ( sublist?
+         )
+  public
+
+------------------------------------------------------------------------
+-- Special properties holding for the special DecSetoid case
+
+sublist? : Decidable _⊆_
+sublist? = SubProp.sublist? S._≟_

src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda

@@ -0,0 +1,16 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- A solver for proving that one list is a sublist of the other.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (DecSetoid)
+
+module Data.List.Relation.Binary.Sublist.DecSetoid.Solver {c ℓ} (S : DecSetoid c ℓ) where
+
+private module S = DecSetoid S
+
+open import Data.List.Relation.Binary.Sublist.Homogeneous.Solver S._≈_ S.refl S._≟_
+  using (Item; module Item; TList; module TList; prove) public

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

@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- 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.Binary.Sublist.Heterogeneous where
+
+open import Level using (_⊔_)
+open import Data.List.Base using (List; []; _∷_; [_])
+open import Data.List.Relation.Unary.Any using (Any; here; there)
+open import Function
+open import Relation.Unary using (Pred)
+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
+
+------------------------------------------------------------------------
+-- Conversion to and from Any
+
+  toAny : ∀ {a bs} → Sublist R [ a ] 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 _ {a b p q r} {A : Set a} {B : Set b} {R : REL A B r}
+         {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 []       ()
+  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)