# Finite Decidable Setoids

## An Agda exploration of decidable equivalence relations over finite sets by means of standard library's finite-subset API.

In set-based mathematics an equivalence relation can be fully characterised in terms of subset-membership into equivalence classes and partitions. This is trivial to prove on paper, but I found it less obvious to be formalised in Agda at least for my novice skills in the discipline of dependent type theory. In fact, to the trained mathematician, "proofs" after the principle of Propositions-as-Types might seem affected by a 21st-century extreme bourbakism. Nonetheless, regarded as a library, I hope the following can be reused in the formalisation of more involved combinatory results dealing with invariants of algebraic structures: the paradigmatic example here is the orbital equation from Group Theory and essential results deriving from it like Sylow Theorems. In order to formalise these facts about quotients of finite sets, we apply to the finite case more general results from Cohen and Altenkirch. The extra fun comes when trying to play-by-the-rules, that is prove these ideas reusing as much as possible existing functions from Agda standard library.

Given an equivalence relation inline_formula not implemented over a finite set inline_formula not implemented, assume we can exhibit a set of representatives inline_formula not implemented, one for each equivalence class in inline_formula not implemented, then inline_formula not implemented is the disjoint union of all classes of elements in inline_formula not implemented and inline_formula not implemented is called a transversal of inline_formula not implemented:

formula not implemented

in other terms inline_formula not implemented induces a partition on inline_formula not implemented and in particular its cardinality is additive on classes:

formula not implemented

We will formalise the above facts in section Properties of Finite Decidable Setoids providing terms as evidence to the following propositions i.e. types:

`Covering : ∀ (x : F) → Any (x ∈_) ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧`
`Disjointness : AllPairs Disj ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧`
`Cardinality : n ≡ List.sum ⟦ ∣ [ x ]ω ∣ ∣ x 𝕚𝕟 Transversal ⟧`
Agda

In the section Partitions we'll show that for all natural numbers `n` the type of finite decidable Setoids on `n` elements is "equivalent" to the type of partitions of the finite type on `n` elements.

Sections Subset Lemmas and List-Relations Properties contain proofs and definitions to show the above results while some boring subset helpers are relegated to the Appendix. All sections are matched with dedicated inter-depending Agda runtime.

## Definitions

Membership and subset relations in type theory is sorted out via type-valued predicates. In the finite case there's a more amenable description which employs vectors of boolean values, the properties of which are better suited for computation and decidability. This is apparent in the following definition of equivalence class

`module FDS where`
1.4s
FDS (Agda)
FDS.Fin.Subset.Lemmas
`record FinDecEq {a} (n : ℕ) : Set (lsuc a) where`
`  field`
`    _ω_ : Rel (Fin n) a`
`    isDecEq : IsDecEquivalence _ω_`
`  std : DecSetoid _ _`
`  std = record { Carrier = (Fin n) ;`
`                _≈_ = _ω_ ;`
`                isDecEquivalence = isDecEq }`
`  open DecSetoid std`
`    renaming (_≟_ to _ω?_ ;`
`              refl to ω-refl ;`
`              sym to ω-sym ;`
`              trans to ω-transitive ;`
`              Carrier to F)`
`    public`
`  [_]ω : F → Subset n`
`  [ o ]ω = Vec.tabulate (does ∘ (_ω? o))`
1.3s
FinDecEqFDS (Agda)
FDS.Fin.Subset.Lemmas

## Properties of Finite Decidable Setoids

The following module reads as take a natural number inline_formula not implemented and a finite decidable Setoid `FDS `over a set of inline_formula not implemented elements

`open import Level`
`open import Data.Nat.Base`
`open import FDS using (FinDecEq)`
`module FDS.Properties {a : Level} {n : ℕ} {FDS : FinDecEq {a} n} where`
`open import FDS.Fin.Subset.Lemmas`
`open import FDS.List.AllPairs.Lemmas`
25.4s
FDS.Properties (Agda)
FDS

by opening its record type, within this module `FinDecEq` definitions are directly available, in particular throughout the this section `F` denotes (the type of) the finite set with `n` elements. We distinguish inline_formula not implemented subset-membership from inline_formula not implemented list-membership. Please forgive the cheesy comprehension syntax for lists

`open FinDecEq FDS`
`import Data.List.Membership.Propositional`
`module MP = Data.List.Membership.Propositional {A = F}`
`open MP renaming (_∈_ to _∈ℓ_)`
`open import Data.List.Membership.Propositional.Properties`
`lmap = List.map`
`syntax lmap (λ x → B) L = ⟦ B ∣ x 𝕚𝕟 L ⟧`
`Fˡ = List.allFin n`
0.5s
syntaxFDS.Properties (Agda)
FDS

First basic fact: being in relation means to belong to the same class

