Add transposition decomposition for permutations (#1271)

Author: alexarice

CHANGELOG.md

@@ -261,6 +261,18 @@ New modules
   System.Environment.Primitive
   ```
 
+* Added a module `Data.Fin.Permutation.Transposition.List` which
+  contains a type `TranspositionList n = List (Fin n × Fin n)` for
+  representing a list of transpositions (a permutation which switches
+  two elements). Also added a function `decompose` that decomposes an
+  arbitrary permutation into a list of transpositions and provided a
+  proof that this list of transpositions evaluates to the originial
+  permutation. Note that currently transpositions of the form (i,i)
+  are allowed as in some literature they are not (in particular the
+  proof that any two transposition decompositions of a permutation
+  have lengths that differ by an even number).
+  ```
+
 * Added the following `Show` modules:
   ```agda
   Data.Fin.Show
@@ -314,6 +326,17 @@ Other minor additions
   CancellativeCommutativeSemiring c ℓ : Set (suc (c ⊔ ℓ))
   ```
 
+* Added new relations, functions and proofs to `Data.Fin.Permutation`:
+  ```
+  _≈_             : Rel (Permutation m n) 0ℓ
+  lift₀           : Permutation m n → Permutation (suc m) (suc n)
+  lift₀-remove    : π ⟨$⟩ʳ 0F ≡ 0F → ∀ i → lift₀ (remove 0F π) ≈ π
+  lift₀-id        : lift₀ id ⟨$⟩ʳ i ≡ i
+  lift₀-comp      : lift₀ π ∘ₚ lift₀ ρ ≈ lift₀ (π ∘ₚ ρ)
+  lift₀-cong      : π ≈ ρ → lift₀ π ≈ lift₀ ρ
+  lift₀-transpose : transpose (suc i) (suc j)≈ lift₀ (transpose i j)
+  ```
+
 * Added new definitions to `Algebra.Definitions`:
   ```agda
   AlmostLeftCancellative  e _•_ = ∀ {x} y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z

src/Data/Fin/Permutation.agda

@@ -8,21 +8,29 @@
 
 module Data.Fin.Permutation where
 
+open import Data.Bool using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base
+open import Data.Fin.Patterns
 open import Data.Fin.Properties
 import Data.Fin.Permutation.Components as PC
 open import Data.Nat.Base using (ℕ; suc; zero)
 open import Data.Product using (proj₂)
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
 open import Function.Equality using (_⟨$⟩_)
 open import Function.Base using (_∘_)
-open import Relation.Nullary using (¬_; yes; no)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel)
+open import Relation.Nullary using (does; ¬_; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Binary.PropositionalEquality as P
   using (_≡_; _≢_; refl; trans; sym; →-to-⟶; cong; cong₂)
 open P.≡-Reasoning
 
+private
+  variable
+    m n o : ℕ
+
 ------------------------------------------------------------------------
 -- Types
 
@@ -42,48 +50,54 @@ Permutation′ n = Permutation n n
 ------------------------------------------------------------------------
 -- Helper functions
 
-permutation : ∀ {m n} (f : Fin m → Fin n) (g : Fin n → Fin m) →
+permutation : ∀ (f : Fin m → Fin n) (g : Fin n → Fin m) →
               (→-to-⟶ g) InverseOf (→-to-⟶ f) → Permutation m n
 permutation f g inv = record
   { to         = →-to-⟶ f
   ; from       = →-to-⟶ g
   ; inverse-of = inv
   }
 
-_⟨$⟩ʳ_ : ∀ {m n} → Permutation m n → Fin m → Fin n
+infixl 5 _⟨$⟩ʳ_ _⟨$⟩ˡ_
+_⟨$⟩ʳ_ : Permutation m n → Fin m → Fin n
 _⟨$⟩ʳ_ = _⟨$⟩_ ∘ Inverse.to
 
-_⟨$⟩ˡ_ : ∀ {m n} → Permutation m n → Fin n → Fin m
+_⟨$⟩ˡ_ : Permutation m n → Fin n → Fin m
 _⟨$⟩ˡ_ = _⟨$⟩_ ∘ Inverse.from
 
-inverseˡ : ∀ {m n} (π : Permutation m n) {i} → π ⟨$⟩ˡ (π ⟨$⟩ʳ i) ≡ i
+inverseˡ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ˡ (π ⟨$⟩ʳ i) ≡ i
 inverseˡ π = Inverse.left-inverse-of π _
 
-inverseʳ : ∀ {m n} (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ i
+inverseʳ : ∀ (π : Permutation m n) {i} → π ⟨$⟩ʳ (π ⟨$⟩ˡ i) ≡ i
 inverseʳ π = Inverse.right-inverse-of π _
 
+------------------------------------------------------------------------
+-- Equality
+
+infix 6 _≈_
+_≈_ : Rel (Permutation m n) 0ℓ
+π ≈ ρ = ∀ i → π ⟨$⟩ʳ i ≡ ρ ⟨$⟩ʳ i
+
 ------------------------------------------------------------------------
 -- Example permutations
 
 -- Identity
 
-id : ∀ {n} → Permutation′ n
+id : Permutation′ n
 id = Inverse.id
 
 -- Transpose two indices
 
-transpose : ∀ {n} → Fin n → Fin n → Permutation′ n
-transpose i j = permutation (PC.transpose i j) (PC.transpose j i)
-  record
+transpose : Fin n → Fin n → Permutation′ n
+transpose i j = permutation (PC.transpose i j) (PC.transpose j i) record
   { left-inverse-of  = λ _ → PC.transpose-inverse _ _
   ; right-inverse-of = λ _ → PC.transpose-inverse _ _
   }
 
 -- Reverse the order of indices
 
-reverse : ∀ {n} → Permutation′ n
-reverse = permutation PC.reverse PC.reverse
-  record
+reverse : Permutation′ n
+reverse = permutation PC.reverse PC.reverse record
   { left-inverse-of  = PC.reverse-involutive
   ; right-inverse-of = PC.reverse-involutive
   }
@@ -93,12 +107,13 @@ reverse = permutation PC.reverse PC.reverse
 
 -- Composition
 
-_∘ₚ_ : ∀ {m n o} → Permutation m n → Permutation n o → Permutation m o
+infixr 9 _∘ₚ_
+_∘ₚ_ : Permutation m n → Permutation n o → Permutation m o
 π₁ ∘ₚ π₂ = π₂ Inverse.∘ π₁
 
 -- Flip
 
-flip : ∀ {m n} → Permutation m n → Permutation n m
+flip : Permutation m n → Permutation n m
 flip = Inverse.sym
 
 -- Element removal
@@ -107,10 +122,8 @@ flip = Inverse.sym
 --
 -- [0 ↦ i₀, …, k-1 ↦ iₖ₋₁, k ↦ iₖ₊₁, k+1 ↦ iₖ₊₂, …, n-1 ↦ iₙ]
 
-remove : ∀ {m n} → Fin (suc m) →
-         Permutation (suc m) (suc n) → Permutation m n
-remove {m} {n} i π = permutation to from
-  record
+remove : Fin (suc m) → Permutation (suc m) (suc n) → Permutation m n
+remove {m} {n} i π = permutation to from record
   { left-inverse-of  = left-inverse-of
   ; right-inverse-of = right-inverse-of
   }
@@ -139,47 +152,97 @@ remove {m} {n} i π = permutation to from
   left-inverse-of : ∀ j → from (to j) ≡ j
   left-inverse-of j = begin
     from (to j)                                                      ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut {i = πʳ i} _)) ⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
     punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong i (inverseˡ π) ⟩
     punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
     j                                                                ∎
 
   right-inverse-of : ∀ j → to (from j) ≡ j
   right-inverse-of j = begin
     to (from j)                                                       ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut {i = i} _)) ⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
     punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
 
+-- lift: takes a permutation m → n and creates a permutation (suc m) → (suc n)
+-- by mapping 0 to 0 and applying the input permutation to everything else
+lift₀ : Permutation m n → Permutation (suc m) (suc n)
+lift₀ {m} {n} π = permutation to from record
+  { left-inverse-of = left-inverse-of
+  ; right-inverse-of = right-inverse-of
+  }
+  where
+  to : Fin (suc m) → Fin (suc n)
+  to 0F      = 0F
+  to (suc i) = suc (π ⟨$⟩ʳ i)
+
+  from : Fin (suc n) → Fin (suc m)
+  from 0F      = 0F
+  from (suc i) = suc (π ⟨$⟩ˡ i)
+
+  left-inverse-of : ∀ j → from (to j) ≡ j
+  left-inverse-of 0F      = refl
+  left-inverse-of (suc j) = cong suc (inverseˡ π)
+
+  right-inverse-of : ∀ j → to (from j) ≡ j
+  right-inverse-of 0F      = refl
+  right-inverse-of (suc j) = cong suc (inverseʳ π)
+
 ------------------------------------------------------------------------
 -- Other properties
 
-module _ {m n} (π : Permutation (suc m) (suc n)) where
+module _ (π : Permutation (suc m) (suc n)) where
   private
     πʳ = π ⟨$⟩ʳ_
     πˡ = π ⟨$⟩ˡ_
 
   punchIn-permute : ∀ i j → πʳ (punchIn i j) ≡ punchIn (πʳ i) (remove i π ⟨$⟩ʳ j)
-  punchIn-permute i j = begin
-    πʳ (punchIn i j)                                           ≡⟨ sym (punchIn-punchOut {i = πʳ i} _) ⟩
-    punchIn (πʳ i) (punchOut {i = πʳ i} {πʳ (punchIn i j)} _)  ≡⟨⟩
-    punchIn (πʳ i) (remove i π ⟨$⟩ʳ j)                         ∎
+  punchIn-permute i j = sym (punchIn-punchOut _)
 
   punchIn-permute′ : ∀ i j → πʳ (punchIn (πˡ i) j) ≡ punchIn i (remove (πˡ i) π ⟨$⟩ʳ j)
   punchIn-permute′ i j = begin
     πʳ (punchIn (πˡ i) j)                         ≡⟨ punchIn-permute _ _ ⟩
     punchIn (πʳ (πˡ i)) (remove (πˡ i) π ⟨$⟩ʳ j)  ≡⟨ cong₂ punchIn (inverseʳ π) refl ⟩
     punchIn i (remove (πˡ i) π ⟨$⟩ʳ j)            ∎
 
-↔⇒≡ : ∀ {m n} → Permutation m n → m ≡ n
+  lift₀-remove : πʳ 0F ≡ 0F → lift₀ (remove 0F π) ≈ π
+  lift₀-remove p 0F      = sym p
+  lift₀-remove p (suc i) = punchOut-zero (πʳ (suc i)) p
+    where
+    punchOut-zero : ∀ {i} (j : Fin (suc n)) {neq} → i ≡ 0F → suc (punchOut {i = i} {j} neq) ≡ j
+    punchOut-zero 0F {neq} p = ⊥-elim (neq p)
+    punchOut-zero (suc j) refl = refl
+
+↔⇒≡ : Permutation m n → m ≡ n
 ↔⇒≡ {zero}  {zero}  π = refl
-↔⇒≡ {zero}  {suc n} π = contradiction (π ⟨$⟩ˡ zero) ¬Fin0
-↔⇒≡ {suc m} {zero}  π = contradiction (π ⟨$⟩ʳ zero) ¬Fin0
-↔⇒≡ {suc m} {suc n} π = cong suc (↔⇒≡ (remove zero π))
+↔⇒≡ {zero}  {suc n} π = contradiction (π ⟨$⟩ˡ 0F) ¬Fin0
+↔⇒≡ {suc m} {zero}  π = contradiction (π ⟨$⟩ʳ 0F) ¬Fin0
+↔⇒≡ {suc m} {suc n} π = cong suc (↔⇒≡ (remove 0F π))
 
-fromPermutation : ∀ {m n} → Permutation m n → Permutation′ m
+fromPermutation : Permutation m n → Permutation′ m
 fromPermutation π = P.subst (Permutation _) (sym (↔⇒≡ π)) π
 
-refute : ∀ {m n} → m ≢ n → ¬ Permutation m n
+refute : m ≢ n → ¬ Permutation m n
 refute m≢n π = contradiction (↔⇒≡ π) m≢n
+
+lift₀-id : (i : Fin (suc n)) → lift₀ id ⟨$⟩ʳ i ≡ i
+lift₀-id 0F      = refl
+lift₀-id (suc i) = refl
+
+lift₀-comp : ∀ (π : Permutation m n) (ρ : Permutation n o) →
+             lift₀ π ∘ₚ lift₀ ρ ≈ lift₀ (π ∘ₚ ρ)
+lift₀-comp π ρ 0F      = refl
+lift₀-comp π ρ (suc i) = refl
+
+lift₀-cong : ∀ (π ρ : Permutation m n) → π ≈ ρ → lift₀ π ≈ lift₀ ρ
+lift₀-cong π ρ f 0F      = refl
+lift₀-cong π ρ f (suc i) = cong suc (f i)
+
+lift₀-transpose : ∀ (i j : Fin n) → transpose (suc i) (suc j) ≈ lift₀ (transpose i j)
+lift₀-transpose i j 0F      = refl
+lift₀-transpose i j (suc k) with does (k ≟ i)
+... | true = refl
+... | false with does (k ≟ j)
+...   | false = refl
+...   | true = refl

src/Data/Fin/Permutation/Transposition/List.agda

@@ -0,0 +1,71 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Decomposition of permutations into a list of transpositions.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Fin.Permutation.Transposition.List where
+
+open import Data.Fin.Base
+open import Data.Fin.Patterns using (0F)
+open import Data.Fin.Permutation as P hiding (lift₀)
+import Data.Fin.Permutation.Components as PC
+open import Data.List using (List; []; _∷_; map)
+open import Data.Nat.Base using (ℕ; suc; zero)
+open import Data.Product using (_×_; _,_)
+open import Function using (_∘_)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; sym; cong; module ≡-Reasoning)
+open ≡-Reasoning
+
+private
+  variable
+    n : ℕ
+
+------------------------------------------------------------------------
+-- Definition
+
+-- This decomposition is not a unique representation of the original
+-- permutation but can be used to simply proofs about permutations (by
+-- instead inducting on the list of transpositions).
+
+TranspositionList : ℕ → Set
+TranspositionList n = List (Fin n × Fin n)
+
+------------------------------------------------------------------------
+-- Operations on transposition lists
+
+lift₀ : TranspositionList n → TranspositionList (suc n)
+lift₀ xs = map (λ (i , j) → (suc i , suc j)) xs
+
+eval : TranspositionList n → Permutation′ n
+eval []             = id
+eval ((i , j) ∷ xs) = transpose i j ∘ₚ eval xs
+
+decompose : Permutation′ n → TranspositionList n
+decompose {zero}  π = []
+decompose {suc n} π = (π ⟨$⟩ˡ 0F , 0F) ∷ lift₀ (decompose (remove 0F ((transpose 0F (π ⟨$⟩ˡ 0F)) ∘ₚ π)))
+
+------------------------------------------------------------------------
+-- Properties
+
+eval-lift : ∀ (xs : TranspositionList n) → eval (lift₀ xs) ≈ P.lift₀ (eval xs)
+eval-lift []               = sym ∘ lift₀-id
+eval-lift ((i , j) ∷ xs) k = begin
+  transpose (suc i) (suc j) ∘ₚ eval (lift₀ xs) ⟨$⟩ʳ k     ≡⟨ cong (eval (lift₀ xs) ⟨$⟩ʳ_) (lift₀-transpose i j k) ⟩
+  P.lift₀ (transpose i j) ∘ₚ eval (lift₀ xs) ⟨$⟩ʳ k       ≡⟨ eval-lift xs (P.lift₀ (transpose i j) ⟨$⟩ʳ k) ⟩
+  P.lift₀ (eval xs) ⟨$⟩ʳ (P.lift₀ (transpose i j) ⟨$⟩ʳ k) ≡⟨ lift₀-comp (transpose i j) (eval xs) k ⟩
+  P.lift₀ (transpose i j ∘ₚ eval xs) ⟨$⟩ʳ k               ∎
+
+eval-decompose : ∀ (π : Permutation′ n) → eval (decompose π) ≈ π
+eval-decompose {suc n} π i = begin
+  tπ0 ∘ₚ eval (lift₀ (decompose (remove 0F (t0π ∘ₚ π))))   ⟨$⟩ʳ i ≡⟨ eval-lift (decompose (remove 0F (t0π ∘ₚ π))) (tπ0 ⟨$⟩ʳ i) ⟩
+  tπ0 ∘ₚ P.lift₀ (eval (decompose (remove 0F (t0π ∘ₚ π)))) ⟨$⟩ʳ i ≡⟨ lift₀-cong _ _ (eval-decompose _) (tπ0 ⟨$⟩ʳ i) ⟩
+  tπ0 ∘ₚ P.lift₀ (remove 0F (t0π ∘ₚ π))                    ⟨$⟩ʳ i ≡⟨ lift₀-remove (t0π ∘ₚ π) (inverseʳ π) (tπ0 ⟨$⟩ʳ i) ⟩
+  tπ0 ∘ₚ t0π ∘ₚ π                                          ⟨$⟩ʳ i ≡⟨ cong (π ⟨$⟩ʳ_) (PC.transpose-inverse 0F (π ⟨$⟩ˡ 0F)) ⟩
+  π                                                        ⟨$⟩ʳ i ∎
+  where
+  tπ0 = transpose (π ⟨$⟩ˡ 0F) 0F
+  t0π = transpose 0F (π ⟨$⟩ˡ 0F)