Add various lemmas about list relations (#1382)

Author: MatthewDaggitt

CHANGELOG.md

@@ -236,6 +236,14 @@ New modules
   Data.List.Relation.Binary.Suffix.Homogeneous.Properties
   ```
 
+* Properties of lists with decidably unique elements:
+  ```
+  Data.List.Relation.Unary.Unique.DecSetoid
+  Data.List.Relation.Unary.Unique.DecSetoid.Properties
+  Data.List.Relation.Unary.Unique.DecPropositional
+  Data.List.Relation.Unary.Unique.DecPropositional.Properties
+  ```
+
 * Added bindings for Haskell's `System.Environment`:
   ```
   System.Environment
@@ -429,12 +437,12 @@ Other minor additions
   xs ⊉ ys = ¬ xs ⊇ ys
   ```
 
-* Added new proofs in `Data.List.Relation.Binary.Subset.Propositional.Properties`:
+* Added new proofs in `Data.List.Relation.Binary.Subset.Setoid.Properties`:
   ```agda
   ⊆-respʳ-≋      : _⊆_ Respectsʳ _≋_
   ⊆-respˡ-≋      : _⊆_ Respectsˡ _≋_
 
-  ↭⇒⊆            : _↭_ ⇒ _⊆_
+  ⊆-reflexive-↭  : _↭_ ⇒ _⊆_
   ⊆-respʳ-↭      : _⊆_ Respectsʳ _↭_
   ⊆-respˡ-↭      : _⊆_ Respectsˡ _↭_
   ⊆-↭-isPreorder : IsPreorder _↭_ _⊆_
@@ -448,23 +456,36 @@ Other minor additions
   ++⁺ʳ           : xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
   ++⁺ˡ           : xs ⊆ ys → xs ++ zs ⊆ ys ++ zs
   ++⁺            : ws ⊆ xs → ys ⊆ zs → ws ++ ys ⊆ xs ++ zs
+
+  filter⁺′       : P ⋐ Q → xs ⊆ ys → filter P? xs ⊆ filter Q? ys
   ```
 
 * Added new proofs in `Data.List.Relation.Binary.Subset.Propositional.Properties`:
   ```agda
-  ↭⇒⊆            : _↭_ ⇒ _⊆_
+  ⊆-reflexive-↭  : _↭_ ⇒ _⊆_
   ⊆-respʳ-↭      : _⊆_ Respectsʳ _↭_
   ⊆-respˡ-↭      : _⊆_ Respectsˡ _↭_
   ⊆-↭-isPreorder : IsPreorder _↭_ _⊆_
   ⊆-↭-preorder   : Preorder _ _ _
 
   Any-resp-⊆     : (Any P) Respects _⊆_
   All-resp-⊇     : (All P) Respects _⊇_
+  Sublist⇒Subset : xs ⊑ ys → xs ⊆ ys
 
   xs⊆xs++ys      : xs ⊆ xs ++ ys
   xs⊆ys++xs      : xs ⊆ ys ++ xs
   ++⁺ʳ           : xs ⊆ ys → zs ++ xs ⊆ zs ++ ys
   ++⁺ˡ           : xs ⊆ ys → xs ++ zs ⊆ ys ++ zs
+
+  filter⁺′       : P ⋐ Q → xs ⊆ ys → filter P? xs ⊆ filter Q? ys
+  ```
+
+* Added new relations to `Data.List.Relation.Binary.Sublist.(Setoid/Propositional)`:
+  ```agda
+  xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys)
+  xs ⊃ ys = ys ⊂ xs
+  xs ⊄ ys = ¬ (xs ⊂ ys)
+  xs ⊅ ys = ¬ (xs ⊃ ys)
   ```
 
 * Added new proof in `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
