Sorted vectors

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

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

open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.functions
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

open import linear-algebra.vectors

open import lists.permutation-vectors

open import order-theory.decidable-total-orders

open import univalent-combinatorics.standard-finite-types

Idea

We define a sorted vector to be a vector such that for every pair of consecutive elements x and y, the inequality x ≤ y holds.

Definitions

The proposition that a vector is sorted

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

  is-sorted-vec-Prop :
    {n : }  vec (type-Decidable-Total-Order X) n  Prop l2
  is-sorted-vec-Prop {0} v = raise-unit-Prop l2
  is-sorted-vec-Prop {1} v = raise-unit-Prop l2
  is-sorted-vec-Prop {succ-ℕ (succ-ℕ n)} (x  y  v) =
    prod-Prop
      ( leq-Decidable-Total-Order-Prop X x y)
      ( is-sorted-vec-Prop (y  v))

  is-sorted-vec :
    {n : }  vec (type-Decidable-Total-Order X) n  UU l2
  is-sorted-vec l = type-Prop (is-sorted-vec-Prop l)

The proposition that an element is less than or equal to every element in a vector

  is-least-element-vec-Prop :
    {n : }  type-Decidable-Total-Order X 
    vec (type-Decidable-Total-Order X) n  Prop l2
  is-least-element-vec-Prop {0} x v = raise-unit-Prop l2
  is-least-element-vec-Prop {succ-ℕ n} x (y  v) =
    prod-Prop
      ( leq-Decidable-Total-Order-Prop X x y)
      ( is-least-element-vec-Prop x v)

  is-least-element-vec :
    {n : }  type-Decidable-Total-Order X 
    vec (type-Decidable-Total-Order X) n  UU l2
  is-least-element-vec x v = type-Prop (is-least-element-vec-Prop x v)

Properties

If a vector is sorted, then its tail is also sorted.

  is-sorted-tail-is-sorted-vec :
    {n : } 
    (v : vec (type-Decidable-Total-Order X) (succ-ℕ n)) 
    is-sorted-vec v  is-sorted-vec (tail-vec v)
  is-sorted-tail-is-sorted-vec {zero-ℕ} (x  empty-vec) s = raise-star
  is-sorted-tail-is-sorted-vec {succ-ℕ n} (x  y  v) s = pr2 s

  is-leq-head-head-tail-is-sorted-vec :
    {n : }  (v : vec (type-Decidable-Total-Order X) (succ-ℕ (succ-ℕ n))) 
    is-sorted-vec v 
    leq-Decidable-Total-Order X (head-vec v) (head-vec (tail-vec v))
  is-leq-head-head-tail-is-sorted-vec (x  y  v) s = pr1 s

If a vector v' = y ∷ v is sorted then for all elements x less than or equal to y, x is less than or equal to every element in the vector

  is-least-element-vec-is-leq-head-sorted-vec :
    {n : }
    (x : type-Decidable-Total-Order X)
    (v : vec (type-Decidable-Total-Order X) (succ-ℕ n)) 
    is-sorted-vec v  leq-Decidable-Total-Order X x (head-vec v) 
    is-least-element-vec x v
  is-least-element-vec-is-leq-head-sorted-vec {zero-ℕ} x (y  v) s p =
    p , raise-star
  is-least-element-vec-is-leq-head-sorted-vec {succ-ℕ n} x (y  v) s p =
    p ,
    ( is-least-element-vec-is-leq-head-sorted-vec
        ( x)
        ( v)
        ( is-sorted-tail-is-sorted-vec (y  v) s)
        ( transitive-leq-Decidable-Total-Order
            ( X)
            ( x)
            ( y)
            ( head-vec v)
            ( is-leq-head-head-tail-is-sorted-vec (y  v) s)
            ( p)))

