open import 1Lab.Prelude

open import Data.Set.Coequaliser
open import Data.Fin.Properties
open import Data.Fin.Base
open import Data.Dec
open import Data.Sum

open import Meta.Invariant

open is-iso

module Data.Fin.Closure where

private variable
â : Level
A B C : Type â
k l m n : Nat


# Closure of finite setsð

In this module, we prove that the finite sets are closed under âtypal arithmeticâ: The initial and terminal objects are finite (they have 1 and 0 elements respectively), products of finite sets are finite, coproducts of finite sets are finite, and functions between finite sets are finite. Moreover, these operations all correspond to arithmetic operations on the natural number indices: etc.

## Zero, one, successorsð

The finite set is an initial object, and the finite set is a terminal object:

Finite-zero-is-initial : Fin 0 â â¥
Finite-zero-is-initial .fst ()
Finite-zero-is-initial .snd .is-eqv ()

Finite-one-is-contr : is-contr (Fin 1)
Finite-one-is-contr .centre = fzero
Finite-one-is-contr .paths fzero = refl


The successor operation on indices corresponds to taking coproducts with the unit set.

Finite-successor : Fin (suc n) â (â€ â Fin n)
Finite-successor {n} = IsoâEquiv (f , iso g f-g g-f) where
f : Fin (suc n) â â€ â Fin n
f fzero = inl tt
f (fsuc x) = inr x

g : â€ â Fin n â Fin (suc n)
g (inr x) = fsuc x
g (inl _) = fzero

f-g : is-right-inverse g f
f-g (inr _) = refl
f-g (inl _) = refl

g-f : is-left-inverse g f
g-f fzero = refl
g-f (fsuc x) = refl


For binary coproducts, we prove the correspondence with addition in steps, to make the proof clearer:

Finite-coproduct : (Fin n â Fin m) â Fin (n + m)
Finite-coproduct {zero} {m}  =
(Fin 0 â Fin m) ââš â-apl Finite-zero-is-initial â©â
(â¥ â Fin m)     ââš â-zerol â©â
Fin m           ââ
Finite-coproduct {suc n} {m} =
(Fin (suc n) â Fin m) ââš â-apl Finite-successor â©â
((â€ â Fin n) â Fin m) ââš â-assoc â©â
(â€ â (Fin n â Fin m)) ââš â-apr (Finite-coproduct {n} {m}) â©â
(â€ â Fin (n + m))     ââš Finite-successor eâ»Â¹ â©â
Fin (suc (n + m))     ââ


### Sumsð

We also have a correspondence between âcoproductsâ and âadditionâ in the iterated case: If you have a family of finite types (represented by a map to their cardinalities), the dependent sum of that family is equivalent to the iterated binary sum of the cardinalities:

sum : â n â (Fin n â Nat) â Nat
sum zero f = zero
sum (suc n) f = f fzero + sum n (f â fsuc)

Finite-sum : (B : Fin n â Nat) â Î£ (Fin _) (Fin â B) â Fin (sum n B)
Finite-sum {zero} B .fst ()
Finite-sum {zero} B .snd .is-eqv ()
Finite-sum {suc n} B =
Î£ (Fin (suc n)) (Fin â B)              ââš Fin-suc-Î£ â©â
Fin (B 0) â Î£ (Fin n) (Fin â B â fsuc) ââš â-apr (Finite-sum (B â fsuc)) â©â
Fin (B 0) â Fin (sum n (B â fsuc))     ââš Finite-coproduct â©â
Fin (sum (suc n) B)                    ââ


## Multiplicationð

Recall (from middle school) that the product is the same thing as summing together copies of the number Correspondingly, we can use the theorem above for general sums to establish the case of binary products:

Finite-multiply : (Fin n Ã Fin m) â Fin (n * m)
Finite-multiply {n} {m} =
(Fin n Ã Fin m)       ââš Finite-sum (Î» _ â m) â©â
Fin (sum n (Î» _ â m)) ââš cast (sumâ¡* n m) , cast-is-equiv _ â©â
Fin (n * m)           ââ
where
sumâ¡* : â n m â sum n (Î» _ â m) â¡ n * m
sumâ¡* zero m = refl
sumâ¡* (suc n) m = ap (m +_) (sumâ¡* n m)


## Productsð

Similarly to the case for sums, the cardinality of a dependent product of finite sets is the product of the cardinalities:

product : â n â (Fin n â Nat) â Nat
product zero f = 1
product (suc n) f = f fzero * product n (f â fsuc)

