diff --git a/CHANGELOG.md b/CHANGELOG.md index a1f857982a..f21f4a66c3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -159,6 +159,10 @@ New modules * `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`. +* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below. + +* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition. + * `Data.List.Relation.Binary.Prefix.Propositional.Properties` showing the equivalence to left divisibility induced by the list monoid. * `Data.List.Relation.Binary.Suffix.Propositional.Properties` showing the equivalence to right divisibility induced by the list monoid. diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda new file mode 100644 index 0000000000..dc69eb47f6 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda @@ -0,0 +1,150 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A alternative definition for the permutation relation using setoid equality +-- Based on Choudhury and Fiore, "Free Commutative Monoids in HoTT" (MFPS, 2022) +-- Constructor `_⋎_` below is rule (3), directly after the proof of Theorem 6.3, +-- and appears as rule `commrel` of their earlier presentation at (HoTT, 2019), +-- "The finite-multiset construction in HoTT". +-- +-- `Algorithmic` ⊆ `Data.List.Relation.Binary.Permutation.Declarative` +-- but enjoys a much smaller space of derivations, without being so (over-) +-- deterministic as to being inductively defined as the relation generated +-- by swapping the top two elements (the relational analogue of bubble-sort). + +-- In particular, transitivity, `↭-trans` below, is an admissible property. +-- +-- So this relation is 'better' for proving properties of `_↭_`, while at the +-- same time also being a better fit, via `_⋎_`, for the operational features +-- of e.g. sorting algorithms which transpose at arbitary positions. +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Algorithmic + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base using (List; []; _∷_; length) +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (_⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl) + +open Setoid S + renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) + +private + variable + a b c d : A + as bs cs ds : List A + n : ℕ + + +------------------------------------------------------------------------------- +-- Definition + +infix 4 _↭_ +infix 5 _⋎_ _⋎[_]_ + +data _↭_ : List A → List A → Set (s ⊔ ℓ) where + [] : [] ↭ [] + _∷_ : a ≈ b → as ↭ bs → a ∷ as ↭ b ∷ bs + _⋎_ : as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs + +-- smart constructor for prefix congruence + +_≡∷_ : ∀ c → as ↭ bs → c ∷ as ↭ c ∷ bs +_≡∷_ c = ≈-refl ∷_ + +-- pattern synonym to allow naming the 'middle' term +pattern _⋎[_]_ {as} {b} {a} {bs} as↭b∷cs cs a∷cs↭bs + = _⋎_ {as} {b} {cs = cs} {a} {bs} as↭b∷cs a∷cs↭bs + +------------------------------------------------------------------------------- +-- Properties + +↭-reflexive : as ≋ bs → as ↭ bs +↭-reflexive [] = [] +↭-reflexive (a≈b ∷ as↭bs) = a≈b ∷ ↭-reflexive as↭bs + +↭-refl : ∀ as → as ↭ as +↭-refl _ = ↭-reflexive ≋-refl + +↭-sym : as ↭ bs → bs ↭ as +↭-sym [] = [] +↭-sym (a≈b ∷ as↭bs) = ≈-sym a≈b ∷ ↭-sym as↭bs +↭-sym (as↭b∷cs ⋎ a∷cs↭bs) = ↭-sym a∷cs↭bs ⋎ ↭-sym as↭b∷cs + +≋∘↭⇒↭ : as ≋ bs → bs ↭ cs → as ↭ cs +≋∘↭⇒↭ [] [] = [] +≋∘↭⇒↭ (a≈b ∷ as≋bs) (b≈c ∷ bs↭cs) = ≈-trans a≈b b≈c ∷ ≋∘↭⇒↭ as≋bs bs↭cs +≋∘↭⇒↭ (a≈b ∷ as≋bs) (bs↭c∷ds ⋎ b∷ds↭cs) = + ≋∘↭⇒↭ as≋bs bs↭c∷ds ⋎ ≋∘↭⇒↭ (a≈b ∷ ≋-refl) b∷ds↭cs + +↭∘≋⇒↭ : as ↭ bs → bs ≋ cs → as ↭ cs +↭∘≋⇒↭ [] [] = [] +↭∘≋⇒↭ (a≈b ∷ as↭bs) (b≈c ∷ bs≋cs) = ≈-trans a≈b b≈c ∷ ↭∘≋⇒↭ as↭bs bs≋cs +↭∘≋⇒↭ (as↭b∷cs ⋎ a∷cs↭bs) (b≈d ∷ bs≋ds) = + ↭∘≋⇒↭ as↭b∷cs (b≈d ∷ ≋-refl) ⋎ ↭∘≋⇒↭ a∷cs↭bs bs≋ds + +↭-length : as ↭ bs → length as ≡ length bs +↭-length [] = ≡.refl +↭-length (a≈b ∷ as↭bs) = ≡.cong suc (↭-length as↭bs) +↭-length (as↭b∷cs ⋎ a∷cs↭bs) = ≡.cong suc (≡.trans (↭-length as↭b∷cs) (↭-length a∷cs↭bs)) + +↭-trans : as ↭ bs → bs ↭ cs → as ↭ cs +↭-trans = lemma ≡.refl + where + lemma : n ≡ length bs → as ↭ bs → bs ↭ cs → as ↭ cs + +-- easy base case for bs = [], eq: 0 ≡ 0 + lemma _ [] [] = [] + +-- fiddly step case for bs = b ∷ bs, where eq : suc n ≡ suc (length bs) +-- hence suc-injective eq : n ≡ length bs + + lemma {n = suc n} eq (a≈b ∷ as↭bs) (b≈c ∷ bs↭cs) + = ≈-trans a≈b b≈c ∷ lemma (suc-injective eq) as↭bs bs↭cs + + lemma {n = suc n} eq (a≈b ∷ as↭bs) (bs↭c∷ys ⋎ b∷ys↭cs) + = ≋∘↭⇒↭ (a≈b ∷ ≋-refl) (lemma (suc-injective eq) as↭bs bs↭c∷ys ⋎ b∷ys↭cs) + + lemma {n = suc n} eq (as↭b∷xs ⋎ a∷xs↭bs) (a≈b ∷ bs↭cs) + = ↭∘≋⇒↭ (as↭b∷xs ⋎ lemma (suc-injective eq) a∷xs↭bs bs↭cs) (a≈b ∷ ≋-refl) + + lemma {n = suc n} {bs = b ∷ bs} {as = a ∷ as} {cs = c ∷ cs} eq + (as↭b∷xs ⋎[ xs ] a∷xs↭bs) (bs↭c∷ys ⋎[ ys ] b∷ys↭cs) = a∷as↭c∷cs + where + n≡∣bs∣ : n ≡ length bs + n≡∣bs∣ = suc-injective eq + + n≡∣b∷xs∣ : n ≡ length (b ∷ xs) + n≡∣b∷xs∣ = ≡.trans n≡∣bs∣ (≡.sym (↭-length a∷xs↭bs)) + + n≡∣b∷ys∣ : n ≡ length (b ∷ ys) + n≡∣b∷ys∣ = ≡.trans n≡∣bs∣ (↭-length bs↭c∷ys) + + a∷as↭c∷cs : a ∷ as ↭ c ∷ cs + a∷as↭c∷cs with lemma n≡∣bs∣ a∷xs↭bs bs↭c∷ys + ... | a≈c ∷ xs↭ys = a≈c ∷ as↭cs + where + as↭cs : as ↭ cs + as↭cs = lemma n≡∣b∷xs∣ as↭b∷xs + (lemma n≡∣b∷ys∣ (b ≡∷ xs↭ys) b∷ys↭cs) + ... | xs↭c∷zs ⋎[ zs ] a∷zs↭ys + = lemma n≡∣b∷xs∣ as↭b∷xs b∷xs↭c∷b∷zs + ⋎[ b ∷ zs ] + lemma n≡∣b∷ys∣ a∷b∷zs↭b∷ys b∷ys↭cs + where + b∷zs↭b∷zs : b ∷ zs ↭ b ∷ zs + b∷zs↭b∷zs = ↭-refl (b ∷ zs) + b∷xs↭c∷b∷zs : b ∷ xs ↭ c ∷ (b ∷ zs) + b∷xs↭c∷b∷zs = xs↭c∷zs ⋎[ zs ] b∷zs↭b∷zs + a∷b∷zs↭b∷ys : a ∷ (b ∷ zs) ↭ b ∷ ys + a∷b∷zs↭b∷ys = b∷zs↭b∷zs ⋎[ zs ] a∷zs↭ys diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda new file mode 100644 index 0000000000..ff858682f1 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda @@ -0,0 +1,84 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Properties of the `Algorithmic` definition of the permutation relation. +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Algorithmic.Properties + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base using (List; []; _∷_; _++_) +open import Data.List.Properties using (++-identityʳ) +import Relation.Binary.PropositionalEquality as ≡ + using (sym) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (≋-reflexive) +open import Data.List.Relation.Binary.Permutation.Algorithmic S +import Data.List.Relation.Binary.Permutation.Setoid S as ↭ₛ + using (_↭_; refl; prep; swap; trans; ↭-refl; ↭-prep; ↭-swap; ↭-trans) + +open Setoid S + renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) + +private + variable + a b c d : A + as bs cs ds : List A + + +------------------------------------------------------------------------------- +-- Properties + +↭-swap : a ≈ c → b ≈ d → cs ↭ ds → a ∷ b ∷ cs ↭ d ∷ c ∷ ds +↭-swap a≈c b≈d cs≈ds = (b≈d ∷ cs≈ds) ⋎ (a≈c ∷ ↭-refl _) + +↭-swap-++ : (as bs : List A) → as ++ bs ↭ bs ++ as +↭-swap-++ [] bs = ↭-reflexive (≋-reflexive (≡.sym (++-identityʳ bs))) +↭-swap-++ (a ∷ as) bs = lemma bs (↭-swap-++ as bs) + where + lemma : ∀ bs → cs ↭ bs ++ as → a ∷ cs ↭ bs ++ a ∷ as + lemma [] cs↭as + = a ≡∷ cs↭as + lemma (b ∷ bs) (a≈b ∷ cs↭bs++as) + = (a≈b ∷ ↭-refl _) ⋎ lemma bs cs↭bs++as + lemma (b ∷ bs) (cs↭b∷ds ⋎ a∷ds↭bs++as) + = (cs↭b∷ds ⋎ (↭-refl _)) ⋎ (lemma bs a∷ds↭bs++as) + +↭-congʳ : ∀ cs → as ↭ bs → cs ++ as ↭ cs ++ bs +↭-congʳ {as = as} {bs = bs} cs as↭bs = lemma cs + where + lemma : ∀ cs → cs ++ as ↭ cs ++ bs + lemma [] = as↭bs + lemma (c ∷ cs) = c ≡∷ lemma cs + +↭-congˡ : as ↭ bs → ∀ cs → as ++ cs ↭ bs ++ cs +↭-congˡ as↭bs cs = lemma as↭bs + where + lemma : as ↭ bs → as ++ cs ↭ bs ++ cs + lemma [] = ↭-refl cs + lemma (a≈b ∷ as↭bs) = a≈b ∷ lemma as↭bs + lemma (as↭b∷xs ⋎ bs↭a∷xs) = lemma as↭b∷xs ⋎ lemma bs↭a∷xs + +↭-cong : as ↭ bs → cs ↭ ds → as ++ cs ↭ bs ++ ds +↭-cong as↭bs cs↭ds = ↭-trans (↭-congˡ as↭bs _) (↭-congʳ _ cs↭ds) + +------------------------------------------------------------------------------- +-- Equivalence with `Setoid` definition of _↭_ + +↭ₛ⇒↭ : as ↭ₛ.↭ bs → as ↭ bs +↭ₛ⇒↭ (↭ₛ.refl as≋bs) = ↭-reflexive as≋bs +↭ₛ⇒↭ (↭ₛ.prep a≈b as↭bs) = a≈b ∷ ↭ₛ⇒↭ as↭bs +↭ₛ⇒↭ (↭ₛ.swap a≈c b≈d cs↭ds) = ↭-swap a≈c b≈d (↭ₛ⇒↭ cs↭ds) +↭ₛ⇒↭ (↭ₛ.trans as↭bs bs↭cs) = ↭-trans (↭ₛ⇒↭ as↭bs) (↭ₛ⇒↭ bs↭cs) + +↭⇒↭ₛ : as ↭ bs → as ↭ₛ.↭ bs +↭⇒↭ₛ [] = ↭ₛ.↭-refl +↭⇒↭ₛ (a≈b ∷ as↭bs) = ↭ₛ.prep a≈b (↭⇒↭ₛ as↭bs) +↭⇒↭ₛ (as↭b∷cs ⋎ a∷cs↭bs) = ↭ₛ.↭-trans (↭ₛ.↭-prep _ (↭⇒↭ₛ as↭b∷cs)) + (↭ₛ.↭-trans (↭ₛ.↭-swap _ _ ↭ₛ.↭-refl) + (↭ₛ.↭-prep _ (↭⇒↭ₛ a∷cs↭bs))) diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda new file mode 100644 index 0000000000..72eb31cf49 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -0,0 +1,115 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A declarative definition of the permutation relation, inductively defined +-- as the least congruence on `List` which makes `_++_` commutative. Thus, for +-- `(A, _≈_)` a setoid, `List A` with equality given by `_↭_` is a constructive +-- presentation of the free commutative monoid on `A`. +-- +-- NB. we do not need to specify symmetry as a constructor; the rules defining +-- `_↭_` are themselves symmetric, by inspection, whence `↭-sym` below. +-- +-- `_↭_` is somehow the 'maximally non-deterministic' (permissive) presentation +-- of the permutation relation on lists, so is 'easiest' to establish for any +-- given pair of lists, while nevertheless provably equivalent to more +-- operationally defined versions, in particular +-- `Declarative` ⊆ `Data.List.Relation.Binary.Permutation.Algorithmic` +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Declarative + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base using (List; []; _∷_; [_]; _++_) +open import Data.List.Properties using (++-identityʳ) +open import Function.Base using (id; _∘_) +open import Level using (_⊔_) +import Relation.Binary.PropositionalEquality as ≡ using (sym) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl; ≋-reflexive) + +open Setoid S + renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) + +private + variable + a b c d : A + as bs cs ds : List A + + +------------------------------------------------------------------------------- +-- Definition + +infix 4 _↭_ + +data _↭_ : List A → List A → Set (s ⊔ ℓ) where + [] : [] ↭ [] + _∷_ : a ≈ b → as ↭ bs → a ∷ as ↭ b ∷ bs + trans : as ↭ bs → bs ↭ cs → as ↭ cs + _++ᵒ_ : ∀ as bs → as ++ bs ↭ bs ++ as + +-- smart constructor for prefix congruence + +_≡∷_ : ∀ c → as ↭ bs → c ∷ as ↭ c ∷ bs +_≡∷_ c = ≈-refl ∷_ + +------------------------------------------------------------------------------- +-- Basic properties and smart constructors + +↭-reflexive : as ≋ bs → as ↭ bs +↭-reflexive [] = [] +↭-reflexive (a≈b ∷ as↭bs) = a≈b ∷ ↭-reflexive as↭bs + +↭-refl : ∀ as → as ↭ as +↭-refl _ = ↭-reflexive ≋-refl + +↭-sym : as ↭ bs → bs ↭ as +↭-sym [] = [] +↭-sym (a≈b ∷ as↭bs) = ≈-sym a≈b ∷ ↭-sym as↭bs +↭-sym (trans as↭cs cs↭bs) = trans (↭-sym cs↭bs) (↭-sym as↭cs) +↭-sym (as ++ᵒ bs) = bs ++ᵒ as + +-- smart constructor for trans + +↭-trans : as ↭ bs → bs ↭ cs → as ↭ cs +↭-trans [] = id +↭-trans (trans as↭bs bs↭cs) = ↭-trans as↭bs ∘ ↭-trans bs↭cs +↭-trans as↭bs = trans as↭bs + +-- smart constructor for swap + +↭-swap-++ : (as bs : List A) → as ++ bs ↭ bs ++ as +↭-swap-++ [] bs = ↭-reflexive (≋-reflexive (≡.sym (++-identityʳ bs))) +↭-swap-++ as@(_ ∷ _) [] = ↭-reflexive (≋-reflexive (++-identityʳ as)) +↭-swap-++ as@(_ ∷ _) bs@(_ ∷ _) = as ++ᵒ bs + +↭-congʳ : as ↭ bs → cs ++ as ↭ cs ++ bs +↭-congʳ {as = as} {bs = bs} {cs = cs} as↭bs = lemma cs + where + lemma : ∀ cs → cs ++ as ↭ cs ++ bs + lemma [] = as↭bs + lemma (c ∷ cs) = c ≡∷ lemma cs + +↭-congˡ : as ↭ bs → as ++ cs ↭ bs ++ cs +↭-congˡ {as = as} {bs = bs} {cs = cs} as↭bs = + ↭-trans (↭-swap-++ as cs) (↭-trans (↭-congʳ as↭bs) (↭-swap-++ cs bs)) + +↭-cong : as ↭ bs → cs ↭ ds → as ++ cs ↭ bs ++ ds +↭-cong as↭bs cs↭ds = ↭-trans (↭-congˡ as↭bs) (↭-congʳ cs↭ds) + +-- smart constructor for generalised swap + +infix 5 _↭-⋎_ + +_↭-⋎_ : as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs +_↭-⋎_ {b = b} {a = a} as↭b∷cs a∷cs↭bs = + trans (a ≡∷ as↭b∷cs) (↭-trans (↭-congˡ ([ a ] ++ᵒ [ b ])) (b ≡∷ a∷cs↭bs)) + +⋎-syntax : ∀ cs → as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs +⋎-syntax cs = _↭-⋎_ {cs = cs} + +syntax ⋎-syntax cs as↭b∷cs a∷cs↭bs = as↭b∷cs ↭-⋎[ cs ] a∷cs↭bs diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda new file mode 100644 index 0000000000..613633866c --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda @@ -0,0 +1,65 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- Properties of declarative definition of permutation +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Declarative.Properties + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base using (List; []; _∷_; length; _++_) +open import Data.List.Properties using (length-++) +open import Data.Nat.Base using (suc; _+_) +open import Data.Nat.Properties using (+-comm) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + using (module ≡-Reasoning) + +open import Data.List.Relation.Binary.Permutation.Algorithmic S + using ([]; _∷_; _⋎_) + renaming (_↭_ to _↭ₐ_; ↭-trans to ↭ₐ-trans) +open import Data.List.Relation.Binary.Permutation.Algorithmic.Properties S + using () + renaming (↭-swap-++ to ↭ₐ-swap-++) +open import Data.List.Relation.Binary.Permutation.Declarative S + +open Setoid S + using () + renaming (Carrier to A) + +private + variable + as bs : List A + + +------------------------------------------------------------------------------- +-- Properties + +↭-length : as ↭ bs → length as ≡ length bs +↭-length [] = ≡.refl +↭-length (a≈b ∷ as↭bs) = ≡.cong suc (↭-length as↭bs) +↭-length (trans as↭cs cs↭bs) = ≡.trans (↭-length as↭cs) (↭-length cs↭bs) +↭-length (as ++ᵒ bs) = begin + length (as ++ bs) ≡⟨ length-++ as ⟩ + length as + length bs ≡⟨ +-comm (length as) (length bs) ⟩ + length bs + length as ≡⟨ length-++ bs ⟨ + length (bs ++ as) ∎ + where open ≡-Reasoning + +------------------------------------------------------------------------------- +-- Equivalence with `Algorithmic` definition of _↭_ + +↭ₐ⇒↭ : as ↭ₐ bs → as ↭ bs +↭ₐ⇒↭ [] = [] +↭ₐ⇒↭ (a≈b ∷ as↭bs) = a≈b ∷ ↭ₐ⇒↭ as↭bs +↭ₐ⇒↭ (as↭b∷cs ⋎ a∷cs↭bs) = ↭ₐ⇒↭ as↭b∷cs ↭-⋎ ↭ₐ⇒↭ a∷cs↭bs + +↭⇒↭ₐ : as ↭ bs → as ↭ₐ bs +↭⇒↭ₐ [] = [] +↭⇒↭ₐ (a≈b ∷ as↭bs) = a≈b ∷ ↭⇒↭ₐ as↭bs +↭⇒↭ₐ (trans as↭cs cs↭bs) = ↭ₐ-trans (↭⇒↭ₐ as↭cs) (↭⇒↭ₐ cs↭bs) +↭⇒↭ₐ (as ++ᵒ bs) = ↭ₐ-swap-++ as bs