------------------------------------------------------------------------
-- The Agda standard library
--
-- Decomposition of permutations into a list of transpositions.
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Fin.Permutation.Transposition.List where

open import Data.Fin.Base using (Fin; suc)
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.Base using (List; []; _∷_; map)
open import Data.Nat.Base using (ℕ; suc; zero)
open import Data.Product.Base using (_×_; _,_)
open import Function.Base using (_∘_)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; sym; cong)
open import Relation.Binary.PropositionalEquality.Properties
  using (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)