Some lemmas to do with transposition lists

CHANGELOG.md

@@ -783,6 +783,18 @@ Non-backwards compatible changes
     ```
 
 
+* In `Data.Fin.Permutation.Transposition.List`, the transpositions are now restricted
+  to being pairs of distinct elements.
+
+  Previously:
+  ```agda
+  TranspositionList n = List (Fin n × Fin n)
+  ```
+  Now:
+  ```agda
+  TranspositionList n = List (∃₂ λ (i j : Fin n) → i ≢ j)
+  ```
+
 Major improvements
 ------------------
 
@@ -1863,6 +1875,7 @@ Other minor changes
 * Added new definitions and proofs in `Data.Fin.Permutation`:
   ```agda
   insert         : Fin (suc m) → Fin (suc n) → Permutation m n → Permutation (suc m) (suc n)
+  transpose-comm : transpose i j ≈ transpose j i
   insert-punchIn : insert i j π ⟨$⟩ʳ punchIn i k ≡ punchIn j (π ⟨$⟩ʳ k)
   insert-remove  : insert i (π ⟨$⟩ʳ i) (remove i π) ≈ π
   remove-insert  : remove i (insert i j π) ≈ π
@@ -1915,6 +1928,12 @@ Other minor changes
   cast-trans    : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
   ```
 
+* Added new proofs in `Data.Fin.Permutation.Transposition.List`:
+  ```agda
+  eval-++ : eval (xs ++ ys) ≈ eval xs ∘ₚ eval ys
+  eval-reverse : eval (reverse xs) ≈ flip (eval xs)
+  ```
+
 * Added new functions in `Data.Integer.Base`:
   ```
   _^_ : ℤ → ℕ → ℤ

src/Data/Fin/Permutation.agda

@@ -223,6 +223,13 @@ insert {m} {n} i j π = permutation to from inverseˡ′ inverseʳ′
 ------------------------------------------------------------------------
 -- Other properties
 
+transpose-comm : ∀ (i j : Fin n) → transpose i j ≈ transpose j i
+transpose-comm i j k with k ≟ i | k ≟ j
+... | no ¬p | no ¬q = refl
+... | no ¬p | yes q = refl
+... | yes p | no ¬q = refl
+... | yes p | yes q = trans (sym q) p
+
 module _ (π : Permutation (suc m) (suc n)) where
   private
     πʳ = π ⟨$⟩ʳ_

src/Data/Fin/Permutation/Components.agda

@@ -8,7 +8,7 @@
 
 module Data.Fin.Permutation.Components where
 
-open import Data.Bool.Base using (Bool; true; false)
+open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Fin.Base
 open import Data.Fin.Properties
 open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
@@ -28,17 +28,32 @@ open ≡-Reasoning
 
 -- 'tranpose 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
+transpose i j k with does (k ≟ i) | does (k ≟ j)
+... | true | _ = j
+... | false | true = i
+... | false | false = k
+-}
+
+transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
+transpose i j k = if does (k ≟ i)
+  then j
+  else if does (k ≟ j)
+    then i
+    else k
 
 --------------------------------------------------------------------------------
 --  Properties
 --------------------------------------------------------------------------------
 
+transpose-comm : ∀ {n} (i j : Fin  n) → transpose i j ≗ transpose j i
+transpose-comm i j k with k ≟ i | k ≟ j
+... | no  _   | no  _   = refl
+... | no  _   | yes _   = refl
+... | yes _   | no  _   = refl
+... | yes k≡i | yes k≡j = trans (sym k≡j) k≡i
+
 transpose-inverse : ∀ {n} (i j : Fin n) {k} →
                     transpose i j (transpose j i k) ≡ k
 transpose-inverse i j {k} with k ≟ j
@@ -51,6 +66,23 @@ transpose-inverse i j {k} with k ≟ j
 ...   | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
                                   | dec-false (k ≟ j) (invert [k≢j]) = refl
 
+transpose-inverse′ : ∀ {n} (i j : Fin n) {k} → transpose i j (transpose i j k) ≡ k
+transpose-inverse′ i j {k} with k ≟ i
+transpose-inverse′ i j {k} | yes k≡i with j ≟ i
+... | yes j≡i = trans j≡i (sym k≡i)
+... | no  j≢i rewrite dec-true (j ≟ j) refl = sym k≡i
+transpose-inverse′ i j {k} | no  k≢i with k ≟ j
+... | yes k≡j rewrite dec-true (i ≟ i) refl = sym k≡j
+... | no  k≢j rewrite dec-false (k ≟ i) k≢i rewrite dec-false (k ≟ j) k≢j = refl
+
+transpose-matchˡ : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
+transpose-matchˡ i j rewrite dec-true (i ≟ i) refl = refl
+
+transpose-matchʳ : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
+transpose-matchʳ i j with j ≟ i
+... | yes j≡i = j≡i
+... | no  j≢i rewrite dec-true (j ≟ j) refl = refl
+
 ------------------------------------------------------------------------
 -- DEPRECATED NAMES
 ------------------------------------------------------------------------

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

