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 fzero    j        le x        = refl
skip-comm (fsuc i) (fsuc j) le fzero    = refl
skip-comm (fsuc i) (fsuc j) (Nat.sā‰¤s le) (fsuc 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 fzero    fzero    le fzero = refl
drop-comm fzero    fzero    le (fsuc x) = refl
drop-comm fzero    (fsuc j) le fzero = refl
drop-comm fzero    (fsuc j) le (fsuc x) = refl
drop-comm (fsuc i) (fsuc j) le fzero = refl
drop-comm (fsuc i) (fsuc j) (Nat.sā‰¤s le) (fsuc 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 fzero j (Nat.sā‰¤s p) x = refl
squish-skip-comm (fsuc i) (fsuc j) (Nat.sā‰¤s p) fzero = refl
squish-skip-comm (fsuc i) (fsuc j) (Nat.sā‰¤s p) (fsuc 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 fzero fzero p x = refl
squish-skip fzero (fsuc j) p x = absurd (fzeroā‰ fsuc p)
squish-skip (fsuc i) fzero p x = refl
squish-skip (fsuc i) (fsuc j) p fzero = refl
squish-skip (fsuc i) (fsuc j) p (fsuc 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 fzero fzero p x = refl
squish-skip-fsuc fzero (fsuc j) p x = absurd (fzeroā‰ fsuc p)
squish-skip-fsuc (fsuc i) fzero p fzero = refl
squish-skip-fsuc (fsuc fzero) fzero p (fsuc x) = refl
squish-skip-fsuc (fsuc (fsuc i)) fzero p (fsuc x) =
  absurd (fzeroā‰ fsuc (fsuc-inj (sym p)))
squish-skip-fsuc (fsuc i) (fsuc j) p fzero = refl
squish-skip-fsuc (fsuc i) (fsuc j) p (fsuc x) =
  ap fsuc (squish-skip-fsuc i j (fsuc-inj p) x)

Fin-peel : āˆ€ {l k} ā†’ Fin (suc l) ā‰ƒ Fin (suc k) ā†’ Fin l ā‰ƒ Fin k
Fin-peel {l} {k} slā‰ƒsk = (Isoā†’Equiv (lā†’k , (iso kā†’l bā†’aā†’b aā†’bā†’a))) where
  skā‰ƒsl : Fin (suc k) ā‰ƒ Fin (suc l)
  skā‰ƒsl = slā‰ƒsk eā»Ā¹
  module slā‰ƒsk = Equiv slā‰ƒsk
  module skā‰ƒsl = Equiv skā‰ƒsl

  lā†’k : Fin l ā†’ Fin k
  lā†’k x with inspect (slā‰ƒsk.to (fsuc x))
  ... | fsuc y , _ = y
  ... | fzero , p with inspect (slā‰ƒsk.to fzero)
  ... | fsuc y , _ = y
  ... | fzero , q = absurd (fzeroā‰ fsuc (slā‰ƒsk.injectiveā‚‚ q p))

  kā†’l : Fin k ā†’ Fin l
  kā†’l x with inspect (skā‰ƒsl.to (fsuc x))
  ... | fsuc x , _ = x
  ... | fzero , p with inspect (skā‰ƒsl.to fzero)
  ... | fsuc y , _ = y
  ... | fzero , q = absurd (fzeroā‰ fsuc (skā‰ƒsl.injectiveā‚‚ q p))

  absurd-path : āˆ€ {ā„“} {A : Type ā„“} {y : A} .{x : āŠ„} ā†’ absurd x ā‰” y
  absurd-path {x = ()}

  aā†’bā†’a : āˆ€ a ā†’ kā†’l (lā†’k a) ā‰” a
  aā†’bā†’a a with inspect (slā‰ƒsk.to (fsuc a))
  aā†’bā†’a a | fsuc x , p' with inspect (skā‰ƒsl.to (fsuc x))
  aā†’bā†’a a | fsuc x , p' | fsuc y , q' = fsuc-inj (
    sym q' āˆ™ ap (skā‰ƒsl.to) (sym p') āˆ™ slā‰ƒsk.Ī· _)
  aā†’bā†’a a | fsuc x , p' | fzero , q' = absurd contra where
    r = slā‰ƒsk.injectiveā‚‚ p' (slā‰ƒsk.Īµ (fsuc x))
    contra = fzeroā‰ fsuc (sym (r āˆ™ q'))
  aā†’bā†’a a | fzero , p' with inspect (slā‰ƒsk.to fzero)
  aā†’bā†’a a | fzero , p' | fsuc x , q' with inspect (skā‰ƒsl.to (fsuc x))
  aā†’bā†’a a | fzero , p' | fsuc x , q' | fsuc y , r' = absurd do
    fzeroā‰ fsuc (sym (sym r' āˆ™ ap skā‰ƒsl.to (sym q') āˆ™ slā‰ƒsk.Ī· fzero))
  aā†’bā†’a a | fzero , p' | fsuc x , q' | fzero , r' with inspect (skā‰ƒsl.to fzero)
  aā†’bā†’a a | fzero , p' | fsuc x , q' | fzero , r' | fsuc z , s = fsuc-inj $
    sym s āˆ™ ap skā‰ƒsl.to (sym p') āˆ™ slā‰ƒsk.Ī· (fsuc a)
  aā†’bā†’a a | fzero , p' | fsuc x , q' | fzero , r' | fzero , s = absurd-path
  aā†’bā†’a a | fzero , p' | fzero , q' = absurd (fzeroā‰ fsuc $
    slā‰ƒsk.injectiveā‚‚ q' p')

  bā†’aā†’b : āˆ€ b ā†’ lā†’k (kā†’l b) ā‰” b
  bā†’aā†’b b with inspect (skā‰ƒsl.to (fsuc b))
  bā†’aā†’b b | fsuc x , p' with inspect (slā‰ƒsk.to (fsuc x))
  bā†’aā†’b b | fsuc x , p' | fsuc y , q' = fsuc-inj $
    sym q' āˆ™ ap (slā‰ƒsk.to) (sym p') āˆ™ skā‰ƒsl.Ī· _
  bā†’aā†’b b | fsuc x , p' | fzero , q' = absurd contra where
    r = skā‰ƒsl.injectiveā‚‚ p' (skā‰ƒsl.Īµ (fsuc x))
    contra = fzeroā‰ fsuc (sym (r āˆ™ q'))
  bā†’aā†’b b | fzero , p' with inspect (skā‰ƒsl.to fzero)
  bā†’aā†’b b | fzero , p' | fsuc x , q' with inspect (slā‰ƒsk.to (fsuc x))
  bā†’aā†’b b | fzero , p' | fsuc x , q' | fsuc y , r'  = absurd (fzeroā‰ fsuc $
    sym (sym r' āˆ™ ap (slā‰ƒsk.to) (sym q') āˆ™ skā‰ƒsl.Ī· _))
  bā†’aā†’b b | fzero , p' | fsuc x , q' | fzero , r' with inspect (slā‰ƒsk.to fzero)
  bā†’aā†’b a | fzero , p' | fsuc x , q' | fzero , r' | fsuc z , s = fsuc-inj $
    sym s āˆ™ ap (slā‰ƒsk.to) (sym p') āˆ™ skā‰ƒsl.Ī· (fsuc a)
  bā†’aā†’b a | fzero , p' | fsuc x , q' | fzero , r' | fzero , s = absurd-path
  bā†’aā†’b b | fzero , p' | fzero , q' = absurd (fzeroā‰ fsuc $
    skā‰ƒsl.injectiveā‚‚ q' p')

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)

to-from-ā„•< : āˆ€ {n} (x : ā„•< n) ā†’ to-ā„•< {n = n} (from-ā„•< x) ā‰” x
to-from-ā„•< {n = suc n} x = Ī£-prop-path! (to-from-ā„• {n = suc n} x) where
  to-from-ā„• : āˆ€ {n} x ā†’ to-nat {n = n} (from-ā„•< x) ā‰” x .fst
  to-from-ā„• {n = suc n} (zero , p) = refl
  to-from-ā„• {n = suc n} (suc x , Nat.sā‰¤s p) = ap suc (to-from-ā„• {n = n} (x , p))

from-to-ā„•< : āˆ€ {n} (x : Fin n) ā†’ from-ā„•< (to-ā„•< x) ā‰” x
from-to-ā„•< fzero = refl
from-to-ā„•< (fsuc x) = ap fsuc (from-to-ā„•< x)

Finā‰ƒā„•< : āˆ€ {n} ā†’ Fin n ā‰ƒ ā„•< n
Finā‰ƒā„•< {n} = to-ā„•< , is-isoā†’is-equiv (iso from-ā„•< (to-from-ā„•< {n}) from-to-ā„•<)

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 fzero {fzero} {k} {iā‰ j} p = absurd (iā‰ j refl)
avoid-injective fzero {fsuc j} {fzero} {iā‰ k = iā‰ k} p = absurd (iā‰ k refl)
avoid-injective {suc n} fzero {fsuc j} {fsuc k} p = ap fsuc p
avoid-injective {suc n} (fsuc i) {fzero} {fzero} p = refl
avoid-injective {suc n} (fsuc i) {fzero} {fsuc k} p = absurd (fzeroā‰ fsuc p)
avoid-injective {suc n} (fsuc i) {fsuc j} {fzero} p = absurd (fzeroā‰ fsuc (sym p))
avoid-injective {suc n} (fsuc i) {fsuc j} {fsuc k} p =
  ap fsuc (avoid-injective {n} i {j} {k} (fsuc-inj p))

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 , f) fzero    ā†’ z
  .snd .is-iso.inv (z , f) (fsuc x) ā†’ f x

  .snd .is-iso.rinv x ā†’ refl

  .snd .is-iso.linv k i fzero    ā†’ k fzero
  .snd .is-iso.linv k i (fsuc n) ā†’ k (fsuc n)

Fin-suc-Ī£
  : āˆ€ {ā„“} {n} {A : Fin (suc n) ā†’ Type ā„“}
  ā†’ Ī£ (Fin (suc n)) A ā‰ƒ (A fzero āŠŽ Ī£ (Fin n) (A āˆ˜ fsuc))
Fin-suc-Ī£ = Isoā†’Equiv Ī» where
  .fst (fzero , a) ā†’ inl a
  .fst (fsuc x , a) ā†’ inr (x , a)

  .snd .is-iso.inv (inl a) ā†’ fzero , a
  .snd .is-iso.inv (inr (x , a)) ā†’ fsuc x , a

  .snd .is-iso.rinv (inl _) ā†’ refl
  .snd .is-iso.rinv (inr _) ā†’ refl

  .snd .is-iso.linv (fzero , a) ā†’ refl
  .snd .is-iso.linv (fsuc x , a) ā†’ 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
  Fin-exhaustible
    : āˆ€ {n ā„“} {A : Fin n ā†’ Type ā„“}
    ā†’ ā¦ƒ āˆ€ {x} ā†’ Dec (A x) ā¦„ ā†’ Dec (āˆ€ x ā†’ A x)
  Fin-exhaustible {n} ā¦ƒ d ā¦„ = Fin-Monoidal n Ī» _ ā†’ d

  Fin-omniscient
    : āˆ€ {n ā„“} {A : Fin n ā†’ Type ā„“}
    ā†’ ā¦ƒ āˆ€ {x} ā†’ Dec (A x) ā¦„ ā†’ Dec (Ī£ (Fin n) A)
  Fin-omniscient {n} ā¦ƒ d ā¦„ = Fin-Alternative n Ī» _ ā†’ d

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
  (fsuc (rec .centre .fst) , avoid-injective (f 0) (rec .centre .snd))
  Ī» where
    (fzero , p) ā†’ absurd (Ā¬p p)
    (fsuc j , p) ā†’ Ī£-prop-path! (ap (fsuc āˆ˜ fst)
      (rec .paths (j , apā‚‚ (avoid (f 0)) p prop!)))
  where
    rec = Fin-injectionā†’equiv {n}
      (Ī» x ā†’ avoid (f 0) (f (fsuc x)) (fzeroā‰ fsuc āˆ˜ inj))
      (Ī» p ā†’ fsuc-inj (inj (avoid-injective (f 0) p)))
      .is-eqv (avoid (f 0) i Ā¬p)

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 {n = n} Ļ fzero a fzero iā‰ j = absurd (iā‰ j refl)
avoid-insert {n = suc n} Ļ fzero a (fsuc j) iā‰ j = refl
avoid-insert {n = suc n} Ļ (fsuc i) a fzero iā‰ j = refl
avoid-insert {n = suc n} Ļ (fsuc i) a (fsuc j) iā‰ 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} Ļ fzero a = refl
insert-lookup {n = suc n} Ļ (fsuc i) a = 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 Ļ fzero a j = refl
delete-insert Ļ (fsuc i) a fzero = refl
delete-insert Ļ (fsuc i) a (fsuc 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 {n = n} Ļ fzero a p fzero = sym p
insert-delete {n = n} Ļ fzero a p (fsuc j) = refl
insert-delete {n = suc n} Ļ (fsuc i) a p fzero = refl
insert-delete {n = suc n} Ļ (fsuc i) a p (fsuc j) = insert-delete (Ļ āˆ˜ fsuc) i a p j