blob: ecc3f47e541f5c3a4bb61ad18b69ddc7b77d82ac (
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
|
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
-- Operations ------------------------------------------------------------------
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)
-- Composition Properties ------------------------------------------------------
-- 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)
|
