> module Math
> import Data.Vect
> import Data.HVect
> import Data.List
> import Data.Fin

We take some tricks from https://boxbase.org/entries/2019/sep/16/grabbag-of-idris-tricks/ and http://firsov.ee/finset/finset.pdf.

Use Pauli group as small example:

> data PauliGroup : Type where
>   X : PauliGroup
>   Y : PauliGroup
>   Zp : PauliGroup
>   I : PauliGroup

We provide a complete list of PauliGroup elements:

> listPauli : List PauliGroup
> listPauli = [X,Y,Zp,I]

> allPauli : (x: PauliGroup) -> Data.List.Elem x Math.listPauli
> allPauli X = Here
> allPauli Y = There Here
> allPauli Zp = There (There Here)
> allPauli I = There (There (There Here))

> xIsNotY : (X = Y) -> Void
> xIsNotY Refl impossible
> xIsNotZ : (X = Zp) -> Void
> xIsNotZ Refl impossible
> xIsNotI : (X = I) -> Void
> xIsNotI Refl impossible
> yIsNotZ : (Y = Zp) -> Void
> yIsNotZ Refl impossible
> yIsNotI : (Y = I) -> Void
> yIsNotI Refl impossible
> zIsNotI : (Zp = I) -> Void
> zIsNotI Refl impossible


> DecEq PauliGroup where
>   decEq X X = Yes Refl
>   decEq X Y = No xIsNotY
>   decEq X Zp = No xIsNotZ
>   decEq X I = No xIsNotI
>   decEq Y X = No (\c => xIsNotY (sym c))
>   decEq Y Y = Yes Refl
>   decEq Y Zp = No yIsNotZ
>   decEq Y I = No yIsNotI
>   decEq Zp X = No (\c => xIsNotZ (sym c))
>   decEq Zp Y = No (\c => yIsNotZ (sym c))
>   decEq Zp Zp = Yes Refl
>   decEq Zp I = No zIsNotI
>   decEq I X = No (\c => xIsNotI (sym c))
>   decEq I Y = No (\c => yIsNotI (sym c))
>   decEq I Zp = No (\c => zIsNotI (sym c))
>   decEq I I = Yes Refl

And we give the group structure:

> multPauli : PauliGroup -> PauliGroup -> PauliGroup
> multPauli X X = I
> multPauli X Y = Zp
> multPauli X Zp = Y
> multPauli X I = X
> multPauli Y X = Zp
> multPauli Y Y = I
> multPauli Y Zp = X
> multPauli Y I = Y
> multPauli Zp X = Y
> multPauli Zp Y = X
> multPauli Zp Zp = I
> multPauli Zp I = Zp
> multPauli I X = X
> multPauli I Y = Y
> multPauli I Zp = Zp
> multPauli I I = I

> commPauli : (x:PauliGroup) -> (y:PauliGroup) -> (multPauli x y = multPauli y x)
> commPauli X X = Refl
> commPauli X Y = Refl
> commPauli X Zp = Refl
> commPauli X I = Refl
> commPauli Y X = Refl
> commPauli Y Y = Refl
> commPauli Y Zp = Refl
> commPauli Y I = Refl
> commPauli Zp X = Refl
> commPauli Zp Y = Refl
> commPauli Zp Zp = Refl
> commPauli Zp I = Refl
> commPauli I X = Refl
> commPauli I Y = Refl
> commPauli I Zp = Refl
> commPauli I I = Refl

Obviously there are a number of shortcomings with this approach.... and associativity
would take 64 lines to prove...

> Injective : {t,u:Type} -> (t -> u) -> Type
> Injective f {t} = (x,y:t) -> (f x = f y) -> (x = y)

> Surjective : {t,u:Type} -> (t -> u) -> Type
> Surjective f {t} {u} = (y:u) -> (x:t ** f x = y)

> getInverse : {t,u:Type} -> {func: t -> u} -> (Injective func) -> (Surjective func) -> (u -> t)
> getInverse {t} {u} {func} inj surj = \y => fst (surj y)

> Bijective : {t,u : Type} -> (t -> u) -> Type
> Bijective f {t} {u} = ?bij

Proofs that a list contain all possible elements of a type:

> All : {t : Type} -> List t -> Type 
> All xs {t} = (x:t) -> Elem x xs