`ω⇒∈ : ∀ {x y} → x ω y → x ∈ [ y ]ω`
`ω⇒∈ {x} {y} xωy = let lkp = begin `
`                              Vec.lookup [ y ]ω x ≡⟨ lookup∘tabulate _ x ⟩`
`                              does (x ω? y) ≡⟨ dec-true (x ω? y) xωy ⟩`
`                              true ∎`
`                  in lookup⇒[]= x [ y ]ω lkp`
1.5s
FDS.Properties (Agda)
FDS

In particular every class is non empty as a consequence of reflexivity.

`o∈[o]ω : ∀ { o : F } → o ∈ [ o ]ω`
`o∈[o]ω = ω⇒∈ ω-refl`
1.5s
FDS.Properties (Agda)
FDS

and the converse is also true

`∈⇒ω : ∀ {x y} → x ∈ [ y ]ω → x ω y`
`∈⇒ω {x} {y} x∈[y] = `
`  let w = begin`
`            isYes (x ω? y) ≡⟨ isYes≗does _ ⟩ `
`            does (x ω? y)  ≡˘⟨ lookup∘tabulate _ x ⟩`
`            Vec.lookup [ y ]ω x ≡⟨ []=⇒lookup x∈[y] ⟩`
`            true ∎`
`      ≡→T : ∀ {b : Bool} → b ≡ true → T b`
`      ≡→T = λ { refl → tt }`
`      r : True (x ω? y)`
`      r = ≡→T w`
`  in toWitness r`
1.5s
FDS.Properties (Agda)
FDS

now by symmetry we have the desired equivalent formulation

`ω⇒⊆ : ∀ {x y} → x ω y → [ x ]ω ⊆ [ y ]ω`
`ω⇒⊆ {x} {y} xωy s∈[x] = ω⇒∈ (ω-transitive (∈⇒ω s∈[x]) xωy )`
`ω⇒≡ : ∀ {x y} → x ω y → [ x ]ω ≡ [ y ]ω`
`ω⇒≡ {x} {y} xωy = ⊆-antisym (ω⇒⊆ xωy) (ω⇒⊆ (ω-sym xωy))`
1.6s
FDS.Properties (Agda)
FDS

### Canonical Representatives

Now the questions we want to answer next is how many distinct classes does an equivalence posses and do such classes partition the carrier set? Or again can we find a subset on which inline_formula not implemented is a bijection? Can we find a prescribed set of computationally well-behaved (i.e. decidable) representatives for the equivalence classes?

We first introduce a canonical choice inline_formula not implemented with the following properties:

• inline_formula not implemented for all inline_formula not implemented

• inline_formula not implemented if and only if inline_formula not implemented

• inline_formula not implemented is idempotent

In the finite setting (as in any well ordering), given any family of nonempty sets it is possible to find a choice-function: the minimum element. In the following code we're using `index` and `index-`inline_formula not implemented functions defined in the section Subset Lemmas

`cc : F → F`
`cc f = index {n} [ f ]ω ( f , o∈[o]ω )`
`ccx∈[x] : ∀ (x : F) → (cc x) ∈ [ x ]ω`
`ccx∈[x] x = proj₁ (proj₂ (index* [ x ]ω ( x , o∈[o]ω )))`
`xωccx : ∀ (x : F) → x ω (cc x)`
`xωccx x = ω-sym (∈⇒ω (ccx∈[x] x))`
`c⇒ω : ∀ {x y} → cc x ≡ cc y → x ω y`
`c⇒ω {x} {y} ccx≡ccy = let P = λ q → q ∈ [ y ]ω`
`                          w : (cc x) ∈ [ y ]ω`
`                          w = subst P (sym ccx≡ccy) (ccx∈[x] y)`
`                    in ω-transitive (xωccx x) (∈⇒ω w)`
`ω⇒c : ∀ {x y} → x ω y → cc x ≡ cc y`
`ω⇒c {x} {y} xωy = index-unique _ _ _ _ (ω⇒≡ xωy)`
`cc-idempt : (x : F) → cc (cc x) ≡ cc x`
`cc-idempt x = ω⇒c {cc x} {x} (ω-sym (xωccx x))`
3.8s
FDS.Properties (Agda)
FDS

A canonical representative of an inline_formula not implemented-class is the minimum element with respect to the natural order on inline_formula not implemented. This is a decidable property because the finite type has a decidable equality. As transversal of inline_formula not implementedwe can take the set of all canonical representatives constructed in this way (recall that inline_formula not implemented is the set inline_formula not implementedrepresented as a list)

`cr : (i : F) → Set`
`cr i = i ≡ (cc i)`
`cr? : Decidable cr`
`cr? = λ i → i ≟ (cc i)`
`Transversal : List F`
`Transversal = (List.filter cr? Fˡ)`
1.8s
FDS.Properties (Agda)
FDS

