module Data.Fin.Properties where
Finite sets - properties🔗
Ordering🔗
As noted in Data.Fin.Base
, we’ve set up
the ordering on Fin
so that we can re-use all the proofs
about the ordering on Nat
.
However, there are still quite a few interesting things one can say
about skip
and
squish
. In particular, we
can prove the simplicial identities, which characterize the
interactions between these two functions.
These lemmas might seem somewhat arbitrary and complicated, which is
true! However, they are enough to describe all the possible interactions
of skip
and squish
, which in turn are
the building blocks for every monotone function between Fin
, so it’s not that
surprising that they would be a bit of a mess!
skip-comm : ∀ {n} (i j : Fin (suc n)) → i ≤ j → ∀ x → skip (weaken i) (skip j x) ≡ skip (fsuc j) (skip i x) skip-comm i j le x with fin-view i | fin-view j | le | fin-view x ... | zero | zero | _ | _ = refl ... | zero | suc _ | _ | _ = refl ... | suc i | suc j | le | zero = refl ... | suc i | suc j | s≤s le | (suc x) = ap fsuc (skip-comm i j le x) drop-comm : ∀ {n} (i j : Fin n) → i ≤ j → ∀ x → squish j (squish (weaken i) x) ≡ squish i (squish (fsuc j) x) drop-comm i j le x with fin-view i | fin-view j | le | fin-view x ... | zero | zero | le | zero = refl ... | zero | zero | le | suc x = refl ... | zero | suc j | le | zero = refl ... | zero | suc j | le | suc x = refl ... | suc i | suc j | le | zero = refl ... | suc i | suc j | s≤s le | suc x = ap fsuc (drop-comm i j le x) squish-skip-comm : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i < fsuc j → ∀ x → squish (fsuc j) (skip (weaken i) x) ≡ skip i (squish j x) squish-skip-comm i j le x with fin-view i | fin-view j | le | fin-view x ... | zero | zero | s≤s p | zero = refl ... | zero | zero | s≤s p | suc _ = refl ... | zero | suc _ | s≤s p | zero = refl ... | zero | suc _ | s≤s p | suc _ = refl ... | suc i | (suc j) | (Nat.s≤s p) | zero = refl ... | suc i | (suc j) | (Nat.s≤s p) | (suc x) = ap fsuc (squish-skip-comm i j p x) squish-skip : ∀ {n} (i j : Fin n) → i ≡ j → ∀ x → squish j (skip (weaken j) x) ≡ x squish-skip i j p x with fin-view i | fin-view j | fin-view x ... | zero | zero | x = refl ... | zero | (suc j) | x = absurd (fzero≠fsuc p) ... | (suc i) | zero | x = refl ... | (suc i) | (suc j) | zero = refl ... | (suc i) | (suc j) | (suc x) = ap fsuc (squish-skip i j (fsuc-inj p) x) squish-skip-fsuc : ∀ {n} (i : Fin (suc n)) (j : Fin n) → i ≡ fsuc j → ∀ x → squish j (skip i x) ≡ x squish-skip-fsuc i j p x with fin-view i | fin-view j | fin-view x ... | zero | zero | x = refl ... | zero | suc j | x = absurd (fzero≠fsuc p) ... | suc i | suc j | zero = refl ... | suc i | suc j | suc x = ap fsuc (squish-skip-fsuc i j (fsuc-inj p) x) ... | suc i | zero | x with fin-view i | x ... | zero | zero = refl ... | zero | suc x = refl ... | suc i | zero = refl ... | suc i | suc x = absurd (Nat.zero≠suc λ i → Nat.pred (p (~ i) .lower)) Fin-suc : ∀ {n} → Fin (suc n) ≃ Maybe (Fin n) Fin-suc = Iso→Equiv (to , iso from ir il) where to : ∀ {n} → Fin (suc n) → Maybe (Fin n) to i with fin-view i ... | suc i = just i ... | zero = nothing from : ∀ {n} → Maybe (Fin n) → Fin (suc n) from (just x) = fsuc x from nothing = fzero ir : is-right-inverse from to ir nothing = refl ir (just x) = refl il : is-left-inverse from to il i with fin-view i ... | suc i = refl ... | zero = refl Fin-peel : ∀ {l k} → Fin (suc l) ≃ Fin (suc k) → Fin l ≃ Fin k Fin-peel {l} {k} sl≃sk = Maybe-injective (Equiv.inverse Fin-suc ∙e sl≃sk ∙e Fin-suc) Fin-injective : ∀ {l k} → Fin l ≃ Fin k → l ≡ k Fin-injective {zero} {zero} l≃k = refl Fin-injective {zero} {suc k} l≃k with equiv→inverse (l≃k .snd) fzero ... | () Fin-injective {suc l} {zero} l≃k with l≃k .fst fzero ... | () Fin-injective {suc l} {suc k} sl≃sk = ap suc $ Fin-injective (Fin-peel sl≃sk) avoid-injective : ∀ {n} (i : Fin (suc n)) {j k : Fin (suc n)} {i≠j : i ≠ j} {i≠k : i ≠ k} → avoid i j i≠j ≡ avoid i k i≠k → j ≡ k avoid-injective i {j} {k} {i≠j} {i≠k} p with fin-view i | fin-view j | fin-view k ... | zero | zero | _ = absurd (i≠j refl) ... | zero | suc j | zero = absurd (i≠k refl) ... | zero | suc j | suc k = ap fsuc p ... | suc i | zero | zero = refl avoid-injective {suc n} _ p | suc i | zero | suc k = absurd (fzero≠fsuc p) avoid-injective {suc n} _ p | suc i | suc j | zero = absurd (fsuc≠fzero p) avoid-injective {suc n} _ p | suc i | suc j | suc k = ap fsuc (avoid-injective {n} i {j} {k} (fsuc-inj p)) skip-injective : ∀ {n} (i : Fin (suc n)) (j k : Fin n) → skip i j ≡ skip i k → j ≡ k skip-injective i j k p with fin-view i | fin-view j | fin-view k ... | zero | j | k = fsuc-inj p ... | suc i | zero | zero = refl ... | suc i | zero | suc k = absurd (fzero≠fsuc p) ... | suc i | suc j | zero = absurd (fsuc≠fzero p) ... | suc i | suc j | suc k = ap fsuc (skip-injective i j k (fsuc-inj p)) skip-skips : ∀ {n} (i : Fin (suc n)) (j : Fin n) → skip i j ≠ i skip-skips i j p with fin-view i | fin-view j ... | zero | j = fsuc≠fzero p ... | suc i | zero = fzero≠fsuc p ... | suc i | suc j = skip-skips i j (fsuc-inj p) avoid-skip : ∀ {n} (i : Fin (suc n)) (j : Fin n) {neq : i ≠ skip i j} → avoid i (skip i j) neq ≡ j avoid-skip i j with fin-view i | fin-view j ... | zero | zero = refl ... | zero | suc j = refl ... | suc i | zero = refl ... | suc i | suc j = ap fsuc (avoid-skip i j) skip-avoid : ∀ {n} (i : Fin (suc n)) (j : Fin (suc n)) {i≠j : i ≠ j} → skip i (avoid i j i≠j) ≡ j skip-avoid i j {i≠j} with fin-view i | fin-view j ... | zero | zero = absurd (i≠j refl) skip-avoid {suc n} _ _ | zero | suc j = refl skip-avoid {suc n} _ _ | suc i | zero = refl skip-avoid {suc n} _ _ | suc i | suc j = ap fsuc (skip-avoid i j)
Iterated products and sums🔗
We can break down and over finite sets as iterated products and sums, respectively.
Fin-suc-Π : ∀ {ℓ} {n} {A : Fin (suc n) → Type ℓ} → (∀ x → A x) ≃ (A fzero × (∀ x → A (fsuc x))) Fin-suc-Π = Iso→Equiv λ where .fst f → f fzero , (λ x → f (fsuc x)) .snd .is-iso.inv (z , s) → fin-cons z s .snd .is-iso.rinv x → refl .snd .is-iso.linv k i fzero → k (fin zero ⦃ forget auto ⦄) .snd .is-iso.linv k i (fin (suc n) ⦃ b ⦄) → k (fin (suc n) ⦃ b ⦄) Fin-suc-Σ : ∀ {ℓ} {n} {A : Fin (suc n) → Type ℓ} → Σ (Fin (suc n)) A ≃ (A fzero ⊎ Σ (Fin n) (A ∘ fsuc)) Fin-suc-Σ {A = A} = Iso→Equiv (to , iso from ir il) where to : ∫ₚ A → A fzero ⊎ ∫ₚ (A ∘ fsuc) to (i , a) with fin-view i ... | zero = inl a ... | suc x = inr (x , a) from : A fzero ⊎ ∫ₚ (A ∘ fsuc) → ∫ₚ A from (inl x) = fzero , x from (inr (x , a)) = fsuc x , a ir : is-right-inverse from to ir (inl x) = refl ir (inr x) = refl il : is-left-inverse from to il (i , a) with fin-view i ... | zero = refl ... | suc _ = refl
Finite choice🔗
An important fact about the (standard) finite sets in constructive
mathematics is that they always support choice, which we phrase
below as a “search” operator: if
is any Monoidal
functor on types, then it commutes with products. Since
over
are
iterated products, we have
that
commutes with
Fin-Monoidal : ∀ {ℓ} n {A : Fin n → Type ℓ} {M} (let module M = Effect M) → ⦃ Monoidal M ⦄ → (∀ x → M.₀ (A x)) → M.₀ (∀ x → A x) Fin-Monoidal zero _ = invmap (λ _ ()) _ munit Fin-Monoidal (suc n) k = Fin-suc-Π e⁻¹ <≃> (k 0 <,> Fin-Monoidal n (k ∘ fsuc))
In particular, instantiating
with the propositional truncation
(which is an Idiom
and
hence Monoidal
),
we get a version of the axiom of choice for finite
sets.
finite-choice : ∀ {ℓ} n {A : Fin n → Type ℓ} → (∀ x → ∥ A x ∥) → ∥ (∀ x → A x) ∥ finite-choice n = Fin-Monoidal n
An immediate consequence is that surjections into a finite set (thus, between finite sets) merely split:
finite-surjection-split : ∀ {ℓ} {n} {B : Type ℓ} → (f : B → Fin n) → is-surjective f → ∥ (∀ x → fibre f x) ∥ finite-surjection-split f = finite-choice _
Dually, we have that any Alternative
functor
commutes with
on finite sets, since those are iterated sums.
Fin-Alternative : ∀ {ℓ} n {A : Fin n → Type ℓ} {M} (let module M = Effect M) → ⦃ Alternative M ⦄ → (∀ x → M.₀ (A x)) → M.₀ (Σ (Fin n) A) Fin-Alternative zero _ = invmap (λ ()) (λ ()) empty Fin-Alternative (suc n) k = Fin-suc-Σ e⁻¹ <≃> (k 0 <+> Fin-Alternative n (k ∘ fsuc))
As a consequence, instantiating
with Dec
, we
get that finite sets are exhaustible and
omniscient, which means that any family of decidable
types indexed by a finite sets yields decidable
and
respectively.
instance Dec-Fin-∀ : ∀ {n ℓ} {A : Fin n → Type ℓ} → ⦃ ∀ {x} → Dec (A x) ⦄ → Dec (∀ x → A x) Dec-Fin-∀ {n} ⦃ d ⦄ = Fin-Monoidal n (λ _ → d) Dec-Fin-Σ : ∀ {n ℓ} {A : Fin n → Type ℓ} → ⦃ ∀ {x} → Dec (A x) ⦄ → Dec (Σ (Fin n) A) Dec-Fin-Σ {n} ⦃ d ⦄ = Fin-Alternative n λ _ → d
Fin-omniscience : ∀ {n ℓ} (P : Fin n → Type ℓ) ⦃ _ : ∀ {x} → Dec (P x) ⦄ → (Σ[ j ∈ Fin n ] P j × ∀ k → P k → j ≤ k) ⊎ (∀ x → ¬ P x) Fin-omniscience {zero} P = inr λ () Fin-omniscience {suc n} P with holds? (P 0) ... | yes here = inl (0 , here , λ _ _ → 0≤x) ... | no ¬here with Fin-omniscience (P ∘ fsuc) ... | inl (ix , pix , least) = inl (fsuc ix , pix , fin-cons (λ here → absurd (¬here here)) λ i pi → Nat.s≤s (least i pi)) ... | inr nowhere = inr (fin-cons ¬here nowhere)
Fin-omniscience-neg : ∀ {n ℓ} (P : Fin n → Type ℓ) ⦃ _ : ∀ {x} → Dec (P x) ⦄ → (∀ x → P x) ⊎ (Σ[ j ∈ Fin n ] ¬ P j × ∀ k → ¬ P k → j ≤ k) Fin-omniscience-neg P with Fin-omniscience (¬_ ∘ P) ... | inr p = inl λ i → dec→dne (p i) ... | inl (j , ¬pj , least) = inr (j , ¬pj , least) Fin-find : ∀ {n ℓ} {P : Fin n → Type ℓ} ⦃ _ : ∀ {x} → Dec (P x) ⦄ → ¬ (∀ x → P x) → Σ[ x ∈ Fin n ] ¬ P x × ∀ y → ¬ P y → x ≤ y Fin-find {P = P} ¬p with Fin-omniscience-neg P ... | inl p = absurd (¬p p) ... | inr p = p
Injections and surjections🔗
The standard finite sets are Dedekind-finite, which means that every injection is a bijection. We prove this by a straightforward but annoying induction on
Fin-injection→equiv : ∀ {n} (f : Fin n → Fin n) → injective f → is-equiv f Fin-injection→equiv {zero} f inj .is-eqv () Fin-injection→equiv {suc n} f inj .is-eqv i with f 0 ≡? i ... | yes p = contr (0 , p) λ (j , p') → Σ-prop-path! (inj (p ∙ sym p')) ... | no ¬p = contr fib cen where rec = Fin-injection→equiv {n} (λ x → avoid (f 0) (f (fsuc x)) (Nat.zero≠suc ∘ ap lower ∘ inj)) (λ p → fsuc-inj (inj (avoid-injective (f 0) p))) .is-eqv (avoid (f 0) i ¬p) fib : fibre f i fib = fsuc (rec .centre .fst) , avoid-injective (f 0) (rec .centre .snd) cen : ∀ x → fib ≡ x cen (i , p) with fin-view i ... | zero = absurd (¬p p) ... | suc j = Σ-prop-path! (ap (fsuc ∘ fst) (rec .paths (j , ap₂ (avoid (f 0)) p prop!)))
Since every surjection between finite sets splits, any surjection has an injective right inverse, which is thus a bijection; by general properties of equivalences, this implies that is also a bijection.
Fin-surjection→equiv : ∀ {n} (f : Fin n → Fin n) → is-surjective f → is-equiv f Fin-surjection→equiv f surj = case finite-surjection-split f surj of λ split → left-inverse→equiv (snd ∘ split) (Fin-injection→equiv (fst ∘ split) (right-inverse→injective f (snd ∘ split)))
Vector operations🔗
avoid-insert : ∀ {n} {ℓ} {A : Type ℓ} → (ρ : Fin n → A) → (i : Fin (suc n)) (a : A) → (j : Fin (suc n)) → (i≠j : i ≠ j) → (ρ [ i ≔ a ]) j ≡ ρ (avoid i j i≠j) avoid-insert ρ i a j i≠j with fin-view i | fin-view j ... | zero | zero = absurd (i≠j refl) ... | zero | suc j = refl avoid-insert {suc n} ρ _ a _ _ | suc i | zero = refl avoid-insert {suc n} ρ _ a _ i≠j | suc i | suc j = avoid-insert (ρ ∘ fsuc) i a j (i≠j ∘ ap fsuc) insert-lookup : ∀ {n} {ℓ} {A : Type ℓ} → (ρ : Fin n → A) → (i : Fin (suc n)) (a : A) → (ρ [ i ≔ a ]) i ≡ a insert-lookup {n = n} ρ i a with fin-view i ... | zero = refl insert-lookup {n = suc n} ρ _ a | suc i = insert-lookup (ρ ∘ fsuc) i a delete-insert : ∀ {n} {ℓ} {A : Type ℓ} → (ρ : Fin n → A) → (i : Fin (suc n)) (a : A) → ∀ j → delete (ρ [ i ≔ a ]) i j ≡ ρ j delete-insert ρ i a j with fin-view i | fin-view j ... | zero | j = refl ... | suc i | zero = refl ... | suc i | (suc j) = delete-insert (ρ ∘ fsuc) i a j insert-delete : ∀ {n} {ℓ} {A : Type ℓ} → (ρ : Fin (suc n) → A) → (i : Fin (suc n)) (a : A) → ρ i ≡ a → ∀ j → ((delete ρ i) [ i ≔ a ]) j ≡ ρ j insert-delete ρ i a p j with fin-view i | fin-view j ... | zero | zero = sym p ... | zero | suc j = refl insert-delete {suc n} ρ _ a p _ | suc i | zero = refl insert-delete {suc n} ρ _ a p _ | suc i | suc j = insert-delete (ρ ∘ fsuc) i a p j ℕ< : Nat → Type ℕ< n = Σ[ k ∈ Nat ] k Nat.< n from-ℕ< : ∀ {n} → ℕ< n → Fin n from-ℕ< (i , p) = fin i ⦃ forget p ⦄ to-ℕ< : ∀ {n} → Fin n → ℕ< n to-ℕ< (fin i ⦃ forget p ⦄) = i , recover p