Given a type t and a proof of t, it is a contradiction to have a proof that the
empty list contains all elements of t.

> allNotEmpty : All {t} [] -> t -> Void
> allNotEmpty f x = absurd (f x)

> voidEmptyAll : Uninhabited t => All {t} []
> voidEmptyAll = \c => absurd c

Decidable list membership:

> DecIn : (t: Type) -> Type
> DecIn t = (x:t) -> (xs : List t) -> Dec (Elem x xs)

Decidable equality and decidable list membership are equivalent:

> decInToDeqEq : DecIn t -> (x:t) -> (y:t) -> Dec (x = y)
> decInToDeqEq f x y = case (f x [y]) of
>   Yes Here => Yes Refl
>   No contra => No (\eq => contra (rewrite eq in Here))

Little helper lemmas:

> matchingSingleton : Data.List.Elem x [y] -> (x = y)
> matchingSingleton Here = Refl
> matchingSingleton (There later) impossible

> deqEqToDeqIn : DecEq t => DecIn t
> deqEqToDeqIn x [] = No absurd
> deqEqToDeqIn x (y::ys) with (deqEqToDeqIn x ys) 
>   deqEqToDeqIn x (y::ys) | No notLater = case decEq x y of
>       Yes Refl => Yes Here
>       No contra => No (\later => 
>                           case later of
>                               Here => contra (matchingSingleton Here)
>                               (There t) => notLater t)
>   deqEqToDeqIn x (y::ys) | Yes later = Yes (There later)


Proof that a given type is a "mere proposition" (i.e. it only has one element)

> Prop : (t:Type) -> Type
> Prop t = (p1:t) -> (p2:t) -> (p1=p2)

We also have a notion of a List with no duplicates:

> NoDupes : {t:Type} -> List t -> Type
> NoDupes {t} xs = (x:t) -> Prop (Elem x xs)

Some trivial helper lemmas:

> noDupesInHeadLemma : Elem x xs -> NoDupes (x :: xs) -> Void
> noDupesInHeadLemma {x = x} {xs = []} _ _ impossible
> noDupesInHeadLemma {x} a b = hereIsNotThere (b x Here (There a))

If a type has decidable equality, then All and NoDupes are decidable.
We need a (somewhat metamathematical) lemma to start stating that any two
void values of the same type are equal (there are in fact zero of them - this
is just a wrapper for "void can prove anything")

> voidsAreEquivalent : {t: Type} -> (t -> Void) -> (a:t) -> (b:t) -> (a=b)
> voidsAreEquivalent f a b = void (f a)

> sameTheresLemma : {a: Data.List.Elem x xs} -> (There a = There a)
> sameTheresLemma = Refl

To avoid an awkward workaround with Void types, we force the caller to prove that
the type isn't void by providing some item. This might need some work...

> deqEqToAllIncomplete : DecEq t => (xs:List t) -> t -> Dec (All xs)
> deqEqToAllIncomplete [] someItem = No (\c => allNotEmpty c someItem)
> deqEqToAllIncomplete (x :: xs) someitem = Yes (\c =>
>   case (decEq x c) of
>       Yes pf => rewrite pf in Here
>       No contra => ?newh2)

After some reflection, I don't think this will work. We need to know *ahead of time*
that All {t} [xs] exists. This method will always fail to converge for Nats.

> thereLemma1 : {a: Data.List.Elem x xs} -> {b : Data.List.Elem x xs} -> (a = b) -> There a = There b
> thereLemma1 {a = Here} {b = Here} Refl = Refl
> thereLemma1 {a = Here} {b = (There _)} Refl impossible
> thereLemma1 {a = (There _)} {b = Here} Refl impossible
> thereLemma1 {a = (There x)} {b = (There x)} Refl = Refl

> thereLemma2 : {a: Data.List.Elem x xs} -> {b : Data.List.Elem x xs} -> (There a = There b) -> a = b
> thereLemma2 {a = Here} {b = Here} pf = Refl
> thereLemma2 {a = Here} {b = (There _)} Refl impossible
> thereLemma2 {a = (There _)} {b = Here} Refl impossible
> thereLemma2 {a = (There x)} {b = (There x)} Refl = Refl


