------------------------------------------------------------------------
-- The Agda standard library
--
-- Component functions of permutations found in `Data.Fin.Permutation`
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe #-}

module Data.Fin.Permutation.Components where

open import Data.Bool.Base using (Bool; true; false)
open import Data.Fin.Base using (Fin; suc; opposite; toℕ)
open import Data.Fin.Properties
  using (_≡?_; ≡?-≡; ≡?-≡-refl
        ; opposite-prop; opposite-involutive; opposite-suc)
open import Relation.Nullary.Decidable.Core using (does; yes; no)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym)

------------------------------------------------------------------------
--  Functions
------------------------------------------------------------------------

-- 'transpose i j' swaps the places of 'i' and 'j'.

transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
transpose i j k with does (k ≡? i)
... | true  = j
... | false with does (k ≡? j)
...   | true  = i
...   | false = k

------------------------------------------------------------------------
--  Properties
------------------------------------------------------------------------

transpose[i,i,j]≡j : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
transpose[i,i,j]≡j i j with j ≡? i in j≡?i
... | yes j≡i           = sym j≡i
... | no  _ rewrite j≡?i = refl

transpose[i,j,j]≡i : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
transpose[i,j,j]≡i i j with j ≡? i
... | yes j≡i                     = j≡i
... | no  _ rewrite ≡?-≡-refl j = refl

transpose[i,j,i]≡j : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
transpose[i,j,i]≡j i j rewrite ≡?-≡-refl i = refl

transpose-transpose : ∀ {n} {i j k l : Fin n} →
                      transpose i j k ≡ l → transpose j i l ≡ k
transpose-transpose {n} {i} {j} {k} {l} eq with k ≡? i in k≡?i
... | yes k≡i rewrite ≡?-≡ (sym eq) = sym k≡i
... | no k≢i with k ≡? j in k≡?j
...   | yes k≡j rewrite eq | transpose[i,j,j]≡i j l = sym k≡j
...   | no  k≢j rewrite eq | k≡?j | k≡?i = refl

transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                    transpose i j (transpose j i k) ≡ k
transpose-inverse i j = transpose-transpose refl


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

reverse = opposite
{-# WARNING_ON_USAGE reverse
"Warning: reverse was deprecated in v2.0.
Please use opposite from Data.Fin.Base instead."
#-}

reverse-prop = opposite-prop
{-# WARNING_ON_USAGE reverse-prop
"Warning: reverse-prop was deprecated in v2.0.
Please use opposite-prop from Data.Fin.Properties instead."
#-}

reverse-involutive = opposite-involutive
{-# WARNING_ON_USAGE reverse-involutive
"Warning: reverse-involutive was deprecated in v2.0.
Please use opposite-involutive from Data.Fin.Properties instead."
#-}

reverse-suc : ∀ {n} {i : Fin n} → toℕ (opposite (suc i)) ≡ toℕ (opposite i)
reverse-suc {i = i} = opposite-suc i
{-# WARNING_ON_USAGE reverse-suc
"Warning: reverse-suc was deprecated in v2.0.
Please use opposite-suc from Data.Fin.Properties instead."
#-}