1 files changed, 217 insertions, 0 deletions
diff --git a/Data/Permutation.agda b/Data/Permutation.agda
new file mode 100644
index 0000000..55c8748
--- /dev/null
+++ b/Data/Permutation.agda
@@ -0,0 +1,217 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Data.Permutation {ℓ : Level} {A : Set ℓ} where
+
+import Data.Fin as Fin
+import Data.Fin.Properties as FinProp
+import Data.Fin.Permutation as ↔-Fin
+import Data.List as List
+import Data.List.Properties as ListProp
+import Data.List.Relation.Binary.Permutation.Propositional as ↭-List
+import Data.Nat as Nat
+import Data.Vec.Functional as Vector
+import Data.Vec.Functional.Properties as VectorProp
+import Data.Vec.Functional.Relation.Binary.Permutation as ↭-Vec
+import Data.Vec.Functional.Relation.Binary.Permutation.Properties as ↭-VecProp
+
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Vec.Functional.Relation.Unary.Any using (Any)
+open import Function.Base using (_∘_)
+
+open ↭-Vec using () renaming (_↭_ to _↭′_)
+open ↭-List using (_↭_; ↭-sym; module PermutationReasoning)
+open ↔-Fin using (Permutation; _⟨$⟩ˡ_; _⟨$⟩ʳ_)
+open List using (List) hiding (module List)
+open Fin using (Fin; cast) hiding (module Fin)
+open Vector using (Vector; toList; fromList)
+open Fin.Fin
+open Nat using (ℕ; zero; suc)
+open _↭_
+
+module _ where
+
+  open Fin using (#_)
+  open ↔-Fin using (lift₀; insert)
+  open ↭-VecProp using (↭-refl; ↭-trans)
+
+  -- convert a List permutation to a Vector permutation
+  fromList-↭
+      : {xs ys : List A}
+      → xs ↭ ys
+      → fromList xs ↭′ fromList ys
+  fromList-↭ refl = ↭-refl
+  fromList-↭ (prep _ xs↭ys)
+    with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = lift₀ n↔m , λ where
+      zero → ≡.refl
+      (suc i) → xs↭ys′ i
+  fromList-↭ (swap x y xs↭ys)
+    with n↔m , xs↭ys′ ← fromList-↭ xs↭ys = insert (# 0) (# 1) (lift₀ n↔m) , λ where
+      zero → ≡.refl
+      (suc zero) → ≡.refl
+      (suc (suc i)) → xs↭ys′ i
+  fromList-↭ (trans {xs} xs↭ys ys↭zs) =
+      ↭-trans {_} {_} {_} {i = fromList xs} (fromList-↭ xs↭ys) (fromList-↭ ys↭zs)
+
+-- witness for an element in a Vector
+_∈_ : A → {n : ℕ} → Vector A n → Set ℓ
+x ∈ xs = Any (x ≡_) xs
+
+-- apply a permutation to a witness
+apply
+    : {n m : ℕ}
+      {xs : Vector A n}
+      {ys : Vector A m}
+      {x : A}
+    → (xs↭ys : xs ↭′ ys)
+    → x ∈ xs
+    → x ∈ ys
+apply {suc n} {zero} (↔n , _) (i , _) with () ← ↔n ⟨$⟩ˡ i
+apply {suc n} {suc m} {xs} {ys} {x} (↔n , ↔≗) (i , x≡xs-i) = i′ , x≡ys-i′
+  where
+    i′ : Fin (suc m)
+    i′ = ↔n ⟨$⟩ˡ i
+    open ≡.≡-Reasoning
+    x≡ys-i′ : x ≡ ys i′
+    x≡ys-i′ = begin
+      x                         ≡⟨ x≡xs-i ⟩
+      xs i                      ≡⟨ ≡.cong xs (↔-Fin.inverseʳ ↔n) ⟨
+      xs (↔n ⟨$⟩ʳ (↔n ⟨$⟩ˡ i))  ≡⟨⟩
+      xs (↔n ⟨$⟩ʳ i′)           ≡⟨ ↔≗ i′ ⟩
+      ys i′                     ∎
+
+-- remove an element from a Vector
+remove : {n : ℕ} {x : A} (xs : Vector A (suc n)) → x ∈ xs → Vector A n
+remove xs (i , _) = Vector.removeAt xs i
+
+-- remove an element and its image from a permutation
+↭-remove
+    : {n m : ℕ}
+      {xs : Vector A (suc n)}
+      {ys : Vector A (suc m)}
+      {x : A}
+    → (xs↭ys : xs ↭′ ys)
+    → (x∈xs : x ∈ xs)
+    → let x∈ys = apply xs↭ys x∈xs in
+      remove xs x∈xs ↭′ remove ys x∈ys
+↭-remove {n} {m} {xs} {ys} {x} xs↭ys@(ρ , ↔≗) x∈xs@(k , _) = ρ⁻ , ↔≗⁻
+  where
+    k′ : Fin (suc m)
+    k′ = ρ ⟨$⟩ˡ k
+    x∈ys : x ∈ ys
+    x∈ys = apply xs↭ys x∈xs
+    ρ⁻ : Permutation m n
+    ρ⁻ = ↔-Fin.remove k′ ρ
+    xs⁻ : Vector A n
+    xs⁻ = remove xs x∈xs
+    ys⁻ : Vector A m
+    ys⁻ = remove ys x∈ys
+    open ≡.≡-Reasoning
+    open Fin using (punchIn)
+    ↔≗⁻ : (i : Fin m) → xs⁻ (ρ⁻ ⟨$⟩ʳ i) ≡ ys⁻ i
+    ↔≗⁻ i = begin
+        xs⁻ (ρ⁻ ⟨$⟩ʳ i)             ≡⟨⟩
+        remove xs x∈xs (ρ⁻ ⟨$⟩ʳ i)  ≡⟨⟩
+        xs (punchIn k (ρ⁻ ⟨$⟩ʳ i))  ≡⟨ ≡.cong xs (↔-Fin.punchIn-permute′ ρ k i) ⟨
+        xs (ρ ⟨$⟩ʳ (punchIn k′ i))  ≡⟨ ↔≗ (punchIn k′ i) ⟩
+        ys (punchIn k′ i)           ≡⟨⟩
+        remove ys x∈ys i            ≡⟨⟩
+        ys⁻ i                       ∎
+
+open List.List
+open List using (length; insertAt)
+
+-- build a permutation which moves the first element of a list to an arbitrary position
+↭-insert-half
+    : {x₀ : A}
+      {xs : List A}
+    → (i : Fin (suc (length xs)))
+    → x₀ ∷ xs ↭ insertAt xs i x₀
+↭-insert-half zero = refl
+↭-insert-half {x₀} {x₁ ∷ xs} (suc i) = trans (swap x₀ x₁ refl) (prep x₁ (↭-insert-half i))
+
+-- add a mapping to a permutation, given a value and its start and end positions
+↭-insert
+    : {xs ys : List A}
+    → xs ↭ ys
+    → (i : Fin (suc (length xs)))
+      (j : Fin (suc (length ys)))
+      (x : A)
+    → insertAt xs i x ↭ insertAt ys j x
+↭-insert {xs} {ys} xs↭ys i j x = xs↭ys⁺
+  where
+    open PermutationReasoning
+    xs↭ys⁺ : insertAt xs i x ↭ insertAt ys j x
+    xs↭ys⁺ = begin
+      insertAt xs i x ↭⟨ ↭-insert-half i ⟨
+      x ∷ xs          <⟨ xs↭ys ⟩
+      x ∷ ys          ↭⟨ ↭-insert-half j ⟩
+      insertAt ys j x ∎
+
+open ListProp using (length-tabulate; tabulate-cong)
+insertAt-toList
+    : {n : ℕ}
+      {v : Vector A n}
+      (i : Fin (suc (length (toList v))))
+      (i′ : Fin (suc n))
+    → i ≡ cast (≡.cong suc (≡.sym (length-tabulate v))) i′
+    → (x : A)
+    → insertAt (toList v) i x
+    ≡ toList (Vector.insertAt v i′ x)
+insertAt-toList zero zero _ x = ≡.refl
+insertAt-toList {suc n} {v} (suc i) (suc i′) ≡.refl x =
+    ≡.cong (v zero ∷_) (insertAt-toList i i′ ≡.refl x)
+
+-- convert a Vector permutation to a List permutation
+toList-↭
+    : {n m : ℕ}
+      {xs : Vector A n}
+      {ys : Vector A m}
+    → xs ↭′ ys
+    → toList xs ↭ toList ys
+toList-↭ {zero} {zero} _ = refl
+toList-↭ {zero} {suc m} (ρ , _) with () ← ρ ⟨$⟩ʳ zero
+toList-↭ {suc n} {zero} (ρ , _) with () ← ρ ⟨$⟩ˡ zero
+toList-↭ {suc n} {suc m} {xs} {ys} xs↭ys′ = xs↭ys
+  where
+    -- first element and its image
+    x₀ : A
+    x₀ = xs zero
+    x₀∈xs : x₀ ∈ xs
+    x₀∈xs = zero , ≡.refl
+    x₀∈ys : x₀ ∈ ys
+    x₀∈ys = apply xs↭ys′ x₀∈xs
+    -- reduce the problem by removing those elements
+    xs⁻ : Vector A n
+    xs⁻ = remove xs x₀∈xs
+    ys⁻ : Vector A m
+    ys⁻ = remove ys x₀∈ys
+    xs↭ys⁻ : xs⁻ ↭′ ys⁻
+    xs↭ys⁻ = ↭-remove xs↭ys′ x₀∈xs
+    -- recursion on the reduced problem
+    xs↭ys⁻′ : toList xs⁻ ↭ toList ys⁻
+    xs↭ys⁻′ = toList-↭ xs↭ys⁻
+    -- indices for working with vectors
+    i : Fin (suc n)
+    i = proj₁ x₀∈xs
+    j : Fin (suc m)
+    j = proj₁ x₀∈ys
+    i′ : Fin (suc (length (toList xs⁻)))
+    i′ = cast (≡.sym (≡.cong suc (length-tabulate xs⁻))) i
+    j′ : Fin (suc (length (toList ys⁻)))
+    j′ = cast (≡.sym (≡.cong suc (length-tabulate ys⁻))) j
+    -- main construction
+    open VectorProp using (insertAt-removeAt)
+    open PermutationReasoning
+    open Vector using () renaming (insertAt to insertAt′)
+    xs↭ys : toList xs ↭ toList ys
+    xs↭ys = begin
+        toList xs                       ≡⟨ tabulate-cong (insertAt-removeAt xs i) ⟨
+        toList (insertAt′ xs⁻ i x₀)     ≡⟨ insertAt-toList i′ i ≡.refl x₀ ⟨
+        insertAt (toList xs⁻) i′ x₀     ↭⟨ ↭-insert xs↭ys⁻′ i′ j′ x₀ ⟩
+        insertAt (toList ys⁻) j′ x₀     ≡⟨ insertAt-toList j′ j ≡.refl x₀ ⟩
+        toList (insertAt′ ys⁻ j x₀)     ≡⟨ ≡.cong (toList ∘ insertAt′ ys⁻ j) (proj₂ x₀∈ys) ⟩
+        toList (insertAt′ ys⁻ j (ys j)) ≡⟨ tabulate-cong (insertAt-removeAt ys j) ⟩
+        toList ys ∎