Skip to content

Commit 69e6700

Browse files
kdxukdxu
committed
added type equality proof
1 parent 8cc08da commit 69e6700

File tree

3 files changed

+84
-24
lines changed

3 files changed

+84
-24
lines changed

‎infer.agda

Lines changed: 61 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,10 @@ mutual
1919
Σ[ m≤m'' ∈ m ≤ m'' ]
2020
Σ[ σ ∈ AListType m'' m' ]
2121
Σ[ τ ∈ Type m' ]
22-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
22+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
23+
erase w ≡ s)
2324
infer m Γ (Var x) = infer-Var m Γ x
24-
infer m Γ (Lam s) = infer-Lam m Γ s
25+
infer m Γ (Lam s) = infer-Lam m Γ s
2526
infer m Γ (App s1 s2) = infer-App m Γ s1 s2
2627
infer m Γ (Fst s) = infer-Fst m Γ s
2728
infer m Γ (Snd s) = infer-Snd m Γ s
@@ -33,30 +34,34 @@ mutual
3334
Σ[ m≤m'' ∈ m ≤ m'' ]
3435
Σ[ σ ∈ AListType m'' m' ]
3536
Σ[ τ ∈ Type m' ]
36-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
37-
infer-Var m Γ x = just (m , m , m≤m m , anil , τ , VarX)
37+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
38+
erase w ≡ Var x)
39+
infer-Var m Γ x = just (m , m , m≤m m , anil , τ , VarX , eq)
3840
where
3941
τ : Type m
4042
τ = lookup x Γ
4143
VarX : WellTypedTerm (substCxt≤ anil (m≤m m) Γ) τ
4244
VarX rewrite substCxt≤Anil Γ (m≤m m) = Var x
45+
eq : erase VarX ≡ Var x
46+
eq rewrite substCxt≤Anil Γ (m≤m m) = refl
4347

4448
infer-Lam : (m : ℕ) → {n : ℕ} → (Γ : Cxt {m} n) → (s : WellScopedTerm (suc n)) →
4549
Maybe (Σ[ m'' ∈ ℕ ]
4650
Σ[ m' ∈ ℕ ]
4751
Σ[ m≤m'' ∈ m ≤ m'' ]
4852
Σ[ σ ∈ AListType m'' m' ]
4953
Σ[ τ ∈ Type m' ]
50-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
54+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
55+
erase w ≡ Lam s)
5156
infer-Lam m {n} Γ s
5257
with let tx : Type (suc m)
5358
tx = TVar (fromℕ m) -- new type variable
5459
Γ' : Cxt {suc m} n
5560
Γ' = liftCxt 1 Γ
5661
in infer (suc m) (tx ∷ Γ') s
5762
... | nothing = nothing
58-
... | just (m'' , m' , 1+m≤m'' , σ , τ , w) =
59-
just (m'' , m' , m≤m'' , σ , tx' ⇒ τ , LamW)
63+
... | just (m'' , m' , 1+m≤m'' , σ , τ , w , eraseW≡S) =
64+
just (m'' , m' , m≤m'' , σ , tx' ⇒ τ , LamW , eraseLamW≡LamS)
6065
where
6166
tx : Type (suc m) -- the same as above
6267
tx = TVar (fromℕ m)
@@ -70,31 +75,34 @@ mutual
7075
σΓ'≡σΓ = substCxt≤+1 Γ 1+m≤m'' m≤m'' σ
7176
LamW : WellTypedTerm (substCxt≤ σ m≤m'' Γ) (tx' ⇒ τ)
7277
LamW rewrite sym σΓ'≡σΓ = Lam tx' w
78+
eraseLamW≡LamS : erase LamW ≡ Lam s
79+
eraseLamW≡LamS rewrite sym σΓ'≡σΓ = cong Lam eraseW≡S
7380

7481
infer-App : (m : ℕ) → {n : ℕ} → (Γ : Cxt {m} n) → (s1 s2 : WellScopedTerm n) →
7582
Maybe (Σ[ m'' ∈ ℕ ]
7683
Σ[ m' ∈ ℕ ]
7784
Σ[ m≤m'' ∈ m ≤ m'' ]
7885
Σ[ σ ∈ AListType m'' m' ]
7986
Σ[ τ ∈ Type m' ]
80-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
87+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
88+
erase w ≡ App s1 s2)
8189
infer-App m {n} Γ s1 s2
8290
with infer m Γ s1
8391
... | nothing = nothing
84-
... | just (m1'' , m1' , m≤m1'' , σ1 , t1 , w1)
92+
... | just (m1'' , m1' , m≤m1'' , σ1 , t1 , w1 , eraseW1≡S1)
8593
with let σ1Γ : Cxt {m1'} n
8694
σ1Γ = substCxt≤ σ1 m≤m1'' Γ
8795
in infer m1' σ1Γ s2
8896
... | nothing = nothing
89-
... | just (m2'' , m2' , m1'≤m2'' , σ2 , t2 , w2)
97+
... | just (m2'' , m2' , m1'≤m2'' , σ2 , t2 , w2 , eraseW2≡S2)
9098
with let t : Type (suc m2')
9199
t = TVar (fromℕ m2') -- new type variable
92100
σ2t1 : Type m2'
93101
σ2t1 = substType≤ σ2 m1'≤m2'' t1
94102
in mgu2 (liftType≤ (n≤m+n 1 m2') σ2t1) (liftType≤ (n≤m+n 1 m2') t2 ⇒ t)
95103
... | nothing = nothing
96104
... | just (m3' , σ3 , σ3σ2t1≡σ3t2⇒σ3t) =
97-
just (m3'' , m3' , m≤m3'' , σ , σ3t , AppW1W2)
105+
just (m3'' , m3' , m≤m3'' , σ , σ3t , AppW1W2 , eraseAppW1W2≡AppS1S2)
98106
where
99107
m3'' : ℕ
100108
m3'' = suc m2' ∸ m2' + (m2'' ∸ m1' + m1'')
@@ -142,8 +150,10 @@ mutual
142150
σ2t1 = substType≤ σ2 m1'≤m2'' t1
143151
σ3σ2t1 : Type m3'
144152
σ3σ2t1 = substType≤ σ3 (n≤m+n 1 m2') σ2t1
153+
σ2w1 : WellTypedTerm σ2σ1Γ σ2t1
154+
σ2w1 = substWTerm≤ σ2 m1'≤m2'' w1
145155
σ3σ2w1 : WellTypedTerm σ3σ2σ1Γ σ3σ2t1
146-
σ3σ2w1 = substWTerm≤ σ3 (n≤m+n 1 m2') (substWTerm≤ σ2 m1'≤m2'' w1)
156+
σ3σ2w1 = substWTerm≤ σ3 (n≤m+n 1 m2') σ2w1
147157
-- w2
148158
σ3t2 : Type m3'
149159
σ3t2 = substType≤ σ3 (n≤m+n 1 m2') t2
@@ -163,26 +173,35 @@ mutual
163173
W2 rewrite σΓ≡σ3σ2σ1Γ = σ3w2
164174
AppW1W2 : WellTypedTerm σΓ σ3t
165175
AppW1W2 = App W1 W2
176+
-- erase
177+
eraseAppW1W2≡AppS1S2 : erase AppW1W2 ≡ App s1 s2
178+
eraseAppW1W2≡AppS1S2
179+
rewrite σΓ≡σ3σ2σ1Γ | σ3t2⇒σ3t≡σ3σ2t1
180+
| eraseSubstWTerm≤ σ3 (n≤m+n 1 m2') σ2w1
181+
| eraseSubstWTerm≤ σ2 m1'≤m2'' w1
182+
| eraseSubstWTerm≤ σ3 (n≤m+n 1 m2') w2 =
183+
cong₂ App eraseW1≡S1 eraseW2≡S2
166184

167185
infer-Fst : (m : ℕ) → {n : ℕ} → (Γ : Cxt {m} n) → (s : WellScopedTerm n) →
168186
Maybe (Σ[ m'' ∈ ℕ ]
169187
Σ[ m' ∈ ℕ ]
170188
Σ[ m≤m'' ∈ m ≤ m'' ]
171189
Σ[ σ ∈ AListType m'' m' ]
172190
Σ[ τ ∈ Type m' ]
173-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
191+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
192+
erase w ≡ Fst s)
174193
infer-Fst m {n} Γ s
175194
with infer m Γ s
176195
... | nothing = nothing
177-
... | just (m1'' , m1' , m≤m1'' , σ1 , t , w)
196+
... | just (m1'' , m1' , m≤m1'' , σ1 , t , w , eraseW≡S)
178197
with let t1 : Type (suc (suc m1')) -- new type variable
179198
t1 = liftType≤ (n≤m+n 1 (suc m1')) (TVar (fromℕ m1'))
180199
t2 : Type (suc (suc m1')) -- new type variable
181200
t2 = TVar (fromℕ (suc m1'))
182201
in mgu2 (liftType≤ (n≤m+n 2 m1') t) (t1 ∏ t2)
183202
... | nothing = nothing
184203
... | just (m2' , σ2 , σ2t≡σ2t1∏σ2t2) =
185-
just (m2'' , m2' , m≤m2'' , σ , σ2t1 , FstW)
204+
just (m2'' , m2' , m≤m2'' , σ , σ2t1 , FstW , eraseFstW≡FstS)
186205
where
187206
m2'' : ℕ
188207
m2'' = suc (suc m1') ∸ m1' + m1''
@@ -228,26 +247,33 @@ mutual
228247
W rewrite σΓ≡σ2σ1Γ | σ2t1∏σ2t2'≡σ2t = σ2w
229248
FstW : WellTypedTerm σΓ σ2t1
230249
FstW = Fst W
250+
-- erase
251+
eraseFstW≡FstS : erase FstW ≡ Fst s
252+
eraseFstW≡FstS
253+
rewrite σΓ≡σ2σ1Γ | σ2t1∏σ2t2'≡σ2t
254+
| eraseSubstWTerm≤ σ2 (n≤m+n 2 m1') w =
255+
cong Fst eraseW≡S
231256

232257
infer-Snd : (m : ℕ) → {n : ℕ} → (Γ : Cxt {m} n) → (s : WellScopedTerm n) →
233258
Maybe (Σ[ m'' ∈ ℕ ]
234259
Σ[ m' ∈ ℕ ]
235260
Σ[ m≤m'' ∈ m ≤ m'' ]
236261
Σ[ σ ∈ AListType m'' m' ]
237262
Σ[ τ ∈ Type m' ]
238-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
263+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
264+
erase w ≡ Snd s)
239265
infer-Snd m {n} Γ s
240266
with infer m Γ s
241267
... | nothing = nothing
242-
... | just (m1'' , m1' , m≤m1'' , σ1 , t , w)
268+
... | just (m1'' , m1' , m≤m1'' , σ1 , t , w , eraseW≡S)
243269
with let t1 : Type (suc (suc m1')) -- new type variable
244270
t1 = liftType≤ (n≤m+n 1 (suc m1')) (TVar (fromℕ m1'))
245271
t2 : Type (suc (suc m1')) -- new type variable
246272
t2 = TVar (fromℕ (suc m1'))
247273
in mgu2 (liftType≤ (n≤m+n 2 m1') t) (t1 ∏ t2)
248274
... | nothing = nothing
249275
... | just (m2' , σ2 , σ2t≡σ2t1∏σ2t2) =
250-
just (m2'' , m2' , m≤m2'' , σ , σ2t2 , SndW)
276+
just (m2'' , m2' , m≤m2'' , σ , σ2t2 , SndW , eraseSndW≡SndS)
251277
where
252278
m2'' : ℕ
253279
m2'' = suc (suc m1') ∸ m1' + m1''
@@ -293,24 +319,31 @@ mutual
293319
W rewrite σΓ≡σ2σ1Γ | σ2t1∏σ2t2'≡σ2t = σ2w
294320
SndW : WellTypedTerm σΓ σ2t2
295321
SndW = Snd W
322+
-- erase
323+
eraseSndW≡SndS : erase SndW ≡ Snd s
324+
eraseSndW≡SndS
325+
rewrite σΓ≡σ2σ1Γ | σ2t1∏σ2t2'≡σ2t
326+
| eraseSubstWTerm≤ σ2 (n≤m+n 2 m1') w =
327+
cong Snd eraseW≡S
296328

297329
infer-Cons : (m : ℕ) → {n : ℕ} → (Γ : Cxt {m} n) → (s1 s2 : WellScopedTerm n) →
298330
Maybe (Σ[ m'' ∈ ℕ ]
299331
Σ[ m' ∈ ℕ ]
300332
Σ[ m≤m'' ∈ m ≤ m'' ]
301333
Σ[ σ ∈ AListType m'' m' ]
302334
Σ[ τ ∈ Type m' ]
303-
WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ)
335+
Σ[ w ∈ WellTypedTerm (substCxt≤ σ m≤m'' Γ) τ ]
336+
erase w ≡ Cons s1 s2)
304337
infer-Cons m {n} Γ s1 s2
305338
with infer m Γ s1
306339
... | nothing = nothing
307-
... | just (m1'' , m1' , m≤m1'' , σ1 , t1 , w1)
340+
... | just (m1'' , m1' , m≤m1'' , σ1 , t1 , w1 , eraseW1≡S1)
308341
with let σ1Γ : Cxt {m1'} n
309342
σ1Γ = substCxt≤ σ1 m≤m1'' Γ
310343
in infer m1' σ1Γ s2
311344
... | nothing = nothing
312-
... | just (m2'' , m2' , m1'≤m2'' , σ2 , t2 , w2) =
313-
just (m2'' ∸ m1' + m1'' , m2' , m≤m2''∸m1'+m1'' , σ , τ , ConsW1W2)
345+
... | just (m2'' , m2' , m1'≤m2'' , σ2 , t2 , w2 , eraseW2≡S2) =
346+
just (m2'' ∸ m1' + m1'' , m2' , m≤m2''∸m1'+m1'' , σ , τ , ConsW1W2 , eraseConsW1W2≡ConsS1S2)
314347
where
315348
m≤m2''∸m1'+m1'' : m ≤ m2'' ∸ m1' + m1''
316349
m≤m2''∸m1'+m1'' =
@@ -350,3 +383,9 @@ mutual
350383
τ = σ2t1 ∏ t2
351384
ConsW1W2 : WellTypedTerm σΓ τ
352385
ConsW1W2 = Cons W1 W2
386+
-- erase
387+
eraseConsW1W2≡ConsS1S2 : erase ConsW1W2 ≡ Cons s1 s2
388+
eraseConsW1W2≡ConsS1S2
389+
rewrite σΓ≡σ2σ1Γ
390+
| eraseSubstWTerm≤ σ2 m1'≤m2'' w1
391+
= cong₂ Cons eraseW1≡S1 eraseW2≡S2

‎term.agda

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -172,7 +172,6 @@ data WellScopedTerm (n : ℕ) : Set where
172172
Snd : WellScopedTerm n → WellScopedTerm n
173173
Cons : WellScopedTerm n → WellScopedTerm n → WellScopedTerm n
174174

175-
176175
-- WellTypedTerm Γ t : 自由変数の数が n 個、型が t であるような well-typed な項
177176
data WellTypedTerm {m n : ℕ} (Γ : Cxt n) : Type m → Set where
178177
Var : (x : Fin n) → WellTypedTerm Γ (lookup x Γ)
@@ -184,6 +183,15 @@ data WellTypedTerm {m n : ℕ} (Γ : Cxt n) : Type m → Set where
184183
Snd : {t1 t2 : Type m} → WellTypedTerm Γ (t1 ∏ t2) → WellTypedTerm Γ t2
185184
Cons : {t1 t2 : Type m} → WellTypedTerm Γ t1 → WellTypedTerm Γ t2 → WellTypedTerm Γ (t1 ∏ t2)
186185

186+
-- WellTypedTerm から型情報を取り除く
187+
erase : {m n : ℕ} → {t : Type m} → {Γ : Cxt n} → WellTypedTerm Γ t → WellScopedTerm n
188+
erase (Var x) = Var x
189+
erase (Lam t w) = Lam (erase w)
190+
erase (App w1 w2) = App (erase w1) (erase w2)
191+
erase (Fst w) = Fst (erase w)
192+
erase (Snd w) = Snd (erase w)
193+
erase (Cons w1 w2) = Cons (erase w1) (erase w2)
194+
187195
-- lookup と liftCxt は順番を変えても良い
188196
lookupLiftCxtCommute : (m' : ℕ) {n m : ℕ} (x : Fin n) (Γ : Cxt {m} n) →
189197
liftType m' (lookup x Γ) ≡ lookup x (liftCxt m' Γ)
@@ -220,6 +228,19 @@ substWTerm≤ σ m≤m' (Fst w) = Fst (substWTerm≤ σ m≤m' w)
220228
substWTerm≤ σ m≤m' (Snd w) = Snd (substWTerm≤ σ m≤m' w)
221229
substWTerm≤ σ m≤m' (Cons w1 w2) = Cons (substWTerm≤ σ m≤m' w1) (substWTerm≤ σ m≤m' w2)
222230

231+
-- substWTerm≤ しても erase 結果は変わらない
232+
eraseSubstWTerm≤ : {m m' m'' n : ℕ} → {t : Type m} → {Γ : Cxt {m} n}
233+
→ (σ : AListType m' m'')
234+
→ (leq : m ≤ m')
235+
→ (w : WellTypedTerm Γ t)
236+
→ erase (substWTerm≤ σ leq w) ≡ erase w
237+
eraseSubstWTerm≤ {Γ = Γ} σ leq (Var x) rewrite lookupSubst≤CxtCommute x Γ σ leq = refl
238+
eraseSubstWTerm≤ σ leq (Lam t w) = cong Lam (eraseSubstWTerm≤ σ leq w)
239+
eraseSubstWTerm≤ σ leq (App w1 w2) = cong₂ App (eraseSubstWTerm≤ σ leq w1) (eraseSubstWTerm≤ σ leq w2)
240+
eraseSubstWTerm≤ σ leq (Fst w) = cong Fst (eraseSubstWTerm≤ σ leq w)
241+
eraseSubstWTerm≤ σ leq (Snd w) = cong Snd (eraseSubstWTerm≤ σ leq w)
242+
eraseSubstWTerm≤ σ leq (Cons w1 w2) = cong₂ Cons (eraseSubstWTerm≤ σ leq w1) (eraseSubstWTerm≤ σ leq w2)
243+
223244
thickxynothing : {m : ℕ} → {x y : Fin (suc m)} →
224245
thick x y ≡ nothing → thick (inject₁ x) (inject₁ y) ≡ nothing
225246
thickxynothing {x = zero} {zero} eq = refl

‎test.agda

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ open import Relation.Binary hiding (_⇒_)
2020
------------------------------------
2121
-- for test
2222

23-
Var1 : WellScopedTerm 2
23+
Var1 : WellScopedTerm 1
2424
Var1 = Var (fromℕ 0)
2525

2626
CxtE : {m : ℕ} → Cxt {m} 1

0 commit comments

Comments
 (0)