Finite-product : (B : Fin n â Nat) â (â x â Fin (B x)) â Fin (product n B)
Finite-product {zero} B .fst _ = fzero
Finite-product {zero} B .snd = is-isoâis-equiv Î» where
.is-iso.inv _ ()
.is-iso.rinv fzero â refl
.is-iso.linv _ â funext Î» ()
Finite-product {suc n} B =
(â x â Fin (B x))                          ââš Fin-suc-Î  â©â
Fin (B fzero) Ã (â x â Fin (B (fsuc x)))   ââš Î£-ap-snd (Î» _ â Finite-product (B â fsuc)) â©â
Fin (B fzero) Ã Fin (product n (B â fsuc)) ââš Finite-multiply â©â
Fin (B fzero * product n (B â fsuc))       ââ


## Decidable subsetsð

Given a decidable predicate on we can compute such that is equivalent to the subset of on which the predicate holds: a decidable proposition is finite (it has either or elements), so we can reuse our proof that finite sums of finite types are finite.

DecâFin
: â {â} {A : Type â} â is-prop A â Dec A
â Î£ Nat Î» n â Fin n â A
DecâFin ap (no Â¬a) .fst = 0
DecâFin ap (no Â¬a) .snd =
is-emptyââ (Finite-zero-is-initial .fst) Â¬a
DecâFin ap (yes a) .fst = 1
DecâFin ap (yes a) .snd =
is-contrââ Finite-one-is-contr (is-propââis-contr ap a)

Finite-subset
: â {n} (P : Fin n â Type â)
â âŠ â {x} â H-Level (P x) 1 âŠ
â âŠ dec : â {x} â Dec (P x) âŠ
â Î£ Nat Î» s â Fin s â Î£ (Fin n) P
Finite-subset {n = n} P âŠ dec = dec âŠ =
sum n ns , Finite-sum ns eâ»Â¹ âe Î£-ap-snd es
where
ns : Fin n â Nat
ns i = DecâFin (hlevel 1) dec .fst
es : (i : Fin n) â Fin (ns i) â P i
es i = DecâFin (hlevel 1) dec .snd


## Decidable quotientsð

As a first step towards coequalisers, we show that the quotient of a finite set by a decidable congruence is finite.

Finite-quotient
: â {n â} (R : Congruence (Fin n) â) (open Congruence R)
â âŠ _ : â {x y} â Dec (x âŒ y) âŠ
â Î£ Nat Î» q â Fin q â Fin n / _âŒ_


This amounts to counting the number of equivalence classes of We proceed by induction on the base case is trivial.

Finite-quotient {zero} R .fst = 0
Finite-quotient {zero} R .snd .fst ()
Finite-quotient {zero} R .snd .snd .is-eqv = elim! Î» ()


For the induction step, we restrict along the successor map to get a congruence on whose quotient is finite.

Finite-quotient {suc n} {â} R = go where
module R = Congruence R

Râ : Congruence (Fin n) â
Râ = Congruence-pullback fsuc R
module Râ = Congruence Râ

n/Râ : Î£ Nat Î» q â Fin q â Fin n / Râ._âŒ_
n/Râ = Finite-quotient {n} Râ


In order to compute the size of the quotient we decide whether is related by to any using the omniscience of finite sets.

  go
: âŠ Dec (Î£ (Fin n) (Î» i â fzero R.âŒ fsuc i)) âŠ
â Î£ Nat (Î» q â Fin q â Fin (suc n) / R._âŒ_)


If so, lives in the same equivalence class as and the size of the quotient remains unchanged.

  go âŠ yes (i , r) âŠ .fst = n/Râ .fst
go âŠ yes (i , r) âŠ .snd = n/Râ .snd âe IsoâEquiv is where
is : Iso (Fin n / Râ._âŒ_) (Fin (suc n) / R._âŒ_)
is .fst = Coeq-rec (Î» x â inc (fsuc x)) Î» (x , y , s) â quot s
is .snd .inv = Coeq-rec
(Î» where fzero â inc i
(fsuc x) â inc x)
(Î» where (fzero , fzero , s) â refl
(fzero , fsuc y , s) â quot (R.symá¶ r R.âá¶ s)
(fsuc x , fzero , s) â quot (s R.âá¶ r)
(fsuc x , fsuc y , s) â quot s)
is .snd .rinv = elim! Î» where
fzero â quot (R.symá¶ r)
(fsuc x) â refl
is .snd .linv = elim! Î» _ â refl