@@ -8,16 +8,25 @@
 
 module Data.Fin.Permutation.Transposition.List where
 
+open import Data.Bool.Base
 open import Data.Fin.Base
 open import Data.Fin.Patterns using (0F)
 open import Data.Fin.Permutation as P hiding (lift₀)
+open import Data.Fin.Properties using (_≟_; suc-injective)
 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 Data.List as L using (List; []; _∷_; _++_; map)
+import Data.List.Membership.DecPropositional as L∈
+import Data.List.Properties as L
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Data.Nat.Base as ℕ using (ℕ; suc; zero; parity)
+import Data.Nat.Properties as ℕ
+open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ)
+open import Data.Product using (Σ-syntax; ∃₂; _×_; _,_; proj₁; proj₂)
+open import Function.Base hiding (id; flip)-- using (_∘_)
+open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Nullary.Decidable hiding (map)
 open import Relation.Binary.PropositionalEquality
-  using (_≡_; sym; cong; module ≡-Reasoning)
+  using (_≡_; _≢_; refl; sym; trans; cong; module ≡-Reasoning)
 open ≡-Reasoning
 
 private
@@ -29,43 +38,208 @@ private
 
 -- 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).
+-- instead inducting on the list of transpositions, where a
+-- transposition is a permutation swapping two distinct elements and
+-- leaving the rest in place).
 
 TranspositionList : ℕ → Set
-TranspositionList n = List (Fin n × Fin n)
+TranspositionList n = List (∃₂ λ (i j : Fin n) → i ≢ j)
 
 ------------------------------------------------------------------------
 -- Operations on transposition lists
 
 lift₀ : TranspositionList n → TranspositionList (suc n)
-lift₀ xs = map (λ (i , j) → (suc i , suc j)) xs
+lift₀ xs = map (λ (i , j , i≢j) → (suc i , suc j , i≢j ∘ suc-injective)) xs
 
 eval : TranspositionList n → Permutation′ n
 eval []             = id
