Operations.lidr 2.71 KB
Newer Older
Nicola Botta's avatar
Nicola Botta committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
> 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)

> -}


> {-

> ---}