Sorting algorithms for vectors

module lists.sorting-algorithms-vectors where
Imports
open import elementary-number-theory.natural-numbers

open import finite-group-theory.permutations-standard-finite-types

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import linear-algebra.vectors

open import lists.permutation-vectors
open import lists.sorted-vectors

open import order-theory.decidable-total-orders

Idea

A function f on vectors is a sort if f is a permutation and if for every vector v, f v is sorted.

Definition

module _
  {l1 l2 : Level}
  (X : Decidable-Total-Order l1 l2)
  (f :
      {n : } 
      vec (type-Decidable-Total-Order X) n 
      vec (type-Decidable-Total-Order X) n)
  where

  is-sort-vec :
    UU (l1  l2)
  is-sort-vec =
    (n : ) 
    is-permutation-vec n f ×
    ((v : vec (type-Decidable-Total-Order X) n)  is-sorted-vec X (f v))

  is-permutation-vec-is-sort-vec :
    is-sort-vec  (n : )  is-permutation-vec n f
  is-permutation-vec-is-sort-vec S n = pr1 (S n)

  permutation-vec-is-sort-vec :
    is-sort-vec  (n : )  vec (type-Decidable-Total-Order X) n  Permutation n
  permutation-vec-is-sort-vec S n v =
    permutation-is-permutation-vec n f (is-permutation-vec-is-sort-vec S n) v

  eq-permute-vec-permutation-is-sort-vec :
    (S : is-sort-vec) (n : ) (v : vec (type-Decidable-Total-Order X) n) 
    f v  permute-vec n v (permutation-vec-is-sort-vec S n v)
  eq-permute-vec-permutation-is-sort-vec S n v =
    eq-permute-vec-permutation-is-permutation-vec
      ( n)
      ( f)
      ( is-permutation-vec-is-sort-vec S n) v

  is-sorting-vec-is-sort-vec :
    is-sort-vec  (n : ) 
    (v : vec (type-Decidable-Total-Order X) n)  is-sorted-vec X (f v)
  is-sorting-vec-is-sort-vec S n = pr2 (S n)