### Covering

for all inline_formula not implemented in inline_formula not implementedthere exists an equivalence class of a canonical representative which inline_formula not implemented belongs to:

`Covering : ∀ (x : F) → Any (x ∈_) ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧`
`Covering x = let`
`               cover : ∀ (x : F) → (∃ λ k → cr k × x ω k)`
`               cover t = (cc t) , sym (cc-idempt t) , xωccx t`
`               (k , crk , xωk) = cover x`
`               k∈ℓFˡ : k ∈ℓ Fˡ`
`               k∈ℓFˡ = ∈-allFin {n} k`
`               k∈ℓTr : k ∈ℓ Transversal`
`               k∈ℓTr = ∈-filter⁺ cr? k∈ℓFˡ crk`
`               a : Any (x ω_) Transversal`
`               a = lose k∈ℓTr xωk`
`               b : Any ((x ∈_) ∘ [_]ω) Transversal`
`               b = Any.map ω⇒∈ a`
`            -- AnyProps.map⁺ : Any (P ∘ f) xs → Any P (List.map f xs)`
`            in AnyProps.map⁺ b`
1.9s
FDS.Properties (Agda)
FDS

### Disjointness

Any two distinct canonical classes are disjoint. The term `filter⁺₃` used below is proven in at the end of section List-Relations Properties while for definitions of `Disj` and `disj⇒Disj` see Subset Lemmas

`Disjointness : AllPairs Disj ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧`
`Disjointness = `
`  let ap₁ : AllPairs _≢_ Fˡ`
`      ap₁ = AllPairsProps.tabulate⁺ id`
`      cr-injective : ∀ {x y} → (cr x) → (cr y) → x ≢ y → ¬ x ω y`
`      cr-injective {x} {y} crx cry x≢y xωy = x≢y (begin x ≡⟨ crx ⟩`
`                                                     cc x ≡⟨ ω⇒c xωy ⟩`
`                                                     cc y ≡˘⟨ cry ⟩`
`                                                     y ∎)`
`      ω-disj : ∀ {x y} → ¬ (x ω y) → Empty ([ x ]ω ∩ [ y ]ω)`
`      ω-disj {x} {y} ¬xωy f∈∩ = let f , [x]∩[y] = f∈∩`
`                                    l , r = x∈p∩q⁻ _ _ [x]∩[y]`
`                                    xωf = ω-sym (∈⇒ω l)`
`                                    fωy = ∈⇒ω r`
`                                    in ¬xωy (ω-transitive xωf fωy)`
`      ω-Disj : ∀ {x y} → ¬ x ω y → Disj [ x ]ω [ y ]ω`
`      ω-Disj ¬xωy = disj⇒Disj (ω-disj ¬xωy)`
`      ap₂ : AllPairs (λ x y → ¬ x ω y) Transversal`
`      ap₂ = filter⁺₃ cr? cr-injective ap₁`
`      ap₃ = AllPairs.map ω-Disj ap₂ `
`      in AllPairsProps.map⁺ ap₃`
2.5s
FDS.Properties (Agda)
FDS

### Conclusions

Now we can transpose the above results in the language of subsets finding first that the union of all canonical classes gives back the whole finite set `F`

`Cover : ⊤ ≡ ⋃ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ `
`Cover = cover-⊤ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ Covering`
2.0s
FDS.Properties (Agda)
FDS

and furthermore since canonical classes are disjoint

`Cardinality : n ≡ List.sum ⟦ ∣ [ x ]ω ∣ ∣ x 𝕚𝕟 Transversal ⟧`
`Cardinality = `
`  let c = ∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ Disjointness`
`      d = map-compose {g = ∣_∣} {f = [_]ω} Transversal`
`      sum = List.sum`
`      in begin `
`          n ≡˘⟨ ∣⊤∣≡n n ⟩`
`          ∣ ⊤ {n} ∣ ≡⟨ cong ∣_∣ Cover ⟩`
`          ∣ ⋃ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ ∣ ≡⟨ c ⟩ `
`          sum (List.map ∣_∣ ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧) ≡˘⟨ cong sum d ⟩`
`          sum ⟦ ∣ [ x ]ω ∣ ∣ x 𝕚𝕟 Transversal ⟧ ∎`
2.5s
FDS.Properties (Agda)
FDS

functions `cover-⊤` and `∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣` used above are defined in Subset Lemmas.

## Partitions

