-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathlemmas-subst-satisfy.agda
355 lines (348 loc) · 16.2 KB
/
lemmas-subst-satisfy.agda
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
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
open import Nat
open import Prelude
open import constraints-core
open import core
open import dynamics-core
open import lemmas-satisfy
open import lemmas-subst-value
open import result-judgements
open import satisfy-decidable
open import statics-core
-- a given satisfaction judgement still holds
-- after substituting a variable in the expression
module lemmas-subst-satisfy where
subst-sat : ∀{x e1 e2 ξ} →
e1 ⊧̇ ξ →
([ e2 / x ] e1) ⊧̇ ξ
subst-sat CSTruth = CSTruth
subst-sat CSNum = CSNum
subst-sat (CSInl sat) = CSInl (subst-sat sat)
subst-sat (CSInr sat) = CSInr (subst-sat sat)
subst-sat (CSPair sat1 sat2) =
CSPair (subst-sat sat1) (subst-sat sat2)
subst-sat (CSNotIntroPair ni sat1 sat2) =
CSNotIntroPair (subst-notintro ni)
(subst-sat sat1) (subst-sat sat2)
subst-sat (CSOrL sat) = CSOrL (subst-sat sat)
subst-sat (CSOrR sat) = CSOrR (subst-sat sat)
final-sat-subst : ∀{x e1 e2 ξ} →
e1 final →
([ e2 / x ] e1) ⊧̇ ξ →
e1 ⊧̇ ξ
final-sat-subst (FVal VUnit) sat = sat
final-sat-subst (FVal VNum) sat = sat
final-sat-subst {x = x} (FVal (VLam {x = y})) sat
with nat-dec y x
... | Inl refl = sat
... | Inr y≠x = lam-sat-all-sat sat
final-sat-subst (FVal (VInl eval)) CSTruth = CSTruth
final-sat-subst (FVal (VInl eval)) (CSInl sat) =
CSInl (final-sat-subst (FVal eval) sat)
final-sat-subst (FVal (VInl eval)) (CSOrL sat) =
CSOrL (final-sat-subst (FVal (VInl eval)) sat)
final-sat-subst (FVal (VInl eval)) (CSOrR sat) =
CSOrR (final-sat-subst (FVal (VInl eval)) sat)
final-sat-subst (FVal (VInr eval)) CSTruth = CSTruth
final-sat-subst (FVal (VInr eval)) (CSInr sat) =
CSInr (final-sat-subst (FVal eval) sat)
final-sat-subst (FVal (VInr eval)) (CSOrL sat) =
CSOrL (final-sat-subst (FVal (VInr eval)) sat)
final-sat-subst (FVal (VInr eval)) (CSOrR sat) =
CSOrR (final-sat-subst (FVal (VInr eval)) sat)
final-sat-subst (FVal (VPair eval1 eval2)) CSTruth = CSTruth
final-sat-subst (FVal (VPair eval1 eval2)) (CSPair sat1 sat2) =
CSPair (final-sat-subst (FVal eval1) sat1)
(final-sat-subst (FVal eval2) sat2)
final-sat-subst (FVal (VPair eval1 eval2)) (CSOrL sat) =
CSOrL (final-sat-subst (FVal (VPair eval1 eval2)) sat)
final-sat-subst (FVal (VPair eval1 eval2)) (CSOrR sat) =
CSOrR (final-sat-subst (FVal (VPair eval1 eval2)) sat)
final-sat-subst (FIndet (IAp ind1 fin2)) sat =
all-notintro-sat NVAp sat NVAp
final-sat-subst (FIndet (IInl ind)) CSTruth = CSTruth
final-sat-subst (FIndet (IInl ind)) (CSInl sat) =
CSInl (final-sat-subst (FIndet ind) sat)
final-sat-subst (FIndet (IInl ind)) (CSOrL sat) =
CSOrL (final-sat-subst (FIndet (IInl ind)) sat)
final-sat-subst (FIndet (IInl ind)) (CSOrR sat) =
CSOrR (final-sat-subst (FIndet (IInl ind)) sat)
final-sat-subst (FIndet (IInr ind)) CSTruth = CSTruth
final-sat-subst (FIndet (IInr ind)) (CSInr sat) =
CSInr (final-sat-subst (FIndet ind) sat)
final-sat-subst (FIndet (IInr ind)) (CSOrL sat) =
CSOrL (final-sat-subst (FIndet (IInr ind)) sat)
final-sat-subst (FIndet (IInr ind)) (CSOrR sat) =
CSOrR (final-sat-subst (FIndet (IInr ind)) sat)
final-sat-subst (FIndet (IMatch fin mmatch)) sat =
all-notintro-sat NVMatch sat NVMatch
final-sat-subst (FIndet (IPairL ind1 val2)) CSTruth = CSTruth
final-sat-subst (FIndet (IPairL ind1 val2)) (CSPair sat1 sat2) =
CSPair (final-sat-subst (FIndet ind1) sat1)
(final-sat-subst (FVal val2) sat2)
final-sat-subst (FIndet (IPairL ind1 val2)) (CSOrL sat) =
CSOrL (final-sat-subst (FIndet (IPairL ind1 val2)) sat)
final-sat-subst (FIndet (IPairL ind1 val2)) (CSOrR sat) =
CSOrR (final-sat-subst (FIndet (IPairL ind1 val2)) sat)
final-sat-subst (FIndet (IPairR val1 ind2)) CSTruth = CSTruth
final-sat-subst (FIndet (IPairR val1 ind2)) (CSPair sat1 sat2) =
CSPair (final-sat-subst (FVal val1) sat1)
(final-sat-subst (FIndet ind2) sat2)
final-sat-subst (FIndet (IPairR val1 ind2)) (CSOrL sat) =
CSOrL (final-sat-subst (FIndet (IPairR val1 ind2)) sat)
final-sat-subst (FIndet (IPairR val1 ind2)) (CSOrR sat) =
CSOrR (final-sat-subst (FIndet (IPairR val1 ind2)) sat)
final-sat-subst (FIndet (IPair ind1 ind2)) CSTruth = CSTruth
final-sat-subst (FIndet (IPair ind1 ind2)) (CSPair sat1 sat2) =
CSPair (final-sat-subst (FIndet ind1) sat1)
(final-sat-subst (FIndet ind2) sat2)
final-sat-subst (FIndet (IPair ind1 ind2)) (CSOrL sat) =
CSOrL (final-sat-subst (FIndet (IPair ind1 ind2)) sat)
final-sat-subst (FIndet (IPair ind1 ind2)) (CSOrR sat) =
CSOrR (final-sat-subst (FIndet (IPair ind1 ind2)) sat)
final-sat-subst (FIndet (IFst npr ind)) sat =
all-notintro-sat NVFst sat NVFst
final-sat-subst (FIndet (ISnd npr ind)) sat =
all-notintro-sat NVSnd sat NVSnd
final-sat-subst (FIndet IEHole) sat =
all-notintro-sat NVEHole sat NVEHole
final-sat-subst (FIndet (IHole ind)) sat =
all-notintro-sat NVHole sat NVHole
final-subst-maysat : ∀{x e1 e2 ξ} →
e1 final →
e1 ⊧̇? ξ →
([ e2 / x ] e1) ⊧̇? ξ
final-subst-maysat fin CMSUnknown = CMSUnknown
final-subst-maysat fin (CMSInl msat) =
CMSInl (final-subst-maysat (inl-final fin) msat)
final-subst-maysat fin (CMSInr msat) =
CMSInr (final-subst-maysat (inr-final fin) msat)
final-subst-maysat fin (CMSPairL msat1 sat2) =
CMSPairL (final-subst-maysat (π1 (pair-final fin)) msat1)
(subst-sat sat2)
final-subst-maysat fin (CMSPairR sat1 msat2) =
CMSPairR (subst-sat sat1)
(final-subst-maysat (π2 (pair-final fin)) msat2)
final-subst-maysat fin (CMSPair msat1 msat2) =
CMSPair (final-subst-maysat (π1 (pair-final fin)) msat1)
(final-subst-maysat (π2 (pair-final fin)) msat2)
final-subst-maysat fin (CMSOrL msat1 ¬sat2) =
CMSOrL (final-subst-maysat fin msat1)
(λ{ssat2 → ¬sat2 (final-sat-subst fin ssat2)})
final-subst-maysat fin (CMSOrR ¬sat1 msat2) =
CMSOrR (λ{ssat1 → ¬sat1 (final-sat-subst fin ssat1)})
(final-subst-maysat fin msat2)
final-subst-maysat fin (CMSNotIntro ni ref pos) =
CMSNotIntro (subst-notintro ni) ref pos
final-maysat-subst : ∀{x e1 e2 ξ} →
e1 final →
([ e2 / x ] e1) ⊧̇? ξ →
e1 ⊧̇? ξ
final-maysat-subst (FVal VUnit) msat = msat
final-maysat-subst (FVal VNum) msat = msat
final-maysat-subst {x = x} (FVal (VLam {x = y})) msat
with nat-dec y x
... | Inl refl = all-lam-maysat msat
... | Inr y≠x = all-lam-maysat msat
final-maysat-subst (FVal (VInl eval)) CMSUnknown = CMSUnknown
final-maysat-subst (FVal (VInl eval)) (CMSInl msat) =
CMSInl (final-maysat-subst (FVal eval) msat)
final-maysat-subst (FVal (VInl eval)) (CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FVal (VInl eval)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FVal (VInl eval)) (CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FVal (VInl eval)) msat2)
final-maysat-subst (FVal (VInr eval)) CMSUnknown = CMSUnknown
final-maysat-subst (FVal (VInr eval)) (CMSInr msat) =
CMSInr (final-maysat-subst (FVal eval) msat)
final-maysat-subst (FVal (VInr eval)) (CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FVal (VInr eval)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FVal (VInr eval)) (CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FVal (VInr eval)) msat2)
final-maysat-subst (FVal (VPair eval1 eval2)) CMSUnknown =
CMSUnknown
final-maysat-subst (FVal (VPair eval1 eval2))
(CMSPairL msat1 sat2) =
CMSPairL (final-maysat-subst (FVal eval1) msat1)
(final-sat-subst (FVal eval2) sat2)
final-maysat-subst (FVal (VPair eval1 eval2))
(CMSPairR sat1 msat2) =
CMSPairR (final-sat-subst (FVal eval1) sat1)
(final-maysat-subst (FVal eval2) msat2)
final-maysat-subst (FVal (VPair eval1 eval2))
(CMSPair msat1 msat2) =
CMSPair (final-maysat-subst (FVal eval1) msat1)
(final-maysat-subst (FVal eval2) msat2)
final-maysat-subst (FVal (VPair eval1 eval2))
(CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FVal (VPair eval1 eval2)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FVal (VPair eval1 eval2))
(CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FVal (VPair eval1 eval2)) msat2)
final-maysat-subst (FIndet (IAp ind1 fin2)) msat =
all-notintro-maysat NVAp msat NVAp
final-maysat-subst (FIndet (IInl ind)) CMSUnknown = CMSUnknown
final-maysat-subst (FIndet (IInl ind)) (CMSInl msat) =
CMSInl (final-maysat-subst (FIndet ind) msat)
final-maysat-subst (FIndet (IInl ind)) (CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FIndet (IInl ind)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FIndet (IInl ind)) (CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FIndet (IInl ind)) msat2)
final-maysat-subst (FIndet (IInr ind)) CMSUnknown = CMSUnknown
final-maysat-subst (FIndet (IInr ind)) (CMSInr sat) =
CMSInr (final-maysat-subst (FIndet ind) sat)
final-maysat-subst (FIndet (IInr ind)) (CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FIndet (IInr ind)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FIndet (IInr ind)) (CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FIndet (IInr ind)) msat2)
final-maysat-subst (FIndet (IMatch fin mmatch)) msat =
all-notintro-maysat NVMatch msat NVMatch
final-maysat-subst (FIndet (IPairL ind1 val2))
CMSUnknown = CMSUnknown
final-maysat-subst (FIndet (IPairL ind1 val2))
(CMSPairL msat1 sat2) =
CMSPairL (final-maysat-subst (FIndet ind1) msat1)
(final-sat-subst (FVal val2) sat2)
final-maysat-subst (FIndet (IPairL ind1 val2))
(CMSPairR sat1 msat2) =
CMSPairR (final-sat-subst (FIndet ind1) sat1)
(final-maysat-subst (FVal val2) msat2)
final-maysat-subst (FIndet (IPairL ind1 val2))
(CMSPair msat1 msat2) =
CMSPair (final-maysat-subst (FIndet ind1) msat1)
(final-maysat-subst (FVal val2) msat2)
final-maysat-subst (FIndet (IPairL ind1 val2))
(CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FIndet (IPairL ind1 val2)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FIndet (IPairL ind1 val2))
(CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FIndet (IPairL ind1 val2)) msat2)
final-maysat-subst (FIndet (IPairR val1 ind2))
CMSUnknown = CMSUnknown
final-maysat-subst (FIndet (IPairR val1 ind2))
(CMSPairL msat1 sat2) =
CMSPairL (final-maysat-subst (FVal val1) msat1)
(final-sat-subst (FIndet ind2) sat2)
final-maysat-subst (FIndet (IPairR val1 ind2))
(CMSPairR sat1 msat2) =
CMSPairR (final-sat-subst (FVal val1) sat1)
(final-maysat-subst (FIndet ind2) msat2)
final-maysat-subst (FIndet (IPairR val1 ind2))
(CMSPair msat1 msat2) =
CMSPair (final-maysat-subst (FVal val1) msat1)
(final-maysat-subst (FIndet ind2) msat2)
final-maysat-subst (FIndet (IPairR val1 ind2))
(CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FIndet (IPairR val1 ind2)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FIndet (IPairR val1 ind2))
(CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FIndet (IPairR val1 ind2)) msat2)
final-maysat-subst (FIndet (IPair ind1 ind2))
CMSUnknown = CMSUnknown
final-maysat-subst (FIndet (IPair ind1 ind2))
(CMSPairL msat1 sat2) =
CMSPairL (final-maysat-subst (FIndet ind1) msat1)
(final-sat-subst (FIndet ind2) sat2)
final-maysat-subst (FIndet (IPair ind1 ind2))
(CMSPairR sat1 msat2) =
CMSPairR (final-sat-subst (FIndet ind1) sat1)
(final-maysat-subst (FIndet ind2) msat2)
final-maysat-subst (FIndet (IPair ind1 ind2))
(CMSPair msat1 msat2) =
CMSPair (final-maysat-subst (FIndet ind1) msat1)
(final-maysat-subst (FIndet ind2) msat2)
final-maysat-subst (FIndet (IPair ind1 ind2))
(CMSOrL msat1 ¬sat2) =
CMSOrL (final-maysat-subst (FIndet (IPair ind1 ind2)) msat1)
(λ{sat2 → ¬sat2 (subst-sat sat2)})
final-maysat-subst (FIndet (IPair ind1 ind2))
(CMSOrR ¬sat1 msat2) =
CMSOrR (λ{sat1 → ¬sat1 (subst-sat sat1)})
(final-maysat-subst (FIndet (IPair ind1 ind2)) msat2)
final-maysat-subst (FIndet (IFst npr ind)) msat =
all-notintro-maysat NVFst msat NVFst
final-maysat-subst (FIndet (ISnd npr ind)) msat =
all-notintro-maysat NVSnd msat NVSnd
final-maysat-subst (FIndet IEHole) msat =
all-notintro-maysat NVEHole msat NVEHole
final-maysat-subst (FIndet (IHole fin)) msat =
all-notintro-maysat NVHole msat NVHole
-- replacing a variable may allow it to satisfy something
-- it previously did not
subst-maysat : ∀{x e1 e2 ξ} →
e1 ⊧̇? ξ →
([ e2 / x ] e1) ⊧̇†? ξ
subst-maysat CMSUnknown = CSMSMay CMSUnknown
subst-maysat (CMSInl msat)
with subst-maysat msat
... | CSMSSat ssat = CSMSSat (CSInl ssat)
... | CSMSMay smsat = CSMSMay (CMSInl smsat)
subst-maysat (CMSInr msat)
with subst-maysat msat
... | CSMSSat ssat = CSMSSat (CSInr ssat)
... | CSMSMay smsat = CSMSMay (CMSInr smsat)
subst-maysat (CMSPairL msat1 sat2)
with subst-maysat msat1
... | CSMSSat ssat1 =
CSMSSat (CSPair ssat1 (subst-sat sat2))
... | CSMSMay smsat1 =
CSMSMay (CMSPairL smsat1 (subst-sat sat2))
subst-maysat (CMSPairR sat1 msat2)
with subst-maysat msat2
... | CSMSSat ssat2 =
CSMSSat (CSPair (subst-sat sat1) ssat2)
... | CSMSMay smsat2 =
CSMSMay (CMSPairR (subst-sat sat1) smsat2)
subst-maysat (CMSPair msat1 msat2)
with subst-maysat msat1 | subst-maysat msat2
... | CSMSSat ssat1 | CSMSSat ssat2 =
CSMSSat (CSPair ssat1 ssat2)
... | CSMSSat ssat1 | CSMSMay smsat2 =
CSMSMay (CMSPairR ssat1 smsat2)
... | CSMSMay smsat1 | CSMSSat ssat2 =
CSMSMay (CMSPairL smsat1 ssat2)
... | CSMSMay smsat1 | CSMSMay smsat2 =
CSMSMay (CMSPair smsat1 smsat2)
subst-maysat {x = x} {e1 = e1} {e2 = e2} {ξ = ξ1 ∨ ξ2}
(CMSOrL msat1 ¬sat2)
with subst-maysat msat1
... | CSMSSat ssat1 = CSMSSat (CSOrL ssat1)
... | CSMSMay smsat1
with satisfy-dec ([ e2 / x ] e1) ξ2
... | Inl ssat2 = CSMSSat (CSOrR ssat2)
... | Inr ¬ssat2 = CSMSMay (CMSOrL smsat1 ¬ssat2)
subst-maysat {x = x} {e1 = e1} {e2 = e2} {ξ = ξ1 ∨ ξ2}
(CMSOrR ¬sat1 msat2)
with subst-maysat msat2
... | CSMSSat ssat2 = CSMSSat (CSOrR ssat2)
... | CSMSMay smsat2
with satisfy-dec ([ e2 / x ] e1) ξ1
... | Inl ssat1 = CSMSSat (CSOrL ssat1)
... | Inr ¬ssat1 = CSMSMay (CMSOrR ¬ssat1 smsat2)
subst-maysat (CMSNotIntro ni ref pos) =
CSMSMay (CMSNotIntro (subst-notintro ni) ref pos)
subst-satormay : ∀{x e1 e2 ξ} →
e1 ⊧̇†? ξ →
([ e2 / x ] e1) ⊧̇†? ξ
subst-satormay (CSMSSat sat) = CSMSSat (subst-sat sat)
subst-satormay (CSMSMay msat) = subst-maysat msat
final-satormay-subst : ∀{x e1 e2 ξ} →
e1 final →
([ e2 / x ] e1) ⊧̇†? ξ →
e1 ⊧̇†? ξ
final-satormay-subst fin (CSMSSat sat) =
CSMSSat (final-sat-subst fin sat)
final-satormay-subst fin (CSMSMay msat) =
CSMSMay (final-maysat-subst fin msat)