module Data.Fin.Base where
Finite sets🔗
The type Fin is the type of size
n. These are defined as an inductive family over Nat, such that
Fin 0 has 0 elements, Fin 1 has 1 element, and
so on.
Another way to view Fin is as the type of numbers
less than some upper bound. For instance, fsuc fzero is of
type Fin 3, but will not typecheck as a
Fin 1!
data Fin : Nat → Type where fzero : ∀ {n} → Fin (suc n) fsuc : ∀ {n} → Fin n → Fin (suc n)
Keeping with the perspective of Fin as a type of bounded
natural numbers, we provide conversion functions going back and
forth.
from-nat : ∀ (n : Nat) → Fin (suc n) from-nat zero = fzero from-nat (suc n) = fsuc (from-nat n) to-nat : ∀ {n : Nat} → Fin n → Nat to-nat fzero = zero to-nat (fsuc i) = suc (to-nat i)
A note of caution: because of some ✨technical reasons✨ cubical agda
cannot handle transports over indexed inductive types very well.
Instead, we define a function cast that computes on the
indices of Fin, rather than on the
path.
cast : ∀ {m n} → m ≡ n → Fin m → Fin n cast {suc m} {zero} p fzero = absurd (Nat.suc≠zero p) cast {suc m} {suc n} p fzero = fzero cast {suc m} {zero} p (fsuc i) = absurd (Nat.suc≠zero p) cast {suc m} {suc n} p (fsuc i) = fsuc (cast (Nat.suc-inj p) i)
cast-uncast : ∀ {m n} → (p : m ≡ n) → ∀ x → cast (sym p) (cast p x) ≡ x cast-uncast {suc m} {zero} p fzero = absurd (Nat.suc≠zero p) cast-uncast {suc m} {suc n} p fzero = refl cast-uncast {suc m} {zero} p (fsuc x) = absurd (Nat.suc≠zero p) cast-uncast {suc m} {suc n} p (fsuc x) = ap fsuc (cast-uncast (Nat.suc-inj p) x) cast-is-equiv : ∀ {m n} (p : m ≡ n) → is-equiv (cast p) cast-is-equiv p = is-iso→is-equiv $ iso (cast (sym p)) (cast-uncast (sym p)) (cast-uncast p)
Next, we move on to one of the most useful functions for Fin: strength.
This allows us to (possibly) strengthen the upper bound on some
Fin n.
strengthen : ∀ {n} → Fin (suc n) → Fin (suc n) ⊎ Fin n strengthen {n = zero} fzero = inl fzero strengthen {n = suc n} fzero = inr fzero strengthen {n = suc n} (fsuc i) = ⊎-map fsuc fsuc (strengthen i)
On the other hand, weaken does the opposite: it
relaxes the upper bound on some Fin n, allowing us to
regard it as a Fin (suc n).
weaken : ∀ {n} → Fin n → Fin (suc n) weaken fzero = fzero weaken (fsuc i) = fsuc (weaken i)
We can also relax the upper bounds if m ≤ n.
inject : ∀ {m n} → m Nat.≤ n → Fin m → Fin n inject {_} {suc n} le fzero = fzero inject {_} {suc n} (Nat.s≤s le) (fsuc i) = fsuc (inject le i)
Discreteness🔗
The proof here mirrors the one found in Data.Nat.Base, just with some
slight tweaks required to handle the indexing.
We begin by showing that one can distinguish zero from
successor:
fzero≠fsuc : ∀ {n} {i : Fin n} → ¬ fzero ≡ fsuc i fzero≠fsuc {n = n} path = subst distinguish path tt where distinguish : Fin (suc n) → Type distinguish fzero = ⊤ distinguish (fsuc _) = ⊥
Next, we show that fsuc is injective. This again follows
the proof in Data.Nat.Base, but some extra
care must be taken to ensure that pred is well typed!
fsuc-inj : ∀ {n} {i j : Fin n} → fsuc i ≡ fsuc j → i ≡ j fsuc-inj {n = suc n} p = ap pred p where pred : Fin (suc (suc n)) → Fin (suc n) pred fzero = fzero pred (fsuc i) = i
Finally, we pull everything together to show that Fin is Discrete. This is not exactly a
shock (after all, Nat is discrete), but it’s
useful nonetheless!
instance Discrete-Fin : ∀ {n} → Discrete (Fin n) Discrete-Fin {x = fzero} {fzero} = yes refl Discrete-Fin {x = fzero} {fsuc j} = no fzero≠fsuc Discrete-Fin {x = fsuc i} {fzero} = no (fzero≠fsuc ∘ sym) Discrete-Fin {x = fsuc i} {fsuc j} with Discrete-Fin {x = i} {j} ... | yes p = yes (ap fsuc p) ... | no ¬i≡j = no λ si=sj → ¬i≡j (fsuc-inj si=sj)
Hedberg’s
theorem implies that Fin is a set, i.e., it only has trivial
paths.
opaque Fin-is-set : ∀ {n} → is-set (Fin n) Fin-is-set = Discrete→is-set Discrete-Fin instance H-Level-Fin : ∀ {n k} → H-Level (Fin n) (2 + k) H-Level-Fin = basic-instance 2 Fin-is-set
instance Number-Fin : ∀ {n} → Number (Fin n) Number-Fin {n} .Number.Constraint k = k Nat.< n Number-Fin {n} .Number.fromNat k {{e}} = go k n e where go : ∀ k n → k Nat.< n → Fin n go zero (suc n) e = fzero go (suc k) (suc n) (Nat.s≤s e) = fsuc (go k n e) open import Data.Nat.Base using (0≤x ; s≤s') public Fin-elim : ∀ {ℓ} (P : ∀ {n} → Fin n → Type ℓ) → (∀ {n} → P {suc n} fzero) → (∀ {i} (j : Fin i) → P j → P (fsuc j)) → ∀ {n} (i : Fin n) → P i Fin-elim P pfzero pfsuc fzero = pfzero Fin-elim P pfzero pfsuc (fsuc x) = pfsuc x (Fin-elim P pfzero pfsuc x) fin-cons : ∀ {ℓ} {n} {P : Fin (suc n) → Type ℓ} → P 0 → (∀ x → P (fsuc x)) → ∀ x → P x fin-cons p0 ps fzero = p0 fin-cons p0 ps (fsuc x) = ps x fin-absurd : Fin 0 → ⊥ fin-absurd ()
Ordering🔗
Keeping with the view that Fin represents the type of
bounded natural numbers, we can re-use the ordering on Nat to induce an ordering on
Fin. This means that any lemmas
about the ordering on natural numbers apply immediately to the ordering
on standard finite sets.
_≤_ : ∀ {n} → Fin n → Fin n → Type i ≤ j = to-nat i Nat.≤ to-nat j infix 7 _≤_ _<_ : ∀ {n} → Fin n → Fin n → Type i < j = to-nat i Nat.< to-nat j infix 7 _<_
Next, we define a pair of functions squish and skip, which are the building
blocks for all monotone functions between Fin. squish i
takes a j : Fin (suc n) to a Fin n by mapping
both i and i+1 to i. Its
counterpart skip i takes some j : Fin n to a
Fin (suc n) by skipping over i instead.
squish : ∀ {n} → Fin n → Fin (suc n) → Fin n squish fzero fzero = fzero squish fzero (fsuc j) = j squish (fsuc i) fzero = fzero squish (fsuc i) (fsuc j) = fsuc (squish i j) skip : ∀ {n} → Fin (suc n) → Fin n → Fin (suc n) skip fzero j = fsuc j skip (fsuc i) fzero = fzero skip (fsuc i) (fsuc j) = fsuc (skip i j)
As a subset🔗
While Fin is very conveniently
defined as an indexed family of types, it can also be defined as a
subset of the natural numbers: Namely, the finite ordinal
is the same type as as
This makes sense! Any set with
elements is equivalent to any other set with
elements, and a very canonical choice is the first
values of
ℕ< : Nat → Type ℕ< x = Σ[ n ∈ Nat ] n Nat.< x from-ℕ< : ∀ {n} → ℕ< n → Fin n from-ℕ< {n = suc n} (zero , q) = fzero from-ℕ< {n = suc n} (suc p , Nat.s≤s q) = fsuc (from-ℕ< (p , q)) to-ℕ< : ∀ {n} → Fin n → ℕ< n to-ℕ< x = to-nat x , p x where p : ∀ {n} (x : Fin n) → suc (to-nat x) Nat.≤ n p {n = suc n} fzero = Nat.s≤s Nat.0≤x p {n = suc n} (fsuc x) = Nat.s≤s (p x)
Arithmetic🔗
weaken-≤ : ∀ {m n} → m Nat.≤ n → Fin m → Fin n weaken-≤ {suc m} {suc n} m≤n fzero = fzero weaken-≤ {suc m} {suc n} (Nat.s≤s m≤n) (fsuc i) = fsuc (weaken-≤ m≤n i) shift-≤ : ∀ {m n} → m Nat.≤ n → Fin m → Fin n shift-≤ {n = suc zero} (Nat.s≤s 0≤x) i = i shift-≤ {n = suc (suc n)} (Nat.s≤s 0≤x) i = fsuc (shift-≤ (Nat.s≤s 0≤x) i) shift-≤ {n = n} (Nat.s≤s (Nat.s≤s m≤n)) fzero = weaken (shift-≤ (Nat.s≤s m≤n) fzero) shift-≤ {n = n} (Nat.s≤s (Nat.s≤s m≤n)) (fsuc i) = fsuc (shift-≤ (Nat.s≤s m≤n) i) split-+ : ∀ {m n} → Fin (m + n) → Fin m ⊎ Fin n split-+ {m = zero} i = inr i split-+ {m = suc m} fzero = inl fzero split-+ {m = suc m} (fsuc i) = ⊎-map fsuc id (split-+ i) avoid : ∀ {n} (i j : Fin (suc n)) → i ≠ j → Fin n avoid fzero fzero i≠j = absurd (i≠j refl) avoid {n = suc n} fzero (fsuc j) i≠j = j avoid {n = suc n} (fsuc i) fzero i≠j = fzero avoid {n = suc n} (fsuc i) (fsuc j) i≠j = fsuc (avoid i j (i≠j ∘ ap fsuc)) fshift : ∀ {n} (m : Nat) → Fin n → Fin (m + n) fshift zero i = i fshift (suc m) i = fsuc (fshift m i) opposite : ∀ {n} → Fin n → Fin n opposite {n = suc n} fzero = from-nat n opposite {n = suc n} (fsuc i) = weaken (opposite i)
Vector operations🔗
_[_≔_] : ∀ {ℓ} {A : Type ℓ} {n} → (Fin n → A) → Fin (suc n) → A → Fin (suc n) → A _[_≔_] {n = n} ρ fzero a fzero = a _[_≔_] {n = n} ρ fzero a (fsuc j) = ρ j _[_≔_] {n = suc n} ρ (fsuc i) a fzero = ρ fzero _[_≔_] {n = suc n} ρ (fsuc i) a (fsuc j) = ((ρ ∘ fsuc) [ i ≔ a ]) j delete : ∀ {ℓ} {A : Type ℓ} {n} → (Fin (suc n) → A) → Fin (suc n) → Fin n → A delete ρ i j = ρ (skip i j)