Skip to content

Commit aef1785

Browse files
jamesmckinnajamesmckinna
authored
[ add ] Choudhury and Fiore's alternative definition of Permutation for Setoids (#2726)
* [ add ] Hinze's definition of `Permutation` for `Setoid`s * fix: `dos2unix` * fix: module name * fix: `dos2unix` * fix: attribution, and module name * fix: attribution, and module name, one more time; also remove `rewrite` * fix: restore new module, with new name * add: `Declarative` definition and properties * fix: whitespace * fix: tweaks * refactor: `Declarative` into definitions and properties * refactor: `Algorithmic` into definitions and properties * fix: `import`s * fix: knock-ons * fix: added more commentary/explanation * add: new modules to `CHANGELOG` * fix: notation * fix: notation * fix: `CHANGELOG`
1 parent aab6732 commit aef1785

File tree

5 files changed

+418
-0
lines changed

5 files changed

+418
-0
lines changed

‎CHANGELOG.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,10 @@ Deprecated names
3535
New modules
3636
-----------
3737

38+
* `Data.List.Relation.Binary.Permutation.Algorithmic{.Properties}` for the Choudhury and Fiore definition of permutation, and its equivalence with `Declarative` below.
39+
40+
* `Data.List.Relation.Binary.Permutation.Declarative{.Properties}` for the least congruence on `List` making `_++_` commutative, and its equivalence with the `Setoid` definition.
41+
3842
Additions to existing modules
3943
-----------------------------
4044

‎src/Data/List/Relation/Binary/Permutation/Algorithmic.agda

