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 

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.


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
FDS (Agda)
record FinDecEq {a} (n : ) : Set (lsuc a) where
    _ω_ : 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)
  [_]ω : F  Subset n
  [ o  = Vec.tabulate (does  (? o))
FinDecEqFDS (Agda)

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
FDS.Properties (Agda)

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 =
syntax lmap (λ x  B) L =  B  x 𝕚𝕟 L 
 = List.allFin n
syntaxFDS.Properties (Agda)

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 
                  in lookup⇒[]= x [ y  lkp
FDS.Properties (Agda)

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

o∈[o]ω :  { o : F }  o  [ o 
o∈[o]ω = ω⇒∈ ω-refl
FDS.Properties (Agda)

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] 
      ≡→T :  {b : Bool}  b  true  T b
      ≡→T = λ { refl  tt }
      r : True (x ω? y)
      r = ≡→T w
  in toWitness r
FDS.Properties (Agda)

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))
FDS.Properties (Agda)

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))
FDS.Properties (Agda)

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? )
FDS.Properties (Agda)


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 ∈ℓ 
               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 = ω⇒∈ a
            --⁺ : Any (P ∘ f) xs → Any P ( f xs)
            in⁺ b
FDS.Properties (Agda)


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 _≢_ 
      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₃ = ω-Disj ap₂ 
      in⁺ ap₃
FDS.Properties (Agda)


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
FDS.Properties (Agda)

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 ( ∣_∣  [ x   x 𝕚𝕟 Transversal ) ≡˘⟨ cong sum d 
          sum   [ x    x 𝕚𝕟 Transversal  
FDS.Properties (Agda)

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


module FDS.Characterisation where
open import FDS
open import FDS.Fin.Subset.Lemmas
open import FDS.List.AllPairs.Lemmas
import FDS.Properties
FDS.Characterisation (Agda)
record Partition (n : ) : Set (sucℓ 0ℓ) where
    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
FDS.Characterisation (Agda)
FDS⇒Partition :  { n}  FinDecEq {} n  Partition n
FDS⇒Partition FDS = 
  record { parts =  [ x   x 𝕚𝕟 Transversal  ;
           disjoint = Disj⇒disj Disjointness ;
           cover = Covering } where
  open FinDecEq FDS
  open FDS.Properties {FDS = FDS}
FDS.Characterisation (Agda)

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 }
    open Partition P
    ωRefl : Reflexive _ωP_
    ωRefl {x} = {P = λ s  x  s} (λ z  z , z) (cover x)
    ωSym : Symmetric _ωP_
    ωSym xωPy = (λ (a , b)  b , a) xωPy
    ωTrans : Transitive _ωP_
    ωTrans {x} {y} {z} xωPy yωPz = 
        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  
              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 }                         
FDS.Characterisation (Agda)

Subset Lemmas

module FDS.Fin.Subset.Lemmas where
open import FDS.Subset.Helpers
FDS.Fin.Subset.Lemmas (Agda)

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⊥)
Disjointness definitionsFDS.Fin.Subset.Lemmas (Agda)

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) =
     (x  xs) ≡⟨ refl 
    x  ( xs) ≡˘⟨ cong (_∪ _) px 
    s  ( xs) ≡⟨ cong (_ ∪_) refl 
    s   ((x  xs) Any. (here {P = P} px)) 
    P : Pred (Subset n)
    P = s ≡_
-remove {n} {x  xs} s (there s∈L) =
    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)) 
FDS.Fin.Subset.Lemmas (Agda)

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∪*
cover-⊤FDS.Fin.Subset.Lemmas (Agda)

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 = 
     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 = 
     (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 = 
     (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)              
∣p⊍q∣≡∣p∣+∣q∣FDS.Fin.Subset.Lemmas (Agda)

which also hold for lists of subsets

∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ :  {n}  (C : List (Subset n))  AllPairs Disj C 
                  C   List.sum ( ∣_∣ C)
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} List.[] Δℓ =
      {n} List.[]  ≡⟨⟩
      {n}  ≡⟨ ∣⊥∣≡0 n 
    0 ≡⟨⟩
    List.foldr _+_ 0 List.[] 
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣ {n} (s  C) (h  t) = 
      (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 ( ∣_∣ C)) ≡⟨⟩
    List.sum ( ∣_∣ (s  C)) 
    a : All (λ x  x   s) C
    a = (disj⇒⊆∁  Disj-sym) h
    c :  C   s
    c = pᵢ⊆q⇒⋃pᵢ⊆q ( s) C a
    DisjUCs : Disj ( C) s
    DisjUCs = ⊆∁⇒disj c
∣⋃ᵢpᵢ∣≡Σᵢ∣pᵢ∣FDS.Fin.Subset.Lemmas (Agda)

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)
FDS.Fin.Subset.Lemmas (Agda)

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)
FDS.Fin.Subset.Lemmas (Agda)
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)
FDS.Fin.Subset.Lemmas (Agda)

List-Relations Properties

missing from the standard library

module FDS.List.AllPairs.Lemmas where
FDS.List.AllPairs.Lemmas (Agda)

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)
FDS.List.AllPairs.Lemmas (Agda)

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)
FDS.List.AllPairs.Lemmas (Agda)

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 = ( ap , hf )
                  y : P  R x  S x
                  y = λ z  Δ p (proj₁ z) (proj₂ z)
                  z : All (S x) (filter P? xs)
                  z = y w
                in z  filter⁺₃ {xs} Δ t
filter⁺₃FDS.List.AllPairs.Lemmas (Agda)


Appendix: Subset Helpers

module FDS.Subset.Helpers where
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 = 
    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 = 
  S  T ≡˘⟨ cong (S ∩_) (¬-involutive T ) 
  S  ( ( T)) ≡⟨ p⊆q⇒p∩∁q≡⊥ s⊆∁t 
  where open Algebra.Properties.BooleanAlgebra (--booleanAlgebra n)           
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
FDS.Subset.Helpers (Agda)
Runtimes (6)