An equivalent definition of being sorted

  is-sorted-least-element-vec-Prop :
    {n : }  vec (type-Decidable-Total-Order X) n  Prop l2
  is-sorted-least-element-vec-Prop {0} v = raise-unit-Prop l2
  is-sorted-least-element-vec-Prop {1} v = raise-unit-Prop l2
  is-sorted-least-element-vec-Prop {succ-ℕ (succ-ℕ n)} (x  v) =
    prod-Prop
      ( is-least-element-vec-Prop x v)
      ( is-sorted-least-element-vec-Prop v)

  is-sorted-least-element-vec :
    {n : }  vec (type-Decidable-Total-Order X) n  UU l2
  is-sorted-least-element-vec v =
    type-Prop (is-sorted-least-element-vec-Prop v)

  is-sorted-least-element-vec-is-sorted-vec :
    {n : }
    (v : vec (type-Decidable-Total-Order X) n) 
    is-sorted-vec v  is-sorted-least-element-vec v
  is-sorted-least-element-vec-is-sorted-vec {0} v x = raise-star
  is-sorted-least-element-vec-is-sorted-vec {1} v x = raise-star
  is-sorted-least-element-vec-is-sorted-vec
    {succ-ℕ (succ-ℕ n)}
    ( x  y  v)
    ( p , q) =
    is-least-element-vec-is-leq-head-sorted-vec x (y  v) q p ,
    is-sorted-least-element-vec-is-sorted-vec (y  v) q

  is-sorted-vec-is-sorted-least-element-vec :
    {n : }
    (v : vec (type-Decidable-Total-Order X) n) 
    is-sorted-least-element-vec v 
    is-sorted-vec v
  is-sorted-vec-is-sorted-least-element-vec {0} v x = raise-star
  is-sorted-vec-is-sorted-least-element-vec {1} v x = raise-star
  is-sorted-vec-is-sorted-least-element-vec
    {succ-ℕ (succ-ℕ n)}
    (x  y  v)
    (p , q) =
    ( pr1 p) ,
    ( is-sorted-vec-is-sorted-least-element-vec (y  v) q)

If the tail of a vector v is sorted and x ≤ head-vec v, then v is sorted

  is-sorted-vec-is-sorted-tail-is-leq-head-vec :
    {n : }
    (v : vec (type-Decidable-Total-Order X) (succ-ℕ (succ-ℕ n))) 
    is-sorted-vec (tail-vec v) 
    (leq-Decidable-Total-Order X (head-vec v) (head-vec (tail-vec v))) 
    is-sorted-vec v
  is-sorted-vec-is-sorted-tail-is-leq-head-vec (x  y  v) s p = p , s

If an element x is less than or equal to every element of a vector v, then it is less than or equal to every element of every permutation of v

  is-least-element-functional-vec-Prop :
    (n : )
    (x : type-Decidable-Total-Order X)
    (fv : functional-vec (type-Decidable-Total-Order X) n) 
    Prop l2
  is-least-element-functional-vec-Prop n x fv =
    Π-Prop (Fin n) λ k  leq-Decidable-Total-Order-Prop X x (fv k)

  is-least-element-functional-vec :
    (n : )
    (x : type-Decidable-Total-Order X)
    (fv : functional-vec (type-Decidable-Total-Order X) n) 
    UU l2
  is-least-element-functional-vec n x fv =
    type-Prop (is-least-element-functional-vec-Prop n x fv)

  is-least-element-permute-functional-vec :
    (n : )
    (x : type-Decidable-Total-Order X)
    (fv : functional-vec (type-Decidable-Total-Order X) n)
    (a : Permutation n) 
    is-least-element-functional-vec n x fv 
    is-least-element-functional-vec n x (fv  map-equiv a)
  is-least-element-permute-functional-vec n x fv a p k =
    p (map-equiv a k)

  is-least-element-vec-is-least-element-functional-vec :
    (n : )
    (x : type-Decidable-Total-Order X)
    (fv : functional-vec (type-Decidable-Total-Order X) n) 
    is-least-element-functional-vec n x fv 
    is-least-element-vec x (listed-vec-functional-vec n fv)
  is-least-element-vec-is-least-element-functional-vec 0 x fv p = raise-star
  is-least-element-vec-is-least-element-functional-vec (succ-ℕ n) x fv p =
    (p (inr star)) ,
    ( is-least-element-vec-is-least-element-functional-vec
        ( n)
        ( x)
        ( tail-functional-vec n fv)
        ( p  inl))

  is-least-element-functional-vec-is-least-element-vec :
    (n : )
    (x : type-Decidable-Total-Order X)
    (v : vec (type-Decidable-Total-Order X) n) 
    is-least-element-vec x v 
    is-least-element-functional-vec n x (functional-vec-vec n v)
  is-least-element-functional-vec-is-least-element-vec
    ( succ-ℕ n)
    ( x)
    ( y  v)
    ( p , q)
    ( inl k) =
    is-least-element-functional-vec-is-least-element-vec n x v q k
  is-least-element-functional-vec-is-least-element-vec
    ( succ-ℕ n)
    ( x)
    ( y  v)
    ( p , q)
    ( inr star) =
    p

  is-least-element-permute-vec :
    {n : }
    (x : type-Decidable-Total-Order X)
    (v : vec (type-Decidable-Total-Order X) n)
    (a : Permutation n) 
    is-least-element-vec x v 
    is-least-element-vec x (permute-vec n v a)
  is-least-element-permute-vec {n} x v a p =
    is-least-element-vec-is-least-element-functional-vec
      ( n)
      ( x)
      ( functional-vec-vec n v  map-equiv a)
      ( is-least-element-permute-functional-vec
          ( n)
          ( x)
          ( functional-vec-vec n v)
          ( a)
          ( is-least-element-functional-vec-is-least-element-vec n x v p))