/
structural.agda
235 lines (216 loc) · 13 KB
/
structural.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
open import Nat
open import Prelude
open import core
open import checks
open import judgemental-erase
module structural where
-- this module contains proofs that the judgements that mention contexts
-- defined throughout the work enjoy the standard structural properties
-- of contexts:
--
-- exchange
--
-- Γ, (x : t1), (y : t2) ⊢ A
-- -------------------------
-- Γ, (y : t2), (x : t1) ⊢ A
--
-- contraction
--
-- Γ, (x : t), (x : t) ⊢ A
-- -----------------------
-- Γ , (x : t) ⊢ A
--
-- weakening
--
-- Γ ⊢ A x # Γ
-- ----------------------
-- Γ , (x : t) ⊢ A
--
-- proofs of the first two are generally easier: viewed as finite
-- functions, the contexts on the top and bottom of both exchange answer
-- every question the same, so an appeal to function extensionality is
-- enough to treat them the same. weakening does not have this property,
-- and there requires some induction to demonstrate.
-- because of our choice to use barendrecht's convention, we need a quite
-- strong form of freshness of a variable for weakening. specifically, we
-- need to know not just that the variable we're using to extend the
-- context doesn't appear in the context, as in a standard presentation,
-- it can't appear anywhere in the term at all; it must be totally
-- fresh. it's possible to drop this requirement with alpha-renaming to
-- recover the standard description of these things, so we allow it here
-- for convenience.
fresh : Nat → ė → Set
fresh x (e ·: t) = fresh x e
fresh x (X y) = natEQp x y
fresh x (·λ y e) = natEQp x y × fresh x e
fresh x (N n) = ⊤
fresh x (e1 ·+ e2) = fresh x e1 × fresh x e2
fresh x ⦇-⦈ = ⊤
fresh x ⦇⌜ e ⌟⦈ = fresh x e
fresh x (e1 ∘ e2) = fresh x e1 × fresh x e2
---- lemmas
-- freshness interacts with erasure as you'd expect. the proofs below mix
-- and match between judgmental and functional erasure as usual, so this
-- is needed enough times to pull it out.
fresh-er-lem : ∀{ e e◆ x} → erase-e e e◆ → fresh x (e ◆e) → fresh x e◆
fresh-er-lem er f = tr (λ q → fresh _ q) ( ! (erasee-det er (rel◆ _))) f
--- a contracted context gives all the same responses as the
--- non-contracted context
lem-contract : (Γ : ·ctx) (x : Nat) (t : τ̇) (y : Nat) →
((Γ ,, (x , t)) ,, (x , t)) y == (Γ ,, (x , t)) y
lem-contract Γ x t y with natEQ x y
lem-contract Γ x t .x | Inl refl = refl
... | Inr qq with natEQ x y
... | Inl pp = abort (qq pp)
... | Inr pp = refl
--- an exchanged context gives all the same responses as the
--- non-exchanged context
lem-swap : (Γ : ·ctx) (x y : Nat) (t1 t2 : τ̇) {x≠y : x == y → ⊥} (z : Nat) →
((Γ ,, (x , t1)) ,, (y , t2)) z == ((Γ ,, (y , t2)) ,, (x , t1)) z
lem-swap Γ x y t1 t2 z with natEQ x z | natEQ y z
lem-swap Γ x y t1 t2 {x≠y} z | Inl p | Inl q = abort (x≠y (p · ! q))
lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ with natEQ x x
lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ | Inl refl = refl
lem-swap Γ x y t1 t2 .x | Inl refl | Inr x₂ | Inr x₁ = abort (x₁ refl)
lem-swap Γ x y t1 t2 .y | Inr x₁ | Inl refl with natEQ y y
lem-swap Γ x₁ y t1 t2 .y | Inr x₂ | Inl refl | Inl refl = refl
lem-swap Γ x₁ y t1 t2 .y | Inr x₂ | Inl refl | Inr x = abort (x refl)
lem-swap Γ x y t1 t2 z | Inr x₁ | Inr x₂ with natEQ x z | natEQ y z
lem-swap Γ x .x t1 t2 .x | Inr x₂ | Inr x₃ | Inl refl | Inl refl = abort (x₃ refl)
lem-swap Γ x y t1 t2 .x | Inr x₂ | Inr x₃ | Inl refl | Inr x₁ = abort (x₂ refl)
lem-swap Γ x y t1 t2 z | Inr x₃ | Inr x₄ | Inr x₁ | Inl x₂ = abort (x₄ x₂)
lem-swap Γ x y t1 t2 z | Inr x₃ | Inr x₄ | Inr x₁ | Inr x₂ = refl
-- extending a context with a new variable doesn't change anything under
lem-extend : ∀{n x Γ t w} →
(n == x → ⊥) → Γ n == w → (Γ ,, (x , t)) n == w
lem-extend {n} {x} neq w with natEQ x n
lem-extend neq w₁ | Inl refl = abort (neq refl)
lem-extend neq w₁ | Inr x₁ = w₁
---- structural properties for the well-typedness jugements
mutual
wt-exchange-synth : {Γ : ·ctx} {x y : Nat} {t1 t2 t : τ̇} {e : ė} →
{x≠y : x == y → ⊥} →
((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e => t →
((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e => t
wt-exchange-synth {Γ} {x} {y} {t1} {t2} {t} {e} {x≠y} d =
tr (λ q → q ⊢ e => t) (funext (lem-swap Γ x y t1 t2 {x≠y = x≠y})) d
wt-exchange-ana : {Γ : ·ctx} {x y : Nat} {t1 t2 t : τ̇} {e : ė} →
(x≠y : x == y → ⊥) →
((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e <= t →
((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e <= t
wt-exchange-ana {Γ} {x} {y} {t1} {t2} {t} {e} x≠y d =
tr (λ q → q ⊢ e <= t) (funext (lem-swap Γ x y t1 t2 {x≠y = x≠y})) d
mutual
wt-contract-synth : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
((Γ ,, (x , t')) ,, (x , t')) ⊢ e => t →
(Γ ,, (x , t')) ⊢ e => t
wt-contract-synth {Γ} {x} {t} {t'} {e} wt =
tr (λ q → q ⊢ e => t) (funext (lem-contract Γ x t')) wt
wt-contract-ana : (Γ : ·ctx) (x : Nat) (t t' : τ̇) (e : ė) →
((Γ ,, (x , t')) ,, (x , t')) ⊢ e <= t →
(Γ ,, (x , t')) ⊢ e <= t
wt-contract-ana Γ x t t' e wt =
tr (λ q → q ⊢ e <= t) (funext (lem-contract Γ x t')) wt
mutual
wt-weak-synth : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
x # Γ →
Γ ⊢ e => t →
fresh x e →
(Γ ,, (x , t')) ⊢ e => t
wt-weak-synth apt (SAsc x₁) f = SAsc (wt-weak-ana apt x₁ f)
wt-weak-synth {x = x} apt (SVar {n = n} x₁) f with natEQ n x
wt-weak-synth apt (SVar x₂) f | Inl refl = abort (somenotnone (! x₂ · apt))
wt-weak-synth apt (SVar x₂) f | Inr x₁ = SVar (lem-extend x₁ x₂)
wt-weak-synth apt (SAp wt x₁ x₂) (f1 , f2) = SAp (wt-weak-synth apt wt f1) x₁ (wt-weak-ana apt x₂ f2)
wt-weak-synth apt SNum f = SNum
wt-weak-synth apt (SPlus x₁ x₂) (f1 , f2) = SPlus (wt-weak-ana apt x₁ f1) (wt-weak-ana apt x₂ f2)
wt-weak-synth apt SEHole f = SEHole
wt-weak-synth apt (SNEHole wt) f = SNEHole (wt-weak-synth apt wt f)
wt-weak-ana : {Γ : ·ctx} {x : Nat} {t t' : τ̇} {e : ė} →
x # Γ →
Γ ⊢ e <= t →
fresh x e →
(Γ ,, (x , t')) ⊢ e <= t
wt-weak-ana apt (ASubsume x₁ x₂) f = ASubsume (wt-weak-synth apt x₁ f) x₂
wt-weak-ana {x = x} apt (ALam {x = x₁} x₂ x₃ wt) f with natEQ x x₁
wt-weak-ana apt (ALam x₃ x₄ wt) (f1 , _) | Inl refl = abort f1
wt-weak-ana apt (ALam x₃ m wt) (f1 , f2) | Inr x₂ = ALam (lem-extend (flip x₂) x₃) m (wt-exchange-ana (flip x₂) (wt-weak-ana (lem-extend x₂ apt) wt f2))
---- structural properties for the action jugements
mutual
act-exchange-synth : ∀{ Γ x y t1 t2 t t' e e' α } →
(x == y → ⊥) →
((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e => t ~ α ~> e' => t' →
((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e => t ~ α ~> e' => t'
act-exchange-synth {Γ} {x} {y} {t1} {t2} {t} {t'} {e} {e'} {α} x≠y d = tr (λ q → q ⊢ e => t ~ α ~> e' => t') (funext (lem-swap Γ x y t1 t2 {x≠y})) d
act-exchange-ana : ∀{ Γ x y t1 t2 t e e' α } →
(x == y → ⊥) →
((Γ ,, (x , t1)) ,, (y , t2)) ⊢ e ~ α ~> e' ⇐ t →
((Γ ,, (y , t2)) ,, (x , t1)) ⊢ e ~ α ~> e' ⇐ t
act-exchange-ana {Γ} {x} {y} {t1} {t2} {t} {e} {e'} {α} x≠y d = tr (λ q → q ⊢ e ~ α ~> e' ⇐ t) (funext (lem-swap Γ x y t1 t2 {x≠y})) d
mutual
act-contract-synth : ∀{ Γ x t t' t'' e e' α } →
((Γ ,, (x , t'')) ,, (x , t'')) ⊢ e => t ~ α ~> e' => t' →
(Γ ,, (x , t'')) ⊢ e => t ~ α ~> e' => t'
act-contract-synth {Γ} {x} {t} {t'} {t''} {e} {e'} {α} d = tr (λ q → q ⊢ e => t ~ α ~> e' => t') (funext (lem-contract Γ x t'')) d
act-contract-ana : ∀{ Γ x t t' e e' α } →
((Γ ,, (x , t')) ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t →
(Γ ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t
act-contract-ana {Γ} {x} {t} {t'} {e} {e'} {α} d = tr (λ q → q ⊢ e ~ α ~> e' ⇐ t) (funext (lem-contract Γ x t')) d
mutual
act-weak-synth : ∀{ Γ x t t' t'' e e' α } →
x # Γ →
fresh x (e ◆e) →
fresh x (e' ◆e) →
(d : Γ ⊢ e => t ~ α ~> e' => t') →
(Γ ,, (x , t'')) ⊢ e => t ~ α ~> e' => t'
act-weak-synth apt f f' (SAMove x₁) = SAMove x₁
act-weak-synth apt f f' SADel = SADel
act-weak-synth apt f f' SAConAsc = SAConAsc
act-weak-synth {x = x} apt f f' (SAConVar {x = y} p) with natEQ x y
act-weak-synth apt f f' (SAConVar p) | Inl refl = abort (somenotnone (! p · apt))
act-weak-synth apt f f' (SAConVar p) | Inr x₂ = SAConVar (lem-extend (flip x₂) p)
act-weak-synth {x = x} apt f f' (SAConLam {x = y} x₂) with natEQ x y
act-weak-synth apt f f' (SAConLam x₃) | Inl refl = abort (π1 f')
act-weak-synth apt f f' (SAConLam x₃) | Inr x₂ = SAConLam (lem-extend (flip x₂) x₃)
act-weak-synth apt f f' (SAConApArr x₁) = SAConApArr x₁
act-weak-synth apt f f' (SAConApOtw x₁) = SAConApOtw x₁
act-weak-synth apt f f' SAConNumlit = SAConNumlit
act-weak-synth apt f f' (SAConPlus1 x₁) = SAConPlus1 x₁
act-weak-synth apt f f' (SAConPlus2 x₁) = SAConPlus2 x₁
act-weak-synth apt f f' SAConNEHole = SAConNEHole
act-weak-synth apt f f' (SAFinish x₁) = SAFinish (wt-weak-synth apt x₁ f')
act-weak-synth apt f f' (SAZipAsc1 x₁) = SAZipAsc1 (act-weak-ana apt f f' x₁)
act-weak-synth apt f f' (SAZipAsc2 x₁ x₂ x₃ x₄) = SAZipAsc2 x₁ x₂ x₃ (wt-weak-ana apt x₄ f')
act-weak-synth apt f f' (SAZipApArr x₁ x₂ x₃ d x₄) = SAZipApArr x₁ x₂ (wt-weak-synth apt x₃ (fresh-er-lem x₂ (π1 f)))
(act-weak-synth apt (π1 f) (π1 f') d)
(wt-weak-ana apt x₄ (π2 f'))
act-weak-synth apt f f' (SAZipApAna x₁ x₂ x₃) = SAZipApAna x₁ (wt-weak-synth apt x₂ (π1 f'))
(act-weak-ana apt (π2 f) (π2 f') x₃)
act-weak-synth apt f f' (SAZipPlus1 x₁) = SAZipPlus1 (act-weak-ana apt (π1 f) (π1 f') x₁)
act-weak-synth apt f f' (SAZipPlus2 x₁) = SAZipPlus2 (act-weak-ana apt (π2 f) (π2 f') x₁)
act-weak-synth apt f f' (SAZipHole x₁ x₂ d) = SAZipHole x₁ (wt-weak-synth apt x₂ (fresh-er-lem x₁ f))
(act-weak-synth apt f f' d)
act-weak-ana : ∀{ Γ x t t' e e' α } →
x # Γ →
fresh x (e ◆e) →
fresh x (e' ◆e) →
(d : Γ ⊢ e ~ α ~> e' ⇐ t) →
(Γ ,, (x , t')) ⊢ e ~ α ~> e' ⇐ t
act-weak-ana apt f f' (AASubsume x₁ x₂ x₃ x₄) = AASubsume x₁ (wt-weak-synth apt x₂ (fresh-er-lem x₁ f)) (act-weak-synth apt f f' x₃) x₄
act-weak-ana apt f f' (AAMove x₁) = AAMove x₁
act-weak-ana apt f f' AADel = AADel
act-weak-ana apt f f' AAConAsc = AAConAsc
act-weak-ana {x = x} apt f f' (AAConVar {x = y} x₂ p) with natEQ x y
act-weak-ana apt f f' (AAConVar x₃ p) | Inl refl = abort (somenotnone (! p · apt))
act-weak-ana apt f f' (AAConVar x₃ p) | Inr x₂ = AAConVar x₃ (lem-extend (flip x₂) p)
act-weak-ana {x = x} apt f f' (AAConLam1 {x = y} x₂ x₃) with natEQ x y
act-weak-ana apt f f' (AAConLam1 x₃ x₄) | Inl refl = abort (π1 f')
act-weak-ana apt f f' (AAConLam1 x₃ x₄) | Inr x₂ = AAConLam1 (lem-extend (flip x₂) x₃) x₄
act-weak-ana {x = x} apt f f' (AAConLam2 {x = y} x₂ x₃) with natEQ x y
act-weak-ana apt f f' (AAConLam2 x₃ x₄) | Inl refl = abort (π1 f')
act-weak-ana apt f f' (AAConLam2 x₃ x₄) | Inr x₂ = AAConLam2 (lem-extend (flip x₂) x₃) x₄
act-weak-ana apt f f' (AAConNumlit x₁) = AAConNumlit x₁
act-weak-ana apt f f' (AAFinish x₁) = AAFinish (wt-weak-ana apt x₁ f')
act-weak-ana {x = x} apt f f' (AAZipLam {x = y} x₂ x₃ d) with natEQ x y
act-weak-ana apt f f' (AAZipLam x₃ x₄ d) | Inl refl = abort (π1 f')
act-weak-ana apt f f' (AAZipLam x₃ x₄ d) | Inr x₂ = AAZipLam (lem-extend (flip x₂) x₃) x₄ (act-exchange-ana (flip x₂) (act-weak-ana (lem-extend x₂ apt) (π2 f) (π2 f') d))