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

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

open import Equality

module Fin
  {reflexive} (eq : ∀ {a p} → Equality-with-J a p reflexive) where

open import Logical-equivalence hiding (id; _∘_; inverse)
open import Prelude hiding (id)

open import Bijection eq as Bijection using (_↔_; module _↔_)
open Derived-definitions-and-properties eq
open import Equality.Decision-procedures eq
open import Equivalence eq as Eq using (_≃_)
open import Function-universe eq hiding (_∘_)
open import H-level eq
open import H-level.Closure eq
open import List eq
open import Nat eq as Nat using (_≤_; ≤-refl; ≤-step)
open import Univalence-axiom eq

------------------------------------------------------------------------
-- Weakening

-- Single-step weakening.

weaken₁ : ∀ {n} → Fin n → Fin (suc n)
weaken₁ {zero}  ()
weaken₁ {suc _} fzero    = fzero
weaken₁ {suc _} (fsuc i) = fsuc (weaken₁ i)

-- Multiple-step weakening.

weaken : ∀ {m n} → m ≤ n → Fin m → Fin n
weaken (Nat.≤-refl′ m≡n)       = subst Fin m≡n
weaken (Nat.≤-step′ m≤k 1+k≡n) = subst Fin 1+k≡n ∘ weaken₁ ∘ weaken m≤k

------------------------------------------------------------------------
-- 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 fzero ⊎ ∃ (P ∘ fsuc)
∃-Fin-suc P =
  ∃ P                          ↔⟨ ∃-⊎-distrib-right ⟩
  ∃ (P ∘ inj₁) ⊎ ∃ (P ∘ inj₂)  ↔⟨ Σ-left-identity ⊎-cong id ⟩□
  P (inj₁ tt) ⊎ ∃ (P ∘ inj₂)   □

------------------------------------------------------------------------
-- Fin n is a set

abstract

  Fin-set : ∀ n → Is-set (Fin n)
  Fin-set zero    = mono₁  ⊥-propositional
  Fin-set (suc n) = ⊎-closure  (mono 0≤2 ⊤-contractible) (Fin-set n)
    where
    0≤2 :  ≤ 
    0≤2 = ≤-step (≤-step ≤-refl)

------------------------------------------------------------------------
-- 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 ( + m) ↔ Fin ( + n)) →
                 Well-behaved (_↔_.to f)
  well-behaved f {b = i} eq₁ eq₂ = ⊎.inj₁≢inj₂ (
    fzero         ≡⟨ sym $ to-from f eq₂ ⟩
    from f fzero  ≡⟨ to-from f eq₁ ⟩∎
    fsuc i        ∎)
    where open _↔_

cancel-suc : ∀ {m n} → Fin ( + m) ↔ Fin ( + 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  _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 → index xs i ≡ index 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 (fsuc i)) | related (fsuc i)
    helper i | fsuc k , eq₁ | hyp₁ =
      index xs i                    ≡⟨ hyp₁ ⟩
      index (x ∷ ys) (to (fsuc i))  ≡⟨ cong (index (x ∷ ys)) eq₁ ⟩
      index (x ∷ ys) (fsuc k)       ≡⟨ refl _ ⟩∎
      index ys k                    ∎
    helper i | fzero , eq₁ | hyp₁
      with inspect (to (fzero)) | related (fzero)
    helper i | fzero , eq₁ | hyp₁ | fsuc j , eq₂ | hyp₂ =
      index xs i                    ≡⟨ hyp₁ ⟩
      index (x ∷ ys) (to (fsuc i))  ≡⟨ cong (index (x ∷ ys)) eq₁ ⟩
      index (x ∷ ys) (fzero)        ≡⟨ refl _ ⟩
      x                             ≡⟨ hyp₂ ⟩
      index (x ∷ ys) (to (fzero))   ≡⟨ cong (index (x ∷ ys)) eq₂ ⟩
      index (x ∷ ys) (fsuc j)       ≡⟨ refl _ ⟩∎
      index ys j                    ∎
    helper i | fzero , eq₁ | hyp₁ | fzero , 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 fzero
    to (suc m) zero    1+m↔0   = ⊥-elim $ _↔_.to 1+m↔0 fzero

------------------------------------------------------------------------
-- "Type arithmetic" using Fin

-- Taking the disjoint union of two finite sets amounts to the same
-- thing as adding the sizes.

Fin⊎Fin↔Fin+ : ∀ m n → Fin m ⊎ Fin n ↔ Fin (m + n)
Fin⊎Fin↔Fin+ zero n =
  Fin  ⊎ Fin n  ↝⟨ id ⟩
  ⊥ ⊎ Fin n      ↝⟨ ⊎-left-identity ⟩
  Fin n          ↝⟨ id ⟩□
  Fin ( + n)    □
