Finite sums of finite types are finite (ugly proof!)

FinSigma.agda

open import Data.Nat
open import Data.Fin hiding (_+_)
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product renaming (map to pmap)
open import Data.Vec renaming (map to vmap) hiding ([_])
open import Data.Unit
open import Data.Sum renaming (map to smap)
open import Level renaming (zero to lzero; suc to lsuc)

record Finite {α} (A : Set α) : Set α where
  constructor rec
  field
    size   : ℕ
    to     : A → Fin size
    from   : Vec A size
    toFrom : ∀ n → to (lookup n from) ≡ n
    fromTo : ∀ a → lookup (to a) from ≡ a

private
  lem1 :
    ∀ {α}{A : Set α}{n m}(i : Fin m)(xs : Vec A n)(ys : Vec A m)
    → lookup (inject+ n i) (ys ++ xs) ≡ lookup i ys
  lem1 () xs []
  lem1 zero    xs (x ∷ ys) = refl
  lem1 (suc i) xs (x ∷ ys) = lem1 i xs ys
  
  lem2 :
    ∀ {α β}{A : Set α}{B : Set β}{n}(f : A → B)(i : Fin n)(xs : Vec A n)
    → f (lookup i xs) ≡ lookup i (vmap f xs)
  lem2 f () []
  lem2 f zero (x ∷ xs) = refl
  lem2 f (suc i) (x ∷ xs) = lem2 f i xs
  
  lem3 :
    ∀ {α}{A : Set α}{n m}(i : Fin m)(xs : Vec A n)(ys : Vec A m)
    → lookup (raise n i) (xs ++ ys) ≡ lookup i ys
  lem3 i []       ys = refl
  lem3 i (x ∷ xs) ys = lem3 i xs ys
  
  lem4 :
    ∀ {α β γ}{A : Set α}{B : A → Set β}{C : Set γ}{a a' b}
    → (p : a ≡ a')
    → (f : ∀ a → B a → C)
    → f a b ≡ f a' (subst B p b)
  lem4 refl f = refl
  
  lem5 :
    ∀ {n m} (i : Fin (n + m))
    → (∃ λ (i' : Fin n) → inject+ m i' ≡ i) ⊎ (∃ λ (i' : Fin m) → raise n i' ≡ i)
  lem5 {zero}  i       = inj₂ (i , refl)
  lem5 {suc n} zero    = inj₁ (zero , refl)
  lem5 {suc n} (suc i) = smap (pmap suc (cong suc)) (pmap id (cong suc)) (lem5 {n} i)
  
  lem6 :
    ∀ {α β γ δ}
      {A : Set α}{A' : Set β}{B : A' → Set γ}{C : Set δ}
      (f : A → A')
      (g : ∀ a → B (f a) → C)
      {a a' b}
      (p : a ≡ a')
      (q : f a ≡ f a')
      → g a b ≡ g a' (subst B q b)
  lem6 f g refl refl = refl

instance  
  Finite∃ :
    ∀ {α β}{A : Set α}{P : A → Set β}
    ⦃ _ : Finite A ⦄
    ⦃ _ : ∀ {a} → Finite (P a) ⦄
    → Finite (∃ P)
  Finite∃ {A = A}{P}⦃ finA ⦄ ⦃ finPa ⦄ = rec size to from toFrom fromTo where
    module F where open Finite ⦃...⦄ public

    sizes : ∀ {n} → Vec A n → Vec ℕ n
    sizes = vmap (λ a → F.size ⦃ finPa {a} ⦄)

    size : ℕ
    size = sum $ sizes F.from
    
    from' : ∀ {n} (xs : Vec A n) → Vec (∃ P) (sum $ sizes xs)
    from' []       = []
    from' (x ∷ xs) = vmap ,_ F.from ++ from' xs

    from : Vec (∃ P) size
    from = from' F.from

    to' : ∀ {n} (xs : Vec A n) (a : Fin n) → P (lookup a xs) → Fin (sum $ sizes xs)
    to' (x ∷ xs) zero    pa = inject+ (sum $ sizes xs) (F.to pa)
    to' (x ∷ xs) (suc a) pa = raise (F.size ⦃ finPa ⦄) (to' xs a pa)

    to : ∃ P → Fin size
    to (a , pa) = to' F.from (F.to a) (subst P (sym $ F.fromTo a) pa)

    fromTo' :
      ∀ {n}(xs : Vec A n)(a : Fin n) (pa : P (lookup a xs)) → 
      lookup (to' xs a pa) (from' xs) ≡ (lookup a xs , pa)
    fromTo' (x ∷ xs) zero pa
      rewrite lem1 (F.to pa) (from' xs) (vmap ,_ F.from)
      = trans
          (sym (lem2 ,_ (F.to pa) F.from))
          (cong ,_ (F.fromTo pa))     
    fromTo' (x ∷ xs) (suc a) pa =
      trans (lem3 (to' xs a pa) (vmap ,_ F.from) (from' xs)) (fromTo' xs a pa) 

    fromTo : (a : ∃ P) → lookup (to a) from ≡ a
    fromTo (a , pa) = trans
      (fromTo' F.from (F.to a) (subst P (sym $ F.fromTo a) pa))
      (sym $ lem4 (sym $ F.fromTo a) _,_)

    toFrom' :
      ∀ {n}(xs : Vec A n)(i : Fin (sum $ sizes xs))
      → ∃₂ λ a pa → to' xs a pa ≡ i
    toFrom' [] ()
    toFrom' (x ∷ xs) i with lem5 {F.size ⦃ finPa ⦄} {sum $ sizes xs} i
    toFrom' (x ∷ xs) ._ | inj₁ (i' , refl) =
      zero , lookup i' (F.from {{finPa}}) ,
      (cong (inject+ (sum $ sizes xs)) $ F.toFrom {{finPa}} i')
    toFrom' (x ∷ xs) ._ | inj₂ (i' , refl) with toFrom' xs i'
    ... | a , pa , p = suc a , pa , cong (raise (F.size ⦃ finPa ⦄)) p

    toFrom : ∀ i → to (lookup i from) ≡ i
    toFrom i with toFrom' (F.from ⦃ finA ⦄) i
    toFrom ._ | a , pa , refl rewrite
      fromTo' (F.from ⦃ finA ⦄) a pa = sym
        (lem6 {B = P}
           (λ a₁ → lookup a₁ F.from) (to' F.from) {a}
           {F.to (lookup a (F.from ⦃ finA ⦄))}
           (sym (F.toFrom ⦃ finA ⦄ a))
           (sym (F.fromTo (lookup a F.from))))