> consNoDupes : DecEq t => {x : t} -> NoDupes {t} xs -> (Not (Elem x xs)) -> NoDupes (x :: xs)
> consNoDupes {x = x} noDupesSublist notIn y pf1 pf2 with (decEq x y)
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | Yes pf = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | Yes pf = absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | Yes pf = absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | Yes pf = absurd (notIn (rewrite pf in later)) --rewrite (noDupesSublist y later z) in Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here Here | No contra = Refl
>   consNoDupes {x = y} noDupesSublist notIn y Here (There later) | No contra = absurd (notIn later)
>   consNoDupes {x = y} noDupesSublist notIn y (There later) Here | No contra = absurd (notIn later)
>   consNoDupes {x = x} noDupesSublist notIn y (There later) (There z) | No contra = let ndupes = (noDupesSublist y later z) in thereLemma1 ndupes


> dupeCons : NoDupes (x :: xs) -> NoDupes xs
> dupeCons dupeBiglist item pf1 pf2 = thereLemma2 (dupeBiglist item (There pf1) (There pf2))

> deqEqToDupe : DecEq t => (xs:List t) -> Dec (NoDupes xs)
> deqEqToDupe [] = Yes (\a => (\b => (\c => (voidsAreEquivalent uninhabited b c))))
> deqEqToDupe (x :: xs) with (isElem x xs)
>   deqEqToDupe (x :: xs) | Yes pf = No (noDupesInHeadLemma pf)
>   deqEqToDupe (x :: xs) | No contra = case deqEqToDupe xs of
>       Yes noDupes => Yes (consNoDupes noDupes contra)
>       No areDupes => No (\c => areDupes (dupeCons c))

If P is a decidable proposition, we can quotient P by the total equivalence relation
and get a "squashed" type {what is this relation?}

> squash : {p:Type} -> Dec p -> Type
> squash (Yes _) = Unit
> squash (No _) = Void

An example: Elem x [x,y,x] is decidable:

> exSquash1 : Dec (Data.List.Elem X [X,Y,X])
> exSquash1 = Yes Here

> exSquash2 : Dec (Data.List.Elem X [X,Y,X])
> exSquash2 = Yes (There (There Here))

Both "squash" to Unit. Note that any two squashed values are trivially equal:

> propSquash : {p: Type} -> (d : Dec p) -> Prop (squash d)
> propSquash (Yes prf) () () = Refl
> propSquash (No contra) v1 _ = absurd v1

> fromSquash : {p:Type} -> (d : Dec p) -> squash d -> p
> fromSquash (Yes prf) () = prf

makeAllFin : (k:Nat) -> (xs:(List (Fin (S k))) ** All (Fin (S k)) xs)
makeAllFin Z = ([FZ] ** (IsAll (\x => Here)))

Kuratowski finiteness:

> Listable : (t : Type) -> Type
> Listable t = (xs ** (All {t} xs))

An alternative idea is to require a surjection Fin n to t for some Nat n:

> FinSurjective : (t: Type) -> Type
> FinSurjective ty = (n:Nat ** (fromFin : (Fin n -> ty) ** (Surjective fromFin)))

These notions are equivalent. We need some helper lemmas... it is quite likely 
that these can be cleaned up considerably...

> getIndexOfElem : Data.List.Elem x xs -> Fin (length xs)
> getIndexOfElem Here = FZ
> getIndexOfElem (There later) = FS (getIndexOfElem later)

> getIndexFromAll : All {t} xs -> t -> Fin (length xs)
> getIndexFromAll {xs = []} pf x = absurd (pf x)
> getIndexFromAll {xs = (y :: xs)} pf x = getIndexOfElem (pf x)

> finIndexList : (l:List t) -> Fin (length l) -> t
> finIndexList [] _ impossible
> finIndexList (x :: _) FZ = x
> finIndexList (_ :: xs) (FS y) = finIndexList xs y

> getIndexOfElemLemma : (pf : Data.List.Elem x xs) -> finIndexList xs (getIndexOfElem pf) = x
> getIndexOfElemLemma {xs = (x :: ys)} Here = Refl
> getIndexOfElemLemma {xs = (y :: ys)} (There later) = getIndexOfElemLemma later

> getIndexOfAllLemma : (pf : All {t} xs) -> (x : t) -> finIndexList xs (getIndexFromAll pf x) = x
> getIndexOfAllLemma {xs} pf x with (pf x)
>   getIndexOfAllLemma {xs= x :: ys} pf x | Here = getIndexOfElemLemma (pf x)
>   getIndexOfAllLemma {xs= y :: ys} pf x | (There later) = getIndexOfElemLemma (pf x)

