Commit 553bf1df authored by Nicola Botta's avatar Nicola Botta
Browse files

Cleanup.

parent f929abf3
......@@ -7,20 +7,20 @@ import Data.Vect
||| 'Tail' of a finite function
public export
tail : {A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
-- tail f k = f (FS k)
tail f = f . FS
||| Maps a finite function to a list
public export
toList : {A : Type} -> {n : Nat} -> (Fin n -> A) -> List A
toList : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> List A
toList {n = Z} _ = Nil
toList {n = S m} f = (f FZ) :: (Fin.Operations.toList (tail f))
||| Maps a finite function to a vector
public export
toVect : {A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (Fin.Operations.toVect (tail f))
......@@ -9,13 +9,13 @@ import Fin.Operations
||| Maps a finite type |A| to a list of |A|-values
public export
toList : {A : Type} -> (Finite A) => List A
toList : (Finite t) => List t
toList = toList (from iso)
||| Maps a finite type |A| of cardinality |n| to a vector of |A|-values of length |n|
public export
toVect : {A : Type} -> (Finite A) => Vect card A
toVect : (Finite t) => Vect (card {t}) t
toVect = toVect (from iso)
......
......@@ -4,14 +4,22 @@ import Data.Vect
import FiniteAsInterface.Finite
import FiniteAsInterface.Operations
import Sigma.Sigma
import Sigma.Operations
import Isomorphism.Isomorphism
import Isomorphism.Properties
import Fin.Operations
import Fin.Properties
import Basic.Operations
import Fun.Predicates
import Vect.Predicates
import Vect.Properties
import Nat.LTProperties
||| |toVect| representations of finite types are complete
public export
toVectComplete : {A : Type} -> (Finite A) => (a : A) -> Elem a toVect
{-
toVectComplete : (Finite t) => (x : t) -> Elem x (toVect {t})
toVectComplete a = s3 where
s1 : Elem (from iso (to iso a)) (toVect (from iso))
s1 = toVectComplete (from iso) (to iso a)
......@@ -20,4 +28,6 @@ toVectComplete a = s3 where
s3 : Elem a (toVect (from iso))
s3 = replace {p = \ z => Elem z (toVect (from iso))} s2 s1
{-
---}
......@@ -30,5 +30,6 @@ nonInjectiveNotInjective f (MkSigma x (MkSigma y (nxeqy , fxeqfy))) =
public export
nonSurjectiveNotSurjective : {s, t : Type} -> (f : s -> t) -> NonSurjective f -> Not (Surjective f)
nonSurjectiveNotSurjective f (MkSigma y faxnfxy) =
\ surjectivef => let x = (outl (surjectivef y)) in (faxnfxy x) (outr (surjectivef y))
-- \ surjectivef => let x = outl (surjectivef y) in (faxnfxy x) (outr (surjectivef y))
\ surjectivef => (faxnfxy (outl (surjectivef y))) (outr (surjectivef y))
......@@ -6,9 +6,9 @@ import Data.Vect
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVect : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVect {n = Z} _ = Nil
toVect {n = S m} f = (f FZ) :: (toVect (tail f))
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
record Iso a b where
constructor MkIso
......@@ -25,5 +25,6 @@ Finite t = DPair Nat (\ n => Iso t (Fin n))
card : Finite t -> Nat
card (MkDPair n _) = n
foo : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
foo (MkDPair _ iso) = toVect (from iso)
toVect : {A : Type} -> (fA : Finite A) -> Vect (card fA) A
toVect (MkDPair _ iso) = toVectFun (from iso)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment