Transfer across some proofs to Permutation.Setoid and deprecate Permutation.Inductive (#820)

Author: MatthewDaggitt

CHANGELOG.md

@@ -121,8 +121,9 @@ New modules
   Data.List.Relation.Binary.Disjoint.Setoid
   Data.List.Relation.Binary.Disjoint.Setoid.Properties
 
-  Data.List.Relation.Binary.Permutation.Setoid
   Data.List.Relation.Binary.Permutation.Homogeneous
+  Data.List.Relation.Binary.Permutation.Setoid
+  Data.List.Relation.Binary.Permutation.Setoid.Properties
 
   Data.List.Relation.Unary.AllPairs
   Data.List.Relation.Unary.AllPairs.Properties
@@ -201,6 +202,10 @@ been attached to all deprecated names.
   moved to `Data.Vec.Recursive` to make place for properly heterogeneous
   n-ary products in `Data.Product.Nary`.
 
+* The modules `Data.List.Relation.Binary.Permutation.Inductive(.Properties)`
+  have been renamed `Data.List.Relation.Binary.Permutation.Propositional(.Properties)`
+  to match the rest of the library.
+
 #### Names
 
 * In `Algebra.Properties.BooleanAlgebra`:
@@ -552,11 +557,17 @@ Other minor additions
   foldr-preservesᵒ : (P x ⊎ P y → P (f x y)) → P e ⊎ Any P xs   → P (foldr f e xs)
   ```
 
-* Defined a new utility in `Data.List.Relation.Binary.Permutation.Inductive.Properties`:
+* Added a new proof in `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
   shifts : xs ++ ys ++ zs ↭ ys ++ xs ++ zs
   ```
 
+* Added new proofs to `Data.List.Relation.Binary.Pointwise`:
+  ```agda
+  ++-cancelˡ : Pointwise _∼_ (xs ++ ys) (xs ++ zs) → Pointwise _∼_ ys zs
+  ++-cancelʳ : Pointwise _∼_ (ys ++ xs) (zs ++ xs) → Pointwise _∼_ ys zs
+  ```
+
 * Added new proof to `Data.List.Relation.Binary.Sublist.Heterogeneous.Properties`:
   ```agda
   concat⁺ : Sublist (Sublist R) ass bss → Sublist R (concat ass) (concat bss)
@@ -597,7 +608,7 @@ Other minor additions
   ```agda
   Any-Σ⁺ʳ : (∃ λ x → Any (_~ x) xs) → Any (∃ ∘ _~_) xs
   Any-Σ⁻ʳ : Any (∃ ∘ _~_) xs → ∃ λ x → Any (_~ x) xs
-  gmap : P ⋐ Q ∘ f → Any P ⋐ Any Q ∘ map f
+  gmap    : P ⋐ Q ∘ f → Any P ⋐ Any Q ∘ map f
   ```
 
 * Added new functions to `Data.Maybe.Base`:

src/Data/List/Relation/BagAndSetEquality.agda

@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- This module is DEPRECATED. Please use
--- Data.List.Relation.Unary.Any.Properties directly.
+-- Data.List.Relation.Binary.BagAndSetEquality directly.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}

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

@@ -1,9 +1,13 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Decidable equality over lists using propositional equality
+-- Decidable pointwise equality over lists using propositional equality
 ------------------------------------------------------------------------
 
+-- Note think carefully about using this module as pointwise
+-- propositional equality can usually be replaced with propositional
+-- equality.
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary

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

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Decidable equality over lists parameterised by some setoid
+-- Pointwise decidable equality over lists parameterised by a setoid
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}

src/Data/List/Relation/Binary/Equality/Propositional.agda

@@ -1,9 +1,13 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Equality over lists using propositional equality
+-- Pointwise equality over lists using propositional equality
 ------------------------------------------------------------------------
 
+-- Note think carefully about using this module as pointwise
+-- propositional equality can usually be replaced with propositional
+-- equality.
+
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary
@@ -15,7 +19,7 @@ import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 ------------------------------------------------------------------------
--- Publically re-export everything from setoid equality
+-- Re-export everything from setoid equality
 
 open SetoidEquality (P.setoid A) public
 

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

@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Equality over lists parameterised by some setoid
+-- Pointwise equality over lists parameterised by a setoid
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -10,26 +10,36 @@ open import Relation.Binary using (Setoid)
 
 module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open import Data.List.Base using (List)
+open import Data.Fin
+open import Data.List.Base
+open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
+open import Function using (_∘_)
 open import Level
 open import Relation.Binary renaming (Rel to Rel₂)
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
-open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
+open import Relation.Unary as U using (Pred)
 
 open Setoid S renaming (Carrier to A)
 
+private
+  variable
+    p q : Level
+
 ------------------------------------------------------------------------
 -- Definition of equality
+------------------------------------------------------------------------
 
 infix 4 _≋_
 
 _≋_ : Rel₂ (List A) (a ⊔ ℓ)
 _≋_ = Pointwise _≈_
 
-open Pointwise public using ([]; _∷_)
+open Pointwise public
+  using ([]; _∷_)
 
 ------------------------------------------------------------------------
 -- Relational properties
+------------------------------------------------------------------------
 
 ≋-refl : Reflexive _≋_
 ≋-refl = PW.refl refl
@@ -50,11 +60,68 @@ open Pointwise public using ([]; _∷_)
 ≋-setoid = PW.setoid S
 
 ------------------------------------------------------------------------
--- Operations
+-- List Operations
+------------------------------------------------------------------------
+
+------------------------------------------------------------------------
+-- length
+
+≋-length : ∀ {xs ys} → xs ≋ ys → length xs ≡ length ys
+≋-length = PW.Pointwise-length
+
+------------------------------------------------------------------------
+-- map
+
+module _ {b ℓ₂} (T : Setoid b ℓ₂) where
+
+  open Setoid T using () renaming (_≈_ to _≈′_)
+  private
+    _≋′_ = Pointwise _≈′_
+
+  map⁺ : ∀ {f} → f Preserves _≈_ ⟶ _≈′_ →
+         ∀ {xs ys} → xs ≋ ys → map f xs ≋′ map f ys
+  map⁺ {f} pres xs≋ys = PW.map⁺ f f (PW.map pres xs≋ys)
+
+------------------------------------------------------------------------
+-- _++_
+
+++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
+++⁺ = PW.++⁺
+
+++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
+++-cancelˡ = PW.++-cancelˡ
+
+++-cancelʳ : ∀ {xs} ys zs → ys ++ xs ≋ zs ++ xs → ys ≋ zs
+++-cancelʳ = PW.++-cancelʳ
+
+------------------------------------------------------------------------
+-- concat
+
+concat⁺ : ∀ {xss yss} → Pointwise _≋_ xss yss → concat xss ≋ concat yss
+concat⁺ = PW.concat⁺
+
+------------------------------------------------------------------------
+-- tabulate
+
+tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
+            (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
+tabulate⁺ = PW.tabulate⁺
+
+tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
+            tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
+tabulate⁻ = PW.tabulate⁻
+
+------------------------------------------------------------------------
+-- filter
+
+module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_)
+  where
+
+  filter⁺ : ∀ {xs ys} → xs ≋ ys → filter P? xs ≋ filter P? ys
+  filter⁺ xs≋ys = PW.filter⁺ P? P? resp (resp ∘ sym) xs≋ys
+
+------------------------------------------------------------------------
+-- filter
 
-open PW public using
-  ( tabulate⁺
-  ; tabulate⁻
-  ; ++⁺
-  ; concat⁺
-  )
+reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys
+reverse⁺ = PW.reverse⁺

src/Data/List/Relation/Binary/Permutation/Homogeneous.agda