`module FDS.Characterisation where`
`open import FDS`
`open import FDS.Fin.Subset.Lemmas`
`open import FDS.List.AllPairs.Lemmas`
`import FDS.Properties`
22.0s
FDS.Characterisation (Agda)
FDS.Properties
`record Partition (n : ℕ) : Set (sucℓ 0ℓ) where`
`  field`
`    parts : List (Subset n)`
`    disjoint : AllPairs disj parts`
`    cover : ∀ (x : Fin n) → Any (x ∈_) parts`
`  `
`  _ωP_ : Rel (Fin n) 0ℓ`
`  x ωP y = Any (λ s → x ∈ s × y ∈ s) parts`
2.4s
FDS.Characterisation (Agda)
FDS.Properties
`FDS⇒Partition : ∀ {ℓ n} → FinDecEq {ℓ} n → Partition n`
`FDS⇒Partition FDS = `
`  record { parts = ⟦ [ x ]ω ∣ x 𝕚𝕟 Transversal ⟧ ;`
`           disjoint = AllPairs.map Disj⇒disj Disjointness ;`
`           cover = Covering } where`
`  open FinDecEq FDS`
`  open FDS.Properties {FDS = FDS}`
1.4s
FDS.Characterisation (Agda)
FDS.Properties

we hide the following proof of decidability of predicate conjunction `dec-×`

`Partition⇒FDS : ∀ {n} → Partition n → FinDecEq n`
`Partition⇒FDS {n} P = `
`  record { _ω_ = _ωP_ ;`
`           isDecEq = isDecEq }`
`  where`
`    open Partition P`
`    ωRefl : Reflexive _ωP_`
`    ωRefl {x} = Any.map {P = λ s → x ∈ s} (λ z → z , z) (cover x)`
`    `
`    ωSym : Symmetric _ωP_`
`    ωSym xωPy = Any.map (λ (a , b) → b , a) xωPy`
`    `
`    ωTrans : Transitive _ωP_`
`    ωTrans {x} {y} {z} xωPy yωPz = `
`      let`
`        s , s∈ℓparts , x∈s , y∈s = Membership.find xωPy`
`        t , t∈ℓparts , y∈t , z∈t = Membership.find yωPz`
`        y∈s∩t : y ∈ s ∩ t`
`        y∈s∩t = x∈p∩q⁺ ( y∈s , y∈t )`
`        i = Any.index s∈ℓparts`
`        j = Any.index t∈ℓparts`
`        ¬d : ¬ (disj s t)`
`        ¬d e = e ( y , y∈s∩t ) `
`        disj-sym : Symmetric disj`
`        disj-sym {x} {y} disjxy = subst Empty (∩-comm x y) disjxy`
`        helper : i ≡ j → x ωP z`
`        helper i≡j = `
`          let s≡t : s ≡ t`
`              s≡t = begin `
`                s ≡⟨ helper₁ s∈ℓparts ⟩ `
`                Any.lookup s∈ℓparts ≡⟨ cong (List.lookup parts) i≡j ⟩`
`                Any.lookup t∈ℓparts ≡˘⟨ helper₁ t∈ℓparts ⟩ `
`                t ∎`
`              x∈t : x ∈ t`
`              x∈t = subst₂ _∈_ refl s≡t x∈s`
`          in Membership.lose t∈ℓparts ( x∈t , z∈t )`
`          `
`        in case i ≟ j of λ {`
`          (yes i≡j) → helper i≡j ;`
`          (no i≢j) → ⊥-elim (¬d (elim-sym disj-sym disjoint s∈ℓparts t∈ℓparts i≢j))`
`        } where`
`            helper₁ : ∀ {A : Set} {x : A} {l : List A} → `
`                      (ξ : x ∈ℓ l) → x ≡ Any.lookup ξ`
`            helper₁ (here px) = px`
`            helper₁ (there χ) = helper₁ χ`
`    `
`    isEq : IsEquivalence _ωP_`
`    isEq = record {`
`            refl = ωRefl ;`
`            sym = ωSym ; `
`            trans = ωTrans }`
`            `
`    -- decidability`
`    ≟P : Decidable ( _ωP_ )`
`    ≟P = λ x y → Any.any (λ t → dec-× (x ∈? t) (y ∈? t)) parts`
`    isDecEq : IsDecEquivalence _ωP_`
`    isDecEq = record { isEquivalence = isEq ; _≟_ = ≟P }                         `
2.2s
FDS.Characterisation (Agda)
FDS.Properties

## Subset Lemmas

`module FDS.Fin.Subset.Lemmas where`
`open import FDS.Subset.Helpers`
1.1s
FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

We'll work with the following equivalent notions of disjointness

