challenge

gistfile1.agda

module Cardinality where

open import Data.Bool using (Bool; true; false)
open import Data.Nat
open import Data.Fin using (Fin; zero; suc)
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function


record Bijection (A B : Set) : Set where
  constructor biject
  field
    A-to-B : A → B
    B-to-A : B → A
    from-to : ∀ x → B-to-A (A-to-B x) ≡ x
    to-from : ∀ x → A-to-B (B-to-A x) ≡ x

open Bijection public

Biject-refl : ∀ {A} → Bijection A A
Biject-refl {A} = biject id id (λ _ → refl) (λ _ → refl)

Biject-sym : ∀ {A B} → Bijection A B → Bijection B A
Biject-sym (biject A-to-B B-to-A from-to to-from) = 
  biject B-to-A A-to-B to-from from-to

Biject-trans : ∀ {A B C} → Bijection A B → Bijection B C → Bijection A C
Biject-trans (biject A-to-B B-to-A from-to to-from) (biject B-to-C C-to-B from-to' to-from') = 
  biject (B-to-C ∘ A-to-B) 
         (B-to-A ∘ C-to-B) 
         (λ x → trans (cong B-to-A (from-to' (A-to-B x))) (from-to x)) 
         (λ x → trans (cong B-to-C (to-from (C-to-B x))) (to-from' x))

Biject-sum : ∀ {A B C D} → Bijection A C → Bijection B D → 
                           Bijection (A ⊎ B) (C ⊎ D)
Biject-sum biject-A-C biject-B-D = 
  biject (λ { (inj₁ x) → inj₁ (A-to-B biject-A-C x) ; 
              (inj₂ x) → inj₂ (A-to-B biject-B-D x) }) 
         (λ { (inj₁ x) → inj₁ (B-to-A biject-A-C x) ; 
              (inj₂ x) → inj₂ (B-to-A biject-B-D x) }) 
         (λ { (inj₁ x) → cong inj₁ (from-to biject-A-C x) ; 
              (inj₂ x) → cong inj₂ (from-to biject-B-D x) }) 
         (λ { (inj₁ x) → cong inj₁ (to-from biject-A-C x) ; 
              (inj₂ x) → cong inj₂ (to-from biject-B-D x) })

Biject-prod : ∀ {A B C D} → Bijection A C → Bijection B D → 
                            Bijection (A × B) (C × D)
Biject-prod biject-A-C biject-B-D = 
  biject (λ { (x , y) → A-to-B biject-A-C x , A-to-B biject-B-D y })
         (λ { (x , y) → B-to-A biject-A-C x , B-to-A biject-B-D y })
         (λ { (x , y) → cong₂ _,_ (from-to biject-A-C x) (from-to biject-B-D y) })
         (λ { (x , y) → cong₂ _,_ (to-from biject-A-C x) (to-from biject-B-D y) })

Cardinality : (A : Set) (n : ℕ) → Set
Cardinality A n = Bijection A (Fin n)

Cardinality-Bool : Cardinality Bool 2
Cardinality-Bool = biject
  (λ { true → zero ; false → suc zero }) 
  (λ { zero → true ; (suc zero) → false ; (suc (suc ())) }) 
  (λ { true → refl ; false → refl }) 
  (λ { zero → refl ; (suc zero) → refl ; (suc (suc ())) })

data T (A : Set) : Set where
  T₁ : T A
  T₂ : A → T A
  T₃ : A → A → T A

Fin-sum : ∀ m n → Cardinality (Fin m ⊎ Fin n) (m + n)
Fin-sum m n = biject merge split split-merge (merge-split {m}) 
  where
    split : ∀ {m n} → Fin (m + n) → Fin m ⊎ Fin n
    split {zero} x = inj₂ x
    split {suc m} zero = inj₁ zero
    split {suc m} (suc x) with split {m} x
    split {suc m} (suc x) | inj₁ x' = inj₁ (suc x')
    split {suc m} (suc x) | inj₂ x' = inj₂ x' 

    merge : ∀ {m n} → Fin m ⊎ Fin n → Fin (m + n)
    merge {zero} (inj₁ ())
    merge {zero} (inj₂ x) = x  
    merge {suc m} (inj₁ zero) = zero
    merge {suc m} (inj₁ (suc x)) = suc (merge (inj₁ x))
    merge {suc m} (inj₂ x) = suc (merge {m} (inj₂ x))

    merge-split : ∀ {m n} (x : Fin (m + n)) → merge (split {m} x) ≡ x
    merge-split {zero} x = refl
    merge-split {suc m} zero = refl
    merge-split {suc m} (suc x) with split {m} x | inspect (split {m}) x
    merge-split {suc m} (suc x) | inj₁ _ | [ i ] rewrite sym i = cong suc (merge-split {m} x)
    merge-split {suc m} (suc x) | inj₂ _ | [ i ] rewrite sym i = cong suc (merge-split {m} x)

    split-merge : ∀ {m n} (x : Fin m ⊎ Fin n) → split {m} (merge {m} x) ≡ x
    split-merge {zero} (inj₁ ())
    split-merge {zero} (inj₂ x) = refl
    split-merge {suc m} (inj₁ zero) = refl
    split-merge {suc m} {n} (inj₁ (suc x)) rewrite split-merge {m} {n} (inj₁ x) = refl 
    split-merge {suc m} {n} (inj₂ x) rewrite split-merge {m} {n} (inj₂ x) = refl

Fin-prod : ∀ m n → Cardinality (Fin m × Fin n) (m * n)
Fin-prod m n = biject merge split split-merge (merge-split {m})
  where
    split : ∀ {m n} → Fin (m * n) → Fin m × Fin n
    split {zero} ()
    split {suc m} {n} x with (B-to-A (Fin-sum n (m * n)) x) 
    split {suc m} x | inj₁ x' = zero , x'
    split {suc m} x | inj₂ x' = suc (proj₁ (split {m} x')) , proj₂ (split {m} x')

    merge : ∀ {m n} → Fin m × Fin n → Fin (m * n)
    merge {zero} (() , x₂)
    merge {suc m} {n} (zero , x₂) = A-to-B (Fin-sum n (m * n)) (inj₁ x₂)
    merge {suc m} {n} (suc x₁ , x₂) = A-to-B (Fin-sum n (m * n)) (inj₂ (merge (x₁ , x₂)))

    merge-split : ∀ {m n} (x : Fin (m * n)) → merge (split {m} x) ≡ x
    merge-split {zero} () 
    merge-split {suc m} {n} x with (B-to-A (Fin-sum n (m * n))) x  | inspect (B-to-A (Fin-sum n (m * n))) x
    merge-split {suc m} {n} x | inj₁ x' | [ i ] rewrite sym i = to-from (Fin-sum n (m * n)) x
    merge-split {suc m} {n} x | inj₂ x' | [ i ] rewrite merge-split {m} {n} x' | sym i = to-from (Fin-sum n (m * n)) x

    split-merge : ∀ {m n} (x : Fin m × Fin n) → split {m} (merge x) ≡ x
    split-merge {zero} (() , x₂)
    split-merge {suc m} {n} (zero , x₂) rewrite from-to (Fin-sum n (m * n)) (inj₁ x₂) = refl
    split-merge {suc m} {n} (suc x₁ , x₂) rewrite from-to (Fin-sum n (m * n)) (inj₂ (merge (x₁ , x₂))) 
      = cong₂ _,_ (cong suc (cong proj₁ (split-merge (x₁ , x₂)))) (cong proj₂ (split-merge (x₁ , x₂)))

Bijection-T : ∀ {A n} → Cardinality A n → Bijection (T A) (Fin 1 ⊎ (Fin n ⊎ (Fin n × Fin n)))
Bijection-T card-A = 
  biject (λ { T₁ → inj₁ zero ; 
              (T₂ x) → inj₂ (inj₁ (A-to-B card-A x)) ; 
              (T₃ x y) → inj₂ (inj₂ (A-to-B card-A x , A-to-B card-A y)) }) 
         (λ { (inj₁ zero) → T₁ ; 
              (inj₁ (suc ())) ; 
              (inj₂ (inj₁ x)) → T₂ (B-to-A card-A x) ; 
              (inj₂ (inj₂ (x , y))) → T₃ (B-to-A card-A x) (B-to-A card-A y) }) 
         (λ { T₁ → refl ; 
              (T₂ x) → cong T₂ (from-to card-A x) ; 
              (T₃ x y) → cong₂ T₃ (from-to card-A x) (from-to card-A y) }) 
         (λ { (inj₁ zero) → refl ; 
              (inj₁ (suc ())) ; 
              (inj₂ (inj₁ x)) → cong inj₂ (cong inj₁ (to-from card-A x)) ; 
              (inj₂ (inj₂ (x , y))) → cong inj₂ (cong inj₂ (cong₂ _,_ (to-from card-A x) (to-from card-A y))) })

Cardinality-T : ∀ {A n} → Cardinality A n → Cardinality (T A) (1 + n + n * n)
Cardinality-T {A} {n} card-A = 
  Biject-trans 
    (Bijection-T card-A) 
    (Biject-trans 
      (Biject-sum 
        Biject-refl 
        (Biject-trans 
          (Biject-sum 
            Biject-refl 
            (Fin-prod n n)) 
          (Fin-sum n (n * n)))) 
      (Fin-sum 1 (n + n * n)))