reg064a.idr

import Data.Vect
import Data.Fin
import Control.Isomorphism

Dec0 : Type -> Type
Dec0 = Dec

Dec1 : {A : Type} -> (P : A -> Type) -> Type
Dec1 {A} P = (a : A) -> Dec0 (P a) 

Unique : Type -> Type
Unique t = (p : t) -> (q : t) -> p = q

Unique0 : Type -> Type
Unique0 = Unique

Unique1 : (t0 -> Type) -> Type
Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)

namespace Iso

  from : {A, B : Type} -> Iso A B -> (B -> A)
  from (MkIso to from toFrom fromTo) = from

namespace Fin

  ||| 'Tail' of a finite function
  tail : {A : Type} -> {n : Nat} ->
         (Fin (S n) -> A) -> (Fin n -> A)
  tail f k = f (FS k)

  ||| Maps a finite function to a vector
  toVect : {A : Type} -> {n : Nat} ->
           (Fin n -> A) -> Vect n A
  toVect {n =   Z} _ = Nil
  toVect {n = S m} f = (f FZ) :: (toVect (tail f))

namespace Finite

  ||| Notion of finiteness for types
  Finite : Type -> Type
  Finite A = Exists (\ n => Iso A (Fin n))

  ||| Cardinality of finite types
  card : {A : Type} -> (fA : Finite A) -> Nat
  card = getWitness

  ||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|
  toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
  toVect (Evidence n iso) = toVect (from iso)

||| Filters a vector on a decidable property and pairs elements with proofs
filterTag : {A : Type} ->
            {P : A -> Type} ->
            Dec1 P ->
            Vect n A -> 
            Sigma Nat (\ m => Vect m (Sigma A P))
filterTag d1P Nil = (_ ** Nil)
filterTag d1P (a :: as) with (filterTag d1P as)
  | (_ ** tail) with (d1P a)
    | (Yes p) = (_ ** (a ** p) :: tail)
    | (No  _) = (_ ** tail)

||| Maps a finite type |A| and a decidable predicate |P| to a vector |Sigma A P| values
toVect : {A : Type} ->
         {P : A -> Type} ->
         Finite A ->
         Dec1 P ->
         (n : Nat ** Vect n (Sigma A P))
toVect fA d1P = filterTag d1P (toVect fA)

sigmaUniqueLemma1 : {A   : Type} ->
                    {P   : A -> Type} ->
                    Unique1 {t0 = A} P ->
                    (a : A) ->
                    (p : P a) ->
                    (ss : Vect n (Sigma A P)) ->
                    Elem a (map getWitness ss) -> 
                    Elem (a ** p) ss

toVectComplete : {A   : Type} ->
                 {P   : A -> Type} ->
                 (fA  : Finite A) -> 
                 (d1P : Dec1 P) -> 
                 Unique1 {t0 = A} P ->
                 (s   : Sigma A P) -> 
                 Elem s (getProof (toVect fA d1P))