blob: d56ada89d1712e6dd82b0b085d5b26b1fe8117b0 (
plain)
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
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
|
module Core.Thinning
import Data.Fin
-- Definition ------------------------------------------------------------------
data Thinner : Nat -> Nat -> Type where
IsBase : Thinner n (S n)
IsDrop : Thinner m n -> Thinner m (S n)
IsKeep : Thinner m n -> Thinner (S m) (S n)
export
data Thins : Nat -> Nat -> Type where
IsId : n `Thins` n
IsThinner : Thinner m n -> m `Thins` n
%name Thinner thin
%name Thins thin
-- Constructors ----------------------------------------------------------------
export
id : (0 n : Nat) -> n `Thins` n
id n = IsId
export
drop : m `Thins` n -> m `Thins` S n
drop IsId = IsThinner IsBase
drop (IsThinner thin) = IsThinner (IsDrop thin)
export
keep : m `Thins` n -> S m `Thins` S n
keep IsId = IsId
keep (IsThinner thin) = IsThinner (IsKeep thin)
public export
wkn1 : (0 n : Nat) -> n `Thins` S n
wkn1 n = drop (id n)
-- Properties
export
keepIdIsId : (0 n : Nat) -> keep (id n) = id (S n)
keepIdIsId n = Refl
-- Non-Identity ----------------------------------------------------------------
export
data IsNotId : m `Thins` n -> Type where
ItIsThinner : IsNotId (IsThinner thin)
%name IsNotId prf
-- Views -----------------------------------------------------------------------
public export
data View : m `Thins` n -> Type where
Id : (0 n : Nat) -> View (id n)
Drop : (thin : m `Thins` n) -> View (drop thin)
Keep : (thin : m `Thins` n) -> {auto 0 prf : IsNotId thin} -> View (keep thin)
%name Thinning.View view
export
view : (thin : m `Thins` n) -> View thin
view IsId = Id m
view (IsThinner IsBase) = Drop (id _)
view (IsThinner (IsDrop thin)) = Drop (IsThinner thin)
view (IsThinner (IsKeep thin)) = Keep (IsThinner thin)
-- Eliminators
export
viewId :
(0 n : Nat) ->
(0 p : View (id n) -> Type) ->
p (Id n) ->
p (view $ id n)
viewId n p x = x
export
viewDrop :
(thin : m `Thins` n) ->
(0 p : View (drop thin) -> Type) ->
p (Drop thin) ->
p (view $ drop thin)
viewDrop IsId p x = x
viewDrop (IsThinner thin) p x = x
export
viewKeep :
forall m, n.
(thin : m `Thins` n) ->
(0 p : View (keep thin) -> Type) ->
((eq1 : m = n) ->
(eq2 : thin = (rewrite eq1 in id n)) ->
p (rewrite eq2 in rewrite eq1 in Id (S n))) ->
({auto 0 prf : IsNotId thin} -> p (Keep thin)) ->
p (view $ keep thin)
viewKeep IsId p id keep = id Refl Refl
viewKeep (IsThinner thin) p id keep = keep
-- Composition -----------------------------------------------------------------
comp : Thinner m n -> Thinner k m -> Thinner k n
comp IsBase thin2 = IsDrop thin2
comp (IsDrop thin1) thin2 = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) IsBase = IsDrop thin1
comp (IsKeep thin1) (IsDrop thin2) = IsDrop (comp thin1 thin2)
comp (IsKeep thin1) (IsKeep thin2) = IsKeep (comp thin1 thin2)
export
(.) : m `Thins` n -> k `Thins` m -> k `Thins` n
IsId . thin2 = thin2
IsThinner thin1 . IsId = IsThinner thin1
IsThinner thin1 . IsThinner thin2 = IsThinner (comp thin1 thin2)
-- Categorical
comp'Assoc :
(thin3 : Thinner m n) ->
(thin2 : Thinner k m) ->
(thin1 : Thinner j k) ->
comp thin3 (comp thin2 thin1) = comp (comp thin3 thin2) thin1
comp'Assoc IsBase thin2 thin1 = Refl
comp'Assoc (IsDrop thin3) thin2 thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) IsBase thin1 = Refl
comp'Assoc (IsKeep thin3) (IsDrop thin2) thin1 = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) IsBase = Refl
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsDrop thin1) = cong IsDrop (comp'Assoc thin3 thin2 thin1)
comp'Assoc (IsKeep thin3) (IsKeep thin2) (IsKeep thin1) = cong IsKeep (comp'Assoc thin3 thin2 thin1)
export
compAssoc :
(thin3 : m `Thins` n) ->
(thin2 : k `Thins` m) ->
(thin1 : j `Thins` k) ->
thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc IsId thin2 thin1 = Refl
compAssoc (IsThinner thin3) IsId thin1 = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) IsId = Refl
compAssoc (IsThinner thin3) (IsThinner thin2) (IsThinner thin1) =
cong IsThinner (comp'Assoc thin3 thin2 thin1)
export
compLeftId : (thin : m `Thins` n) -> id n . thin = thin
compLeftId thin = Refl
export
compRightId : (thin : m `Thins` n) -> thin . id m = thin
compRightId IsId = Refl
compRightId (IsThinner thin) = Refl
-- Specific Cases
export
compLeftDrop :
(thin2 : m `Thins` n) ->
(thin1 : k `Thins` m) ->
drop thin2 . thin1 = drop (thin2 . thin1)
compLeftDrop IsId IsId = Refl
compLeftDrop IsId (IsThinner thin1) = Refl
compLeftDrop (IsThinner thin2) IsId = Refl
compLeftDrop (IsThinner thin2) (IsThinner thin1) = Refl
export
compRightDrop :
(thin2 : m `Thins` n) ->
(thin1 : k `Thins` m) ->
keep thin2 . drop thin1 = drop (thin2 . thin1)
compRightDrop IsId thin1 = Refl
compRightDrop (IsThinner thin2) IsId = Refl
compRightDrop (IsThinner thin2) (IsThinner thin1) = Refl
export
compKeep :
(thin1 : m `Thins` n) ->
(thin2 : k `Thins` m) ->
keep thin1 . keep thin2 = keep (thin1 . thin2)
compKeep IsId thin2 = Refl
compKeep (IsThinner thin1) IsId = Refl
compKeep (IsThinner thin1) (IsThinner thin2) = Refl
export
compLeftWkn1 : (thin : m `Thins` n) -> wkn1 n . thin = drop thin
compLeftWkn1 thin = trans (compLeftDrop (id n) thin) (cong drop $ compLeftId thin)
export
compRightWkn1 : (thin : m `Thins` n) -> keep thin . wkn1 m = drop thin
compRightWkn1 thin = trans (compRightDrop thin (id m)) (cong drop $ compRightId thin)
export
wkn1Comm : (thin : m `Thins` n) -> keep thin . wkn1 m = wkn1 n . thin
wkn1Comm thin = trans (compRightWkn1 thin) (sym $ compLeftWkn1 thin)
-- Weakening -------------------------------------------------------------------
wkn' : Fin m -> Thinner m n -> Fin n
wkn' i IsBase = FS i
wkn' i (IsDrop thin) = FS (wkn' i thin)
wkn' FZ (IsKeep thin) = FZ
wkn' (FS i) (IsKeep thin) = FS (wkn' i thin)
export
wkn : Fin m -> m `Thins` n -> Fin n
wkn i IsId = i
wkn i (IsThinner thin) = wkn' i thin
-- Categorical
export
wknId : (i : Fin n) -> wkn i (id n) = i
wknId i = Refl
wkn'Homo :
(i : Fin k) ->
(thin2 : Thinner m n) ->
(thin1 : Thinner k m) ->
wkn' (wkn' i thin1) thin2 = wkn' i (comp thin2 thin1)
wkn'Homo i IsBase thin1 = Refl
wkn'Homo i (IsDrop thin2) thin1 = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo i (IsKeep thin2) IsBase = Refl
wkn'Homo i (IsKeep thin2) (IsDrop thin1) = cong FS (wkn'Homo i thin2 thin1)
wkn'Homo FZ (IsKeep thin2) (IsKeep thin1) = Refl
wkn'Homo (FS i) (IsKeep thin2) (IsKeep thin1) = cong FS (wkn'Homo i thin2 thin1)
export
wknHomo :
(i : Fin k) ->
(thin1 : k `Thins` m) ->
(thin2 : m `Thins` n) ->
wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i IsId thin2 = sym $ cong (wkn i) $ compRightId thin2
wknHomo i (IsThinner thin1) IsId = Refl
wknHomo i (IsThinner thin1) (IsThinner thin2) = wkn'Homo i thin2 thin1
-- Specific Cases
export
wknDrop : (i : Fin m) -> (thin : m `Thins` n) -> wkn i (drop thin) = FS (wkn i thin)
wknDrop i IsId = Refl
wknDrop i (IsThinner thin) = Refl
export
wknKeepFZ : (thin : m `Thins` n) -> wkn 0 (keep thin) = 0
wknKeepFZ IsId = Refl
wknKeepFZ (IsThinner thin) = Refl
export
wknKeepFS : (i : Fin m) -> (thin : m `Thins` n) -> wkn (FS i) (keep thin) = FS (wkn i thin)
wknKeepFS i IsId = Refl
wknKeepFS i (IsThinner thin) = Refl
|