-eval ((i , j) ∷ xs) = transpose i j ∘ₚ eval xs
+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)) ∘ₚ π)))
+decompose {suc n} π with π ⟨$⟩ˡ 0F
+... | 0F = lift₀ (decompose (remove 0F π))
+... | x@(suc _) = (x , 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
+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 ∎
+eval-decompose {suc n} π i with π ⟨$⟩ˡ 0F in p
+... | 0F = begin
+  eval (lift₀ (decompose (remove 0F π)))   ⟨$⟩ʳ i ≡⟨ eval-lift (decompose (remove 0F π)) i ⟩
+  P.lift₀ (eval (decompose (remove 0F π))) ⟨$⟩ʳ i ≡⟨ lift₀-cong _ _ (eval-decompose (remove 0F π)) i ⟩
+  P.lift₀ (remove 0F π)                    ⟨$⟩ʳ i ≡⟨ lift₀-remove π (trans (cong (π ⟨$⟩ʳ_) (sym p)) (P.inverseʳ π)) i ⟩
+  π                                        ⟨$⟩ʳ i ∎
+... | x@(suc _) = begin
+  tx0 ∘ₚ eval (lift₀ (decompose (remove 0F (t0π ∘ₚ π))))   ⟨$⟩ʳ i ≡⟨ eval-lift (decompose (remove 0F (t0π ∘ₚ π))) (tx0 ⟨$⟩ʳ i) ⟩
+  tx0 ∘ₚ P.lift₀ (eval (decompose (remove 0F (t0π ∘ₚ π)))) ⟨$⟩ʳ i ≡⟨ lift₀-cong _ _ (eval-decompose _) (tx0 ⟨$⟩ʳ i) ⟩
+  tx0 ∘ₚ P.lift₀ (remove 0F (t0π ∘ₚ π))                    ⟨$⟩ʳ i ≡⟨ lift₀-remove (t0π ∘ₚ π) (inverseʳ π) (tx0 ⟨$⟩ʳ i) ⟩
+  tx0 ∘ₚ t0π ∘ₚ π                                          ⟨$⟩ʳ i ≡⟨ cong (λ x′ → tx0 ∘ₚ transpose 0F x′ ∘ₚ π ⟨$⟩ʳ i) p ⟩
+  tx0 ∘ₚ transpose 0F x ∘ₚ π                               ⟨$⟩ʳ i ≡⟨ cong (π ⟨$⟩ʳ_) (PC.transpose-inverse 0F x) ⟩
+  π                                                       ⟨$⟩ʳ i ∎
+    where
+      tx0 = transpose x 0F
+      t0π = transpose 0F (π ⟨$⟩ˡ 0F)
+
+eval-++ : ∀ (xs ys : TranspositionList n) → eval (xs ++ ys) ≈ eval xs ∘ₚ eval ys
+eval-++ [] ys i = refl
+eval-++ ((a , b , _) ∷ xs) ys i = eval-++ xs ys (transpose a b ⟨$⟩ʳ i)
+
+eval-reverse : ∀ (xs : TranspositionList n) → eval (L.reverse xs) ≈ flip (eval xs)
+eval-reverse [] i = refl
+eval-reverse (x@(a , b , _) ∷ xs) i = begin
+  eval (L.reverse (x ∷ xs))            ⟨$⟩ʳ i ≡⟨ cong (λ p → eval p ⟨$⟩ʳ i) (L.unfold-reverse x xs) ⟩
+  eval (L.reverse xs L.∷ʳ x)           ⟨$⟩ʳ i ≡⟨ eval-++ (L.reverse xs) L.[ x ] i ⟩
+  eval (L.reverse xs) ∘ₚ transpose a b ⟨$⟩ʳ i ≡⟨ cong (transpose a b ⟨$⟩ʳ_) (eval-reverse xs i) ⟩
+  flip (eval xs) ∘ₚ transpose a b      ⟨$⟩ʳ i ≡⟨ transpose-comm a b (flip (eval xs) ⟨$⟩ʳ i) ⟩
+  flip (eval xs) ∘ₚ transpose b a      ⟨$⟩ʳ i ∎
+
+-- Properties of transposition lists that evaluate to the identity
+
+eval[xs]≈id⇒length[xs]≢1 : ∀ (xs : TranspositionList n) → eval xs ≈ id → L.length xs ≢ 1
+eval[xs]≈id⇒length[xs]≢1 [] _ = λ ()
+eval[xs]≈id⇒length[xs]≢1 ((i , j , i≢j) ∷ []) p with j≡i ← p i rewrite dec-true (i ≟ i) refl = contradiction (sym j≡i) i≢j
+eval[xs]≈id⇒length[xs]≢1 (_ ∷ _ ∷ _) _ = λ ()
+
+-- this is the workhorse of the parity theorem!
+-- If we have a representation of the identity permutations in 2 + k transpositions we can find one in k transpositions
+p₂ : ∀ (xs : TranspositionList n) → eval xs ≈ id → ∀ {k} → L.length xs ≡ 2 ℕ.+ k → Σ[ ys ∈ TranspositionList n ] (eval ys ≈ id × L.length ys ≡ k)
+p₂ {n = n} ((i₀ , j , i₀≢j) ∷ xs₀) p q = let (ys , r , s) = machine i₀ i₀≢j xs₀ xs₀[i₀]≡j xs₀[j]≡i₀ (ℕ.suc-injective q) in ys , (λ k → trans (sym (r k)) (p k)) , s
   where
-  tπ0 = transpose (π ⟨$⟩ˡ 0F) 0F
-  t0π = transpose 0F (π ⟨$⟩ˡ 0F)
+    xs₀[i₀]≡j : eval xs₀ ⟨$⟩ʳ i₀ ≡ j
+    xs₀[i₀]≡j = begin
+      eval xs₀ ⟨$⟩ʳ i₀                  ≡˘⟨ cong (eval xs₀ ⟨$⟩ʳ_) (PC.transpose-matchʳ i₀ j) ⟩
+      transpose i₀ j ∘ₚ eval xs₀ ⟨$⟩ʳ j ≡⟨ p j ⟩
+      j                                 ∎
+
+    xs₀[j]≡i₀ : eval xs₀ ⟨$⟩ʳ j ≡ i₀
+    xs₀[j]≡i₀ = begin
+      eval xs₀ ⟨$⟩ʳ j                    ≡˘⟨ cong (eval xs₀ ⟨$⟩ʳ_) (PC.transpose-matchˡ i₀ j) ⟩
+      transpose i₀ j ∘ₚ eval xs₀ ⟨$⟩ʳ i₀ ≡⟨ p i₀ ⟩
+      i₀                                 ∎
+
+    open L∈ _≟_
+
+    machine :  ∀ (i : Fin n) (i≢j : i ≢ j) (xs : TranspositionList n) → eval xs ⟨$⟩ʳ i ≡ j → eval xs ⟨$⟩ʳ j ≡ i → ∀ {k} → L.length xs ≡ 1 ℕ.+ k → Σ[ ys ∈ TranspositionList n ] transpose i j ∘ₚ eval xs ≈ eval ys × L.length ys ≡ k
+    machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j xs[j]≡i {k} 1+∣xs∣≡1+k with iₕ ∈? i ∷ j ∷ []
+    machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j xs[j]≡i {k} 1+∣xs∣≡1+k | no ¬p with jₕ ∈? i ∷ j ∷ []
+    ... | no ¬q
+      rewrite dec-false (i ≟ iₕ) λ i≡iₕ → ¬p (here (sym i≡iₕ))
+      rewrite dec-false (i ≟ jₕ) λ i≡jₕ → ¬q (here (sym i≡jₕ))
+      rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
+      rewrite dec-false (j ≟ jₕ) λ j≡jₕ → ¬q (there (here (sym j≡jₕ)))
+      = (iₕ , jₕ , iₕ≢jₕ) ∷ ys , ys′-eval , trans (cong suc (proj₂ (proj₂ rec))) (ℕ.suc-pred k {{ℕ.≢-nonZero k≢0}})
+      where
+        xs≢[] : xs ≢ []
+        xs≢[] refl = i≢j xs[i]≡j
+
+        k≢0 : k ≢ 0
+        k≢0 k≡0 = xs≢[] (L.length[xs]≡0⇒xs≡[] (trans (ℕ.suc-injective 1+∣xs∣≡1+k) k≡0))
+
+        k′ : ℕ
+        k′ = ℕ.pred k
+
+        rec = machine i i≢j xs xs[i]≡j xs[j]≡i {k′} (trans (ℕ.suc-injective 1+∣xs∣≡1+k) (sym (ℕ.suc-pred k {{ℕ.≢-nonZero k≢0}})))
+
+        ys : TranspositionList n
+        ys = proj₁ rec
+
+        ys-eval : transpose i j ∘ₚ eval xs ≈ eval ys
+        ys-eval = proj₁ (proj₂ rec)
+
+        ys′-eval : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ transpose iₕ jₕ ∘ₚ eval ys
+        ys′-eval k with k ∈? i ∷ j ∷ iₕ ∷ jₕ ∷ []
+        ... | no ¬r
+          with ys[k] ← ys-eval k
+          rewrite dec-false (k ≟ i)  λ k≡i  → ¬r (here k≡i)
+          rewrite dec-false (k ≟ j)  λ k≡j  → ¬r (there (here k≡j))
+          rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬r (there (there (here k≡iₕ)))
+          rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬r (there (there (there (here k≡jₕ))))
+          = ys[k]
+        ... | yes (here k≡i)
+          with ys[k] ← ys-eval k
+          rewrite dec-true  (k ≟ i) k≡i
+          rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬p (here (trans (sym k≡iₕ) k≡i))
+          rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬q (here (trans (sym k≡jₕ) k≡i))
+          rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
+          rewrite dec-false (j ≟ jₕ) λ j≡jₕ → ¬q (there (here (sym j≡jₕ)))
+          = ys[k]
+        ... | yes (there (here k≡j))
+          with ys[k] ← ys-eval k
+          rewrite dec-false (k ≟ i)  λ k≡i  → i≢j (trans (sym k≡i) k≡j)
+          rewrite dec-true  (k ≟ j) k≡j
+          rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬p (there (here (trans (sym k≡iₕ) k≡j)))
+          rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬q (there (here (trans (sym k≡jₕ) k≡j)))
+          rewrite dec-false (i ≟ iₕ) λ i≡iₕ → ¬p (here (sym i≡iₕ))
+          rewrite dec-false (i ≟ jₕ) λ i≡jₕ → ¬q (here (sym i≡jₕ))
+          = ys[k]
+        ... | yes (there (there (here k≡iₕ)))
+          with ys[jₕ] ← ys-eval jₕ
+          rewrite dec-false (k ≟ i)  λ k≡i  → ¬p (here (trans (sym k≡iₕ) k≡i))
+          rewrite dec-false (k ≟ j)  λ k≡j  → ¬p (there (here (trans (sym k≡iₕ) k≡j)))
+          rewrite dec-true  (k ≟ iₕ) k≡iₕ
+          rewrite dec-false (jₕ ≟ i) λ jₕ≡i → ¬q (here jₕ≡i)
+          rewrite dec-false (jₕ ≟ j) λ jₕ≡j → ¬q (there (here jₕ≡j))
+          = ys[jₕ]
+        ... | yes (there (there (there (here k≡jₕ))))
+          with ys[iₕ] ← ys-eval iₕ
+          rewrite dec-false (k ≟ i)  λ k≡i  → ¬q (here (trans (sym k≡jₕ) k≡i))
+          rewrite dec-false (k ≟ j)  λ k≡j  → ¬q (there (here (trans (sym k≡jₕ) k≡j)))
+          rewrite dec-false (k ≟ iₕ) λ k≡iₕ → iₕ≢jₕ (trans (sym k≡iₕ) k≡jₕ)
+          rewrite dec-true  (k ≟ jₕ) k≡jₕ
+          rewrite dec-false (iₕ ≟ i) λ iₕ≡i → ¬p (here iₕ≡i)
+          rewrite dec-false (iₕ ≟ j) λ iₕ≡j → ¬p (there (here iₕ≡j))
+          = ys[iₕ]
+    ... | yes (here jₕ≡i)
+      rewrite dec-false (i ≟ iₕ) λ i≡iₕ → iₕ≢jₕ (sym (trans jₕ≡i i≡iₕ))
+      rewrite dec-true  (i ≟ jₕ) (sym jₕ≡i)
+      rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
+      rewrite dec-false (j ≟ jₕ) λ j≡jₕ → i≢j (sym (trans j≡jₕ jₕ≡i))
+      = {!!}
+      where
+        xs≢[] : xs ≢ []
+        xs≢[] refl = i≢j (sym xs[j]≡i)
+
+        k≢0 : k ≢ 0
+        k≢0 k≡0 = xs≢[] (L.length[xs]≡0⇒xs≡[] (trans (ℕ.suc-injective 1+∣xs∣≡1+k) k≡0))
+
+        k′ : ℕ
+        k′ = ℕ.pred k
+
+        rec = machine iₕ (λ iₕ≡j → ¬p (there (here iₕ≡j))) xs xs[i]≡j {!xs[j]≡i!} {k′} {!!}
+
+
+    ... | yes (there (here jₕ≡j)) = {!!}
+    machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j {k} 1+∣xs∣≡1+k | yes (here iₕ≡i) with jₕ ≟ j
+    ... | no jₕ≢j = {!!}
+    ... | yes jₕ≡j = xs , prop , ℕ.suc-injective 1+∣xs∣≡1+k
+      where
+        prop : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ eval xs
+        prop k rewrite iₕ≡i rewrite jₕ≡j = cong (eval xs ⟨$⟩ʳ_) (PC.transpose-inverse′ i j)
+    machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j {k} 1+∣xs∣≡1+k | yes (there (here iₕ≡j)) with jₕ ≟ i
+    ... | no jₕ≢i = {!!}
+    ... | yes jₕ≡i = xs , prop , ℕ.suc-injective 1+∣xs∣≡1+k
+      where
+        prop : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ eval xs
+        prop k rewrite iₕ≡j rewrite jₕ≡i = cong (eval xs ⟨$⟩ʳ_) (PC.transpose-inverse j i)
+
+{-
+
+p₃ : ∀ (xs : TranspositionList n) → eval xs ≈ id → parity (L.length xs) ≡ 0ℙ
+p₃ [] p = refl
+p₃ xs@(_ ∷ []) p = contradiction refl (eval[xs]≈id⇒length[xs]≢1 xs p)
+p₃ xs@(_ ∷ _ ∷ _) p with p₂ xs p refl
+... | ys , p′ , ys-shorter = {!parity (L.length ys)!}
+
+p₄ : ∀ (xs ys : TranspositionList n) → eval xs ≈ eval ys → parity (L.length xs) ≡ parity (L.length ys)
+p₄ = {!!}
+-}

src/Data/List/Properties.agda

@@ -75,6 +75,9 @@ module _ {x y : A} {xs ys : List A} where
 ≡-dec _≟_ []       (y ∷ ys) = no λ()
 ≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys)
 
+length[xs]≡0⇒xs≡[] : {xs : List A} → length xs ≡ 0 → xs ≡ []
+length[xs]≡0⇒xs≡[] {xs = []} _ = refl
+
 ------------------------------------------------------------------------
 -- map