module Permutations where

module +1-mod-n-module where
  open import Data.Nat
  import Data.Nat as ℕ
  import Data.Nat.Properties as ℕ
  open import Data.Fin renaming (Fin to 𝔽)
  open import Data.Fin.Properties hiding (setoid)
  open import Function.Inverse
  open import Relation.Binary.PropositionalEquality
     using (_≡_; refl; cong; module ≡-Reasoning)
  open import Relation.Nullary
  open import Function.LeftInverse
  open import Function.Equality using (_⟶_)
  open import Level using (0ℓ)
  open import Relation.Binary.Bundles
  open import Data.Product

--pandoc-begin Perm
  Perm : ℕ → Set
  Perm n = 𝔽 n ↔ 𝔽 n
--pandoc-end Perm

--pandoc-begin plus-one-mod-n
  +1-mod-n : {n : ℕ} → 𝔽 n → 𝔽 n
  +1-mod-n {ℕ.suc n} m with n ℕ.≟ toℕ m
  ... | no m≢n  = suc (lower₁ m m≢n)
  ... | yes _ = zero
--pandoc-end plus-one-mod-n

--pandoc-begin minus-one-mod-n
  -1-mod-n : {n : ℕ} → 𝔽 n → 𝔽 n
  -1-mod-n {ℕ.suc n} zero = fromℕ n
  -1-mod-n {ℕ.suc n} (suc m) = inject₁ m
--pandoc-end minus-one-mod-n

--pandoc-begin ugly-left-inverse-proof
  i≡j⇒j<i+1 : ∀ {i j } → i ≡ j → j ℕ.< ℕ.suc i
  i≡j⇒j<i+1 {i} {j} i≡j =
    begin
      ℕ.suc j
    ≡⟨ cong ℕ.suc (≡-sym i≡j) ⟩
      ℕ.suc i
    ∎
    where
      open Relation.Binary.PropositionalEquality renaming (sym to ≡-sym)
      open ℕ.≤-Reasoning

  open ≡-Reasoning

  left-inverse′ : (n : ℕ) → (x : 𝔽 n) → -1-mod-n (+1-mod-n x) ≡ x
  left-inverse′ ℕ.zero ()
  left-inverse′ (ℕ.suc ℕ.zero) zero = refl
  left-inverse′ (ℕ.suc (ℕ.suc n′)) x
              with ℕ.suc n′ ℕ.≟ toℕ x
  ...  | no n+1≢x with x
  ...               | zero = refl
  ...               | suc x =
      begin
        -1-mod-n (suc (lower₁ (suc x) n+1≢x))
      ≡⟨⟩
        inject₁ (lower₁ (suc x) n+1≢x)
      ≡⟨  inject₁-lower₁ (suc x) n+1≢x ⟩
        suc x
      ∎
  left-inverse′ (ℕ.suc (ℕ.suc n)) x
       | yes n+1≡x =
     begin
       -1-mod-n zero
     ≡⟨⟩
       fromℕ (ℕ.suc n)
     ≡⟨ fromℕ-def (ℕ.suc n) ⟩
       fromℕ< n+1<n+2
     ≡⟨ fromℕ<-cong (ℕ.suc n) (toℕ x) n+1≡x n+1<n+2 (i≡j⇒j<i+1 n+1≡x) ⟩
        fromℕ< (i≡j⇒j<i+1 n+1≡x )
     ≡⟨ fromℕ<-toℕ x (i≡j⇒j<i+1 n+1≡x)  ⟩
       x
     ∎
     where
       n+1<n+2 : ℕ.suc n ℕ.< ℕ.suc (ℕ.suc n)
       n+1<n+2 = ℕ.s≤s (ℕ.s≤s (ℕ.≤-reflexive refl))
--pandoc-end ugly-left-inverse-proof

module RewriteOfJoin where
  import Data.Nat as ℕ
  open import Data.Fin renaming (join to join′)
  open import Data.Sum

  -- A more direct definition of `join`
  join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)
--pandoc-begin join-direct
  join m n (inj₁ x) = inject+ n x
  join m n (inj₂ y) = raise {n} m y
--pandoc-end join-direct