Lines changed: 150 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,150 @@
1+
-------------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- A alternative definition for the permutation relation using setoid equality
5+
-- Based on Choudhury and Fiore, "Free Commutative Monoids in HoTT" (MFPS, 2022)
6+
-- Constructor `_⋎_` below is rule (3), directly after the proof of Theorem 6.3,
7+
-- and appears as rule `commrel` of their earlier presentation at (HoTT, 2019),
8+
-- "The finite-multiset construction in HoTT".
9+
--
10+
-- `Algorithmic` ⊆ `Data.List.Relation.Binary.Permutation.Declarative`
11+
-- but enjoys a much smaller space of derivations, without being so (over-)
12+
-- deterministic as to being inductively defined as the relation generated
13+
-- by swapping the top two elements (the relational analogue of bubble-sort).
14+
15+
-- In particular, transitivity, `↭-trans` below, is an admissible property.
16+
--
17+
-- So this relation is 'better' for proving properties of `_↭_`, while at the
18+
-- same time also being a better fit, via `_⋎_`, for the operational features
19+
-- of e.g. sorting algorithms which transpose at arbitary positions.
20+
-------------------------------------------------------------------------------
21+
22+
{-# OPTIONS --cubical-compatible --safe #-}
23+
24+
open import Relation.Binary.Bundles using (Setoid)
25+
26+
module Data.List.Relation.Binary.Permutation.Algorithmic
27+
{s ℓ} (S : Setoid s ℓ) where
28+
29+
open import Data.List.Base using (List; []; _∷_; length)
30+
open import Data.List.Properties using (++-identityʳ)
31+
open import Data.Nat.Base using (ℕ; suc)
32+
open import Data.Nat.Properties using (suc-injective)
33+
open import Level using (_⊔_)
34+
open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
35+
36+
open import Data.List.Relation.Binary.Equality.Setoid S as ≋
37+
using (_≋_; []; _∷_; ≋-refl)
38+
39+
open Setoid S
40+
renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
41+
42+
private
43+
variable
44+
a b c d : A
45+
as bs cs ds : List A
46+
n : ℕ
47+
48+
49+
-------------------------------------------------------------------------------
50+
-- Definition
51+
52+
infix 4 _↭_
53+
infix 5 _⋎_ _⋎[_]_
54+
55+
data _↭_ : List A → List A → Set (s ⊔ ℓ) where
56+
[] : [] ↭ []
57+
_∷_ : a ≈ b → as ↭ bs → a ∷ as ↭ b ∷ bs
58+
_⋎_ : as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs
59+
60+
-- smart constructor for prefix congruence
61+
62+
_≡∷_ : ∀ c → as ↭ bs → c ∷ as ↭ c ∷ bs
63+
_≡∷_ c = ≈-refl ∷_
64+
65+
-- pattern synonym to allow naming the 'middle' term
66+
pattern _⋎[_]_ {as} {b} {a} {bs} as↭b∷cs cs a∷cs↭bs
67+
= _⋎_ {as} {b} {cs = cs} {a} {bs} as↭b∷cs a∷cs↭bs
68+
69+
-------------------------------------------------------------------------------
70+
-- Properties
71+
72+
↭-reflexive : as ≋ bs → as ↭ bs
73+
↭-reflexive [] = []
74+
↭-reflexive (a≈b ∷ as↭bs) = a≈b ∷ ↭-reflexive as↭bs
75+
76+
↭-refl : ∀ as → as ↭ as
77+
↭-refl _ = ↭-reflexive ≋-refl
78+
79+
↭-sym : as ↭ bs → bs ↭ as
80+
↭-sym [] = []
81+
↭-sym (a≈b ∷ as↭bs) = ≈-sym a≈b ∷ ↭-sym as↭bs
82+
↭-sym (as↭b∷cs ⋎ a∷cs↭bs) = ↭-sym a∷cs↭bs ⋎ ↭-sym as↭b∷cs
83+
84+
≋∘↭⇒↭ : as ≋ bs → bs ↭ cs → as ↭ cs
85+
≋∘↭⇒↭ [] [] = []
86+
≋∘↭⇒↭ (a≈b ∷ as≋bs) (b≈c ∷ bs↭cs) = ≈-trans a≈b b≈c ∷ ≋∘↭⇒↭ as≋bs bs↭cs
87+
≋∘↭⇒↭ (a≈b ∷ as≋bs) (bs↭c∷ds ⋎ b∷ds↭cs) =
88+
≋∘↭⇒↭ as≋bs bs↭c∷ds ⋎ ≋∘↭⇒↭ (a≈b ∷ ≋-refl) b∷ds↭cs
89+
90+
↭∘≋⇒↭ : as ↭ bs → bs ≋ cs → as ↭ cs
91+
↭∘≋⇒↭ [] [] = []
92+
↭∘≋⇒↭ (a≈b ∷ as↭bs) (b≈c ∷ bs≋cs) = ≈-trans a≈b b≈c ∷ ↭∘≋⇒↭ as↭bs bs≋cs
93+
↭∘≋⇒↭ (as↭b∷cs ⋎ a∷cs↭bs) (b≈d ∷ bs≋ds) =
94+
↭∘≋⇒↭ as↭b∷cs (b≈d ∷ ≋-refl) ⋎ ↭∘≋⇒↭ a∷cs↭bs bs≋ds
95+
96+
↭-length : as ↭ bs → length as ≡ length bs
97+
↭-length [] = ≡.refl
98+
↭-length (a≈b ∷ as↭bs) = ≡.cong suc (↭-length as↭bs)
99+
↭-length (as↭b∷cs ⋎ a∷cs↭bs) = ≡.cong suc (≡.trans (↭-length as↭b∷cs) (↭-length a∷cs↭bs))
100+
101+
↭-trans : as ↭ bs → bs ↭ cs → as ↭ cs
102+
↭-trans = lemma ≡.refl
103+
where
104+
lemma : n ≡ length bs → as ↭ bs → bs ↭ cs → as ↭ cs
105+
106+
-- easy base case for bs = [], eq: 0 ≡ 0
107+
lemma _ [] [] = []
108+
109+
-- fiddly step case for bs = b ∷ bs, where eq : suc n ≡ suc (length bs)
110+
-- hence suc-injective eq : n ≡ length bs
111+
112+
lemma {n = suc n} eq (a≈b ∷ as↭bs) (b≈c ∷ bs↭cs)
113+
= ≈-trans a≈b b≈c ∷ lemma (suc-injective eq) as↭bs bs↭cs
114+
115+
lemma {n = suc n} eq (a≈b ∷ as↭bs) (bs↭c∷ys ⋎ b∷ys↭cs)
116+
= ≋∘↭⇒↭ (a≈b ∷ ≋-refl) (lemma (suc-injective eq) as↭bs bs↭c∷ys ⋎ b∷ys↭cs)
117+
118+
lemma {n = suc n} eq (as↭b∷xs ⋎ a∷xs↭bs) (a≈b ∷ bs↭cs)
119+
= ↭∘≋⇒↭ (as↭b∷xs ⋎ lemma (suc-injective eq) a∷xs↭bs bs↭cs) (a≈b ∷ ≋-refl)
120+
121+
lemma {n = suc n} {bs = b ∷ bs} {as = a ∷ as} {cs = c ∷ cs} eq
122+
(as↭b∷xs ⋎[ xs ] a∷xs↭bs) (bs↭c∷ys ⋎[ ys ] b∷ys↭cs) = a∷as↭c∷cs
123+
where
124+
n≡∣bs∣ : n ≡ length bs
125+
n≡∣bs∣ = suc-injective eq
126+
127+
n≡∣b∷xs∣ : n ≡ length (b ∷ xs)
128+
n≡∣b∷xs∣ = ≡.trans n≡∣bs∣ (≡.sym (↭-length a∷xs↭bs))
129+
130+
n≡∣b∷ys∣ : n ≡ length (b ∷ ys)
131+
n≡∣b∷ys∣ = ≡.trans n≡∣bs∣ (↭-length bs↭c∷ys)
132+
133+
a∷as↭c∷cs : a ∷ as ↭ c ∷ cs
134+
a∷as↭c∷cs with lemma n≡∣bs∣ a∷xs↭bs bs↭c∷ys
135+
... | a≈c ∷ xs↭ys = a≈c ∷ as↭cs
136+
where
137+
as↭cs : as ↭ cs
138+
as↭cs = lemma n≡∣b∷xs∣ as↭b∷xs
139+
(lemma n≡∣b∷ys∣ (b ≡∷ xs↭ys) b∷ys↭cs)
140+
... | xs↭c∷zs ⋎[ zs ] a∷zs↭ys
141+
= lemma n≡∣b∷xs∣ as↭b∷xs b∷xs↭c∷b∷zs
142+
⋎[ b ∷ zs ]
143+
lemma n≡∣b∷ys∣ a∷b∷zs↭b∷ys b∷ys↭cs
144+
where
145+
b∷zs↭b∷zs : b ∷ zs ↭ b ∷ zs
146+
b∷zs↭b∷zs = ↭-refl (b ∷ zs)
147+
b∷xs↭c∷b∷zs : b ∷ xs ↭ c ∷ (b ∷ zs)
148+
b∷xs↭c∷b∷zs = xs↭c∷zs ⋎[ zs ] b∷zs↭b∷zs
149+
a∷b∷zs↭b∷ys : a ∷ (b ∷ zs) ↭ b ∷ ys
150+
a∷b∷zs↭b∷ys = b∷zs↭b∷zs ⋎[ zs ] a∷zs↭ys

‎src/Data/List/Relation/Binary/Permutation/Algorithmic/Properties.agda

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
-------------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Properties of the `Algorithmic` definition of the permutation relation.
5+
-------------------------------------------------------------------------------
6+
7+
{-# OPTIONS --cubical-compatible --safe #-}
8+
9+
open import Relation.Binary.Bundles using (Setoid)
10+
11+
module Data.List.Relation.Binary.Permutation.Algorithmic.Properties
12+
{s ℓ} (S : Setoid s ℓ) where
13+
14+
open import Data.List.Base using (List; []; _∷_; _++_)
15+
open import Data.List.Properties using (++-identityʳ)
16+
import Relation.Binary.PropositionalEquality as ≡
17+
using (sym)
18+
19+
open import Data.List.Relation.Binary.Equality.Setoid S as ≋
20+
using (≋-reflexive)
21+
open import Data.List.Relation.Binary.Permutation.Algorithmic S
22+
import Data.List.Relation.Binary.Permutation.Setoid S as ↭ₛ
23+
using (_↭_; refl; prep; swap; trans; ↭-refl; ↭-prep; ↭-swap; ↭-trans)
24+
25+
open Setoid S
26+
renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
27+
28+
private
29+
variable
30+
a b c d : A
31+
as bs cs ds : List A
32+
33+
34+
-------------------------------------------------------------------------------
35+
-- Properties
36+
37+
↭-swap : a ≈ c → b ≈ d → cs ↭ ds → a ∷ b ∷ cs ↭ d ∷ c ∷ ds
38+
↭-swap a≈c b≈d cs≈ds = (b≈d ∷ cs≈ds) ⋎ (a≈c ∷ ↭-refl _)
39+
40+
↭-swap-++ : (as bs : List A) → as ++ bs ↭ bs ++ as
41+
↭-swap-++ [] bs = ↭-reflexive (≋-reflexive (≡.sym (++-identityʳ bs)))
42+
↭-swap-++ (a ∷ as) bs = lemma bs (↭-swap-++ as bs)
43+
where
44+
lemma : ∀ bs → cs ↭ bs ++ as → a ∷ cs ↭ bs ++ a ∷ as
45+
lemma [] cs↭as
46+
= a ≡∷ cs↭as
47+
lemma (b ∷ bs) (a≈b ∷ cs↭bs++as)
48+
= (a≈b ∷ ↭-refl _) ⋎ lemma bs cs↭bs++as
49+
lemma (b ∷ bs) (cs↭b∷ds ⋎ a∷ds↭bs++as)
50+
= (cs↭b∷ds ⋎ (↭-refl _)) ⋎ (lemma bs a∷ds↭bs++as)
51+
52+
↭-congʳ : ∀ cs → as ↭ bs → cs ++ as ↭ cs ++ bs
53+
↭-congʳ {as = as} {bs = bs} cs as↭bs = lemma cs
54+
where
55+
lemma : ∀ cs → cs ++ as ↭ cs ++ bs
56+
lemma [] = as↭bs
57+
lemma (c ∷ cs) = c ≡∷ lemma cs
58+
59+
↭-congˡ : as ↭ bs → ∀ cs → as ++ cs ↭ bs ++ cs
60+
↭-congˡ as↭bs cs = lemma as↭bs
61+
where
62+
lemma : as ↭ bs → as ++ cs ↭ bs ++ cs
63+
lemma [] = ↭-refl cs
64+
lemma (a≈b ∷ as↭bs) = a≈b ∷ lemma as↭bs
65+
lemma (as↭b∷xs ⋎ bs↭a∷xs) = lemma as↭b∷xs ⋎ lemma bs↭a∷xs
66+
67+
↭-cong : as ↭ bs → cs ↭ ds → as ++ cs ↭ bs ++ ds
68+
↭-cong as↭bs cs↭ds = ↭-trans (↭-congˡ as↭bs _) (↭-congʳ _ cs↭ds)
69+
70+
-------------------------------------------------------------------------------
71+
-- Equivalence with `Setoid` definition of _↭_
72+
73+
↭ₛ⇒↭ : as ↭ₛ.↭ bs → as ↭ bs
74+
↭ₛ⇒↭ (↭ₛ.refl as≋bs) = ↭-reflexive as≋bs
75+
↭ₛ⇒↭ (↭ₛ.prep a≈b as↭bs) = a≈b ∷ ↭ₛ⇒↭ as↭bs
76+
↭ₛ⇒↭ (↭ₛ.swap a≈c b≈d cs↭ds) = ↭-swap a≈c b≈d (↭ₛ⇒↭ cs↭ds)
77+
↭ₛ⇒↭ (↭ₛ.trans as↭bs bs↭cs) = ↭-trans (↭ₛ⇒↭ as↭bs) (↭ₛ⇒↭ bs↭cs)
78+
79+
↭⇒↭ₛ : as ↭ bs → as ↭ₛ.↭ bs
80+
↭⇒↭ₛ [] = ↭ₛ.↭-refl
81+
↭⇒↭ₛ (a≈b ∷ as↭bs) = ↭ₛ.prep a≈b (↭⇒↭ₛ as↭bs)
82+
↭⇒↭ₛ (as↭b∷cs ⋎ a∷cs↭bs) = ↭ₛ.↭-trans (↭ₛ.↭-prep _ (↭⇒↭ₛ as↭b∷cs))
83+
(↭ₛ.↭-trans (↭ₛ.↭-swap _ _ ↭ₛ.↭-refl)
84+
(↭ₛ.↭-prep _ (↭⇒↭ₛ a∷cs↭bs)))

‎src/Data/List/Relation/Binary/Permutation/Declarative.agda

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
-------------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- A declarative definition of the permutation relation, inductively defined
5+
-- as the least congruence on `List` which makes `_++_` commutative. Thus, for
6+
-- `(A, _≈_)` a setoid, `List A` with equality given by `_↭_` is a constructive
7+
-- presentation of the free commutative monoid on `A`.
8+
--
9+
-- NB. we do not need to specify symmetry as a constructor; the rules defining
10+
-- `_↭_` are themselves symmetric, by inspection, whence `↭-sym` below.
11+
--
12+
-- `_↭_` is somehow the 'maximally non-deterministic' (permissive) presentation
13+
-- of the permutation relation on lists, so is 'easiest' to establish for any
14+
-- given pair of lists, while nevertheless provably equivalent to more
15+
-- operationally defined versions, in particular
16+
-- `Declarative` ⊆ `Data.List.Relation.Binary.Permutation.Algorithmic`
17+
-------------------------------------------------------------------------------
18+
19+
{-# OPTIONS --cubical-compatible --safe #-}
20+
21+
open import Relation.Binary.Bundles using (Setoid)
22+
23+
module Data.List.Relation.Binary.Permutation.Declarative
24+
{s ℓ} (S : Setoid s ℓ) where
25+
26+
open import Data.List.Base using (List; []; _∷_; [_]; _++_)
27+
open import Data.List.Properties using (++-identityʳ)
28+
open import Function.Base using (id; _∘_)
29+
open import Level using (_⊔_)
30+
import Relation.Binary.PropositionalEquality as ≡ using (sym)
31+
32+
open import Data.List.Relation.Binary.Equality.Setoid S as ≋
33+
using (_≋_; []; _∷_; ≋-refl; ≋-reflexive)
34+
35+
open Setoid S
36+
renaming (Carrier to A; refl to ≈-refl; sym to ≈-sym; trans to ≈-trans)
37+
38+
private
39+
variable
40+
a b c d : A
41+
as bs cs ds : List A
42+
43+
44+
-------------------------------------------------------------------------------
45+
-- Definition
46+
47+
infix 4 _↭_
48+
49+
data _↭_ : List A → List A → Set (s ⊔ ℓ) where
50+
[] : [] ↭ []
51+
_∷_ : a ≈ b → as ↭ bs → a ∷ as ↭ b ∷ bs
52+
trans : as ↭ bs → bs ↭ cs → as ↭ cs
53+
_++ᵒ_ : ∀ as bs → as ++ bs ↭ bs ++ as
54+
55+
-- smart constructor for prefix congruence
56+
57+
_≡∷_ : ∀ c → as ↭ bs → c ∷ as ↭ c ∷ bs
58+
_≡∷_ c = ≈-refl ∷_
59+
60+
-------------------------------------------------------------------------------
61+
-- Basic properties and smart constructors
62+
63+
↭-reflexive : as ≋ bs → as ↭ bs
64+
↭-reflexive [] = []
65+
↭-reflexive (a≈b ∷ as↭bs) = a≈b ∷ ↭-reflexive as↭bs
66+
67+
↭-refl : ∀ as → as ↭ as
68+
↭-refl _ = ↭-reflexive ≋-refl
69+
70+
↭-sym : as ↭ bs → bs ↭ as
71+
↭-sym [] = []
72+
↭-sym (a≈b ∷ as↭bs) = ≈-sym a≈b ∷ ↭-sym as↭bs
73+
↭-sym (trans as↭cs cs↭bs) = trans (↭-sym cs↭bs) (↭-sym as↭cs)
74+
↭-sym (as ++ᵒ bs) = bs ++ᵒ as
75+
76+
-- smart constructor for trans
77+
78+
↭-trans : as ↭ bs → bs ↭ cs → as ↭ cs
79+
↭-trans [] = id
80+
↭-trans (trans as↭bs bs↭cs) = ↭-trans as↭bs ∘ ↭-trans bs↭cs
81+
↭-trans as↭bs = trans as↭bs
82+
83+
-- smart constructor for swap
84+
85+
↭-swap-++ : (as bs : List A) → as ++ bs ↭ bs ++ as
86+
↭-swap-++ [] bs = ↭-reflexive (≋-reflexive (≡.sym (++-identityʳ bs)))
87+
↭-swap-++ as@(_ ∷ _) [] = ↭-reflexive (≋-reflexive (++-identityʳ as))
88+
↭-swap-++ as@(_ ∷ _) bs@(_ ∷ _) = as ++ᵒ bs
89+
90+
↭-congʳ : as ↭ bs → cs ++ as ↭ cs ++ bs
91+
↭-congʳ {as = as} {bs = bs} {cs = cs} as↭bs = lemma cs
92+
where
93+
lemma : ∀ cs → cs ++ as ↭ cs ++ bs
94+
lemma [] = as↭bs
95+
lemma (c ∷ cs) = c ≡∷ lemma cs
96+
97+
↭-congˡ : as ↭ bs → as ++ cs ↭ bs ++ cs
98+
↭-congˡ {as = as} {bs = bs} {cs = cs} as↭bs =
99+
↭-trans (↭-swap-++ as cs) (↭-trans (↭-congʳ as↭bs) (↭-swap-++ cs bs))
100+
101+
↭-cong : as ↭ bs → cs ↭ ds → as ++ cs ↭ bs ++ ds
102+
↭-cong as↭bs cs↭ds = ↭-trans (↭-congˡ as↭bs) (↭-congʳ cs↭ds)
103+
104+
-- smart constructor for generalised swap
105+
106+
infix 5 _↭-⋎_
107+
108+
_↭-⋎_ : as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs
109+
_↭-⋎_ {b = b} {a = a} as↭b∷cs a∷cs↭bs =
110+
trans (a ≡∷ as↭b∷cs) (↭-trans (↭-congˡ ([ a ] ++ᵒ [ b ])) (b ≡∷ a∷cs↭bs))
111+
112+
⋎-syntax : ∀ cs → as ↭ b ∷ cs → a ∷ cs ↭ bs → a ∷ as ↭ b ∷ bs
113+
⋎-syntax cs = _↭-⋎_ {cs = cs}
114+
115+
syntax ⋎-syntax cs as↭b∷cs a∷cs↭bs = as↭b∷cs ↭-⋎[ cs ] a∷cs↭bs

0 commit comments

Comments
 (0)