Otherwise, creates a new equivalence class for itself.

  go âŠ no Â¬r âŠ .fst = suc (n/Râ .fst)
go âŠ no Â¬r âŠ .snd = Finite-successor âe â-apr (n/Râ .snd) âe IsoâEquiv is where
to : Fin (suc n) â â€ â (Fin n / Râ._âŒ_)
to fzero = inl _
to (fsuc x) = inr (inc x)

is : Iso (â€ â (Fin n / Râ._âŒ_)) (Fin (suc n) / R._âŒ_)
is .fst (inl tt) = inc 0
is .fst (inr x) = Coeq-rec (Î» x â inc (fsuc x)) (Î» (x , y , s) â quot s) x
is .snd .inv = Coeq-rec to Î» where
(fzero , fzero , s) â refl
(fzero , fsuc y , s) â absurd (Â¬r (y , s))
(fsuc x , fzero , s) â absurd (Â¬r (x , R.symá¶ s))
(fsuc x , fsuc y , s) â ap inr (quot s)
is .snd .rinv = elim! go' where
go' : â x â is .fst (to x) â¡ inc x
go' fzero = refl
go' (fsuc _) = refl
is .snd .linv (inl tt) = refl
is .snd .linv (inr x) = elim x where
elim : â x â is .snd .inv (is .fst (inr x)) â¡ inr x
elim = elim! Î» _ â refl


## Coequalisersð

Given two functions we can compute such that is equivalent to the coequaliser of and We start by expressing the coequaliser as the quotient of by the congruence generated by the relation so that we can apply the result above. Since this relation is clearly decidable by the omniscience of all that remains is to show that the closure of a decidable relation on a finite set is decidable.

instance
Closure-Fin-Dec
: â {n â} {R : Fin n â Fin n â Type â}
â âŠ â {x y} â Dec (R x y) âŠ
â â {x y} â Dec (Closure R x y)


This amounts to writing a (verified!) pathfinding algorithm: given we need to decide whether there is a path between and in the undirected graph whose edges are given by

We proceed by induction on the base case is trivial, so we are left with the inductive case The simplest1 way forward is to find a decidable congruence that is equivalent to the closure

We start by defining the restriction of along the successor map written as well as the symmetric closure of written

  Closure-Fin-Dec {suc n} {R = R} {x} {y} = R*-dec where
open Congruence
module R = Congruence (Closure-congruence R)

Râ : Fin n â Fin n â Type _
Râ x y = R (fsuc x) (fsuc y)
module Râ = Congruence (Closure-congruence Râ)

RââR : â {x y} â Closure Râ x y â Closure R (fsuc x) (fsuc y)
RââR = Closure-rec-congruence Râ
(Congruence-pullback fsuc (Closure-congruence R)) inc

RË¢ : Fin (suc n) â Fin (suc n) â Type _
RË¢ x y = R x y â R y x

RË¢âR : â {x y} â RË¢ x y â Closure R x y
RË¢âR = [ inc , R.symá¶ â inc ]


We build by cases. is trivial, since the closure is reflexive.

    D : Fin (suc n) â Fin (suc n) â Type _
D fzero fzero = Lift _ â€


For we use the omniscience of to search for an such that and Here we rely on the closure of being decidable by the induction hypothesis. The case is symmetric.

    D fzero (fsuc y) = Î£[ x â Fin n ] RË¢ 0 (fsuc x) Ã Closure Râ x y
D (fsuc x) fzero = Î£[ y â Fin n ] Closure Râ x y Ã RË¢ (fsuc y) 0


Finally, in order to decide whether and are related by we have two possibilities: either there is a path from to in which we can find using the induction hypothesis, or there are are paths from to and from to in which we can find using the previous two cases.

    D (fsuc x) (fsuc y) = Closure Râ x y â D (fsuc x) 0 Ã D 0 (fsuc y)


Proving that (the propositional truncation of) is a decidable congruence is tedious but not difficult.

    D-cong : Congruence (Fin (suc n)) _
instance D-Dec : â {x y} â Dec (D x y)

    D-refl : â x â D x x
D-refl fzero = _
D-refl (fsuc x) = inl Râ.reflá¶

