refactor: add new lemmas, simplify old proof

Author: jamesmckinna

CHANGELOG.md

@@ -237,6 +237,14 @@ Additions to existing modules
   ∙-cong-∣ : x ∣ y → a ∣ b → x ∙ a ∣ y ∙ b
   ```
 
+* In `Data.Fin.Permutation.Components`:
+  ```agda
+  transpose-iij : (i j : Fin n) → transpose i i j ≡ j
+  transpose-ijj : (i j : Fin n) → transpose i j j ≡ i
+  transpose-iji : (i j : Fin n) → transpose i j i ≡ j
+  transpose-transpose : transpose i j k ≡ l → transpose j i l ≡ k
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   ≡-irrelevant : Irrelevant {A = Fin n} _≡_

src/Data/Fin/Permutation/Components.agda

@@ -11,25 +11,18 @@ 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 (_≟_; opposite-prop; opposite-involutive; opposite-suc)
-open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
-open import Data.Product.Base using (proj₂)
-open import Function.Base using (_∘_)
+  using (_≟_; ≟-diag; ≟-diag-refl
+        ; opposite-prop; opposite-involutive; opposite-suc)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (does; _because_; yes; no)
-open import Relation.Nullary.Decidable using (dec-true; dec-false)
+open import Relation.Nullary.Decidable.Core using (does; _because_)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; trans)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-open import Algebra.Definitions using (Involutive)
-open ≡-Reasoning
+  using (_≡_; refl; sym)
 
 ------------------------------------------------------------------------
 --  Functions
 ------------------------------------------------------------------------
 
--- 'tranpose i j' swaps the places of 'i' and 'j'.
+-- '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)
@@ -42,17 +35,31 @@ transpose i j k with does (k ≟ i)
 --  Properties
 ------------------------------------------------------------------------
 
+transpose-iij : ∀ {n} (i j : Fin n) → transpose i i j ≡ j
+transpose-iij i j with j ≟ i in j≟i
+... | true  because [j≡i] = sym (invert [j≡i])
+... | false because _ rewrite j≟i = refl
+
+transpose-ijj : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
+transpose-ijj i j with j ≟ i
+... | true  because [j≡i] = invert [j≡i]
+... | false because _ rewrite ≟-diag-refl j = refl
+
+transpose-iji : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
+transpose-iji i j rewrite ≟-diag-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
+... | true  because [k≡i] rewrite ≟-diag (sym eq) = sym (invert [k≡i])
+... | false because [k≢i] with k ≟ j in k≟j
+...   | true  because [k≡j] rewrite eq | transpose-ijj j l = sym (invert [k≡j])
+...   | false because [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 {k} with k ≟ j
-... | true  because [k≡j] rewrite dec-true (i ≟ i) refl = sym (invert [k≡j])
-... | false because [k≢j] with k ≟ i
-...   | true  because [k≡i]
-        rewrite dec-false (j ≟ i) (invert [k≢j] ∘ trans (invert [k≡i]) ∘ sym)
-                | dec-true (j ≟ j) refl
-                = sym (invert [k≡i])
-...   | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
-                                  | dec-false (k ≟ j) (invert [k≢j]) = refl
+transpose-inverse i j = transpose-transpose refl
+
 
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES