From 96f9e134fce1188bb80874b7d3b56c54dbe73a00 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 2 Jun 2025 21:05:52 +0100 Subject: [PATCH 01/19] [ add ] Hinze's definition of `Permutation` for `Setoid`s --- .../Relation/Binary/Permutation/Hinze.agda | 185 ++++++++++++++++++ 1 file changed, 185 insertions(+) create mode 100644 src/Data/List/Relation/Binary/Permutation/Hinze.agda diff --git a/src/Data/List/Relation/Binary/Permutation/Hinze.agda b/src/Data/List/Relation/Binary/Permutation/Hinze.agda new file mode 100644 index 0000000000..113c5312f8 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Hinze.agda @@ -0,0 +1,185 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A alternative definition for the permutation relation using setoid equality +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Hinze {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl) +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 + 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 + +∼-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 + +∼-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 rewrite ++-identityʳ bs = ∼-refl 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) + +∼-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 + +∼-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From 3c133cafc0a36ea70d0866701fab30a5fcc0abdb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 2 Jun 2025 21:41:50 +0100 Subject: [PATCH 02/19] fix: `dos2unix` --- .../Relation/Binary/Permutation/Hinze.agda | 370 +++++++++--------- 1 file changed, 185 insertions(+), 185 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Hinze.agda b/src/Data/List/Relation/Binary/Permutation/Hinze.agda index 113c5312f8..9d6b5b7feb 100644 --- a/src/Data/List/Relation/Binary/Permutation/Hinze.agda +++ b/src/Data/List/Relation/Binary/Permutation/Hinze.agda @@ -1,185 +1,185 @@ -------------------------------------------------------------------------------- --- The Agda standard library --- --- A alternative definition for the permutation relation using setoid equality -------------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Relation.Binary.Bundles using (Setoid) - -module Hinze {s ℓ} (S : Setoid s ℓ) where - -open import Data.List.Base -open import Data.List.Properties using (++-identityʳ) -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Nat.Properties using (suc-injective) -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open import Data.List.Relation.Binary.Equality.Setoid S as ≋ - using (_≋_; []; _∷_; ≋-refl) -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-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 - 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 - -∼-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 - -∼-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 rewrite ++-identityʳ bs = ∼-refl 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) - -∼-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 - -∼-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 _↭_ - -↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) - (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A alternative definition for the permutation relation using setoid equality +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Hinze {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl) +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 + 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 + +∼-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 + +∼-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 rewrite ++-identityʳ bs = ∼-refl 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) + +∼-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 + +∼-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From 18f112cce37865a9988656ac4231d5084b1b386c Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 3 Jun 2025 06:01:11 +0100 Subject: [PATCH 03/19] fix: module name --- .../Relation/Binary/Permutation/Hinze.agda | 371 +++++++++--------- 1 file changed, 186 insertions(+), 185 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Hinze.agda b/src/Data/List/Relation/Binary/Permutation/Hinze.agda index 9d6b5b7feb..62c8c2bb26 100644 --- a/src/Data/List/Relation/Binary/Permutation/Hinze.agda +++ b/src/Data/List/Relation/Binary/Permutation/Hinze.agda @@ -1,185 +1,186 @@ -------------------------------------------------------------------------------- --- The Agda standard library --- --- A alternative definition for the permutation relation using setoid equality -------------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Relation.Binary.Bundles using (Setoid) - -module Hinze {s ℓ} (S : Setoid s ℓ) where - -open import Data.List.Base -open import Data.List.Properties using (++-identityʳ) -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Nat.Properties using (suc-injective) -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open import Data.List.Relation.Binary.Equality.Setoid S as ≋ - using (_≋_; []; _∷_; ≋-refl) -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-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 - 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 - -∼-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 - -∼-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 rewrite ++-identityʳ bs = ∼-refl 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) - -∼-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 - -∼-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 _↭_ - -↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) - (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A alternative definition for the permutation relation using setoid equality +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Hinze + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl) +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 + 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 + +∼-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 + +∼-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 rewrite ++-identityʳ bs = ∼-refl 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) + +∼-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 + +∼-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From c4b106996f25ef2cec050ac755480d2e87ef2072 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Tue, 3 Jun 2025 06:12:23 +0100 Subject: [PATCH 04/19] fix: `dos2unix` --- .../Relation/Binary/Permutation/Hinze.agda | 372 +++++++++--------- 1 file changed, 186 insertions(+), 186 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Hinze.agda b/src/Data/List/Relation/Binary/Permutation/Hinze.agda index 62c8c2bb26..c6ca72e261 100644 --- a/src/Data/List/Relation/Binary/Permutation/Hinze.agda +++ b/src/Data/List/Relation/Binary/Permutation/Hinze.agda @@ -1,186 +1,186 @@ -------------------------------------------------------------------------------- --- The Agda standard library --- --- A alternative definition for the permutation relation using setoid equality -------------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Relation.Binary.Bundles using (Setoid) - -module Data.List.Relation.Binary.Permutation.Hinze - {s ℓ} (S : Setoid s ℓ) where - -open import Data.List.Base -open import Data.List.Properties using (++-identityʳ) -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Nat.Properties using (suc-injective) -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open import Data.List.Relation.Binary.Equality.Setoid S as ≋ - using (_≋_; []; _∷_; ≋-refl) -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-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 - 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 - -∼-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 - -∼-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 rewrite ++-identityʳ bs = ∼-refl 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) - -∼-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 - -∼-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 _↭_ - -↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) - (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A alternative definition for the permutation relation using setoid equality +------------------------------------------------------------------------------- + +{-# OPTIONS --cubical-compatible --safe #-} + +open import Relation.Binary.Bundles using (Setoid) + +module Data.List.Relation.Binary.Permutation.Hinze + {s ℓ} (S : Setoid s ℓ) where + +open import Data.List.Base +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl) +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 + 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 + +∼-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 + +∼-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 rewrite ++-identityʳ bs = ∼-refl 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) + +∼-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 + +∼-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From 51c98f8c8c0cc917c14ab94014092d240889b142 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 09:29:02 +0100 Subject: [PATCH 05/19] fix: attribution, and module name --- .../Binary/Permutation/{Hinze.agda => ChowdhuryFiore.agda} | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) rename src/Data/List/Relation/Binary/Permutation/{Hinze.agda => ChowdhuryFiore.agda} (97%) diff --git a/src/Data/List/Relation/Binary/Permutation/Hinze.agda b/src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda similarity index 97% rename from src/Data/List/Relation/Binary/Permutation/Hinze.agda rename to src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda index c6ca72e261..22ca66362a 100644 --- a/src/Data/List/Relation/Binary/Permutation/Hinze.agda +++ b/src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda @@ -2,13 +2,15 @@ -- 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) +-- (`_⋎_` below is rule (3) on p.12, directly after the proof of Theorem 6.3) ------------------------------------------------------------------------------- {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Bundles using (Setoid) -module Data.List.Relation.Binary.Permutation.Hinze +module Data.List.Relation.Binary.Permutation.ChowdhuryFiore {s ℓ} (S : Setoid s ℓ) where open import Data.List.Base From c8e42a0f380e656d1cab437284b3375a1a5079ed Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 09:52:17 +0100 Subject: [PATCH 06/19] fix: attribution, and module name, one more time; also remove `rewrite` --- .../Binary/Permutation/ChowdhuryFiore.agda | 188 ------------------ 1 file changed, 188 deletions(-) delete mode 100644 src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda diff --git a/src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda b/src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda deleted file mode 100644 index 22ca66362a..0000000000 --- a/src/Data/List/Relation/Binary/Permutation/ChowdhuryFiore.agda +++ /dev/null @@ -1,188 +0,0 @@ -------------------------------------------------------------------------------- --- 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) --- (`_⋎_` below is rule (3) on p.12, directly after the proof of Theorem 6.3) -------------------------------------------------------------------------------- - -{-# OPTIONS --cubical-compatible --safe #-} - -open import Relation.Binary.Bundles using (Setoid) - -module Data.List.Relation.Binary.Permutation.ChowdhuryFiore - {s ℓ} (S : Setoid s ℓ) where - -open import Data.List.Base -open import Data.List.Properties using (++-identityʳ) -open import Data.Nat.Base using (ℕ; zero; suc) -open import Data.Nat.Properties using (suc-injective) -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) - -open import Data.List.Relation.Binary.Equality.Setoid S as ≋ - using (_≋_; []; _∷_; ≋-refl) -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-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 - 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 - -∼-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 - -∼-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 rewrite ++-identityʳ bs = ∼-refl 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) - -∼-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 - -∼-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 _↭_ - -↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) - (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From 50922beaba8c238d738cf4f3e854f81c78e2c7ee Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 12:10:54 +0100 Subject: [PATCH 07/19] fix: restore new module, with new name --- .../Binary/Permutation/Algorithmic.agda | 190 ++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 src/Data/List/Relation/Binary/Permutation/Algorithmic.agda 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..e800d31cd9 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda @@ -0,0 +1,190 @@ +------------------------------------------------------------------------------- +-- 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". +------------------------------------------------------------------------------- + +{-# 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 +open import Data.List.Properties using (++-identityʳ) +open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Properties using (suc-injective) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl; ≋-reflexive) +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 + 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 + +∼-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 + +∼-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) + +∼-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 + +∼-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From c68166ddbea1ecca7574d7a497bad6700c777d4e Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 19:10:45 +0100 Subject: [PATCH 08/19] add: `Declarative` definition and properties --- .../Binary/Permutation/Declarative.agda | 123 ++++++++++++++++++ 1 file changed, 123 insertions(+) create mode 100644 src/Data/List/Relation/Binary/Permutation/Declarative.agda 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..7b97e8e869 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -0,0 +1,123 @@ +------------------------------------------------------------------------------- +-- The Agda standard library +-- +-- A declarative definition of the permutation relation +------------------------------------------------------------------------------- + +{-# 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 +open import Data.List.Properties using (++-identityʳ; length-++) +open import Data.Nat.Base using (ℕ; zero; suc; _+_) +open import Data.Nat.Properties using (suc-injective; +-comm) +open import Level using (Level; _⊔_) +open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) +open import Relation.Binary.PropositionalEquality.Properties as ≡ + using (module ≡-Reasoning) + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using (_≋_; []; _∷_; ≋-refl; ≋-reflexive) +open import Data.List.Relation.Binary.Permutation.Algorithmic S + using ([]; _∷_; _⋎_) + renaming (_∼_ to _∼ₐ_; ∼-trans to ∼ₐ-trans; ∼-swap-++ to ∼ₐ-swap-++) + +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 _∼_ + +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 prefx congruence + +_≡∷_ : ∀ c → as ∼ bs → c ∷ as ∼ c ∷ bs +_≡∷_ c = ≈-refl ∷_ + + +------------------------------------------------------------------------------- +-- 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 (trans as∼cs cs∼bs) = trans (∼-sym cs∼bs) (∼-sym as∼cs) +∼-sym (as ++ᵒ bs) = bs ++ᵒ as + +∼-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 as ≡⟨ length-++ bs ⟨ + length (bs ++ as) ∎ + where open ≡-Reasoning + +∼-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 = as} {bs = bs} as∼bs cs = + trans (as ++ᵒ cs) (trans (∼-congʳ _ as∼bs) (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} {cs = cs} {a = a} as∼b∷cs a∷cs∼bs = + trans (a ≡∷ as∼b∷cs) (trans (∼-congˡ ([ a ] ++ᵒ [ b ]) cs) (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 + + +------------------------------------------------------------------------------- +-- 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 From 37999b501ab3168c6c23b637a44593a9bbae08cb Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 19:13:41 +0100 Subject: [PATCH 09/19] fix: whitespace --- src/Data/List/Relation/Binary/Permutation/Declarative.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda index 7b97e8e869..1793f36c33 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -1,7 +1,7 @@ ------------------------------------------------------------------------------- -- The Agda standard library -- --- A declarative definition of the permutation relation +-- A declarative definition of the permutation relation ------------------------------------------------------------------------------- {-# OPTIONS --cubical-compatible --safe #-} From 678f7e098e9dd410bdfc4d62fb0727a4c11bb316 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 5 Jun 2025 19:20:37 +0100 Subject: [PATCH 10/19] fix: tweaks --- src/Data/List/Relation/Binary/Permutation/Declarative.agda | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda index 1793f36c33..de9ed8f41f 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -1,7 +1,8 @@ ------------------------------------------------------------------------------- -- The Agda standard library -- --- A declarative definition of the permutation relation +-- A declarative definition of the permutation relation, +-- as the least congruence making `_++_` commutative ------------------------------------------------------------------------------- {-# OPTIONS --cubical-compatible --safe #-} @@ -47,7 +48,7 @@ data _∼_ : List A → List A → Set (s ⊔ ℓ) where trans : as ∼ bs → bs ∼ cs → as ∼ cs _++ᵒ_ : ∀ as bs → as ++ bs ∼ bs ++ as --- smart constructor for prefx congruence +-- smart constructor for prefix congruence _≡∷_ : ∀ c → as ∼ bs → c ∷ as ∼ c ∷ bs _≡∷_ c = ≈-refl ∷_ From 705bee4b00a9e81dd7c7b43a24965cb717427ba1 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 6 Jun 2025 09:37:17 +0100 Subject: [PATCH 11/19] refactor: `Declarative` into definitions and properties --- .../Binary/Permutation/Declarative.agda | 76 +++++++------------ .../Permutation/Declarative/Properties.agda | 62 +++++++++++++++ 2 files changed, 90 insertions(+), 48 deletions(-) create mode 100644 src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda index de9ed8f41f..757eea9761 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -12,20 +12,14 @@ open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Binary.Permutation.Declarative {s ℓ} (S : Setoid s ℓ) where -open import Data.List.Base -open import Data.List.Properties using (++-identityʳ; length-++) -open import Data.Nat.Base using (ℕ; zero; suc; _+_) -open import Data.Nat.Properties using (suc-injective; +-comm) -open import Level using (Level; _⊔_) -open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) -open import Relation.Binary.PropositionalEquality.Properties as ≡ - using (module ≡-Reasoning) +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 import Data.List.Relation.Binary.Permutation.Algorithmic S - using ([]; _∷_; _⋎_) - renaming (_∼_ to _∼ₐ_; ∼-trans to ∼ₐ-trans; ∼-swap-++ to ∼ₐ-swap-++) open Setoid S renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) @@ -34,7 +28,6 @@ private variable a b c d : A as bs cs ds : List A - n : ℕ ------------------------------------------------------------------------------- @@ -53,9 +46,8 @@ data _∼_ : List A → List A → Set (s ⊔ ℓ) where _≡∷_ : ∀ c → as ∼ bs → c ∷ as ∼ c ∷ bs _≡∷_ c = ≈-refl ∷_ - ------------------------------------------------------------------------------- --- Properties +-- Basic properties and smart constructors ∼-reflexive : as ≋ bs → as ∼ bs ∼-reflexive [] = [] @@ -70,55 +62,43 @@ _≡∷_ c = ≈-refl ∷_ ∼-sym (trans as∼cs cs∼bs) = trans (∼-sym cs∼bs) (∼-sym as∼cs) ∼-sym (as ++ᵒ bs) = bs ++ᵒ as -∼-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 as ≡⟨ length-++ bs ⟨ - length (bs ++ as) ∎ - where open ≡-Reasoning - -∼-congʳ : ∀ cs → as ∼ bs → cs ++ as ∼ cs ++ bs -∼-congʳ {as = as} {bs = bs} cs as∼bs = lemma cs +-- 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 → ∀ cs → as ++ cs ∼ bs ++ cs -∼-congˡ {as = as} {bs = bs} as∼bs cs = - trans (as ++ᵒ cs) (trans (∼-congʳ _ as∼bs) (cs ++ᵒ bs)) +∼-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) +∼-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} {cs = cs} {a = a} as∼b∷cs a∷cs∼bs = - trans (a ≡∷ as∼b∷cs) (trans (∼-congˡ ([ a ] ++ᵒ [ b ]) cs) (b ≡∷ a∷cs∼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 - - -------------------------------------------------------------------------------- --- 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 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..0d28e8d4cb --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda @@ -0,0 +1,62 @@ +------------------------------------------------------------------------------- +-- 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; ∼-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 From a4560f6db7b3e2d1944a4bd0fc072fd3af3008ba Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 6 Jun 2025 10:21:53 +0100 Subject: [PATCH 12/19] refactor: `Algorithmic` into definitions and properties --- .../Binary/Permutation/Algorithmic.agda | 59 +------------ .../Permutation/Algorithmic/Properties.agda | 83 +++++++++++++++++++ 2 files changed, 87 insertions(+), 55 deletions(-) create mode 100644 src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda index e800d31cd9..eb87182709 100644 --- a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda @@ -15,17 +15,15 @@ open import Relation.Binary.Bundles using (Setoid) module Data.List.Relation.Binary.Permutation.Algorithmic {s ℓ} (S : Setoid s ℓ) where -open import Data.List.Base +open import Data.List.Base using (List; []; _∷_; length) open import Data.List.Properties using (++-identityʳ) -open import Data.Nat.Base using (ℕ; zero; suc) +open import Data.Nat.Base using (ℕ; suc) open import Data.Nat.Properties using (suc-injective) -open import Level using (Level; _⊔_) +open import Level using (_⊔_) open import Relation.Binary.PropositionalEquality as ≡ using (_≡_) open import Data.List.Relation.Binary.Equality.Setoid S as ≋ - using (_≋_; []; _∷_; ≋-refl; ≋-reflexive) -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-swap; ↭-trans) + using (_≋_; []; _∷_; ≋-refl) open Setoid S renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) @@ -84,36 +82,6 @@ pattern _⋎[_]_ {as} {b} {a} {bs} as∼b∷cs cs a∷cs∼bs ∼∘≋⇒∼ (as∼b∷cs ⋎ a∷cs∼bs) (b≈d ∷ bs≋ds) = ∼∘≋⇒∼ as∼b∷cs (b≈d ∷ ≋-refl) ⋎ ∼∘≋⇒∼ a∷cs∼bs bs≋ds -∼-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 - -∼-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) - ∼-length : as ∼ bs → length as ≡ length bs ∼-length [] = ≡.refl ∼-length (a≈b ∷ as∼bs) = ≡.cong suc (∼-length as∼bs) @@ -169,22 +137,3 @@ pattern _⋎[_]_ {as} {b} {a} {bs} as∼b∷cs cs a∷cs∼bs 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 - -∼-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 _↭_ - -↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) - (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) 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..4d835e0753 --- /dev/null +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda @@ -0,0 +1,83 @@ +------------------------------------------------------------------------------- +-- 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 ≡ + +open import Data.List.Relation.Binary.Equality.Setoid S as ≋ + using ([]; ≋-reflexive) +open import Data.List.Relation.Binary.Permutation.Algorithmic S +open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ + using (_↭_; ↭-refl; ↭-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 _↭_ + +↭⇒∼ : 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 ≈-refl (∼⇒↭ as∼b∷cs)) + (↭-trans (↭-swap _ _ ↭-refl) + (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) From a240e9c3568cb12c3250cba6cb1b54d5f92417f4 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 6 Jun 2025 11:09:26 +0100 Subject: [PATCH 13/19] fix: `import`s --- .../Binary/Permutation/Algorithmic/Properties.agda | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda index 4d835e0753..883bc4b813 100644 --- a/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda @@ -14,12 +14,13 @@ module Data.List.Relation.Binary.Permutation.Algorithmic.Properties 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) + using (≋-reflexive) open import Data.List.Relation.Binary.Permutation.Algorithmic S open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-swap; ↭-trans) + using (_↭_; ↭-refl; ↭-prep; ↭-swap; ↭-trans) open Setoid S renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans) @@ -76,8 +77,8 @@ private ↭⇒∼ (↭.trans as∼bs bs∼cs) = ∼-trans (↭⇒∼ as∼bs) (↭⇒∼ bs∼cs) ∼⇒↭ : as ∼ bs → as ↭ bs -∼⇒↭ [] = ↭.refl [] +∼⇒↭ [] = ↭.↭-refl ∼⇒↭ (a≈b ∷ as∼bs) = ↭.prep a≈b (∼⇒↭ as∼bs) -∼⇒↭ (as∼b∷cs ⋎ a∷cs∼bs) = ↭-trans (↭.prep ≈-refl (∼⇒↭ as∼b∷cs)) +∼⇒↭ (as∼b∷cs ⋎ a∷cs∼bs) = ↭-trans (↭-prep _ (∼⇒↭ as∼b∷cs)) (↭-trans (↭-swap _ _ ↭-refl) - (↭.prep ≈-refl (∼⇒↭ a∷cs∼bs))) + (↭-prep _ (∼⇒↭ a∷cs∼bs))) From e4905d56f0749fd8bcfb9b950115da5117df91cf Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Fri, 6 Jun 2025 11:32:00 +0100 Subject: [PATCH 14/19] fix: knock-ons --- .../Relation/Binary/Permutation/Declarative/Properties.agda | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda index 0d28e8d4cb..962581e821 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda @@ -21,7 +21,10 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Data.List.Relation.Binary.Permutation.Algorithmic S using ([]; _∷_; _⋎_) - renaming (_∼_ to _∼ₐ_; ∼-trans to ∼ₐ-trans; ∼-swap-++ to ∼ₐ-swap-++) + 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 From e9dbd97c921433bba66ed85b1b24705b360f8a11 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Sun, 29 Jun 2025 08:56:11 +0100 Subject: [PATCH 15/19] fix: added more commentary/explanation --- .../Relation/Binary/Permutation/Algorithmic.agda | 11 +++++++++++ .../Relation/Binary/Permutation/Declarative.agda | 15 +++++++++++++-- 2 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda index eb87182709..54c3b28c6f 100644 --- a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda @@ -6,6 +6,17 @@ -- 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 #-} diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda index 757eea9761..6344eefdd4 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -1,8 +1,19 @@ ------------------------------------------------------------------------------- -- The Agda standard library -- --- A declarative definition of the permutation relation, --- as the least congruence making `_++_` commutative +-- 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 #-} From b3eef5d3ba7ddfaf24fa16e6672a6f97f649dc95 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:39:02 +0100 Subject: [PATCH 16/19] add: new modules to `CHANGELOG` --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) 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. From 4d51459e8c8346555a8066c79f12db011ad1843d Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:39:27 +0100 Subject: [PATCH 17/19] fix: notation --- .../Binary/Permutation/Algorithmic.agda | 132 +++++++++--------- .../Permutation/Algorithmic/Properties.agda | 82 +++++------ 2 files changed, 107 insertions(+), 107 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda index 54c3b28c6f..dc69eb47f6 100644 --- a/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic.agda @@ -12,9 +12,9 @@ -- 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. +-- In particular, transitivity, `↭-trans` below, is an admissible property. -- --- So this relation is 'better' for proving properties of `_∼_`, while at the +-- 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. ------------------------------------------------------------------------------- @@ -49,59 +49,59 @@ private ------------------------------------------------------------------------------- -- Definition -infix 4 _∼_ +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 +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 → 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 +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 +↭-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 + lemma : n ≡ length bs → as ↭ bs → bs ↭ cs → as ↭ cs -- easy base case for bs = [], eq: 0 ≡ 0 lemma _ [] [] = [] @@ -109,42 +109,42 @@ pattern _⋎[_]_ {as} {b} {a} {bs} as∼b∷cs cs a∷cs∼bs -- 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) (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 (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} 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 + (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∷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) + 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 + 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 + 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 + 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 + 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 index 883bc4b813..ff858682f1 100644 --- a/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda @@ -19,8 +19,8 @@ import Relation.Binary.PropositionalEquality as ≡ open import Data.List.Relation.Binary.Equality.Setoid S as ≋ using (≋-reflexive) open import Data.List.Relation.Binary.Permutation.Algorithmic S -open import Data.List.Relation.Binary.Permutation.Setoid S as ↭ - using (_↭_; ↭-refl; ↭-prep; ↭-swap; ↭-trans) +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) @@ -34,51 +34,51 @@ private ------------------------------------------------------------------------------- -- 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 : 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) +↭-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 + 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 : ∀ 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 +↭-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 + 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) +↭-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 _↭_ - -↭⇒∼ : 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))) +-- 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))) From a1f50fa5008c985aa2f62ac0b58da1d3baf10c52 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Thu, 3 Jul 2025 08:41:35 +0100 Subject: [PATCH 18/19] fix: notation --- .../Binary/Permutation/Declarative.agda | 88 +++++++++---------- .../Permutation/Declarative/Properties.agda | 34 +++---- 2 files changed, 61 insertions(+), 61 deletions(-) diff --git a/src/Data/List/Relation/Binary/Permutation/Declarative.agda b/src/Data/List/Relation/Binary/Permutation/Declarative.agda index 6344eefdd4..72eb31cf49 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative.agda @@ -3,13 +3,13 @@ -- -- 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 +-- `(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. +-- `_↭_` are themselves symmetric, by inspection, whence `↭-sym` below. -- --- `_∼_` is somehow the 'maximally non-deterministic' (permissive) presentation +-- `_↭_` 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 @@ -44,72 +44,72 @@ private ------------------------------------------------------------------------------- -- Definition -infix 4 _∼_ +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 +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 → 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 +↭-reflexive : as ≋ bs → as ↭ bs +↭-reflexive [] = [] +↭-reflexive (a≈b ∷ as↭bs) = a≈b ∷ ↭-reflexive as↭bs -∼-refl : ∀ as → as ∼ as -∼-refl _ = ∼-reflexive ≋-refl +↭-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 +↭-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 +↭-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 +↭-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 +↭-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 : ∀ 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 → 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) +↭-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 _∼-⋎_ +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)) +_↭-⋎_ : 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 : ∀ 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 +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 index 962581e821..613633866c 100644 --- a/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda +++ b/src/Data/List/Relation/Binary/Permutation/Declarative/Properties.agda @@ -21,10 +21,10 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡ open import Data.List.Relation.Binary.Permutation.Algorithmic S using ([]; _∷_; _⋎_) - renaming (_∼_ to _∼ₐ_; ∼-trans to ∼ₐ-trans) + renaming (_↭_ to _↭ₐ_; ↭-trans to ↭ₐ-trans) open import Data.List.Relation.Binary.Permutation.Algorithmic.Properties S using () - renaming (∼-swap-++ to ∼ₐ-swap-++) + renaming (↭-swap-++ to ↭ₐ-swap-++) open import Data.List.Relation.Binary.Permutation.Declarative S open Setoid S @@ -39,11 +39,11 @@ private ------------------------------------------------------------------------------- -- 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 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 ⟨ @@ -51,15 +51,15 @@ private where open ≡-Reasoning ------------------------------------------------------------------------------- --- Equivalence with `Algorithmic` definition of _∼_ +-- 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 +↭ₐ⇒↭ (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 +↭⇒↭ₐ : 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 From 1089a933d9c13b14968a396a1146f7b2d151b21b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 21 Jul 2025 21:27:49 +0100 Subject: [PATCH 19/19] fix: `CHANGELOG` --- CHANGELOG.md | 530 +-------------------------------------------------- 1 file changed, 2 insertions(+), 528 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c4628a726..99117f9617 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,7 +1,7 @@ -Version 2.3-dev +Version 2.4-dev =============== -The library has been tested using Agda 2.7.0 and 2.7.0.1. +The library has been tested using Agda 2.8.0. Highlights ---------- @@ -9,550 +9,24 @@ Highlights Bug-fixes --------- -* In `Algebra.Apartness.Structures`, renamed `sym` from `IsApartnessRelation` - to `#-sym` in order to avoid overloaded projection. - `irrefl` and `cotrans` are similarly renamed for the sake of consistency. - -* In `Algebra.Definitions.RawMagma` and `Relation.Binary.Construct.Interior.Symmetric`, - the record constructors `_,_` incorrectly had no declared fixity. They have been given - the fixity `infixr 4 _,_`, consistent with that of `Data.Product.Base`. - -* In `Data.Product.Function.Dependent.Setoid`, `left-inverse` defined a - `RightInverse`. - This has been deprecated in favor or `rightInverse`, and a corrected (and - correctly-named) function `leftInverse` has been added. - -* The implementation of `_IsRelatedTo_` in `Relation.Binary.Reasoning.Base.Partial` - has been modified to correctly support equational reasoning at the beginning and the end. - The detail of this issue is described in [#2677](https://github.com/agda/agda-stdlib/pull/2677). Since the names of constructors - of `_IsRelatedTo_` are changed and the reduction behaviour of reasoning steps - are changed, this modification is non-backwards compatible. - Non-backwards compatible changes -------------------------------- -* The implementation of `≤-total` in `Data.Nat.Properties` has been altered - to use operations backed by primitives, rather than recursion, making it - significantly faster. However, its reduction behaviour on open terms may have - changed. - Minor improvements ------------------ -* Moved the concept `Irrelevant` of irrelevance (h-proposition) from `Relation.Nullary` - to its own dedicated module `Relation.Nullary.Irrelevant`. - Deprecated modules ------------------ Deprecated names ---------------- -* In `Algebra.Definitions.RawMagma`: - ```agda - _∣∣_ ↦ _∥_ - _∤∤_ ↦ _∦_ - ``` - -* In `Algebra.Lattice.Properties.BooleanAlgebra` - ```agda - ⊥≉⊤ ↦ ¬⊥≈⊤ - ⊤≉⊥ ↦ ¬⊤≈⊥ - ``` - -* In `Algebra.Module.Consequences` - ```agda - *ₗ-assoc+comm⇒*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ᵣ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - *ᵣ-assoc+comm⇒*ₗ-assoc ↦ *ᵣ-assoc∧comm⇒*ₗ-assoc - *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc - ``` - -* In `Algebra.Modules.Structures.IsLeftModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Modules.Structures.IsRightModule`: - ```agda - uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ - uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣∣-sym ↦ ∥-sym - ∣∣-respˡ-≈ ↦ ∥-respˡ-≈ - ∣∣-respʳ-≈ ↦ ∥-respʳ-≈ - ∣∣-resp-≈ ↦ ∥-resp-≈ - ∤∤-sym -≈ ↦ ∦-sym - ∤∤-respˡ-≈ ↦ ∦-respˡ-≈ - ∤∤-respʳ-≈ ↦ ∦-respʳ-≈ - ∤∤-resp-≈ ↦ ∦-resp-≈ - ∣-respʳ-≈ ↦ ∣ʳ-respʳ-≈ - ∣-respˡ-≈ ↦ ∣ʳ-respˡ-≈ - ∣-resp-≈ ↦ ∣ʳ-resp-≈ - x∣yx ↦ x∣ʳyx - xy≈z⇒y∣z ↦ xy≈z⇒y∣ʳz - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ∣∣-refl ↦ ∥-refl - ∣∣-reflexive ↦ ∥-reflexive - ∣∣-isEquivalence ↦ ∥-isEquivalence - ε∣_ ↦ ε∣ʳ_ - ∣-refl ↦ ∣ʳ-refl - ∣-reflexive ↦ ∣ʳ-reflexive - ∣-isPreorder ↦ ∣ʳ-isPreorder - ∣-preorder ↦ ∣ʳ-preorder - ``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣∣-trans ↦ ∥-trans - ∣-trans ↦ ∣ʳ-trans - ``` - -* In `Algebra.Structures.Group`: - ```agda - uniqueˡ-⁻¹ ↦ Algebra.Properties.Group.inverseˡ-unique - uniqueʳ-⁻¹ ↦ Algebra.Properties.Group.inverseʳ-unique - ``` - -* In `Data.List.Base`: - ```agda - and ↦ Data.Bool.ListAction.and - or ↦ Data.Bool.ListAction.or - any ↦ Data.Bool.ListAction.any - all ↦ Data.Bool.ListAction.all - sum ↦ Data.Nat.ListAction.sum - product ↦ Data.Nat.ListAction.product - ``` - -* In `Data.List.Properties`: - ```agda - sum-++ ↦ Data.Nat.ListAction.Properties.sum-++ - ∈⇒∣product ↦ Data.Nat.ListAction.Properties.∈⇒∣product - product≢0 ↦ Data.Nat.ListAction.Properties.product≢0 - ∈⇒≤product ↦ Data.Nat.ListAction.Properties.∈⇒≤product - ∷-ʳ++-eqFree ↦ Data.List.Properties.ʳ++-ʳ++-eqFree - ``` - -* In `Data.List.Relation.Binary.Permutation.Propositional.Properties`: - ```agda - sum-↭ ↦ Data.Nat.ListAction.Properties.sum-↭ - product-↭ ↦ Data.Nat.ListAction.Properties.product-↭ - ``` - -* In `Data.Product.Function.Dependent.Setoid`: - ```agda - left-inverse ↦ rightInverse - ``` - -* In `Data.Product.Nary.NonDependent`: - ```agda - Allₙ ↦ Pointwiseₙ - ``` - New modules ----------- -* `Algebra.Module.Properties.{Bimodule|LeftModule|RightModule}`. - -* `Algebra.Morphism.Construct.DirectProduct`. - -* `Data.List.Base.{and|or|any|all}` have been lifted out into `Data.Bool.ListAction`. - -* `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. - -* `Data.List.Sort.InsertionSort.{agda|Base|Properties}` defines insertion sort and proves properties of insertion sort such as Sorted and Permutation properties. - -* `Data.List.Sort.MergenSort.{agda|Base|Properties}` is a refactor of the previous `Data.List.Sort.MergenSort`. - -* `Data.Sign.Show` to show a sign. - -* `Relation.Binary.Morphism.Construct.Product` to plumb in the (categorical) product structure on `RawSetoid`. - -* `Relation.Binary.Properties.PartialSetoid` to systematise properties of a PER - -* `Relation.Nullary.Recomputable.Core` - Additions to existing modules ----------------------------- - -* In `Algebra.Consequences.Base`: - ```agda - module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_) - where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Consequences.Setoid`: - ```agda - module Congruence (cong : Congruent₂ _≈_ _∙_) where - ∙-congˡ : LeftCongruent _≈_ _∙_ - ∙-congʳ : RightCongruent _≈_ _∙_ - ``` - -* In `Algebra.Construct.Pointwise`: - ```agda - isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → - IsNearSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiringWithoutOne : IsCommutativeSemiringWithoutOne _≈_ _+_ _*_ 0# → - IsCommutativeSemiringWithoutOne (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) - isCommutativeSemiring : IsCommutativeSemiring _≈_ _+_ _*_ 0# 1# → - IsCommutativeSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isIdempotentSemiring : IsIdempotentSemiring _≈_ _+_ _*_ 0# 1# → - IsIdempotentSemiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isKleeneAlgebra : IsKleeneAlgebra _≈_ _+_ _*_ _⋆ 0# 1# → - IsKleeneAlgebra (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ _⋆) (lift₀ 0#) (lift₀ 1#) - isQuasiring : IsQuasiring _≈_ _+_ _*_ 0# 1# → - IsQuasiring (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₀ 0#) (lift₀ 1#) - isCommutativeRing : IsCommutativeRing _≈_ _+_ _*_ -_ 0# 1# → - IsCommutativeRing (liftRel _≈_) (lift₂ _+_) (lift₂ _*_) (lift₁ -_) (lift₀ 0#) (lift₀ 1#) - commutativeMonoid : CommutativeMonoid c ℓ → CommutativeMonoid (a ⊔ c) (a ⊔ ℓ) - nearSemiring : NearSemiring c ℓ → NearSemiring (a ⊔ c) (a ⊔ ℓ) - semiringWithoutOne : SemiringWithoutOne c ℓ → SemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiringWithoutOne : CommutativeSemiringWithoutOne c ℓ → CommutativeSemiringWithoutOne (a ⊔ c) (a ⊔ ℓ) - commutativeSemiring : CommutativeSemiring c ℓ → CommutativeSemiring (a ⊔ c) (a ⊔ ℓ) - idempotentSemiring : IdempotentSemiring c ℓ → IdempotentSemiring (a ⊔ c) (a ⊔ ℓ) - kleeneAlgebra : KleeneAlgebra c ℓ → KleeneAlgebra (a ⊔ c) (a ⊔ ℓ) - quasiring : Quasiring c ℓ → Quasiring (a ⊔ c) (a ⊔ ℓ) - commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) - ``` - -* In `Algebra.Modules.Properties`: - ```agda - inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y - inverseʳ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → y ≈ -ᴹ x - ``` - -* In `Algebra.Properties.Magma.Divisibility`: - ```agda - ∣ˡ-respʳ-≈ : _∣ˡ_ Respectsʳ _≈_ - ∣ˡ-respˡ-≈ : _∣ˡ_ Respectsˡ _≈_ - ∣ˡ-resp-≈ : _∣ˡ_ Respects₂ _≈_ - x∣ˡxy : ∀ x y → x ∣ˡ x ∙ y - xy≈z⇒x∣ˡz : ∀ x y {z} → x ∙ y ≈ z → x ∣ˡ z - ``` - -* In `Algebra.Properties.Monoid.Divisibility`: - ```agda - ε∣ˡ_ : ∀ x → ε ∣ˡ x - ∣ˡ-refl : Reflexive _∣ˡ_ - ∣ˡ-reflexive : _≈_ ⇒ _∣ˡ_ - ∣ˡ-isPreorder : IsPreorder _≈_ _∣ˡ_ - ∣ˡ-preorder : Preorder a ℓ _ - ``` - -* In `Algebra.Properties.Semigroup` adding consequences for associativity for semigroups - -``` - uv≈w⇒xu∙v≈xw : ∀ x → (x ∙ u) ∙ v ≈ x ∙ w - uv≈w⇒u∙vx≈wx : ∀ x → u ∙ (v ∙ x) ≈ w ∙ x - uv≈w⇒u[vx∙y]≈w∙xy : ∀ x y → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ (x ∙ y) - uv≈w⇒x[uv∙y]≈x∙wy : ∀ x y → x ∙ (u ∙ (v ∙ y)) ≈ x ∙ (w ∙ y) - uv≈w⇒[x∙yu]v≈x∙yw : ∀ x y → (x ∙ (y ∙ u)) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒[xu∙v]y≈x∙wy : ∀ x y → ((x ∙ u) ∙ v) ∙ y ≈ x ∙ (w ∙ y) - uv≈w⇒[xy∙u]v≈x∙yw : ∀ x y → ((x ∙ y) ∙ u) ∙ v ≈ x ∙ (y ∙ w) - uv≈w⇒xu∙vy≈x∙wy : ∀ x y → (x ∙ u) ∙ (v ∙ y) ≈ x ∙ (w ∙ y) - uv≈w⇒xy≈z⇒u[vx∙y]≈wz : ∀ z → x ∙ y ≈ z → u ∙ ((v ∙ x) ∙ y) ≈ w ∙ z - uv≈w⇒x∙wy≈x∙[u∙vy] : x ∙ (w ∙ y) ≈ x ∙ (u ∙ (v ∙ y)) - [uv∙w]x≈u[vw∙x] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ ((v ∙ w) ∙ x) - [uv∙w]x≈u[v∙wx] : ((u ∙ v) ∙ w) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - [u∙vw]x≈uv∙wx : (u ∙ (v ∙ w)) ∙ x ≈ (u ∙ v) ∙ (w ∙ x) - [u∙vw]x≈u[v∙wx] : (u ∙ (v ∙ w)) ∙ x ≈ u ∙ (v ∙ (w ∙ x)) - uv∙wx≈u[vw∙x] : (u ∙ v) ∙ (w ∙ x) ≈ u ∙ ((v ∙ w) ∙ x) - uv≈wx⇒yu∙v≈yw∙x : ∀ y → (y ∙ u) ∙ v ≈ (y ∙ w) ∙ x - uv≈wx⇒u∙vy≈w∙xy : ∀ y → u ∙ (v ∙ y) ≈ w ∙ (x ∙ y) - uv≈wx⇒yu∙vz≈yw∙xz : ∀ y z → (y ∙ u) ∙ (v ∙ z) ≈ (y ∙ w) ∙ (x ∙ z) -``` - -* In `Algebra.Properties.Semigroup.Divisibility`: - ```agda - ∣ˡ-trans : Transitive _∣ˡ_ - x∣ʳy⇒x∣ʳzy : x ∣ʳ y → x ∣ʳ z ∙ y - x∣ʳy⇒xz∣ʳyz : x ∣ʳ y → x ∙ z ∣ʳ y ∙ z - x∣ˡy⇒zx∣ˡzy : x ∣ˡ y → z ∙ x ∣ˡ z ∙ y - x∣ˡy⇒x∣ˡyz : x ∣ˡ y → x ∣ˡ y ∙ z - ``` - -* In `Algebra.Properties.CommutativeSemigroup.Divisibility`: - ```agda - ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b - ``` - -* In `Data.Bool.Properties`: - ```agda - if-eta : ∀ b → (if b then x else x) ≡ x - if-idem-then : ∀ b → (if b then (if b then x else y) else y) ≡ (if b then x else y) - if-idem-else : ∀ b → (if b then x else (if b then x else y)) ≡ (if b then x else y) - if-swap-then : ∀ b c → (if b then (if c then x else y) else y) ≡ (if c then (if b then x else y) else y) - if-swap-else : ∀ b c → (if b then x else (if c then x else y)) ≡ (if c then x else (if b then x else y)) - if-not : ∀ b → (if not b then x else y) ≡ (if b then y else x) - if-∧ : ∀ b → (if b ∧ c then x else y) ≡ (if b then (if c then x else y) else y) - if-∨ : ∀ b → (if b ∨ c then x else y) ≡ (if b then x else (if c then x else y)) - if-xor : ∀ b → (if b xor c then x else y) ≡ (if b then (if c then y else x) else (if c then x else y)) - if-cong : b ≡ c → (if b then x else y) ≡ (if c then x else y) - if-cong-then : ∀ b → x ≡ z → (if b then x else y) ≡ (if b then z else y) - if-cong-else : ∀ b → y ≡ z → (if b then x else y) ≡ (if b then x else z) - if-cong₂ : ∀ b → x ≡ z → y ≡ w → (if b then x else y) ≡ (if b then z else w) - ``` - -* In `Data.Fin.Base`: - ```agda - _≰_ : Rel (Fin n) 0ℓ - _≮_ : Rel (Fin n) 0ℓ - lower : ∀ (i : Fin m) → .(toℕ i ℕ.< n) → Fin n - ``` - -* In `Data.Fin.Permutation`: - ```agda - cast-id : .(m ≡ n) → Permutation m n - swap : Permutation m n → Permutation (2+ m) (2+ n) - ``` - -* In `Data.Fin.Properties`: - ```agda - cast-involutive : .(eq₁ : m ≡ n) .(eq₂ : n ≡ m) → ∀ k → cast eq₁ (cast eq₂ k) ≡ k - inject!-injective : Injective _≡_ _≡_ inject! - inject!-< : (k : Fin′ i) → inject! k < i - lower-injective : lower i i