------------------------------------------------------------------------ -- 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)