blob: 0b1de68e1952e057e2915c69f27add2433ff765c (
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
|
module Core.Thinning
import Core.Context
import Syntax.PreorderReasoning
-- Definition ------------------------------------------------------------------
data Thinner : Context -> Context -> Type where
IsBase : (0 n : Name) -> Thinner sx (sx :< n)
IsDrop : Thinner sx sy -> (0 n : Name) -> Thinner sx (sy :< n)
IsKeep : Thinner sx sy -> (0 n : Name) -> Thinner (sx :< n) (sy :< n)
export
data Thins : Context -> Context -> Type where
IsId : sx `Thins` sx
IsThinner : Thinner sx sy -> sx `Thins` sy
%name Thinner thinner
%name Thins thin
export
data IsNotId : sx `Thins` sy -> Type where
ItIsThinner : IsNotId (IsThinner thinner)
-- Constructors ----------------------------------------------------------------
export
id : (0 sx : Context) -> sx `Thins` sx
id sx = IsId
export
drop : sx `Thins` sy -> (0 n : Name) -> sx `Thins` sy :< n
drop IsId n = IsThinner (IsBase n)
drop (IsThinner thinner) n = IsThinner (IsDrop thinner n)
export
keep : sx `Thins` sy -> (0 n : Name) -> sx :< n `Thins` sy :< n
keep IsId n = IsId
keep (IsThinner thinner) n = IsThinner (IsKeep thinner n)
-- Views -----------------------------------------------------------------------
public export
data View : sx `Thins` sy -> Type where
Id : (0 sx : Context) -> View (id sx)
Drop : (thin : sx `Thins` sy) -> (0 n : Name) -> View (drop thin n)
Keep :
(thin : sx `Thins` sy) ->
{auto 0 prf : IsNotId thin} -> -- For uniqueness
(0 n : Name) ->
View (keep thin n)
%name View view
export
view : (thin : sx `Thins` sy) -> View thin
view IsId = Id sx
view (IsThinner (IsBase n)) = Drop IsId n
view (IsThinner (IsDrop thinner n)) = Drop (IsThinner thinner) n
view (IsThinner (IsKeep thinner n)) = Keep (IsThinner thinner) n
-- Unique
viewInverse : {0 thin : sx `Thins` sy} -> View thin -> sx `Thins` sy
viewInverse (Id sy) = id sy
viewInverse (Drop thin n) = drop thin n
viewInverse (Keep thin n) = keep thin n
viewInversePrf1 : (view : View thin) -> viewInverse view = thin
viewInversePrf1 (Id _) = Refl
viewInversePrf1 (Drop _ _) = Refl
viewInversePrf1 (Keep _ _) = Refl
viewInversePrf2 : (v : View thin) -> view (viewInverse v) = (rewrite viewInversePrf1 v in v)
viewInversePrf2 (Id sy) = Refl
viewInversePrf2 (Drop IsId n) = Refl
viewInversePrf2 (Drop (IsThinner thinner) n) = Refl
viewInversePrf2 (Keep {prf} IsId n) impossible
viewInversePrf2 (Keep {prf = ItIsThinner} (IsThinner thinner) n) = Refl
export
viewUnique : (view1, view2 : View thin) -> view1 = view2
viewUnique view1 view2 =
rewrite sym $ viewInversePrf2 view1 in
rewrite sym $ viewInversePrf2 view2 in
rewrite viewInversePrf1 view1 in
rewrite viewInversePrf1 view2 in
Refl
-- Composition -----------------------------------------------------------------
comp : Thinner sy sz -> Thinner sx sy -> Thinner sx sz
comp (IsBase n) thinner1 = IsDrop thinner1 n
comp (IsDrop thinner2 n) thinner1 = IsDrop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsBase n) = IsDrop thinner2 n
comp (IsKeep thinner2 n) (IsDrop thinner1 n) = IsDrop (comp thinner2 thinner1) n
comp (IsKeep thinner2 n) (IsKeep thinner1 n) = IsKeep (comp thinner2 thinner1) n
export
(.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
IsId . thin1 = thin1
(IsThinner thinner2) . IsId = IsThinner thinner2
(IsThinner thinner2) . (IsThinner thinner1) = IsThinner (comp thinner2 thinner1)
-- Identities
export
compLeftIdentity : (thin : sx `Thins` sy) -> id sy . thin = thin
compLeftIdentity thin = Refl
export
compRightIdentity : (thin : sx `Thins` sy) -> thin . id sx = thin
compRightIdentity IsId = Refl
compRightIdentity (IsThinner thinner) = Refl
-- Drop
export
compLeftDrop :
(thin2 : sy `Thins` sz) ->
(thin1 : sx `Thins` sy) ->
(0 n : Name) ->
drop thin2 n . thin1 = drop (thin2 . thin1) n
compLeftDrop IsId IsId n = Refl
compLeftDrop IsId (IsThinner thinner) n = Refl
compLeftDrop (IsThinner thinner) IsId n = Refl
compLeftDrop (IsThinner thinner) (IsThinner thinner1) n = Refl
export
compRightDrop :
(thin2 : sy `Thins` sz) ->
(thin1 : sx `Thins` sy) ->
(0 n : Name) ->
keep thin2 n . drop thin1 n = drop (thin2 . thin1) n
compRightDrop IsId thin1 n = Refl
compRightDrop (IsThinner thinner) IsId n = Refl
compRightDrop (IsThinner thinner) (IsThinner thinner1) n = Refl
-- Keep
export
compKeep :
(thin2 : sy `Thins` sz) ->
(thin1 : sx `Thins` sy) ->
(0 n : Name) ->
keep thin2 n . keep thin1 n = keep (thin2 . thin1) n
compKeep IsId thin1 n = Refl
compKeep (IsThinner thinner) IsId n = Refl
compKeep (IsThinner thinner) (IsThinner thinner1) n = Refl
-- Associative
compAssoc' :
{thin3 : sz `Thins` sw} ->
{thin2 : sy `Thins` sz} ->
{thin1 : sx `Thins` sy} ->
View thin3 ->
View thin2 ->
View thin1 ->
thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc' (Id sw) view2 view1 = Refl
compAssoc' (Drop thin3 n) view2 view1 = Calc $
|~ drop thin3 n . (thin2 . thin1)
~~ drop (thin3 . (thin2 . thin1)) n ...(compLeftDrop thin3 (thin2 . thin1) n)
~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) view2 view1)
~~ drop (thin3 . thin2) n . thin1 ..<(compLeftDrop (thin3 . thin2) thin1 n)
~~ (drop thin3 n . thin2) . thin1 ..<(cong (. thin1) $ compLeftDrop thin3 thin2 n)
compAssoc' (Keep thin3 n) (Id _) view1 = cong (. thin1) $ sym $ compRightIdentity (keep thin3 n)
compAssoc' (Keep thin3 n) (Drop thin2 n) view1 = Calc $
|~ keep thin3 n . (drop thin2 n . thin1)
~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compLeftDrop thin2 thin1 n)
~~ drop (thin3 . (thin2 . thin1)) n ...(compRightDrop thin3 (thin2 . thin1) n)
~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) view1)
~~ drop (thin3 . thin2) n . thin1 ..<(compLeftDrop (thin3 . thin2) thin1 n)
~~ (keep thin3 n . drop thin2 n) . thin1 ..<(cong (. thin1) $ compRightDrop thin3 thin2 n)
compAssoc' (Keep thin3 n) (Keep thin2 n) (Id _) = Calc $
|~ keep thin3 n . (keep thin2 n . id _)
~~ keep thin3 n . keep thin2 n ...(cong (keep thin3 n .) $ compRightIdentity (keep thin2 n))
~~ (keep thin3 n . keep thin2 n) . id _ ..<(compRightIdentity (keep thin3 n . keep thin2 n))
compAssoc' (Keep thin3 n) (Keep thin2 n) (Drop thin1 n) = Calc $
|~ keep thin3 n . (keep thin2 n . drop thin1 n)
~~ keep thin3 n . drop (thin2 . thin1) n ...(cong (keep thin3 n .) $ compRightDrop thin2 thin1 n)
~~ drop (thin3 . (thin2 . thin1)) n ...(compRightDrop thin3 (thin2 . thin1) n)
~~ drop ((thin3 . thin2) . thin1) n ...(cong (\thin => drop thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
~~ keep (thin3 . thin2) n . drop thin1 n ..<(compRightDrop (thin3 . thin2) thin1 n)
~~ (keep thin3 n . keep thin2 n) . drop thin1 n ..<(cong (. drop thin1 n) $ compKeep thin3 thin2 n)
compAssoc' (Keep thin3 n) (Keep thin2 n) (Keep thin1 n) = Calc $
|~ keep thin3 n . (keep thin2 n . keep thin1 n)
~~ keep thin3 n . keep (thin2 . thin1) n ...(cong (keep thin3 n .) $ compKeep thin2 thin1 n)
~~ keep (thin3 . (thin2 . thin1)) n ...(compKeep thin3 (thin2 . thin1) n)
~~ keep ((thin3 . thin2) . thin1) n ...(cong (\thin => keep thin n) $ compAssoc' (view thin3) (view thin2) (view thin1))
~~ keep (thin3 . thin2) n . keep thin1 n ..<(compKeep (thin3 . thin2) thin1 n)
~~ (keep thin3 n . keep thin2 n) . keep thin1 n ..<(cong (. keep thin1 n) $ compKeep thin3 thin2 n)
export
compAssoc :
(thin3 : sz `Thins` sw) ->
(thin2 : sy `Thins` sz) ->
(thin1 : sx `Thins` sy) ->
thin3 . (thin2 . thin1) = (thin3 . thin2) . thin1
compAssoc thin3 thin2 thin1 = compAssoc' (view thin3) (view thin2) (view thin1)
-- Non-Identities
export
compPresNotId : IsNotId thin2 -> IsNotId thin1 -> IsNotId (thin2 . thin1)
compPresNotId ItIsThinner ItIsThinner = ItIsThinner
|