`Disj : ∀ {n} → Subset n → Subset n → Set`
`Disj S T = S ∩ T ≡ ⊥`
`disj : ∀ {n} → Subset n → Subset n → Set`
`disj S T = Empty (S ∩ T)`
`Disj-sym : ∀ {n} → Symmetric (Disj {n = n})`
`Disj-sym {n} {S} {T} S∩T≡⊥ = begin T ∩ S ≡⟨ ∩-comm T S ⟩ S ∩ T ≡⟨ S∩T≡⊥ ⟩ ⊥ ∎`
`Empty⊥ : ∀ {n} → Empty { n } ⊥`
`Empty⊥ (i , n) = let`
`                    x : Vec.lookup ⊥ i ≡ outside`
`                    x = lookup-replicate i outside`
`                    y : Vec.lookup ⊥ i ≡ inside`
`                    y = []=⇒lookup n`
`                    z = trans (sym x) y`
`                  in contradiction z (not-¬ refl)`
`                  `
`disj⇒Disj : ∀ {n} → ∀ {s t : Subset n} → disj s t → Disj s t`
`disj⇒Disj d = Empty-unique d`
`Disj⇒disj : ∀ {n} → ∀ {s t : Subset n} → Disj s t → disj s t`
`Disj⇒disj D = subst Empty (sym D) (Empty⊥)`
1.6s
Disjointness definitionsFDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

We borrow the following proof from standard library, where it's related to monoids in general and is proved for tables while we need it for unions of lists

`⋃-remove : ∀ {n} {L : List (Subset n)} → ∀ s → (s∈L : s ∈ℓ L) →`
`           ⋃ L ≡ s ∪ ⋃ (L Any.─ s∈L)`
`⋃-remove {n} {List.[]} _ = λ ()`
`⋃-remove {n} {x ∷ xs} s (here px) =`
`  begin`
`    ⋃ (x ∷ xs) ≡⟨ refl ⟩`
`    x ∪ (⋃ xs) ≡˘⟨ cong (_∪ _) px ⟩`
`    s ∪ (⋃ xs) ≡⟨ cong (_ ∪_) refl ⟩`
`    s ∪ ⋃ ((x ∷ xs) Any.─ (here {P = P} px)) ∎`
`    where`
`    P : Pred (Subset n) Level.zero`
`    P = s ≡_`
`⋃-remove {n} {x ∷ xs} s (there s∈L) =`
`  begin`
`    x ∪ (⋃ xs) ≡⟨ cong (x ∪_) (⋃-remove {L = xs} s s∈L) ⟩`
`    x ∪ (s ∪ ⋃ (xs Any.─ s∈L)) ≡˘⟨ ∪-assoc _ _ _ ⟩ -- TODO: -- use solver`
`    (x ∪ s) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ cong (_∪ _) (∪-comm x s) ⟩`
`    (s ∪ x) ∪ ⋃ (xs Any.─ s∈L) ≡⟨ ∪-assoc _ _ _ ⟩`
`    s ∪ (x ∪ ⋃ (xs Any.─ s∈L)) ≡⟨ refl ⟩`
`    s ∪ ⋃ ((x ∷ xs) Any.─ (there s∈L)) ∎`
2.0s
FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

We'll also make use of the following covering lemma: if a family of sets covers the whole carrier then its union is the whole set

`cover-⊤ : ∀ {n} → (L : List (Subset n)) →`
`          (∀ (x : Fin n) → Any (x ∈_) L ) →`
`          ⊤ {n} ≡ ⋃ L`
`cover-⊤ {n} L ∃lx∈l = ⊆-antisym ⊤⊆⋃L (⊆-max (⋃ L)) where`
`  ⊤⊆⋃L : ⊤ ⊆ (⋃ L)`
`  ⊤⊆⋃L {x} _ = let`
`                  (l , l∈ℓL , x∈l) = find {P = x ∈_} (∃lx∈l x)`
`                  l⊆l∪* = p⊆p∪q {p = l} (⋃ (L Any.─ l∈ℓL))`
`                  x∈l∪* = l⊆l∪* {x} x∈l`
`                in subst₂ _∈_ refl (sym (⋃-remove l l∈ℓL)) x∈l∪*`
2.2s
cover-⊤FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

and the following additive property of cardinality on disjoint sets