Fin⊎Fin↔Fin+ (suc m) n =
  Fin (suc m) ⊎ Fin n  ↝⟨ id ⟩
  (⊤ ⊎ Fin m) ⊎ Fin n  ↝⟨ inverse ⊎-assoc ⟩
  ⊤ ⊎ (Fin m ⊎ Fin n)  ↝⟨ id ⊎-cong Fin⊎Fin↔Fin+ m n ⟩
  ⊤ ⊎ Fin (m + n)      ↝⟨ id ⟩
  Fin (suc (m + n))    ↝⟨ id ⟩□
  Fin (suc m + n)      □

-- Taking the product of two finite sets amounts to the same thing as
-- multiplying the sizes.

Fin×Fin↔Fin* : ∀ m n → Fin m × Fin n ↔ Fin (m * n)
Fin×Fin↔Fin* zero n =
  Fin  × Fin n  ↝⟨ id ⟩
  ⊥ × Fin n      ↝⟨ ×-left-zero ⟩
  ⊥              ↝⟨ id ⟩□
  Fin           □
Fin×Fin↔Fin* (suc m) n =
  Fin (suc m) × Fin n        ↝⟨ id ⟩
  (⊤ ⊎ Fin m) × Fin n        ↝⟨ ∃-⊎-distrib-right ⟩
  ⊤ × Fin n ⊎ Fin m × Fin n  ↝⟨ ×-left-identity ⊎-cong Fin×Fin↔Fin* m n ⟩
  Fin n ⊎ Fin (m * n)        ↝⟨ Fin⊎Fin↔Fin+ _ _ ⟩
  Fin (n + m * n)            ↝⟨ id ⟩□
  Fin (suc m * n)            □

-- Forming the function space between two finite sets amounts to the
-- same thing as raising one size to the power of the other (assuming
-- extensionality).