@@ -17,40 +17,38 @@ private
     a r s : Level
     A : Set a
 
-data Permutation (R : Rel {a} A r) : Rel (List A) (a ⊔ r) where
-  refl : ∀ {xs} → Permutation R xs xs
-  prep : ∀ {xs ys} {x} {x'} (eq : R x x') → Permutation R xs ys →
-               Permutation R (x ∷ xs) (x' ∷ ys)
-  swap : ∀ {xs ys} {x} {y} {x'} {y'} (eq₁ : R x x') (eq₂ : R y y') →
-               Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y' ∷ x' ∷ ys)
+data Permutation {A : Set a} (R : Rel A r) : Rel (List A) (a ⊔ r) where
+  refl  : ∀ {xs} → Permutation R xs xs
+  prep  : ∀ {xs ys x y} (eq : R x y) → Permutation R xs ys → Permutation R (x ∷ xs) (y ∷ ys)
+  swap  : ∀ {xs ys x y x' y'} (eq₁ : R x x') (eq₂ : R y y') → Permutation R xs ys → Permutation R (x ∷ y ∷ xs) (y' ∷ x' ∷ ys)
   trans : ∀ {xs ys zs} → Permutation R xs ys → Permutation R ys zs → Permutation R xs zs
 
 ------------------------------------------------------------------------
 -- The Permutation relation is an equivalence
 
-module _ {R : Rel A r} (R-sym : Symmetric R) where
+module _ {R : Rel A r}  where
 
-  sym : Symmetric (Permutation R)
-  sym refl                   = refl
-  sym (prep x∼x' xs↭ys)      = prep (R-sym x∼x') (sym xs↭ys)
-  sym (swap x∼x' y∼y' xs↭ys) = swap (R-sym y∼y') (R-sym x∼x') (sym xs↭ys)
-  sym (trans xs↭ys ys↭zs)    = trans (sym ys↭zs) (sym xs↭ys)
+  sym : Symmetric R → Symmetric (Permutation R)
+  sym R-sym refl                   = refl
+  sym R-sym (prep x∼x' xs↭ys)      = prep (R-sym x∼x') (sym R-sym xs↭ys)
+  sym R-sym (swap x∼x' y∼y' xs↭ys) = swap (R-sym y∼y') (R-sym x∼x') (sym R-sym xs↭ys)
+  sym R-sym (trans xs↭ys ys↭zs)    = trans (sym R-sym ys↭zs) (sym R-sym xs↭ys)
 
-  isEquivalence : IsEquivalence (Permutation R)
-  isEquivalence = record
+  isEquivalence : Symmetric R → IsEquivalence (Permutation R)
+  isEquivalence R-sym = record
     { refl  = refl
-    ; sym   = sym
+    ; sym   = sym R-sym
     ; trans = trans
     }
 
-  setoid : Setoid _ _
-  setoid = record
-    { isEquivalence = isEquivalence
+  setoid : Symmetric R → Setoid _ _
+  setoid R-sym = record
+    { isEquivalence = isEquivalence R-sym
     }
 
 map : ∀ {R : Rel A r} {S : Rel A s} →
       (R ⇒ S) → (Permutation R ⇒ Permutation S)
-map R⇒S refl = refl
-map R⇒S (prep eq xs∼ys) = prep (R⇒S eq) (map R⇒S xs∼ys)
-map R⇒S (swap eq₁ eq₂ xs∼ys) = swap (R⇒S eq₁) (R⇒S eq₂) (map R⇒S xs∼ys)
-map R⇒S (trans xs∼ys ys∼zs) = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)
+map R⇒S refl                 = refl
+map R⇒S (prep e xs∼ys)       = prep (R⇒S e) (map R⇒S xs∼ys)
+map R⇒S (swap e₁ e₂ xs∼ys)   = swap (R⇒S e₁) (R⇒S e₂) (map R⇒S xs∼ys)
+map R⇒S (trans xs∼ys ys∼zs)  = trans (map R⇒S xs∼ys) (map R⇒S ys∼zs)