@@ -477,6 +498,40 @@ Other minor additions
   ++↭ʳ++ : xs ++ ys ↭ xs ʳ++ ys
   ```
 
+* Added new proofs in `Data.List.Extrema`:
+  ```agda
+  min-mono-⊆ : ⊥₁ ≤ ⊥₂ → xs ⊇ ys → min ⊥₁ xs ≤ min ⊥₂ ys
+  max-mono-⊆ : ⊥₁ ≤ ⊥₂ → xs ⊆ ys → max ⊥₁ xs ≤ max ⊥₂ ys
+  ```
+
+* Added new operator in `Data.List.Membership.DecSetoid`:
+  ```agda
+  _∉?_ : Decidable _∉_
+  ```
+
+* Added new proofs in `Data.List.Relation.Unary.Any.Properties`:
+  ```agda
+  lookup-index   : (p : Any P xs) → P (lookup xs (index p))
+  applyDownFrom⁺ : P (f i) → i < n → Any P (applyDownFrom f n)
+  applyDownFrom⁻ : Any P (applyDownFrom f n) → ∃ λ i → i < n × P (f i)
+  ```
+
+* Added new proofs in `Data.List.Membership.Setoid.Properties`:
+  ```agda
+  ∈-applyDownFrom⁺ : i < n → f i ∈ applyDownFrom f n
+  ∈-applyDownFrom⁻ : v ∈ applyDownFrom f n → ∃ λ i → i < n × v ≈ f i
+  ```
+
+* Added new proofs in `Data.List.Membership.Propositional.Properties`:
+  ```agda
+  ∈-applyDownFrom⁺ : i < n → f i ∈ applyDownFrom f n
+  ∈-applyDownFrom⁻ : v ∈ applyDownFrom f n → ∃ λ i → i < n × v ≡ f i
+  ∈-upTo⁺          : i < n → i ∈ upTo n
+  ∈-upTo⁻          : i ∈ upTo n → i < n
+  ∈-downFrom⁺      : i < n → i ∈ downFrom n
+  ∈-downFrom⁻      : i ∈ downFrom n → i < n
+  ```
+
 * Added new definition in `Data.Nat.Base`:
   ```agda
   _≤ᵇ_ : (m n : ℕ) → Bool