`∣p⊍q∣≡∣p∣+∣q∣ : ∀ {n} → ∀ (p q : Subset n) → `
`                Disj p q → ∣ p ∪ q ∣ ≡ ∣ p ∣ + ∣ q ∣`
`      `
`∣p⊍q∣≡∣p∣+∣q∣ {zero} [] [] d = refl`
`∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (outside ∷ q) d = `
`  begin`
`    ∣ p ∪ q ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {outside} d) ⟩`
`    ∣ (outside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎`
`∣p⊍q∣≡∣p∣+∣q∣ {suc n} (inside ∷ p) (outside ∷ q) d = `
`  begin`
`    ∣ (inside ∷ p) ∪ (outside ∷ q) ∣ ≡⟨ refl ⟩`
`    suc ∣ p ∪ q ∣ `
`      ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {inside} {outside} d)) ⟩`
`    suc (∣ p ∣ + ∣ q ∣) ≡⟨⟩`
`    (suc ∣ p ∣) + ∣ q ∣ ≡⟨⟩`
`    ∣ (inside ∷ p) ∣ + ∣ (outside ∷ q) ∣ ∎`
`∣p⊍q∣≡∣p∣+∣q∣ {suc n} (outside ∷ p) (inside ∷ q) d = `
`  begin`
`    ∣ (outside ∷ p) ∪ (inside ∷ q) ∣ ≡⟨ refl ⟩`
`    suc ∣ p ∪ q ∣ `
`      ≡⟨ cong suc (∣p⊍q∣≡∣p∣+∣q∣ {_} p q (drop-disj {n} {outside} {inside} d)) ⟩`
`    suc (∣ p ∣ + ∣ q ∣) ≡⟨ cong suc (+-comm ∣ p ∣ ∣ q ∣) ⟩`
`    suc (∣ q ∣ + ∣ p ∣) ≡⟨ refl ⟩`
`    (suc ∣ q ∣) + ∣ p ∣ ≡⟨⟩`
`    ∣ (inside ∷ q) ∣ + ∣ (outside ∷ p) ∣ `
`      ≡⟨ +-comm ∣ (inside ∷ q) ∣ ∣ (outside ∷ p) ∣  ⟩`
`    ∣ (outside ∷ p) ∣ + ∣ (inside ∷ q) ∣ ∎            `
3.9s
∣p⊍q∣≡∣p∣+∣q∣FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

which also hold for lists of subsets

`∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ : ∀ {n} → (C : List (Subset n)) → AllPairs Disj C →`
`                ∣ ⋃ C ∣ ≡ List.sum (List.map ∣_∣ C)`
`∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} List.[] Δℓ =`
`  begin`
`    ∣ ⋃ {n} List.[] ∣ ≡⟨⟩`
`    ∣ ⊥ {n} ∣ ≡⟨ ∣⊥∣≡0 n ⟩`
`    0 ≡⟨⟩`
`    List.foldr _+_ 0 List.[] ∎`
`∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} (s ∷ C) (h ∷ t) = `
`  begin`
`    ∣ ⋃ (s ∷ C) ∣ ≡⟨⟩`
`    ∣ s ∪ (⋃ C) ∣ ≡⟨ ∣p⊍q∣≡∣p∣+∣q∣ s (⋃ C) (Disj-sym DisjUCs) ⟩`
`    ∣ s ∣ + ∣ ⋃ C ∣ ≡⟨ cong (∣ s ∣ +_) (∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} C t ) ⟩`
`    ∣ s ∣ + (List.sum (List.map ∣_∣ C)) ≡⟨⟩`
`    List.sum (List.map ∣_∣ (s ∷ C)) ∎`
`    where`
`    a : All (λ x → x ⊆ ∁ s) C`
`    a = All.map (disj⇒⊆∁ ∘ Disj-sym) h`
`    c : ⋃ C ⊆ ∁ s`
`    c = pᵢ⊆q⇒⋃pᵢ⊆q (∁ s) C a`
`    DisjUCs : Disj (⋃ C) s`
`    DisjUCs = ⊆∁⇒disj c`
2.2s
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

we conclude with a proof of existence for a finite choice function

`fsuc∈ : ∀ {n} → {p : Subset n} → {x : Fin n} → {s : Side} → `
`        (x ∈ p) → (fsuc x) ∈ (s ∷ p)`
`fsuc∈ here = there here`
`fsuc∈ (there x∈p) = there (fsuc∈ x∈p)`
2.0s
FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

Since finite sets carry a natural order we can always find the smallest element in a non empty subset. Note how Agda type checker eliminates obvious non matching patterns given we're dealing with non-empty sets only.

`index* : ∀ {n} → (s : Subset n) → Nonempty s →`
`         ∃ (λ x → ( x ∈ s × (∀ {y} → (y ∈ s) → x ≤ y )))`
`index* {suc n} (inside ∷ rest) _ = (fzero , here , λ _ → z≤n )`
`index* {suc n} (outside ∷ rest) ne with (∃-toSum ne)`
`... | inj₂ b = let w = drop-there (proj₂ b)`
`                   z = (proj₁ b , w)`
`                   ( a , bb , c ) = (index* rest z)`
`               in (fsuc a , fsuc∈ bb , λ { (there y∈s) → s≤s (c y∈s) } )`
`index : ∀ {n} → (s : Subset n) → Nonempty s → Fin n`
`index s ne = proj₁ (index* s ne)`
2.1s
FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas
`index-unique : ∀ {n} → ∀ (s t : Subset n) → (ns : Nonempty s) →`
`             (nt : Nonempty t) →`
`             s ≡ t → (index s ns) ≡ (index t nt)`
`index-unique s t ns nt s≡t = let fs , fs∈s , fs≤ = index* s ns`
`                                 ft , ft∈t , ft≤ = index* t nt`
`                                 ft∈s : ft ∈ s`
`                                 ft∈s = subst _ (sym s≡t) ft∈t`
`                                 fs∈t : fs ∈ t`
`                                 fs∈t = subst _ s≡t fs∈s`
`                              in ≤-antisym (fs≤ ft∈s) (ft≤ fs∈t)`
2.3s
FDS.Fin.Subset.Lemmas (Agda)
FDS.List.AllPairs.Lemmas

