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))
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 extension system (for example, the propositional truncation monad), then commutes with finite products:
finite-choice : β {β} n {A : Fin n β Type β} {M} (let module M = Effect M) β β¦ Idiom M β¦ β (β x β M.β (A x)) β M.β (β x β A x) finite-choice zero _ = pure Ξ» () finite-choice (suc n) {A} k = β¦ elim (k fzero) (finite-choice n (k β fsuc)) β¦ where elim : A fzero β (β x β A (fsuc x)) β β x β A x elim azero asuc fzero = azero elim azero asuc (fsuc x) = asuc x
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 _
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