[Fin→Fin]↔Fin^ :
  Extensionality (# ) (# ) →
  ∀ m n → (Fin m → Fin n) ↔ Fin (n ^ m)
[Fin→Fin]↔Fin^ ext zero n =
  (Fin  → Fin n)  ↝⟨ id ⟩
  (⊥ → Fin n)      ↝⟨ Π⊥↔⊤ ext ⟩
  ⊤                ↝⟨ inverse ⊎-right-identity ⟩□
  Fin             □
[Fin→Fin]↔Fin^ ext (suc m) n =
  (Fin (suc m) → Fin n)          ↝⟨ id ⟩
  (⊤ ⊎ Fin m → Fin n)            ↝⟨ Π⊎↔Π×Π ext ⟩
  (⊤ → Fin n) × (Fin m → Fin n)  ↝⟨ Π-left-identity ×-cong [Fin→Fin]↔Fin^ ext m n ⟩
  Fin n × Fin (n ^ m)            ↝⟨ Fin×Fin↔Fin* _ _ ⟩
  Fin (n * n ^ m)                ↝⟨ id ⟩□
  Fin (n ^ suc m)                □

-- Automorphisms on Fin n are isomorphic to Fin (n !) (assuming
-- extensionality).

[Fin↔Fin]↔Fin! :
  Extensionality (# ) (# ) →
  ∀ n → (Fin n ↔ Fin n) ↔ Fin (n !)
[Fin↔Fin]↔Fin! ext zero =
  Fin  ↔ Fin   ↝⟨ Eq.↔↔≃ ext (Fin-set ) ⟩
  Fin  ≃ Fin   ↝⟨ id ⟩
  ⊥ ≃ ⊥          ↔⟨ ≃⊥≃¬ ext ⟩
  ¬ ⊥            ↝⟨ ¬⊥↔⊤ ext ⟩
  ⊤              ↝⟨ inverse ⊎-right-identity ⟩
  ⊤ ⊎ ⊥          ↝⟨ id ⟩□
  Fin           □
[Fin↔Fin]↔Fin! ext (suc n) =
  Fin (suc n) ↔ Fin (suc n)      ↝⟨ [⊤⊎↔⊤⊎]↔[⊤⊎×↔] ext Fin._≟_ ⟩
  Fin (suc n) × (Fin n ↔ Fin n)  ↝⟨ id ×-cong [Fin↔Fin]↔Fin! ext n ⟩
  Fin (suc n) × Fin (n !)        ↝⟨ Fin×Fin↔Fin* _ _ ⟩□
  Fin (suc n !)                  □

-- A variant of the previous property.

[Fin≡Fin]↔Fin! :
  Extensionality (# ) (# ) →
  Univalence (# ) →
  ∀ n → (Fin n ≡ Fin n) ↔ Fin (n !)
[Fin≡Fin]↔Fin! ext univ n =
  Fin n ≡ Fin n  ↔⟨ ≡≃≃ univ ⟩
  Fin n ≃ Fin n  ↝⟨ inverse $ Eq.↔↔≃ ext (Fin-set n) ⟩
  Fin n ↔ Fin n  ↝⟨ [Fin↔Fin]↔Fin! ext n ⟩□
  Fin (n !)      □

------------------------------------------------------------------------
-- Inequality and a related isomorphism

-- Inequality.

Distinct : ∀ {n} → Fin n → Fin n → Set
Distinct {zero}  ()
Distinct {suc _} fzero    fzero    = ⊥
Distinct {suc _} fzero    (fsuc j) = ⊤
Distinct {suc _} (fsuc i) fzero    = ⊤
Distinct {suc _} (fsuc i) (fsuc j) = Distinct i j

-- This definition of inequality is pointwise logically equivalent to
-- _≢_, and in the presence of extensionality the two definitions are
-- pointwise isomorphic.

Distinct↔≢ :
  ∀ {k n} {i j : Fin n} →
  Extensionality? ⌊ k ⌋-sym lzero lzero →
  Distinct i j ↝[ ⌊ k ⌋-sym ] i ≢ j
Distinct↔≢ {n = zero}  {}
Distinct↔≢ {n = suc _} {fzero} {fzero} ext =
  ⊥              ↔⟨ inverse Π-left-identity ⟩
  ¬ ⊤            ↝⟨ →-cong ext (from-bijection $ inverse tt≡tt↔⊤) id ⟩
  tt ≢ tt        ↝⟨ →-cong ext (from-bijection Bijection.≡↔inj₁≡inj₁) id ⟩□
  fzero ≢ fzero  □

Distinct↔≢ {n = suc _} {fzero} {fsuc j} ext =
  ⊤               ↝⟨ inverse $ ¬⊥↔⊤ ext ⟩
  ¬ ⊥             ↝⟨ →-cong ext (from-bijection $ inverse Bijection.≡↔⊎) id ⟩□
  fzero ≢ fsuc j  □

Distinct↔≢ {n = suc _} {fsuc i} {fzero} ext =
  ⊤               ↝⟨ inverse $ ¬⊥↔⊤ ext ⟩
  ¬ ⊥             ↝⟨ →-cong ext (from-bijection $ inverse Bijection.≡↔⊎) id ⟩□
  fsuc i ≢ fzero  □

Distinct↔≢ {n = suc _} {fsuc i} {fsuc j} ext =
  Distinct i j     ↝⟨ Distinct↔≢ ext ⟩
  i ≢ j            ↝⟨ →-cong ext (from-bijection Bijection.≡↔inj₂≡inj₂) id ⟩□
  fsuc i ≢ fsuc j  □

-- For every i : Fin (suc n) there is a bijection between Fin n and
-- numbers in Fin (suc n) distinct from i.
--
-- The forward direction of this bijection corresponds to the function
-- "thin" from McBride's "First-order unification by structural
-- recursion", with an added inequality proof, and the other direction
-- is a total variant of "thick".

Fin↔Fin+≢ :
  ∀ {n} (i : Fin (suc n)) →
  Fin n ↔ ∃ λ (j : Fin (suc n)) → Distinct j i
Fin↔Fin+≢ {n} fzero =
  Fin n                                       ↝⟨ inverse ⊎-left-identity ⟩
  ⊥ ⊎ Fin n                                   ↝⟨ inverse $ id ⊎-cong ×-right-identity ⟩
  ⊥ ⊎ Fin n × ⊤                               ↝⟨ inverse $ ∃-Fin-suc _ ⟩□
  (∃ λ (j : Fin (suc n)) → Distinct j fzero)  □

Fin↔Fin+≢ {zero}  (fsuc ())
Fin↔Fin+≢ {suc n} (fsuc i)  =
  Fin ( + n)                                    ↔⟨⟩
  ⊤ ⊎ Fin n                                      ↝⟨ id ⊎-cong Fin↔Fin+≢ i ⟩
  ⊤ ⊎ (∃ λ (j : Fin ( + n)) → Distinct j i)     ↔⟨ inverse $ ∃-Fin-suc _ ⟩□
  (∃ λ (j : Fin ( + n)) → Distinct j (fsuc i))  □