------------------------------------------------------------------------
-- The Agda standard library
--
-- Finite sets
------------------------------------------------------------------------

-- Note that elements of Fin n can be seen as natural numbers in the
-- set {m | m < n}. The notation "m" in comments below refers to this
-- natural number view.
{-# OPTIONS --cubical-compatible --safe #-}

module Data.Fin.Base where

open import Data.Bool.Base using (Bool; true; false; T; not)
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base as  using (; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (id; _∘_; _on_; flip)
open import Level using (0ℓ)
open import Relation.Nullary.Negation.Core using (contradiction)
open import Relation.Nullary.Decidable.Core using (yes; no; True; toWitness)
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
open import Relation.Binary.Indexed.Heterogeneous.Core using (IRel)

private
  variable
    m n : 

------------------------------------------------------------------------
-- Types

-- Fin n is a type with n elements.

data Fin :   Set where
  zero : Fin (suc n)
  suc  : (i : Fin n)  Fin (suc n)

-- A conversion: toℕ "i" = i.

toℕ : Fin n  
toℕ zero    = 0
toℕ (suc i) = suc (toℕ i)

-- A Fin-indexed variant of Fin.

Fin′ : Fin n  Set
Fin′ i = Fin (toℕ i)

------------------------------------------------------------------------
-- A cast that actually computes on constructors (as opposed to subst)

cast : .(m  n)  Fin m  Fin n
cast {zero}  {zero}  eq k       = k
cast {suc m} {suc n} eq zero    = zero
cast {suc m} {suc n} eq (suc k) = suc (cast (cong ℕ.pred eq) k)

------------------------------------------------------------------------
-- Conversions

-- toℕ is defined above.

-- fromℕ n = "n".

fromℕ : (n : )  Fin (suc n)
fromℕ zero    = zero
fromℕ (suc n) = suc (fromℕ n)

-- fromℕ< {m} _ = "m".

fromℕ< : m ℕ.< n  Fin n
fromℕ< {zero}  {suc n} z<s = zero
fromℕ< {suc m} {suc n} (s<s m<n) = suc (fromℕ< m<n)

-- fromℕ<″ m _ = "m".

fromℕ<″ :  m {n}  m ℕ.<″ n  Fin n
fromℕ<″ zero    (ℕ.less-than-or-equal refl) = zero
fromℕ<″ (suc m) (ℕ.less-than-or-equal refl) =
  suc (fromℕ<″ m (ℕ.less-than-or-equal refl))

-- canonical liftings of i:Fin m to larger index

-- injection on the left: "i" ↑ˡ n = "i" in Fin (m + n)
infixl 5 _↑ˡ_
_↑ˡ_ :  {m}  Fin m   n  Fin (m ℕ.+ n)
zero    ↑ˡ n = zero
(suc i) ↑ˡ n = suc (i ↑ˡ n)

-- injection on the right: n ↑ʳ "i" = "n + i" in Fin (n + m)
infixr 5 _↑ʳ_
_↑ʳ_ :  {m} n  Fin m  Fin (n ℕ.+ m)
zero    ↑ʳ i = i
(suc n) ↑ʳ i = suc (n ↑ʳ i)

-- reduce≥ "m + i" _ = "i".

reduce≥ :  (i : Fin (m ℕ.+ n)) (i≥m : toℕ i ℕ.≥ m)  Fin n
reduce≥ {zero}  i       i≥m       = i
reduce≥ {suc m} (suc i) (s≤s i≥m) = reduce≥ i i≥m

-- inject⋆ m "i" = "i".

inject :  {i : Fin n}  Fin′ i  Fin n
inject {i = suc i} zero    = zero
inject {i = suc i} (suc j) = suc (inject j)

inject! :  {i : Fin (suc n)}  Fin′ i  Fin n
inject! {n = suc _} {i = suc _}  zero    = zero
inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)

inject₁ : Fin n  Fin (suc n)
inject₁ zero    = zero
inject₁ (suc i) = suc (inject₁ i)

inject≤ : Fin m  m ℕ.≤ n  Fin n
inject≤ {_} {suc n} zero    _        = zero
inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)

