```------------------------------------------------------------------------
-- Some definitions related to and properties of finite sets
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

-- Note that this module is not parametrised by a definition of
-- equality; it uses ordinary propositional equality.

module Fin where

open import Equality.Propositional as P
open import Equivalence hiding (id; _∘_; inverse)
open import Prelude hiding (id)

import Bijection
open Bijection P.equality-with-J using (_↔_; module _↔_)
import Equality.Decision-procedures as ED; open ED P.equality-with-J
import Function-universe as FU; open FU P.equality-with-J hiding (_∘_)

------------------------------------------------------------------------
-- Some bijections relating Fin and ∃

∃-Fin-zero : ∀ {p ℓ} (P : Fin zero → Set p) → ∃ P ↔ ⊥ {ℓ = ℓ}
∃-Fin-zero P = Σ-left-zero

∃-Fin-suc : ∀ {p n} (P : Fin (suc n) → Set p) →
∃ P ↔ P (inj₁ tt) ⊎ ∃ (P ∘ inj₂)
∃-Fin-suc P =
∃ P                          ↔⟨ ∃-⊎-distrib-right ⟩
∃ (P ∘ inj₁) ⊎ ∃ (P ∘ inj₂)  ↔⟨ Σ-left-identity ⊎-cong id ⟩□
P (inj₁ tt) ⊎ ∃ (P ∘ inj₂)   □

------------------------------------------------------------------------
-- If two nonempty finite sets are isomorphic, then we can remove one
-- element from each and get new isomorphic finite sets

private

well-behaved : ∀ {m n} (f : Fin (1 + m) ↔ Fin (1 + n)) →
Well-behaved (_↔_.to f)
well-behaved f {b = i} eq₁ eq₂ =  ⊎.inj₁≢inj₂ (
inj₁ tt           ≡⟨ sym \$ to-from f eq₂ ⟩
from f (inj₁ tt)  ≡⟨ to-from f eq₁ ⟩∎
inj₂ i            ∎)
where open _↔_

cancel-suc : ∀ {m n} → Fin (1 + m) ↔ Fin (1 + n) → Fin m ↔ Fin n
cancel-suc f =
⊎-left-cancellative f (well-behaved f) (well-behaved \$ inverse f)

-- In fact, we can do it in such a way that, if the input bijection
-- relates elements of two lists with equal heads, then the output
-- bijection relates elements of the tails of the lists.
--
-- xs And ys Are-related-by f is inhabited if the indices of xs and ys
-- which are related by f point to equal elements.

infix 4 _And_Are-related-by_

_And_Are-related-by_ :
∀ {a} {A : Set a}
(xs ys : List A) → Fin (length xs) ↔ Fin (length ys) → Set a
xs And ys Are-related-by f =
∀ i → lookup xs i ≡ lookup ys (_↔_.to f i)

abstract

-- The tails are related.

cancel-suc-preserves-relatedness :
∀ {a} {A : Set a} (x : A) xs ys
(f : Fin (length (x ∷ xs)) ↔ Fin (length (x ∷ ys))) →
x ∷ xs And x ∷ ys Are-related-by f →
xs And ys Are-related-by cancel-suc f
cancel-suc-preserves-relatedness x xs ys f related = helper
where
open _↔_ f

helper : xs And ys Are-related-by cancel-suc f
helper i with inspect (to (inj₂ i)) | related (inj₂ i)
helper i | inj₂ k with-≡ eq₁ | hyp₁ =
lookup xs i                    ≡⟨ hyp₁ ⟩
lookup (x ∷ ys) (to (inj₂ i))  ≡⟨ cong (lookup (x ∷ ys)) eq₁ ⟩
lookup (x ∷ ys) (inj₂ k)       ≡⟨ refl ⟩∎
lookup ys k                    ∎
helper i | inj₁ tt with-≡ eq₁ | hyp₁
with inspect (to (inj₁ tt)) | related (inj₁ tt)
helper i | inj₁ tt with-≡ eq₁ | hyp₁ | inj₂ j with-≡ eq₂ | hyp₂ =
lookup xs i                     ≡⟨ hyp₁ ⟩
lookup (x ∷ ys) (to (inj₂ i))   ≡⟨ cong (lookup (x ∷ ys)) eq₁ ⟩
lookup (x ∷ ys) (inj₁ tt)       ≡⟨ refl ⟩
x                               ≡⟨ hyp₂ ⟩
lookup (x ∷ ys) (to (inj₁ tt))  ≡⟨ cong (lookup (x ∷ ys)) eq₂ ⟩
lookup (x ∷ ys) (inj₂ j)        ≡⟨ refl ⟩∎
lookup ys j                     ∎
helper i | inj₁ tt with-≡ eq₁ | hyp₁ | inj₁ tt with-≡ eq₂ | hyp₂ =
⊥-elim \$ well-behaved f eq₁ eq₂

-- By using cancel-suc we can show that finite sets are isomorphic iff
-- they have equal size.

isomorphic-same-size : ∀ {m n} → (Fin m ↔ Fin n) ⇔ m ≡ n
isomorphic-same-size {m} {n} = record
{ to   = to m n
; from = λ m≡n → subst (λ n → Fin m ↔ Fin n) m≡n id
}
where
abstract
to : ∀ m n → (Fin m ↔ Fin n) → m ≡ n
to zero    zero    _       = refl
to (suc m) (suc n) 1+m↔1+n = cong suc \$ to m n \$ cancel-suc 1+m↔1+n
to zero    (suc n)   0↔1+n = ⊥-elim \$ _↔_.from 0↔1+n (inj₁ tt)
to (suc m) zero    1+m↔0   = ⊥-elim \$ _↔_.to 1+m↔0 (inj₁ tt)
```