## List-Relations Properties

missing from the standard library

`module FDS.List.AllPairs.Lemmas where`
0.5s
FDS.List.AllPairs.Lemmas (Agda)
FDS.Subset.Helpers

let's hide here a pair of tedious helpers `drop∷` and `drop-suc` used in the next lemma, that can be stated as evidence of membership implies a list is non empty.

this is an all-pairs elimination, which surprisingly is not in the standard library unless I've overseen something crucial

`module _ {a ℓ} {A : Set a} {R : Rel A ℓ } where`
`  elim : ∀ {xs x y} → AllPairs R xs → `
`           (x∈ : x ∈ xs) → (y∈ : y ∈ xs) →`
`           (Any.index x∈) <f (Any.index y∈) → R x y`
`  elim {xs} {x} {y} ap x∈ y∈ i<j =`
`    let  i = (Any.index x∈) `
`         j = (Any.index y∈)`
`         xs' = drop (toℕ i) xs`
`         ¬∅ : xs' ≡ x ∷ _`
`         ¬∅ = drop∷ xs x∈`
`         d : AllPairs R xs'`
`         d = drop⁺ (toℕ i) ap`
`         d' = subst (AllPairs R) ¬∅ d`
`         h = AllPairs.head d'`
`    in All.lookup h (drop-suc xs x∈ y∈ i<j)`
1.3s
FDS.List.AllPairs.Lemmas (Agda)
FDS.Subset.Helpers

in case of symmetric relations the order of indices is actually irrelevant

`module _ {a ℓ} {A : Set a} {R : Rel A ℓ } (S : Symmetric R) where`
`  elim-sym : ∀ {xs x y} → AllPairs R xs → `
`          (x∈ : x ∈ xs) → (y∈ : y ∈ xs) → `
`          (Any.index x∈) ≢ (Any.index y∈) → R x y`
`  elim-sym ap x∈ y∈ i≢j with <-cmp (Any.index x∈) (Any.index y∈)`
`  ...| tri< i<j _ _ = elim ap x∈ y∈ i<j`
`  ...| tri> _ _ j<i = S (elim ap y∈ x∈ j<i)`
`  ...| tri≈ _ i≈j _ = ⊥-elim (i≢j i≈j)`
1.4s
FDS.List.AllPairs.Lemmas (Agda)
FDS.Subset.Helpers

to conclude this section we'll show an alternative form of filter introduction rule for the AllPairs predicate, namely

`module _ {a ℓ ℓ₁ ℓ₂} {A : Set a}`
`         {R : Rel A ℓ₁} {S : Rel A ℓ₂}`
`         {P : Pred A ℓ} (P? : Decidable P) where`
`  filter⁺₃ : ∀ {xs} → (∀ {x y} → P x → P y → R x y → S x y) →`
`            AllPairs R xs → AllPairs S (filter P? xs)`
`  filter⁺₃ {[]} _ _ = []`
`  filter⁺₃ {x ∷ xs} Δ (h ∷ t) with (P? x)`
`  ... | no  ¬p = filter⁺₃ {xs} Δ t`
`  ... | yes p = let`
`                  hf : All (R x) (filter P? xs)`
`                  hf = filter⁺ P? h`
`                  ap : All P (filter P? xs)`
`                  ap = all-filter P? xs`
`                  w : All (P ∩ R x) (filter P? xs)`
`                  w = All.zip ( ap , hf )`
`                  y : P ∩ R x ⊆ S x`
`                  y = λ z → Δ p (proj₁ z) (proj₂ z)`
`                  z : All (S x) (filter P? xs)`
`                  z =  All.map y w`
`                in z ∷ filter⁺₃ {xs} Δ t`
1.4s
filter⁺₃FDS.List.AllPairs.Lemmas (Agda)
FDS.Subset.Helpers

## Appendix: Subset Helpers

