------------------------------------------------------------------------
-- The Agda standard library
--
-- Component functions of permutations found in `Data.Fin.Permutation`
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --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."
#-}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4