{-# 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 as F hiding (_∘_; Distinct↔≢)
open import H-level eq hiding (⌞_⌟)
open import H-level.Closure eq
open import List eq
open import Nat eq as Nat using (_≤_; ≤-refl; ≤-step; _<_; pred)
open import Univalence-axiom eq
∃-Fin-zero : ∀ {p ℓ} (P : Fin zero → Type p) → ∃ P ↔ ⊥ {ℓ = ℓ}
∃-Fin-zero P = Σ-left-zero
∃-Fin-suc : ∀ {p n} (P : Fin (suc n) → Type 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₂) □
abstract
Fin-set : ∀ n → Is-set (Fin n)
Fin-set zero = mono₁ 1 ⊥-propositional
Fin-set (suc n) = ⊎-closure 0 (mono 0≤2 ⊤-contractible) (Fin-set n)
where
0≤2 : 0 ≤ 2
0≤2 = ≤-step (≤-step ≤-refl)
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₂ (
fzero ≡⟨ sym $ to-from f eq₂ ⟩
from f fzero ≡⟨ to-from f eq₁ ⟩∎
fsuc 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)
infix 4 _And_Are-related-by_
_And_Are-related-by_ :
∀ {a} {A : Type a}
(xs ys : List A) → Fin (length xs) ↔ Fin (length ys) → Type a
xs And ys Are-related-by f =
∀ i → index xs i ≡ index ys (_↔_.to f i)
abstract
cancel-suc-preserves-relatedness :
∀ {a} {A : Type 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₂
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
⌞_⌟ : ∀ {n} → Fin n → ℕ
⌞_⌟ {n = zero} ()
⌞_⌟ {n = suc _} fzero = zero
⌞_⌟ {n = suc _} (fsuc i) = suc ⌞ i ⌟
⌞subst⌟ : ∀ {m n} (p : m ≡ n) (i : Fin m) → ⌞ subst Fin p i ⌟ ≡ ⌞ i ⌟
⌞subst⌟ {m} p i =
⌞ subst Fin p i ⌟ ≡⟨ cong (uncurry λ n p → ⌞ subst Fin p i ⌟) (Σ-≡,≡→≡ (sym p) (
subst (m ≡_) (sym p) p ≡⟨ sym trans-subst ⟩
trans p (sym p) ≡⟨ trans-symʳ p ⟩∎
refl m ∎)) ⟩
⌞ subst Fin (refl m) i ⌟ ≡⟨ cong ⌞_⌟ (subst-refl _ _) ⟩∎
⌞ i ⌟ ∎
cancel-⌞⌟ : ∀ {n} {i j : Fin n} → ⌞ i ⌟ ≡ ⌞ j ⌟ → i ≡ j
cancel-⌞⌟ {zero} {}
cancel-⌞⌟ {suc _} {fzero} {fzero} _ = refl _
cancel-⌞⌟ {suc _} {fzero} {fsuc _} 0≡+ = ⊥-elim (Nat.0≢+ 0≡+)
cancel-⌞⌟ {suc _} {fsuc _} {fzero} +≡0 = ⊥-elim (Nat.0≢+ (sym +≡0))
cancel-⌞⌟ {suc _} {fsuc _} {fsuc _} +≡+ =
cong fsuc (cancel-⌞⌟ (Nat.cancel-suc +≡+))
from-ℕ′ : ∀ {m} (n : ℕ) → m ≤ n ⊎ ∃ λ (i : Fin m) → ⌞ i ⌟ ≡ n
from-ℕ′ {zero} _ = inj₁ (Nat.zero≤ _)
from-ℕ′ {suc m} zero = inj₂ (fzero , refl _)
from-ℕ′ {suc m} (suc n) =
⊎-map Nat.suc≤suc (Σ-map fsuc (cong suc)) (from-ℕ′ {m} n)
from-ℕ : ∀ {m} (n : ℕ) → m ≤ n ⊎ Fin m
from-ℕ = ⊎-map id proj₁ ∘ from-ℕ′
Fin↔< : ∀ n → Fin n ↔ ∃ λ m → m < n
Fin↔< zero =
⊥ ↝⟨ inverse ×-right-zero ⟩
ℕ × ⊥ ↔⟨ ∃-cong (λ _ → inverse <zero↔) ⟩□
(∃ λ m → m < zero) □
Fin↔< (suc n) =
⊤ ⊎ Fin n ↝⟨ inverse (_⇔_.to contractible⇔↔⊤ (singleton-contractible 0)) ⊎-cong Fin↔< n ⟩
(∃ λ m → m ≡ 0) ⊎ (∃ λ m → m < n) ↝⟨ id ⊎-cong ∃<↔∃0<×≤ ⟩
(∃ λ m → m ≡ 0) ⊎ (∃ λ m → 0 < m × m ≤ n) ↝⟨ inverse ∃-⊎-distrib-left ⟩
(∃ λ m → m ≡ 0 ⊎ 0 < m × m ≤ n) ↝⟨ ∃-cong (λ _ → inverse ≤↔≡0⊎0<×≤) ⟩
(∃ λ m → m ≤ n) ↝⟨ ∃-cong (λ _ → inverse suc≤suc↔) ⟩
(∃ λ m → suc m ≤ suc n) ↔⟨⟩
(∃ λ m → m < suc n) □
Fin↔<≡⌞⌟ :
∀ {n} (i : Fin n) → proj₁ (_↔_.to (Fin↔< n) i) ≡ ⌞ i ⌟
Fin↔<≡⌞⌟ {n = zero} ()
Fin↔<≡⌞⌟ {n = suc _} fzero = refl _
Fin↔<≡⌞⌟ {n = suc _} (fsuc i) = cong suc (Fin↔<≡⌞⌟ i)
largest : ∀ n → Fin (suc n)
largest zero = fzero
largest (suc n) = fsuc (largest n)
largest-correct : ∀ n → ⌞ largest n ⌟ ≡ n
largest-correct zero = refl _
largest-correct (suc n) = cong suc (largest-correct n)
largest≡Fin↔< :
∀ {n} → largest n ≡ _↔_.from (Fin↔< (suc n)) (n , ≤-refl)
largest≡Fin↔< {n} =
largest n ≡⟨ sym (_↔_.left-inverse-of (Fin↔< (suc n)) _) ⟩
_↔_.from (Fin↔< (suc n)) (_↔_.to (Fin↔< (suc n)) (largest n)) ≡⟨ cong (_↔_.from (Fin↔< (suc n))) (Σ-≡,≡→≡ (Fin↔<≡⌞⌟ (largest n)) (refl _)) ⟩
_↔_.from (Fin↔< (suc n)) (⌞ largest n ⌟ , p₁) ≡⟨ cong (_↔_.from (Fin↔< (suc n)))
(Σ-≡,≡→≡ (largest-correct n) (≤-propositional p₂ ≤-refl)) ⟩∎
_↔_.from (Fin↔< (suc n)) (n , ≤-refl) ∎
where
p₁ = subst (_< suc n) (Fin↔<≡⌞⌟ (largest n))
(proj₂ (_↔_.to (Fin↔< (suc n)) (largest n)))
p₂ = subst (_< suc n) (largest-correct n) p₁
weaken₁ : ∀ {n} → Fin n → Fin (suc n)
weaken₁ {zero} ()
weaken₁ {suc _} fzero = fzero
weaken₁ {suc _} (fsuc i) = fsuc (weaken₁ i)
weaken₁-correct : ∀ {n} (i : Fin n) → ⌞ weaken₁ i ⌟ ≡ ⌞ i ⌟
weaken₁-correct {zero} ()
weaken₁-correct {suc _} fzero = refl _
weaken₁-correct {suc _} (fsuc i) = cong suc (weaken₁-correct i)
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
weaken-correct : ∀ {m n} (m≤n : m ≤ n) (i : Fin m) →
⌞ weaken m≤n i ⌟ ≡ ⌞ i ⌟
weaken-correct (Nat.≤-refl′ m≡n) i =
⌞ subst Fin m≡n i ⌟ ≡⟨ ⌞subst⌟ _ _ ⟩∎
⌞ i ⌟ ∎
weaken-correct (Nat.≤-step′ m≤k 1+k≡n) i =
⌞ subst Fin 1+k≡n (weaken₁ (weaken m≤k i)) ⌟ ≡⟨ ⌞subst⌟ _ _ ⟩
⌞ weaken₁ (weaken m≤k i) ⌟ ≡⟨ weaken₁-correct _ ⟩
⌞ weaken m≤k i ⌟ ≡⟨ weaken-correct m≤k _ ⟩∎
⌞ i ⌟ ∎
predᶠ : ∀ {n} → Fin n → Fin n
predᶠ {n = zero} ()
predᶠ {n = suc _} fzero = fzero
predᶠ {n = suc _} (fsuc i) = weaken₁ i
predᶠ-correct : ∀ {n} (i : Fin n) → ⌞ predᶠ i ⌟ ≡ Nat.pred ⌞ i ⌟
predᶠ-correct {n = zero} ()
predᶠ-correct {n = suc _} fzero = refl _
predᶠ-correct {n = suc _} (fsuc i) = weaken₁-correct i
sucᶠ : ∀ {n} (i : Fin (suc n)) →
i ≡ largest n ⊎
i ≢ largest n × ∃ λ (j : Fin (suc n)) → ⌞ j ⌟ ≡ suc ⌞ i ⌟
sucᶠ {zero} fzero = inj₁ (refl _)
sucᶠ {zero} (fsuc ())
sucᶠ {suc _} fzero = inj₂ (⊎.inj₁≢inj₂ , fsuc fzero , refl _)
sucᶠ {suc _} (fsuc i) =
⊎-map (cong fsuc)
(Σ-map (_∘ ⊎.cancel-inj₂) (Σ-map fsuc (cong suc)))
(sucᶠ i)
_+ᶠ_ : ∀ {m n} → Fin m → Fin n → Fin (m + n)
_+ᶠ_ {m = zero} ()
_+ᶠ_ {m = suc m} fzero j = weaken (Nat.m≤n+m _ (suc m)) j
_+ᶠ_ {m = suc _} (fsuc i) j = fsuc (i +ᶠ j)
+ᶠ-correct :
∀ {m n} (i : Fin m) (j : Fin n) → ⌞ i +ᶠ j ⌟ ≡ ⌞ i ⌟ + ⌞ j ⌟
+ᶠ-correct {m = zero} ()
+ᶠ-correct {m = suc m} fzero j = weaken-correct
(Nat.m≤n+m _ (suc m)) _
+ᶠ-correct {m = suc _} (fsuc i) j = cong suc (+ᶠ-correct i j)
Fin⊎Fin↔Fin+ : ∀ m n → Fin m ⊎ Fin n ↔ Fin (m + n)
Fin⊎Fin↔Fin+ zero n =
Fin 0 ⊎ Fin n ↝⟨ id ⟩
⊥ ⊎ Fin n ↝⟨ ⊎-left-identity ⟩
Fin n ↝⟨ id ⟩□
Fin (0 + 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) □
Fin×Fin↔Fin* : ∀ m n → Fin m × Fin n ↔ Fin (m * n)
Fin×Fin↔Fin* zero n =
Fin 0 × Fin n ↝⟨ id ⟩
⊥ × Fin n ↝⟨ ×-left-zero ⟩
⊥ ↝⟨ id ⟩□
Fin 0 □
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) □
[Fin→Fin]↔Fin^ :
Extensionality (# 0) (# 0) →
∀ m n → (Fin m → Fin n) ↔ Fin (n ^ m)
[Fin→Fin]↔Fin^ ext zero n =
(Fin 0 → Fin n) ↝⟨ id ⟩
(⊥ → Fin n) ↝⟨ Π⊥↔⊤ ext ⟩
⊤ ↝⟨ inverse ⊎-right-identity ⟩□
Fin 1 □
[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) □
[Fin↔Fin]↔Fin! :
Extensionality (# 0) (# 0) →
∀ n → (Fin n ↔ Fin n) ↔ Fin (n !)
[Fin↔Fin]↔Fin! ext zero =
Fin 0 ↔ Fin 0 ↝⟨ Eq.↔↔≃ ext (Fin-set 0) ⟩
Fin 0 ≃ Fin 0 ↝⟨ id ⟩
⊥ ≃ ⊥ ↔⟨ ≃⊥≃¬ ext ⟩
¬ ⊥ ↝⟨ ¬⊥↔⊤ ext ⟩
⊤ ↝⟨ inverse ⊎-right-identity ⟩
⊤ ⊎ ⊥ ↝⟨ id ⟩□
Fin 1 □
[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 !) □
[Fin≡Fin]↔Fin! :
Extensionality (# 0) (# 0) →
Univalence (# 0) →
∀ 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 !) □
Distinct : ∀ {n} → Fin n → Fin n → Type
Distinct i j = Nat.Distinct ⌞ i ⌟ ⌞ j ⌟
Distinct↔≢ :
∀ {k n} {i j : Fin n} →
Extensionality? ⌊ k ⌋-sym lzero lzero →
Distinct i j ↝[ ⌊ k ⌋-sym ] i ≢ j
Distinct↔≢ {i = i} {j} ext =
Distinct i j ↔⟨⟩
Nat.Distinct ⌞ i ⌟ ⌞ j ⌟ ↝⟨ F.Distinct↔≢ ext ⟩
⌞ i ⌟ ≢ ⌞ j ⌟ ↝⟨ generalise-ext?
≢⇔≢
(λ ext → from-isomorphism $
_↔_.to (Eq.⇔↔≃ ext (¬-propositional ext) (¬-propositional ext)) ≢⇔≢)
ext ⟩□
i ≢ j □
where
≢⇔≢ : ⌞ i ⌟ ≢ ⌞ j ⌟ ⇔ i ≢ j
≢⇔≢ = record { to = _∘ cong ⌞_⌟; from = _∘ cancel-⌞⌟ }
Fin↔Fin+≢ :
∀ {n} (i : Fin n) →
Fin (pred n) ↔ ∃ λ (j : Fin n) → Distinct j i
Fin↔Fin+≢ {suc 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+≢ {suc (suc n)} (fsuc i) =
Fin (1 + n) ↔⟨⟩
⊤ ⊎ Fin n ↝⟨ id ⊎-cong Fin↔Fin+≢ i ⟩
⊤ ⊎ (∃ λ (j : Fin (1 + n)) → Distinct j i) ↔⟨ inverse $ ∃-Fin-suc _ ⟩□
(∃ λ (j : Fin (2 + n)) → Distinct j (fsuc i)) □
Fin↔Fin+≢ {zero} ()
Fin↔Fin+≢ {suc zero} (fsuc ())