blob: 791151d13c7fff88c7dfa75b4aadefb1f10c8f86 (
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
|
module Core.Var
import Core.Context
import Core.Thinning
%prefix_record_projections off
-- Variables -------------------------------------------------------------------
data IsVar : Nat -> Context -> Type where
Here : IsVar 0 (sx :< n)
There : IsVar k sx -> IsVar (S k) (sx :< n)
export
record Var (sx : Context) where
constructor MakeVar
index : Nat
0 prf : IsVar index sx
%name IsVar prf
%name Var i, j, k
-- Constructors ----------------------------------------------------------------
export
here : Var (sx :< n)
here = MakeVar 0 Here
export
there : Var sx -> Var (sx :< n)
there (MakeVar index prf) = MakeVar (S index) (There prf)
-- Views -----------------------------------------------------------------------
namespace View
public export
data View : Var sx -> Type where
Here : View Core.Var.here
There : (i : Var sx) -> View (there i)
%name View.View view
export
view : (i : Var sx) -> View i
view (MakeVar 0 Here) = Here
view (MakeVar (S k) (There prf)) = There (MakeVar k prf)
-- Views are Unique
viewInverse : {0 i : Var sx} -> View i -> Var sx
viewInverse Here = here
viewInverse (There i) = there i
viewInversePrf1 : (view : View i) -> viewInverse view = i
viewInversePrf1 Here = Refl
viewInversePrf1 (There i) = Refl
viewInversePrf2 :
{0 i : Var sx} ->
(v : View i) ->
view (viewInverse v) = (rewrite viewInversePrf1 v in v)
viewInversePrf2 Here = Refl
viewInversePrf2 (There (MakeVar index prf)) = Refl
export
viewUnique : {0 i : Var sx} -> (view1, view2 : View i) -> view1 = view2
viewUnique view1 view2 =
rewrite sym $ viewInversePrf2 view1 in
rewrite sym $ viewInversePrf2 view2 in
rewrite viewInversePrf1 view1 in
rewrite viewInversePrf1 view2 in
Refl
-- Weakening -------------------------------------------------------------------
doWkn : Var sx -> {0 thin : sx `Thins` sy} -> View thin -> Var sy
doWkn' : {0 i : Var (sx :< n)} -> View i -> sx `Thins` sy -> Var (sy :< n)
doWkn i (Id sy) = i
doWkn i (Drop thin n) = there $ doWkn i (view thin)
doWkn i (Keep thin n) = doWkn' (view i) thin
doWkn' Here thin = here
doWkn' (There i) thin = there $ doWkn i (view thin)
export
wkn : Var sx -> sx `Thins` sy -> Var sy
wkn i thin = doWkn i (view thin)
-- Is Homomorphic
export
doWknHomo :
(i : Var sx) ->
{thin1 : sx `Thins` sy} ->
{thin2 : sy `Thins` sz} ->
(view1 : View thin1) ->
(view2 : View thin2) ->
doWkn (doWkn i view1) view2 = wkn i (thin2 . thin1)
doWknHomo' :
{0 i : Var (sx :< n)} ->
(v : View i) ->
(thin1 : sx `Thins` sy) ->
(thin2 : sy `Thins` sz) ->
doWkn' (view $ doWkn' v thin1) thin2 = doWkn' v (thin2 . thin1)
doWknHomo i view1 (Id sz) =
rewrite compLeftIdentity thin1 in
cong (doWkn i) $ viewUnique view1 (view thin1)
doWknHomo i view1 (Drop thin2 n) =
rewrite compLeftDrop thin2 thin1 n in
rewrite
viewUnique
(view $ drop (thin2 . thin1) n)
(Drop (thin2 . thin1) n)
in
cong there $ doWknHomo i view1 (view thin2)
doWknHomo i (Id _) (Keep thin2 n) =
rewrite compRightIdentity $ keep thin2 n in
rewrite
viewUnique
(view $ keep thin2 n)
(Keep thin2 n)
in
Refl
doWknHomo i (Drop thin1 n) (Keep thin2 n) =
rewrite compRightDrop thin2 thin1 n in
rewrite
viewUnique
(view $ drop (thin2 . thin1) n)
(Drop (thin2 . thin1) n)
in
rewrite
Var.viewUnique
(view $ there {n} $ doWkn i $ view thin1)
(There $ doWkn i $ view thin1)
in
cong there $ doWknHomo i (view thin1) (view thin2)
doWknHomo i (Keep {prf = prf1} thin1 n) (Keep {prf = prf2} thin2 n) =
rewrite compKeep thin2 thin1 n in
rewrite
viewUnique
(view $ keep (thin2 . thin1) n)
(Keep {prf = compPresNotId prf2 prf1} (thin2 . thin1) n)
in
doWknHomo' (view i) thin1 thin2
doWknHomo' Here thin1 thin2 = Refl
doWknHomo' (There i) thin1 thin2 =
rewrite
viewUnique
(view $ there {n} $ doWkn i $ view thin1)
(There $ doWkn i $ view thin1)
in
cong there $ doWknHomo i (view thin1) (view thin2)
export
wknHomo :
(i : Var sx) ->
(thin1 : sx `Thins` sy) ->
(thin2 : sy `Thins` sz) ->
wkn (wkn i thin1) thin2 = wkn i (thin2 . thin1)
wknHomo i thin1 thin2 = doWknHomo i (view thin1) (view thin2)
|