-- lower₁ "i" _ = "i".

lower₁ :  (i : Fin (suc n))  n  toℕ i  Fin n
lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
lower₁ {suc n} zero    _  = zero
lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne  cong suc))

-- A strengthening injection into the minimal Fin fibre.
strengthen :  (i : Fin n)  Fin′ (suc i)
strengthen zero    = zero
strengthen (suc i) = suc (strengthen i)

-- splitAt m "i" = inj₁ "i"      if i < m
--                 inj₂ "i - m"  if i ≥ m
-- This is dual to splitAt from Data.Vec.

splitAt :  m {n}  Fin (m ℕ.+ n)  Fin m  Fin n
splitAt zero    i       = inj₂ i
splitAt (suc m) zero    = inj₁ zero
splitAt (suc m) (suc i) = Sum.map suc id (splitAt m i)

-- inverse of above function
join :  m n  Fin m  Fin n  Fin (m ℕ.+ n)
join m n = [ _↑ˡ n , m ↑ʳ_ ]′

-- quotRem k "i" = "i % k" , "i / k"
-- This is dual to group from Data.Vec.

quotRem :  n  Fin (m ℕ.* n)  Fin n × Fin m
quotRem {suc m} n i with splitAt n i
... | inj₁ j = j , zero
... | inj₂ j = Product.map₂ suc (quotRem {m} n j)

-- a variant of quotRem the type of whose result matches the order of multiplication
remQuot :  n  Fin (m ℕ.* n)  Fin m × Fin n
remQuot i = Product.swap  quotRem i

quotient :  n  Fin (m ℕ.* n)  Fin m
quotient n = proj₁  remQuot n

remainder :  n  Fin (m ℕ.* n)  Fin n
remainder {m} n = proj₂  remQuot {m} n

-- inverse of remQuot
combine : Fin m  Fin n  Fin (m ℕ.* n)
combine {suc m} {n} zero    j = j ↑ˡ (m ℕ.* n)
combine {suc m} {n} (suc i) j = n ↑ʳ (combine i j)

-- Next in progression after splitAt and remQuot
finToFun : Fin (m ^ n)  (Fin n  Fin m)
finToFun {m} {suc n} i zero    = quotient (m ^ n) i
finToFun {m} {suc n} i (suc j) = finToFun (remainder {m} (m ^ n) i) j

-- inverse of above function
funToFin : (Fin m  Fin n)  Fin (n ^ m)
funToFin {zero}  f = zero
funToFin {suc m} f = combine (f zero) (funToFin (f  suc))

------------------------------------------------------------------------
-- Operations

-- Folds.

fold :  {t} (T :   Set t) {m} 
       (∀ {n}  T n  T (suc n)) 
       (∀ {n}  T (suc n)) 
       Fin m  T m
fold T f x zero    = x
fold T f x (suc i) = f (fold T f x i)

fold′ :  {n t} (T : Fin (suc n)  Set t) 
        (∀ i  T (inject₁ i)  T (suc i)) 
        T zero 
         i  T i
fold′             T f x zero     = x
fold′ {n = suc n} T f x (suc i)  =
  f i (fold′ (T  inject₁) (f  inject₁) x i)

-- Lifts functions.

lift :  k  (Fin m  Fin n)  Fin (k ℕ.+ m)  Fin (k ℕ.+ n)
lift zero    f i       = f i
lift (suc k) f zero    = zero
lift (suc k) f (suc i) = suc (lift k f i)

-- "i" + "j" = "i + j".

infixl 6 _+_

_+_ :  (i : Fin m) (j : Fin n)  Fin (toℕ i ℕ.+ n)
zero  + j = j
suc i + j = suc (i + j)

-- "i" - "j" = "i ∸ j".

infixl 6 _-_

_-_ :  (i : Fin n) (j : Fin′ (suc i))  Fin (n ℕ.∸ toℕ j)
i     - zero   = i
suc i - suc j  = i - j

-- m ℕ- "i" = "m ∸ i".

infixl 6 _ℕ-_

_ℕ-_ : (n : ) (j : Fin (suc n))  Fin (suc n ℕ.∸ toℕ j)
n     ℕ- zero   = fromℕ n
suc n ℕ- suc i  = n ℕ- i

-- m ℕ-ℕ "i" = m ∸ i.

infixl 6 _ℕ-ℕ_

_ℕ-ℕ_ : (n : )  Fin (suc n)  
n     ℕ-ℕ zero   = n
suc n ℕ-ℕ suc i  = n ℕ-ℕ i

-- pred "i" = "pred i".

pred : Fin n  Fin n
pred zero    = zero
pred (suc i) = inject₁ i

-- opposite "i" = "n - i" (i.e. the additive inverse).

opposite : Fin n  Fin n
opposite {suc n} zero    = fromℕ n
opposite {suc n} (suc i) = inject₁ (opposite i)

-- The function f(i,j) = if j>i then j-1 else j
-- This is a variant of the thick function from Conor
-- McBride's "First-order unification by structural recursion".

punchOut :  {i j : Fin (suc n)}  i  j  Fin n
punchOut {_}     {zero}   {zero}  i≢j = ⊥-elim (i≢j refl)
punchOut {_}     {zero}   {suc j} _   = j
punchOut {suc _} {suc i}  {zero}  _   = zero
punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j  cong suc))

-- The function f(i,j) = if j≥i then j+1 else j

punchIn : Fin (suc n)  Fin n  Fin (suc n)
punchIn zero    j       = suc j
punchIn (suc i) zero    = zero
punchIn (suc i) (suc j) = suc (punchIn i j)

-- The function f(i,j) such that f(i,j) = if j≤i then j else j-1

pinch : Fin n  Fin (suc n)  Fin n
pinch {suc n} _       zero    = zero
pinch {suc n} zero    (suc j) = j
pinch {suc n} (suc i) (suc j) = suc (pinch i j)

------------------------------------------------------------------------
-- Order relations

infix 4 _≤_ _≥_ _<_ _>_

_≤_ : IRel Fin 0ℓ
i  j = toℕ i ℕ.≤ toℕ j

_≥_ : IRel Fin 0ℓ
i  j = toℕ i ℕ.≥ toℕ j

_<_ : IRel Fin 0ℓ
i < j = toℕ i ℕ.< toℕ j

_>_ : IRel Fin 0ℓ
i > j = toℕ i ℕ.> toℕ j


------------------------------------------------------------------------
-- An ordering view.

data Ordering {n : } : Fin n  Fin n  Set where
  less    :  greatest (least : Fin′ greatest) 
            Ordering (inject least) greatest
  equal   :  i  Ordering i i
  greater :  greatest (least : Fin′ greatest) 
            Ordering greatest (inject least)

compare :  (i j : Fin n)  Ordering i j
compare zero    zero    = equal   zero
compare zero    (suc j) = less    (suc j) zero
compare (suc i) zero    = greater (suc i) zero
compare (suc i) (suc j) with compare i j
... | less    greatest least = less    (suc greatest) (suc least)
... | greater greatest least = greater (suc greatest) (suc least)
... | equal   i              = equal   (suc i)


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

raise = _↑ʳ_
{-# WARNING_ON_USAGE raise
"Warning: raise was deprecated in v2.0.
Please use _↑_ʳ instead."
#-}
inject+ :  {m} n  Fin m  Fin (m ℕ.+ n)
inject+ n i = i ↑ˡ n
{-# WARNING_ON_USAGE inject+
"Warning: inject+ was deprecated in v2.0.
Please use _↑ˡ_ instead.
NB argument order has been flipped:
the left-hand argument is the Fin m
the right-hand is the Nat index increment."
#-}

data _≺_ :     Set where
  _≻toℕ_ :  n (i : Fin n)  toℕ i  n

{-# WARNING_ON_USAGE _≺_
"Warning: _≺_ was deprecated in v2.0.
Please use equivalent relation _<_ instead."
#-}
{-# WARNING_ON_USAGE _≻toℕ_
"Warning: _≻toℕ_ was deprecated in v2.0.
Please use toℕ<n from Data.Fin.Properties instead."
#-}