src/Data/List/Relation/Binary/Permutation/Inductive.agda

@@ -1,81 +1,12 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- An inductive definition for the permutation relation
+-- This module is DEPRECATED. Please use
+-- Data.List.Relation.Binary.Permutation.Propositional directly.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.List.Relation.Binary.Permutation.Inductive
-  {a} {A : Set a} where
+module Data.List.Relation.Binary.Permutation.Inductive where
 
-open import Data.List using (List; []; _∷_)
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-
-------------------------------------------------------------------------
--- An inductive definition of permutation
-
-infix 3 _↭_
-
-data _↭_ : Rel (List A) a where
-  refl  : ∀ {xs}        → xs ↭ xs
-  prep  : ∀ {xs ys} x   → xs ↭ ys → x ∷ xs ↭ x ∷ ys
-  swap  : ∀ {xs ys} x y → xs ↭ ys → x ∷ y ∷ xs ↭ y ∷ x ∷ ys
-  trans : ∀ {xs ys zs}  → xs ↭ ys → ys ↭ zs → xs ↭ zs
-
-------------------------------------------------------------------------
--- _↭_ is an equivalence
-
-↭-reflexive : _≡_ ⇒ _↭_
-↭-reflexive refl = refl
-
-↭-refl : Reflexive _↭_
-↭-refl = refl
-
-↭-sym : ∀ {xs ys} → xs ↭ ys → ys ↭ xs
-↭-sym refl                = refl
-↭-sym (prep x xs↭ys)      = prep x (↭-sym xs↭ys)
-↭-sym (swap x y xs↭ys)    = swap y x (↭-sym xs↭ys)
-↭-sym (trans xs↭ys ys↭zs) = trans (↭-sym ys↭zs) (↭-sym xs↭ys)
-
-↭-trans : Transitive _↭_
-↭-trans = trans
-
-↭-isEquivalence : IsEquivalence _↭_
-↭-isEquivalence = record
-  { refl  = refl
-  ; sym   = ↭-sym
-  ; trans = trans
-  }
-
-↭-setoid : Setoid _ _
-↭-setoid = record
-  { isEquivalence = ↭-isEquivalence
-  }
-
-------------------------------------------------------------------------
--- A reasoning API to chain permutation proofs and allow "zooming in"
--- to localised reasoning.
-
-module PermutationReasoning where
-
-  open EqReasoning ↭-setoid
-    using (_IsRelatedTo_; relTo)
-
-  open EqReasoning ↭-setoid public
-    using (begin_ ; _∎ ; _≡⟨⟩_; _≡⟨_⟩_)
-    renaming (_≈⟨_⟩_ to _↭⟨_⟩_; _≈˘⟨_⟩_ to _↭˘⟨_⟩_)
-
-  infixr 2 _∷_<⟨_⟩_  _∷_∷_<<⟨_⟩_
-
-  -- Skip reasoning on the first element
-  _∷_<⟨_⟩_ : ∀ x xs {ys zs : List A} → xs ↭ ys →
-               (x ∷ ys) IsRelatedTo zs → (x ∷ xs) IsRelatedTo zs
-  x ∷ xs <⟨ xs↭ys ⟩ rel = relTo (trans (prep x xs↭ys) (begin rel))
-
-  -- Skip reasoning about the first two elements
-  _∷_∷_<<⟨_⟩_ : ∀ x y xs {ys zs : List A} → xs ↭ ys →
-                  (y ∷ x ∷ ys) IsRelatedTo zs → (x ∷ y ∷ xs) IsRelatedTo zs
-  x ∷ y ∷ xs <<⟨ xs↭ys ⟩ rel = relTo (trans (swap x y xs↭ys) (begin rel))
+open import Data.List.Relation.Binary.Permutation.Propositional public