> finIndexListSurjectiveIfAll : All {t} xs -> Surjective (finIndexList xs)
> finIndexListSurjectiveIfAll {xs} pf = \y => ((getIndexFromAll pf y) ** (getIndexOfAllLemma pf y))

> indexIntoAll : All {t} xs -> (f : (Fin (length xs) -> t) ** Surjective f)
> indexIntoAll {xs} pf = ((finIndexList xs) ** (finIndexListSurjectiveIfAll pf))

> natToListFin : (n : Nat) -> List (Fin n)
> natToListFin Z = []
> natToListFin (S n) = (the (Fin (S n)) last) :: (map weaken (natToListFin n))

> lastFinLemma : {n: Nat} -> (((FS k) = last {n=n}) -> Void) -> ((k = last {n=n}) -> Void)
> lastFinLemma {n = Z} {k=_} _ impossible
> lastFinLemma {n = (S Z)} {k = FZ} contra = absurd (contra Refl)
> lastFinLemma {n = (S (S k))} {k = FZ} contra = ?lastFinLemma_rhs_4
> lastFinLemma {n = (S j)} {k = (FS x)} contra = ?lastFinLemma_rhs_3

 lastFinLemma {n = Z} {k = FZ} _ impossible
 lastFinLemma {n = Z} {k = (FS _)} _ impossible


> safeStrengthen : (f : Fin (S n)) -> (contra : (f = last {n=n}) -> Void) -> Fin n
> safeStrengthen {n=Z} FZ contra = absurd (contra Refl)
> safeStrengthen {n=(S k)} FZ contra = FZ
> safeStrengthen {n=(S k)} (FS x) contra = ?ssh_2

> natToListFinIsAll : (n : Nat) -> (All (natToListFin n))
> natToListFinIsAll Z = voidEmptyAll
> natToListFinIsAll (S n) = \f => 
>   case (decEq (the (Fin (S n)) last) f) of
>       Yes pf => rewrite pf in Here
>       No _ => ?newhole -- There (natToListFinIsAll n (safeStrengthen f))

natToListFinIsAll (S Z) = (\FZ => Here)


> getAllFins : (n : Nat) -> (xs : (List (Fin n)) ** All xs)
> getAllFins n = ((natToListFin n) ** (natToListFinIsAll n))

 getAllFins (S k) = ((getAllFinsInner (S k)) ** )

> listableIsFinSurjective : Listable t -> FinSurjective t
> listableIsFinSurjective (xs ** pf) = ((length xs) ** (indexIntoAll pf))

> finSurjectiveToList : FinSurjective t -> List t
> finSurjectiveToList (bd ** (surj ** pf)) = map surj (fst (getAllFins bd))


> finSurjectiveIsListable : FinSurjective t -> Listable t
> finSurjectiveIsListable (bound ** (surj ** pf)) = ?finSurjectiveIsListable_rhs_2

> contrapositive : (a -> b) -> Not b -> Not a
> contrapositive f nb a = nb (f a)

makeAllFin (S k) = ?makeAllFin_rhs_2

> interface Countable t where
>   FromNat : Nat -> t
>   ToNat : t -> Nat

> Countable Nat where
>   FromNat = id
>   ToNat = id

An $n$-place relation on a collection of sets $S_1, S_2,\dots,S_n$ is a set $R\subset 
S_1 \times S_2 \times \dots \times S_n$. We say $s_1\in S_1,s_2\in S_2,\dots, s_n\in S_n$ 
are related by $R$ if $(s_1,s_2,\dots,s_n)\in R$.

> NaryRelation : Vect n Type -> Type
> NaryRelation xs = List (HVect xs) -- for our purposes it is fine to use lists instead of sets

> BinaryRelation : Vect 2 Type -> Type
> BinaryRelation = NaryRelation

> domain : BinaryRelation [xt,yt] -> List yt
> domain [] = []
> domain ([x,y] :: xs) = y :: (domain xs)

> codomain : BinaryRelation [xt,yt] -> List xt
> codomain [] = []
> codomain ([x,y] :: xs) = x :: (codomain xs)

> data PartialFunction : BinaryRelation [xy,yt] -> Type where
>   