@@ -657,3 +712,8 @@ Other minor additions
   intersection  : ⟨Set⟩ → ⟨Set⟩ → ⟨Set⟩
   intersections : List ⟨Set⟩ → ⟨Set⟩
   ```
+
+* Added new proof to `Relation.Binary.PropositionalEquality`:
+  ```agda
+  resp : (P : Pred A ℓ) → P Respects _≡_
+  ```

src/Data/List/Base.agda

@@ -200,7 +200,7 @@ applyUpTo f zero    = []
 applyUpTo f (suc n) = f zero ∷ applyUpTo (f ∘ suc) n
 
 applyDownFrom : (ℕ → A) → ℕ → List A
-applyDownFrom f zero = []
+applyDownFrom f zero    = []
 applyDownFrom f (suc n) = f n ∷ applyDownFrom f n
 
 tabulate : ∀ {n} (f : Fin n → A) → List A

src/Data/List/Extrema.agda

@@ -19,10 +19,10 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_; lookup; map; tab
 open import Data.List.Membership.Propositional using (_∈_; lose)
 open import Data.List.Membership.Propositional.Properties
   using (foldr-selective)
-open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_)
+open import Data.List.Relation.Binary.Subset.Propositional using (_⊆_; _⊇_)
 open import Data.List.Properties
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base using (id; flip; _on_)
+open import Function.Base using (id; flip; _on_; _∘_)
 open import Level using (Level)
 open import Relation.Unary using (Pred)
 import Relation.Binary.Construct.NonStrictToStrict as NonStrictToStrict
@@ -205,6 +205,10 @@ min[xs]<min[ys]⁺ : ∀ ⊤₁ {⊤₂} xs {ys} → (⊤₁ < ⊤₂) ⊎ Any (
                    min ⊤₁ xs < min ⊤₂ ys
 min[xs]<min[ys]⁺ = argmin[xs]<argmin[ys]⁺
 
+min-mono-⊆ : ∀ {⊥₁ ⊥₂ xs ys} → ⊥₁ ≤ ⊥₂ → xs ⊇ ys → min ⊥₁ xs ≤ min ⊥₂ ys
+min-mono-⊆ ⊥₁≤⊥₂ ys⊆xs = min[xs]≤min[ys]⁺ _ _ (inj₁ ⊥₁≤⊥₂)
+  (tabulate (inj₂ ∘ Any.map (λ {≡-refl → refl}) ∘ ys⊆xs))
+
 ------------------------------------------------------------------------------
 -- Properties of max
 
@@ -238,3 +242,7 @@ max[xs]<max[ys]⁺ : ∀ {⊥₁} ⊥₂ {xs} ys → ⊥₁ < ⊥₂ ⊎ Any (
                    All (λ x → x < ⊥₂ ⊎ Any (x <_) ys) xs →
                    max ⊥₁ xs < max ⊥₂ ys
 max[xs]<max[ys]⁺ = argmax[xs]<argmax[ys]⁺
+
+max-mono-⊆ : ∀ {⊥₁ ⊥₂ xs ys} → ⊥₁ ≤ ⊥₂ → xs ⊆ ys → max ⊥₁ xs ≤ max ⊥₂ ys
+max-mono-⊆ ⊥₁≤⊥₂ xs⊆ys = max[xs]≤max[ys]⁺ _ _ (inj₁ ⊥₁≤⊥₂)
+  (tabulate (inj₂ ∘ Any.map (λ {≡-refl → refl}) ∘ xs⊆ys))

src/Data/List/Membership/DecPropositional.agda

@@ -17,5 +17,5 @@ module Data.List.Membership.DecPropositional
 
 open import Data.List.Membership.Propositional {A = A} public
 open import Data.List.Membership.DecSetoid (decSetoid _≟_) public
-  using (_∈?_)
+  using (_∈?_; _∉?_)
 

src/Data/List/Membership/DecSetoid.agda

@@ -7,6 +7,7 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary using (Decidable; DecSetoid)
+open import Relation.Nullary.Negation using (¬?)
 
 module Data.List.Membership.DecSetoid {a ℓ} (DS : DecSetoid a ℓ) where
 
@@ -21,7 +22,10 @@ open import Data.List.Membership.Setoid (DecSetoid.setoid DS) public
 ------------------------------------------------------------------------
 -- Other operations
 
-infix 4 _∈?_
+infix 4 _∈?_ _∉?_
 
 _∈?_ : Decidable _∈_
 x ∈? xs = any? (x ≟_) xs
+
+_∉?_ : Decidable _∉_
+x ∉? xs = ¬? (x ∈? xs)

src/Data/List/Membership/Propositional/Properties.agda

@@ -185,6 +185,38 @@ module _ (f : ℕ → A) where
                  ∃ λ i → i < n × v ≡ f i
   ∈-applyUpTo⁻ = Membershipₛ.∈-applyUpTo⁻ (P.setoid _) f
 
+------------------------------------------------------------------------
+-- upTo
+
+∈-upTo⁺ : ∀ {n i} → i < n → i ∈ upTo n
+∈-upTo⁺ = ∈-applyUpTo⁺ id
+
+∈-upTo⁻ : ∀ {n i} → i ∈ upTo n → i < n
+∈-upTo⁻ p with ∈-applyUpTo⁻ id p
+... | _ , i<n , refl = i<n
+
+------------------------------------------------------------------------
+-- applyDownFrom
+
+module _ (f : ℕ → A) where
+
+  ∈-applyDownFrom⁺ : ∀ {i n} → i < n → f i ∈ applyDownFrom f n
+  ∈-applyDownFrom⁺ = Membershipₛ.∈-applyDownFrom⁺ (P.setoid _) f
+
+  ∈-applyDownFrom⁻ : ∀ {v n} → v ∈ applyDownFrom f n →
+                     ∃ λ i → i < n × v ≡ f i
+  ∈-applyDownFrom⁻ = Membershipₛ.∈-applyDownFrom⁻ (P.setoid _) f
+
+------------------------------------------------------------------------
+-- downFrom
+
+∈-downFrom⁺ : ∀ {n i} → i < n → i ∈ downFrom n
+∈-downFrom⁺ i<n = ∈-applyDownFrom⁺ id i<n
+
+∈-downFrom⁻ : ∀ {n i} → i ∈ downFrom n → i < n
+∈-downFrom⁻ p with ∈-applyDownFrom⁻ id p
+... | _ , i<n , refl = i<n
+
 ------------------------------------------------------------------------
 -- tabulate
 

src/Data/List/Membership/Setoid/Properties.agda

@@ -255,6 +255,16 @@ module _ (S : Setoid c ℓ) where
                  ∃ λ i → i < n × v ≈ f i
   ∈-applyUpTo⁻ = Any.applyUpTo⁻
 
+------------------------------------------------------------------------
+-- applyDownFrom
+
+  ∈-applyDownFrom⁺ : ∀ f {i n} → i < n → f i ∈ applyDownFrom f n
+  ∈-applyDownFrom⁺ f = Any.applyDownFrom⁺ f refl
+
+  ∈-applyDownFrom⁻ : ∀ {v} f {n} → v ∈ applyDownFrom f n →
+                     ∃ λ i → i < n × v ≈ f i
+  ∈-applyDownFrom⁻ = Any.applyDownFrom⁻
+
 ------------------------------------------------------------------------
 -- tabulate
 

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

@@ -23,7 +23,7 @@ import Data.List.Relation.Binary.Sublist.Heterogeneous.Core
   as HeterogeneousCore
 import Data.List.Relation.Binary.Sublist.Heterogeneous.Properties
   as HeterogeneousProperties
-open import Data.Product using (∃; ∃₂; _,_; proj₂)
+open import Data.Product using (∃; ∃₂; _×_; _,_; proj₂)
 
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
@@ -35,30 +35,50 @@ open SetoidEquality S
 ------------------------------------------------------------------------
 -- Definition
 
-infix 4 _⊆_ _⊇_ _⊈_ _⊉_
+infix 4 _⊆_ _⊇_ _⊂_ _⊃_ _⊈_ _⊉_ _⊄_ _⊅_
 
 _⊆_ : Rel (List A) (c ⊔ ℓ)
 _⊆_ = Heterogeneous.Sublist _≈_
 
 _⊇_ : Rel (List A) (c ⊔ ℓ)
 xs ⊇ ys = ys ⊆ xs
 
+_⊂_ : Rel (List A) (c ⊔ ℓ)
+xs ⊂ ys = xs ⊆ ys × ¬ (xs ≋ ys)
+
+_⊃_ : Rel (List A) (c ⊔ ℓ)
+xs ⊃ ys = ys ⊂ xs
+
 _⊈_ : Rel (List A) (c ⊔ ℓ)
 xs ⊈ ys = ¬ (xs ⊆ ys)
 
 _⊉_ : Rel (List A) (c ⊔ ℓ)
 xs ⊉ ys = ¬ (xs ⊇ ys)
 
+_⊄_ : Rel (List A) (c ⊔ ℓ)
+xs ⊄ ys = ¬ (xs ⊂ ys)
+
+_⊅_ : Rel (List A) (c ⊔ ℓ)
+xs ⊅ ys = ¬ (xs ⊃ ys)
+
 ------------------------------------------------------------------------
 -- Re-export definitions and operations from heterogeneous sublists
 
-open HeterogeneousCore _≈_ using ([]; _∷_; _∷ʳ_) public
-open Heterogeneous {R = _≈_} hiding (Sublist; []; _∷_; _∷ʳ_) public
+open HeterogeneousCore _≈_ public
+  using ([]; _∷_; _∷ʳ_)
+
+open Heterogeneous {R = _≈_} public
+  hiding (Sublist; []; _∷_; _∷ʳ_)
   renaming
-  (toAny to to∈; fromAny to from∈)
+  ( toAny   to to∈
+  ; fromAny to from∈
+  )
+
+open Disjoint public
+  using ([])
 
-open Disjoint      public using ([])
-open DisjointUnion public using ([])
+open DisjointUnion public
+  using ([])
 
 ------------------------------------------------------------------------
 -- Relational properties holding for Setoid case

src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda

@@ -33,17 +33,17 @@ open import Function.Inverse as Inv using (_↔_; module Inverse)
 open import Function.Equivalence using (module Equivalence)
 open import Level using (Level)
 open import Relation.Nullary using (¬_; yes; no)
-open import Relation.Unary using (Decidable; Pred)
+open import Relation.Unary using (Decidable; Pred) renaming (_⊆_ to _⋐_)
 open import Relation.Binary using (_⇒_; _Respects_)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; _≗_; isEquivalence; subst; refl; setoid; module ≡-Reasoning)
+  using (_≡_; _≗_; isEquivalence; subst; resp; refl; setoid; module ≡-Reasoning)
 import Relation.Binary.Reasoning.Preorder as PreorderReasoning
 
 private
   open module ListMonad {ℓ} = RawMonad (monad {ℓ = ℓ})
 
   variable
-    a b p : Level
+    a b p q : Level
     A : Set a
     B : Set b
     ws xs ys zs : List A
@@ -80,8 +80,8 @@ module _ (A : Set a) where
 ------------------------------------------------------------------------
 -- See issue #1354 for why these proofs can't be taken from `Setoidₚ`
 
-↭⇒⊆ : _↭_ {A = A} ⇒ _⊆_
-↭⇒⊆ xs↭ys = Permutation.∈-resp-↭ xs↭ys
+⊆-reflexive-↭ : _↭_ {A = A} ⇒ _⊆_
+⊆-reflexive-↭ xs↭ys = Permutation.∈-resp-↭ xs↭ys
 
 ⊆-respʳ-↭ : _⊆_ {A = A} Respectsʳ _↭_
 ⊆-respʳ-↭ xs↭ys = Permutation.∈-resp-↭ xs↭ys ∘_
@@ -94,7 +94,7 @@ module _ (A : Set a) where
   ⊆-↭-isPreorder : IsPreorder {A = List A} _↭_ _⊆_
   ⊆-↭-isPreorder = record
     { isEquivalence = ↭-isEquivalence
-    ; reflexive     = ↭⇒⊆
+    ; reflexive     = ⊆-reflexive-↭
     ; trans         = ⊆-trans
     }
 
@@ -231,6 +231,10 @@ module _ {P : Pred A p} (P? : Decidable P) where
   filter-⊆ : ∀ xs → filter P? xs ⊆ xs
   filter-⊆ = Setoidₚ.filter-⊆ (setoid A) P?
 
+  module _ {Q : Pred A q} (Q? : Decidable Q) where
+
+    filter⁺′ : P ⋐ Q → ∀ {xs ys} → xs ⊆ ys → filter P? xs ⊆ filter Q? ys
+    filter⁺′ = Setoidₚ.filter⁺′ (setoid A) P? (resp P) Q? (resp Q)
 
 
 ------------------------------------------------------------------------