module SplitPermute1 where

  open import Data.Nat using (ℕ; _+_)
  open import Data.Fin renaming (Fin to 𝔽) hiding (_+_)
  open import Data.Fin.Properties hiding (setoid)
  open import Relation.Binary.PropositionalEquality using (_≡_; _≗_)
  open import Data.Sum
  open import Data.Sum.Properties
  open import Function
  open import Function.Bundles
  open import Level using (Level)

--pandoc-begin splitPermute
  splitPermute : (m : ℕ) {n : ℕ} → (𝔽 (m + n) → 𝔽 (n + m))
  splitPermute m {n} = join n m ∘ swap ∘ splitAt m
--pandoc-end splitPermute

--pandoc-begin composition-cong
  cong-[_]∘⟨_⟩∘[_] :
    {a : Level} {A′ A B B′ : Set a}
    → (h : B → B′)
    → {f g : A → B}
    → f ≗ g
    → (h′ : A′ → A)
    → h ∘ f ∘ h′ ≗ h ∘ g ∘ h′
  cong-[_]∘⟨_⟩∘[_] h {f} {g} f≗g h′ = λ x → cong h (f≗g (h′ x))
    where
      open Relation.Binary.PropositionalEquality using (cong)
--pandoc-end composition-cong

--pandoc-begin inverse-proof
  inverse : {m n : ℕ} → splitPermute n ∘ splitPermute m ≗ id
  inverse {m} {n} =
    begin
      (splitPermute n ∘ splitPermute m)
    ≡⟨⟩
      (join m n ∘ swap ∘ splitAt n) ∘ (join n m ∘ swap ∘ splitAt m)
    ≡⟨⟩
      (join m n ∘ swap ∘ splitAt n ∘ join n m ∘ swap ∘ splitAt m)
    ≈⟨ cong-[ join m n ∘ swap ]∘⟨ splitAt-join n m ⟩∘[ swap ∘ splitAt m ] ⟩
--pandoc-begin inverse-proof-snippet-1
      (join m n ∘ swap ∘ swap ∘ splitAt m)
    ≈⟨ cong-[ join m n ]∘⟨ swap-involutive ⟩∘[ splitAt m ] ⟩
      (join m n ∘ splitAt m)
--pandoc-end inverse-proof-snippet-1
    ≈⟨ join-splitAt m n ⟩
      id
    ∎
    where
      open import Relation.Binary.PropositionalEquality
      open import Relation.Binary.Reasoning.Setoid (𝔽 (m + n) →-setoid 𝔽 (m + n))
--pandoc-end inverse-proof

--pandoc-begin splitPermute-bijection-1
  splitPermute↔ : (m : ℕ) {n : ℕ} → (𝔽 (m + n) ↔ 𝔽 (n + m))
  splitPermute↔ m {n} = mk↔′ (splitPermute m) (splitPermute n) (inverse {n} {m}) (inverse {m} {n})
--pandoc-end splitPermute-bijection-1

module SplitPermuteWithConstructiveCorrectness where

  open import Data.Nat using (ℕ; _+_)
  open import Data.Fin renaming (Fin to 𝔽) hiding (_+_)
  open import Data.Fin.Properties hiding (setoid)
  open import Function.Construct.Composition hiding (inverse)
  open import Function.Construct.Symmetry using (sym-↔)
  open import Function using (mk↔′; _↔_)
  open import Function.Bundles using (Inverse)
  open import Data.Sum
  open import Data.Sum.Properties
  open Inverse

--pandoc-begin swap-bijection
  swap↔ : ∀ {a b} {A : Set a} {B : Set b} →  (A ⊎ B) ↔ (B ⊎ A)
  swap↔ {a} {b} {A} {B} = mk↔′ swap swap swap-involutive swap-involutive
--pandoc-end swap-bijection

--pandoc-begin splitPermute-bijection-2
  splitPermute↔ : (m : ℕ) {n : ℕ} → 𝔽 (m + n) ↔ 𝔽 (n + m)
  splitPermute↔ m {n} = (+↔⊎ {m} {n} ∘-↔ swap↔) ∘-↔ sym-↔ +↔⊎
--pandoc-end splitPermute-bijection-2