Commit 6176d58e by Nicola Botta

### Initial.

parent cb037b89
 > module Fin.Operations > import Data.Fin > import Data.Vect > -- import Sigma.Sigma > %default total > %access public export > %auto_implicits off > ||| 'Tail' of a finite function > tail : {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 > toList : {A : Type} -> {n : Nat} -> > (Fin n -> A) -> List A > toList {n = Z} _ = Nil > toList {n = S m} f = (f FZ) :: (toList (tail f)) > ||| 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)) > -- toVect f = map f range > ||| Inverse image as list > invImageList : {n : Nat} -> {B : Type} -> (Eq B) => > (Fin n -> B) -> B -> List (Fin n) > invImageList {n = Z} _ _ = [] > invImageList {n = S m} f b = [k | k <- [FZ .. last], f k == b] > ||| Size of the inverse image > invImageSize : {n : Nat} -> {B : Type} -> (Eq B) => > (Fin n -> B) -> B -> Nat > invImageSize f b = length (invImageList f b) > ||| Inverse image as vector > invImageVect : {n : Nat} -> {B : Type} -> (Eq B) => > (f : Fin n -> B) -> (b : B) -> Vect (invImageSize f b) (Fin n) > invImageVect f b = fromList (invImageList f b) > ||| Sum of the values of a finite function > sum : {n : Nat} -> (Fin n -> Nat) -> Nat > sum {n = Z} f = Z > sum {n = S m} f = f FZ + sum (tail f) > ||| Fold function for Fin > foldFin : {X : Nat -> Type} -> {n : Nat} -> > (f1 : (n : Nat) -> X (S n)) -> > (f2 : (n : Nat) -> X n -> X (S n)) -> > Fin n -> X n > foldFin {n = Z} f1 f2 x impossible > foldFin {n = S m} f1 f2 FZ = f1 m > foldFin {n = S m} f1 f2 (FS i) = f2 m (foldFin f1 f2 i) Obs: Previous functions are not folds, since they do not take a |Fin| as argument. The function |Data.Fin.strengthen| has the "wrong" kind of type for many (most?) purposes. > lastLemma : FZ = last {n = Z} > lastLemma = Refl > strengthen : {n : Nat} -> (k : Fin (S n)) -> {auto contra : Not (k = last)} -> Fin n > strengthen {n = Z} FZ {contra} = void (contra lastLemma) > strengthen {n = S m} FZ {contra} = FZ > strengthen {n = S m} (FS k) {contra} = FS (strengthen k {contra = contra'}) > where contra' : Not (k = last) > contra' k_is_last = contra (cong k_is_last) > {- > strengthen : (k : Fin (S n)) -> Not (k = maxBound {b = Fin (S n)}) -> Fin n > strengthen {n = Z} FZ prf = void (prf Refl) > strengthen {n = (S m)} FZ prf = FZ > strengthen {n = (S m)} (FS k) prf = FS (strengthen k prf') > where > prf' : Not (k = maxBound {b = Fin (S m)}) > prf' k_is_maxBound = prf (cong k_is_maxBound) > -} > {- > ---}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!