{-# OPTIONS --without-K --safe #-}
module Data.Fin.Base where
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s)
open import Data.Nat.Properties.Core using (≤-pred)
open import Data.Product as Product using (_×_; _,_)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
open import Function.Base using (id; _∘_; _on_)
open import Level using (0ℓ)
open import Relation.Nullary using (yes; no)
open import Relation.Nullary.Decidable.Core using (True; toWitness)
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} (i : Fin n) → Fin (suc n)
toℕ : ∀ {n} → Fin n → ℕ
toℕ zero = 0
toℕ (suc i) = suc (toℕ i)
Fin′ : ∀ {n} → Fin n → Set
Fin′ i = Fin (toℕ i)
cast : ∀ {m n} → .(_ : 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)
fromℕ : (n : ℕ) → Fin (suc n)
fromℕ zero = zero
fromℕ (suc n) = suc (fromℕ n)
fromℕ< : ∀ {m n} → m ℕ.< n → Fin n
fromℕ< {zero} {suc n} m≤n = zero
fromℕ< {suc m} {suc n} m≤n = suc (fromℕ< (≤-pred m≤n))
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))
raise : ∀ {m} n → Fin m → Fin (n ℕ.+ m)
raise zero i = i
raise (suc n) i = suc (raise n i)
reduce≥ : ∀ {m n} (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 : ∀ {n} {i : Fin n} → Fin′ i → Fin n
inject {i = suc i} zero = zero
inject {i = suc i} (suc j) = suc (inject j)
inject! : ∀ {n} {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+ : ∀ {m} n → Fin m → Fin (m ℕ.+ n)
inject+ n zero = zero
inject+ n (suc i) = suc (inject+ n i)
inject₁ : ∀ {m} → Fin m → Fin (suc m)
inject₁ zero = zero
inject₁ (suc i) = suc (inject₁ i)
inject≤ : ∀ {m n} → Fin m → m ℕ.≤ n → Fin n
inject≤ {_} {suc n} zero le = zero
inject≤ {_} {suc n} (suc i) le = suc (inject≤ i (≤-pred le))
lower₁ : ∀ {n} → (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 λ x → ne (cong suc x))
strengthen : ∀ {n} (i : Fin n) → Fin′ (suc i)
strengthen zero = zero
strengthen (suc i) = suc (strengthen i)
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)
join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)
join m n = [ inject+ n , raise {n} m ]′
quotRem : ∀ {n} k → Fin (n ℕ.* k) → Fin k × Fin n
quotRem {suc n} k i with splitAt k i
... | inj₁ j = j , zero
... | inj₂ j = Product.map₂ suc (quotRem {n} k j)
remQuot : ∀ {n} k → Fin (n ℕ.* k) → Fin n × Fin k
remQuot k = Product.swap ∘ quotRem k
combine : ∀ {n k} → Fin n → Fin k → Fin (n ℕ.* k)
combine {suc n} {k} zero y = inject+ (n ℕ.* k) y
combine {suc n} {k} (suc x) y = raise k (combine x y)
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)
lift : ∀ {m n} 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)
infixl 6 _+_
_+_ : ∀ {m n} (i : Fin m) (j : Fin n) → Fin (toℕ i ℕ.+ n)
zero + j = j
suc i + j = suc (i + j)
infixl 6 _-_
_-_ : ∀ {m} (i : Fin m) (j : Fin′ (suc i)) → Fin (m ℕ.∸ toℕ j)
i - zero = i
suc i - suc j = i - j
infixl 6 _ℕ-_
_ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
n ℕ- zero = fromℕ n
suc n ℕ- suc i = n ℕ- i
infixl 6 _ℕ-ℕ_
_ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
n ℕ-ℕ zero = n
suc n ℕ-ℕ suc i = n ℕ-ℕ i
pred : ∀ {n} → Fin n → Fin n
pred zero = zero
pred (suc i) = inject₁ i
opposite : ∀ {n} → Fin n → Fin n
opposite {suc n} zero = fromℕ n
opposite {suc n} (suc i) = inject₁ (opposite i)
punchOut : ∀ {m} {i j : Fin (suc m)} → i ≢ j → Fin m
punchOut {_} {zero} {zero} i≢j = ⊥-elim (i≢j refl)
punchOut {_} {zero} {suc j} _ = j
punchOut {suc m} {suc i} {zero} _ = zero
punchOut {suc m} {suc i} {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))
punchIn : ∀ {m} → Fin (suc m) → Fin m → Fin (suc m)
punchIn zero j = suc j
punchIn (suc i) zero = zero
punchIn (suc i) (suc j) = suc (punchIn i j)
pinch : ∀ {n} → 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)
infix 4 _≤_ _≥_ _<_ _>_
_≤_ : ∀ {n} → Rel (Fin n) 0ℓ
_≤_ = ℕ._≤_ on toℕ
_≥_ : ∀ {n} → Rel (Fin n) 0ℓ
_≥_ = ℕ._≥_ on toℕ
_<_ : ∀ {n} → Rel (Fin n) 0ℓ
_<_ = ℕ._<_ on toℕ
_>_ : ∀ {n} → Rel (Fin n) 0ℓ
_>_ = ℕ._>_ on toℕ
data _≺_ : ℕ → ℕ → Set where
_≻toℕ_ : ∀ n (i : Fin n) → toℕ i ≺ n
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 : ∀ {n} (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)
fromℕ≤ = fromℕ<
{-# WARNING_ON_USAGE fromℕ≤
"Warning: fromℕ≤ was deprecated in v1.2.
Please use fromℕ< instead."
#-}
fromℕ≤″ = fromℕ<″
{-# WARNING_ON_USAGE fromℕ≤″
"Warning: fromℕ≤″ was deprecated in v1.2.
Please use fromℕ<″ instead."
#-}