`module FDS.Subset.Helpers where`
0.5s
FDS.Subset.Helpers (Agda)
`∩-⊆-stable : ∀ {n} → ∀ {p q} → (r : Subset n) → p ⊆ q → (p ∩ r) ⊆ (q ∩ r)`
`∩-⊆-stable {_} {p} {q} r p⊆q x∈p∩r = `
`  let`
`    x∈p = proj₁ (x∈p∩q⁻ p r x∈p∩r)`
`    x∈r = proj₂ (x∈p∩q⁻ p r x∈p∩r)`
`  in x∈p∩q⁺ ( p⊆q x∈p , x∈r )`
`idʳ⇒⊆ : ∀ {n} → (S T : Subset n) → (S ∪ T) ≡ T → S ⊆ T`
`idʳ⇒⊆ {n} S T sut≡t = subst₂ _⊆_ refl sut≡t (p⊆p∪q T)`
`p∩∁p≡⊥ : ∀ {n} → (p : Subset n) → p ∩ ∁ p ≡ ⊥`
`p∩∁p≡⊥ [] = refl`
`p∩∁p≡⊥ (outside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)`
`p∩∁p≡⊥ (inside ∷ p) = cong (outside ∷_) (p∩∁p≡⊥ p)`
`p⊆q⇒p∩∁q≡⊥ : ∀ {n} → {S T : Subset n} → S ⊆ T → S ∩ (∁ T) ≡ ⊥`
`p⊆q⇒p∩∁q≡⊥ {_} {S} {T} s⊆t = let`
`                               a = p∩∁p≡⊥ _`
`                               b : S ∩ (∁ T) ⊆ T ∩ (∁ T)`
`                               b = ∩-⊆-stable (∁ T) s⊆t`
`                               c = subst₂ _⊆_ refl a b`
`                               in ⊆-antisym c (⊆-min _)`
`disj⇒⊆∁ : ∀ {n} → {S T : Subset n} → S ∩ T ≡ ⊥ → S ⊆ (∁ T)`
`disj⇒⊆∁ {n} {S} {T} dst = `
`  let ct≡suct = begin`
`                ∁ T ≡˘⟨ ∪-identityˡ _ ⟩`
`                ⊥ ∪ (∁ T) ≡˘⟨ cong (_∪ (∁ T)) dst ⟩`
`                (S ∩ T) ∪ (∁ T) ≡⟨ ∪-distribʳ-∩ _ _ _ ⟩`
`                (S ∪ (∁ T)) ∩ (T ∪ (∁ T)) ≡⟨ cong ((S ∪ (∁ T)) ∩_) (p∪∁p≡⊤ T) ⟩`
`                (S ∪ (∁ T)) ∩ ⊤ ≡⟨ ∩-identityʳ _ ⟩`
`                S ∪ (∁ T) ∎`
`  in idʳ⇒⊆ S (∁ T) (sym ct≡suct)`
`⊆∁⇒disj : ∀ {n} → {S T : Subset n} → S ⊆ (∁ T) → S ∩ T ≡ ⊥`
`⊆∁⇒disj {n} {S} {T} s⊆∁t = `
`  begin`
`  S ∩ T ≡˘⟨ cong (S ∩_) (¬-involutive T ) ⟩`
`  S ∩ (∁ (∁ T)) ≡⟨ p⊆q⇒p∩∁q≡⊥ s⊆∁t ⟩`
`  ⊥ ∎`
`  where open Algebra.Properties.BooleanAlgebra (∪-∩-booleanAlgebra n)           `
1.6s
FDS.Subset.Helpers (Agda)
`p⊆r×q⊆r⇒p∪q⊆r : ∀ {n} → { p q r : Subset n} → (p ⊆ r) × (q ⊆ r) → (p ∪ q) ⊆ r`
`p⊆r×q⊆r⇒p∪q⊆r {n} {p} {q} {r} (p⊆r , q⊆r) x∈p∪q = `
`  let y = x∈p∪q⁻ {n} p q x∈p∪q`
`  in (p⊆r ⊞ q⊆r) y`
`pᵢ⊆q⇒⋃pᵢ⊆q : ∀ {n} → ∀ S → ∀ (L : List (Subset n)) →`
`             All (_⊆ S) L → (⋃ L) ⊆ S`
`pᵢ⊆q⇒⋃pᵢ⊆q S <> _ = ⊆-min S`
`pᵢ⊆q⇒⋃pᵢ⊆q S (x ∷ xs) (h ∷ t) = `
`  subst₂ _⊆_ refl refl (p⊆r×q⊆r⇒p∪q⊆r ( h , pᵢ⊆q⇒⋃pᵢ⊆q S xs t ))`
` `
`drop-disj : ∀ {n} → {x y : Side} → {p q : Subset n} → `
`            (x ∷ p) ∩ (y ∷ q) ≡ ⊥ → p ∩ q ≡ ⊥`
`drop-disj {zero} {_} {_} {[]} {[]} _ = refl`
`drop-disj d = cong V.tail d`
1.8s
FDS.Subset.Helpers (Agda)