D-trans : â x y z â D x y â D y z â D x z
D-trans fzero fzero z _ d = d
D-trans fzero (fsuc y) fzero _ _ = _
D-trans fzero (fsuc y) (fsuc z) (y' , ry , cy) (inl c) = y' , ry , cy Râ.âá¶ c
D-trans fzero (fsuc y) (fsuc z) _ (inr (_ , dz)) = dz
D-trans (fsuc x) fzero fzero d _ = d
D-trans (fsuc x) fzero (fsuc z) dx dy = inr (dx , dy)
D-trans (fsuc x) (fsuc y) fzero (inl c) (y' , cy , ry) = y' , c Râ.âá¶ cy , ry
D-trans (fsuc x) (fsuc y) fzero (inr (dx , _)) _ = dx
D-trans (fsuc x) (fsuc y) (fsuc z) (inl c) (inl d) = inl (c Râ.âá¶ d)
D-trans (fsuc x) (fsuc y) (fsuc z) (inl c) (inr ((y' , cy , ry) , dz)) =
inr ((y' , c Râ.âá¶ cy , ry) , dz)
D-trans (fsuc x) (fsuc y) (fsuc z) (inr (dx , (y' , ry , cy))) (inl c) =
inr (dx , y' , ry , cy Râ.âá¶ c)
D-trans (fsuc x) (fsuc y) (fsuc z) (inr (dx , dy)) (inr (dy' , dz)) =
inr (dx , dz)

D-sym : â x y â D x y â D y x
D-sym fzero fzero _ = _
D-sym fzero (fsuc y) (y' , r , c) = y' , Râ.symá¶ c , â-comm .fst r
D-sym (fsuc x) fzero (x' , c , r) = x' , â-comm .fst r , Râ.symá¶ c
D-sym (fsuc x) (fsuc y) (inl r) = inl (Râ.symá¶ r)
D-sym (fsuc x) (fsuc y) (inr (dx , dy)) =
inr (D-sym fzero (fsuc y) dy , D-sym (fsuc x) fzero dx)

D-cong ._âŒ_ x y = â¥ D x y â¥
D-cong .has-is-prop _ _ = hlevel 1
D-cong .reflá¶ {x} = inc (D-refl x)
D-cong ._âá¶_ {x} {y} {z} = â¥-â¥-mapâ (D-trans x y z)
D-cong .symá¶ {x} {y} = map (D-sym x y)

{-# INCOHERENT D-Dec #-}
D-Dec {fzero} {fzero} = auto
D-Dec {fzero} {fsuc y} = auto
D-Dec {fsuc x} {fzero} = auto
D-Dec {fsuc x} {fsuc y} = auto


To complete the proof, we show that is indeed equivalent to it suffices to show that lies between and

    RâD : â {x y} â R x y â D x y
RâD {fzero} {fzero} _ = _
RâD {fzero} {fsuc y} r = y , inl r , Râ.reflá¶
RâD {fsuc x} {fzero} r = x , Râ.reflá¶ , inl r
RâD {fsuc x} {fsuc y} r = inl (inc r)

DâR* : â {x y} â D x y â Closure R x y
DâR* {fzero} {fzero} _ = R.reflá¶
DâR* {fzero} {fsuc y} (y' , r , c) = RË¢âR r R.âá¶ RââR c
DâR* {fsuc x} {fzero} (x' , c , r) = RââR c R.âá¶ RË¢âR r
DâR* {fsuc x} {fsuc y} (inl r) = RââR r
DâR* {fsuc x} {fsuc y} (inr (dx , dy)) = DâR* dx R.âá¶ DâR* {fzero} dy

R*âD : â {x y} â Closure R x y â â¥ D x y â¥
R*âD = Closure-rec-congruence R D-cong (inc â RâD)

R*-dec : Dec (Closure R x y)
R*-dec = invmap (rec! DâR*) R*âD (holds? â¥ D x y â¥)


We can finally assemble the pieces together: given the coequaliser of and is equivalent to the quotient of by the decidable relation induced by and and hence by its congruence closure But we know that quotients of finite sets by decidable congruences are finite, and we just proved that the closure of a decidable relation on a finite set is decidable, so weâre done.

Finite-coequaliser
: â {n m} (f g : Fin m â Fin n)
â Î£ Nat Î» q â Fin q â Coeq f g
Finite-coequaliser {n} f g
= n/R .fst
, n/R .snd
âe Closure-quotient R eâ»Â¹
âe Coeqâquotient f g eâ»Â¹
where
R = spanâR f g

n/R : Î£ Nat Î» q â Fin q â Fin n / Closure R
n/R = Finite-quotient (Closure-congruence R)


1. In terms of ease of implementation; the complexity of the resulting algorithm is catastrophic.â©ïž