-
Notifications
You must be signed in to change notification settings - Fork 0
/
Utils.idr
86 lines (73 loc) · 2.34 KB
/
Utils.idr
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
module Utils
import Data.Fin
import Data.Vect
total
export
finE : Fin n -> {auto lte : LTE n m} -> Fin m
finE {n = Z} f = void $ FinZAbsurd f
finE {n = S Z} (FS f) = void $ FinZAbsurd f
finE {n = S n} {m = Z} f {lte} = void $ succNotLTEzero lte
finE {n = S n} {m = S m} FZ = FZ
finE {n = S$ S$ n} {m = S$ Z} (FS f) {lte = LTESucc lte} = void $ succNotLTEzero lte
finE {n = S$ S$ n} {m = S$ S$ m} (FS f) {lte = LTESucc lte} = FS $ finE f
total
fseq : (a = b) -> (FS a = FS b)
fseq Refl = Refl
public export
data FinOrd : Fin n -> Fin n -> Type where
FLT : LT (finToNat a) (finToNat b) -> FinOrd a b
FEQ : a = b -> FinOrd a b
FGT : GT (finToNat a) (finToNat b) -> FinOrd a b
total
export
fcompare : (a : Fin n) -> (b : Fin n) -> FinOrd a b
fcompare {n=Z} a b = void $ FinZAbsurd a
fcompare {n=S n} FZ FZ = FEQ Refl
fcompare {n=S n} FZ (FS b) = FLT $ LTESucc LTEZero
fcompare {n=S n} (FS a) FZ = FGT $ LTESucc LTEZero
fcompare {n=S n} (FS a) (FS b) with (fcompare a b)
| FLT lt = FLT $ LTESucc lt
| FEQ eq = FEQ $ fseq eq
| FGT gt = FGT $ LTESucc gt
total
export
finD : (f : Fin (S n)) -> {g : Fin (S n)} -> {gt : GT (finToNat f) (finToNat g)} -> Fin n
finD FZ {g} {gt} = void $ succNotLTEzero gt
finD (FS f) = f
total
export
finDown : {l : Fin (S n)} -> (f : Fin (S n)) -> {lt : LT (finToNat f) (finToNat l)} -> Fin n
finDown {l = FZ} _ {lt} = void $ succNotLTEzero lt
finDown {n = Z} {l = FS l} _ = void $ FinZAbsurd l
finDown {n = S n} {l = FS l} FZ = FZ
finDown {n = S n} {l = FS l} (FS f) {lt = LTESucc lt} = FS $ finDown f {lt}
total
export
ltePlus : LTE n m -> LTE (a + n) (a + m)
ltePlus {a=Z} lte = lte
ltePlus {a=S a} lte = LTESucc $ ltePlus lte
total
export
ltePlus' : LTE a (a + n)
ltePlus' {a=Z} = LTEZero
ltePlus' {a=S a} = LTESucc ltePlus'
total
export
ltePlus'' : LTE n (a + n)
ltePlus'' {n=Z} = LTEZero
ltePlus'' {n=S n} {a} = replace (plusSuccRightSucc a n) $ LTESucc ltePlus''
total
export
nonEmptyNub : NonEmpty l -> NonEmpty (nubBy f l)
nonEmptyNub {l=[]} IsNonEmpty impossible
nonEmptyNub {l=h::t} IsNonEmpty = IsNonEmpty
total
export
nonEmptySort : NonEmpty l -> NonEmpty (sortBy f l)
nonEmptySort {l=[]} IsNonEmpty impossible
nonEmptySort {l=h::t} IsNonEmpty = believe_me $ the (NonEmpty [1, 2]) IsNonEmpty
total
export
nonEmptyMap : NonEmpty l -> NonEmpty (map f l)
nonEmptyMap {l=[]} IsNonEmpty impossible
nonEmptyMap {l=h::t} IsNonEmpty = IsNonEmpty