1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/lists/list.ma".
16 include "basics/deqsets.ma".
17 include "binding/names.ma".
18 include "binding/fp.ma".
20 definition alpha : Nset β X. check alpha
21 notation "πΈ" non associative with precedence 90 for @{'alphabet}.
22 interpretation "set of names" 'alphabet = alpha.
24 inductive tp : Type[0] β
26 | arr : tp β tp β tp.
27 inductive pretm : Type[0] β
29 | par : πΈ β pretm
30 | abs : tp β pretm β pretm
31 | app : pretm β pretm β pretm.
33 let rec Nth T n (l:list T) on n β
36 | cons hd tl β match n with
38 | S n0 β Nth T n0 tl ] ].
40 let rec vclose_tm_aux u x k β match u with
41 [ var n β if (leb k n) then var (S n) else u
42 | par x0 β if (x0 == x) then (var k) else u
43 | app v1 v2 β app (vclose_tm_aux v1 x k) (vclose_tm_aux v2 x k)
44 | abs s v β abs s (vclose_tm_aux v x (S k)) ].
45 definition vclose_tm β Ξ»u,x.vclose_tm_aux u x O.
47 definition vopen_var β Ξ»n,x,k.match eqb n k with
49 | false β match leb n k with
51 | false β var (pred n) ] ].
53 let rec vopen_tm_aux u x k β match u with
54 [ var n β vopen_var n x k
56 | app v1 v2 β app (vopen_tm_aux v1 x k) (vopen_tm_aux v2 x k)
57 | abs s v β abs s (vopen_tm_aux v x (S k)) ].
58 definition vopen_tm β Ξ»u,x.vopen_tm_aux u x O.
60 let rec FV u β match u with
62 | app v1 v2 β FV v1@FV v2
66 definition lam β Ξ»x,s,u.abs s (vclose_tm u x).
68 let rec Pi_map_tm p u on u β match u with
71 | app v1 v2 β app (Pi_map_tm p v1) (Pi_map_tm p v2)
72 | abs s v β abs s (Pi_map_tm p v) ].
74 interpretation "permutation of tm" 'middot p x = (Pi_map_tm p x).
76 notation "hvbox(uβxβ)"
81 notation "hvbox(uβxβ)"
84 notation "β΄ u β΅ x" non associative with precedence 90 for @{ 'open $u $x }.
86 interpretation "ln term variable open" 'open u x = (vopen_tm u x).
87 notation < "hvbox(Ξ½ x break . u)"
90 notation > "Ξ½ list1 x sep , . term 19 u" with precedence 20
91 for ${ fold right @{$u} rec acc @{'nu $x $acc)} }.
92 interpretation "ln term variable close" 'nu x u = (vclose_tm u x).
94 let rec tm_height u β match u with
95 [ app v1 v2 β S (max (tm_height v1) (tm_height v2))
96 | abs s v β S (tm_height v)
99 theorem le_n_O_rect_Type0 : βn:nat. n β€ O β βP: nat βType[0]. P O β P n.
100 #n (cases n) // #a #abs cases (?:False) /2/ qed.
102 theorem nat_rect_Type0_1 : βn:nat.βP:nat β Type[0].
103 (βm.(βp. p < m β P p) β P m) β P n.
105 cut (βq:nat. q β€ n β P q) /2/
107 [#q #HleO (* applica male *)
108 @(le_n_O_rect_Type0 ? HleO)
109 @H #p #ltpO cases (?:False) /2/ (* 3 *)
111 @H #a #lta @Hind @le_S_S_to_le /2/
115 lemma leb_false_to_lt : βn,m. leb n m = false β m < n.
117 [ #m normalize #H destruct(H)
118 | #n0 #IH * // #m normalize #H @le_S_S @IH // ]
121 lemma nominal_eta_aux : βx,u.x β FV u β βk.vclose_tm_aux (vopen_tm_aux u x k) x k = u.
123 [ #n #_ #k normalize cases (decidable_eq_nat n k) #Hnk
124 [ >Hnk >eqb_n_n whd in β’ (??%?); >(\b ?) //
125 | >(not_eq_to_eqb_false β¦ Hnk) normalize cases (true_or_false (leb n k)) #Hleb
126 [ >Hleb normalize >(?:leb k n = false) //
127 @lt_to_leb_false @not_eq_to_le_to_lt /2/
128 | >Hleb normalize >(?:leb k (pred n) = true) normalize
129 [ cases (leb_false_to_lt β¦ Hleb) //
130 | @le_to_leb_true cases (leb_false_to_lt β¦ Hleb) normalize /2/ ] ] ]
131 | #y normalize in β’ (%β?β?); #Hy whd in β’ (?β??%?); >(\bf ?) // @(not_to_not β¦ Hy) //
132 | #s #v #IH normalize #Hv #k >IH // @Hv
133 | #v1 #v2 #IH1 #IH2 normalize #Hv1v2 #k
134 >IH1 [ >IH2 // | @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_l ]
135 @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_r ]
138 corollary nominal_eta : βx,u.x β FV u β (Ξ½x.uβxβ) = u.
139 #x #u #Hu @nominal_eta_aux //
142 lemma eq_height_vopen_aux : βv,x,k.tm_height (vopen_tm_aux v x k) = tm_height v.
144 [ #n #k normalize cases (eqb n k) // cases (leb n k) //
146 | #s #u #IH #k normalize >IH %
147 | #u1 #u2 #IH1 #IH2 #k normalize >IH1 >IH2 % ]
150 corollary eq_height_vopen : βv,x.tm_height (vβxβ) = tm_height v.
151 #v #x @eq_height_vopen_aux
154 theorem pretm_ind_plus_aux :
155 βP:pretm β Type[0].
156 (βx:πΈ.P (par x)) β
157 (βn:β.P (var n)) β
158 (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
160 (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
161 βn,u.tm_height u β€ n β P u.
162 #P #Hpar #Hvar #Happ #C #Hlam #n change with ((Ξ»n.?) n); @(nat_rect_Type0_1 n ??)
165 [ normalize #s #v #Hfalse cases (?:False) cases (not_le_Sn_O (tm_height v)) /2/
166 | #v1 #v2 whd in β’ (?%?β?); #Hfalse cases (?:False) cases (not_le_Sn_O (S (max ??))) /2/ ] ]
168 [ #s #v whd in β’ (?%?β?); #Hv
169 lapply (p_fresh β¦ (C@FV v)) letin y β (N_fresh β¦ (C@FV v)) #Hy
170 >(?:abs s v = lam y s (vβyβ))
171 [| whd in β’ (???%); >nominal_eta // @(not_to_not β¦ Hy) @in_list_to_in_list_append_r ]
173 [ @(not_to_not β¦ Hy) @in_list_to_in_list_append_r
174 | @(not_to_not β¦ Hy) @in_list_to_in_list_append_l ]
175 @IH [| @Hv | >eq_height_vopen % ]
176 | #v1 #v2 whd in β’ (?%?β?); #Hv @Happ
177 [ @IH [| @Hv | // ] | @IH [| @Hv | // ] ] ]
180 corollary pretm_ind_plus :
181 βP:pretm β Type[0].
182 (βx:πΈ.P (par x)) β
183 (βn:β.P (var n)) β
184 (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
186 (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
188 #P #Hpar #Hvar #Happ #C #Hlam #u @pretm_ind_plus_aux /2/
191 (* maps a permutation to a list of terms *)
192 definition Pi_map_list : (πΈ β πΈ) β list πΈ β list πΈ β map πΈ πΈ .
194 (* interpretation "permutation of name list" 'middot p x = (Pi_map_list p x).*)
197 inductive tm : pretm β Prop β
198 | tm_par : βx:πΈ.tm (par x)
199 | tm_app : βu,v.tm u β tm v β tm (app u v)
200 | tm_lam : βx,s,u.tm u β tm (lam x s u).
202 inductive ctx_aux : nat β pretm β Prop β
203 | ctx_var : βn,k.n < k β ctx_aux k (var n)
204 | ctx_par : βx,k.ctx_aux k (par x)
205 | ctx_app : βu,v,k.ctx_aux k u β ctx_aux k v β ctx_aux k (app u v)
206 (* Γ¨ sostituibile da ctx_lam ? *)
207 | ctx_abs : βs,u.ctx_aux (S k) u β ctx_aux k (abs s u).
210 inductive tm_or_ctx (k:nat) : pretm β Type[0] β
211 | toc_var : βn.n < k β tm_or_ctx k (var n)
212 | toc_par : βx.tm_or_ctx k (par x)
213 | toc_app : βu,v.tm_or_ctx k u β tm_or_ctx k v β tm_or_ctx k (app u v)
214 | toc_lam : βx,s,u.tm_or_ctx k u β tm_or_ctx k (lam x s u).
216 definition tm β Ξ»t.tm_or_ctx O t.
217 definition ctx β Ξ»t.tm_or_ctx 1 t.
219 record TM : Type[0] β {
220 pretm_of_TM :> pretm;
221 tm_of_TM : tm pretm_of_TM
224 record CTX : Type[0] β {
225 pretm_of_CTX :> pretm;
226 ctx_of_CTX : ctx pretm_of_CTX
229 inductive tm2 : pretm β Type[0] β
230 | tm_par : βx.tm2 (par x)
231 | tm_app : βu,v.tm2 u β tm2 v β tm2 (app u v)
232 | tm_lam : βx,s,u.x β FV u β (βy.y β FV u β tm2 (uβyβ)) β tm2 (lam x s (uβxβ)).
235 inductive tm' : pretm β Prop β
236 | tm_par : βx.tm' (par x)
237 | tm_app : βu,v.tm' u β tm' v β tm' (app u v)
238 | tm_lam : βx,s,u,C.x β FV u β x β C β (βy.y β FV u β tm' (β΄uβ΅y)) β tm' (lam x s (β΄uβ΅x)).
241 axiom swap_inj : βN.βz1,z2,x,y.swap N z1 z2 x = swap N z1 z2 y β x = y.
244 βz1,z2,x,u.swap πΈ z1 z2Β·(Ξ½x.u) = (Ξ½ swap ? z1 z2 x.swap πΈ z1 z2 Β· u).
246 change with (vclose_tm_aux ???) in match (vclose_tm ??);
247 change with (vclose_tm_aux ???) in β’ (???%); lapply O elim u
248 [3:whd in β’ (?β?β(?β ??%%)β?β??%%); //
249 |4:whd in β’ (?β?β(?β??%%)β(?β??%%)β?β??%%); //
250 | #n #k whd in β’ (??(??%)%); cases (leb k n) normalize %
251 | #x0 #k cases (true_or_false (x0==z1)) #H1 >H1 whd in β’ (??%%);
252 [ cases (true_or_false (x0==x)) #H2 >H2 whd in β’ (??(??%)%);
253 [ <(\P H2) >H1 whd in β’ (??(??%)%); >(\b ?) // >(\b ?) //
254 | >H2 whd in match (swap ????); >H1
255 whd in match (if false then var k else ?);
256 whd in match (if true then z2 else ?); >(\bf ?)
257 [ >(\P H1) >swap_left %
258 | <(swap_inv ? z1 z2 z2) in β’ (?(??%?)); % #H3
259 lapply (swap_inj β¦ H3) >swap_right #H4 <H4 in H2; >H1 #H destruct (H) ]
261 | >(?:(swap ? z1 z2 x0 == swap ? z1 z2 x) = (x0 == x))
262 [| cases (true_or_false (x0==x)) #H2 >H2
264 | @(\bf ?) % #H >(swap_inj β¦ H) in H2; >(\b ?) // #H0 destruct (H0) ] ]
265 cases (true_or_false (x0==x)) #H2 >H2 whd in β’ (??(??%)%);
266 [ <(\P H2) >H1 >(\b (refl ??)) %
273 βz1,z2,x,u.swap πΈ z1 z2Β·(uβxβ) = (swap πΈ z1 z2 Β· uβswap πΈ z1 z2 xβ).
275 change with (vopen_tm_aux ???) in match (vopen_tm ??);
276 change with (vopen_tm_aux ???) in β’ (???%); lapply O elim u //
277 [2: #s #v whd in β’ ((?β??%%)β?β??%%); //
278 |3: #v1 #v2 whd in β’ ((?β??%%)β(?β??%%)β?β??%%); /2/ ]
279 #n #k whd in β’ (??(??%)%); cases (true_or_false (eqb n k)) #H1 >H1 //
280 cases (true_or_false (leb n k)) #H2 >H2 normalize //
284 βz1,z2,x,s,u.swap πΈ z1 z2 Β· lam x s u = lam (swap πΈ z1 z2 x) s (swap πΈ z1 z2 Β· u).
285 #z1 #z2 #x #s #u whd in β’ (???%); <(pi_vclose_tm β¦) %
288 lemma eqv_FV : βz1,z2,u.FV (swap πΈ z1 z2 Β· u) = Pi_map_list (swap πΈ z1 z2) (FV u).
291 | #v1 #v2 whd in β’ (??%%β??%%β??%%); #H1 #H2 >H1 >H2
292 whd in β’ (???(????%)); /2/ ]
295 lemma swap_inv_tm : βz1,z2,u.swap πΈ z1 z2 Β· (swap πΈ z1 z2 Β· u) = u.
298 |3: #s #v whd in β’ (?β??%%); //
299 |4: #v1 #v2 #Hv1 #Hv2 whd in β’ (??%%); // ]
300 #x whd in β’ (??%?); >swap_inv %
303 lemma eqv_in_list : βx,l,z1,z2.x β l β swap πΈ z1 z2 x β Pi_map_list (swap πΈ z1 z2) l.
304 #x #l #z1 #z2 #Hin elim Hin
306 | #x1 #x2 #l0 #Hin #IH %2 @IH ]
309 lemma eqv_tm2 : βu.tm2 u β βz1,z2.tm2 ((swap ? z1 z2)Β·u).
310 #u #Hu #z1 #z2 letin p β (swap ? z1 z2) elim Hu /2/
311 #x #s #v #Hx #Hv #IH >pi_lam >pi_vopen_tm %3
312 [ @(not_to_not β¦ Hx) -Hx #Hx
313 <(swap_inv ? z1 z2 x) <(swap_inv_tm z1 z2 v) >eqv_FV @eqv_in_list //
314 | #y #Hy <(swap_inv ? z1 z2 y)
315 <pi_vopen_tm @IH @(not_to_not β¦ Hy) -Hy #Hy <(swap_inv ? z1 z2 y)
316 >eqv_FV @eqv_in_list //
320 lemma vclose_vopen_aux : βx,u,k.vopen_tm_aux (vclose_tm_aux u x k) x k = u.
321 #x #u elim u [1,3,4:normalize //]
322 [ #n #k cases (true_or_false (leb k n)) #H >H whd in β’ (??%?);
323 [ cases (true_or_false (eqb (S n) k)) #H1 >H1
324 [ <(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_true_to_le β¦ H) -H #H
325 cases (le_to_not_lt β¦ H) -H #H cases (H ?) %
326 | whd in β’ (??%?); >lt_to_leb_false // @le_S_S /2/ ]
327 | cases (true_or_false (eqb n k)) #H1 >H1 normalize
328 [ >(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_false_to_not_le β¦ H) -H
330 | >le_to_leb_true // @not_lt_to_le % #H2 >le_to_leb_true in H;
331 [ #H destruct (H) | /2/ ]
334 | #x0 #k whd in β’ (??(?%??)?); cases (true_or_false (x0==x))
335 #H1 >H1 normalize // >(\P H1) >eqb_n_n % ]
338 lemma vclose_vopen : βx,u.((Ξ½x.u)βxβ) = u. #x #u @vclose_vopen_aux
342 theorem tm_to_tm : βt.tm' t β tm t.
346 lemma in_list_singleton : βT.βt1,t2:T.t1 β [t2] β t1 = t2.
347 #T #t1 #t2 #H @(in_list_inv_ind ??? H) /2/
350 lemma fresh_vclose_tm_aux : βu,x,k.x β FV (vclose_tm_aux u x k).
352 [ #n #k normalize cases (leb k n) normalize //
353 | #x0 #k whd in β’ (?(???(?%))); cases (true_or_false (x0==x)) #H >H normalize //
354 lapply (\Pf H) @not_to_not #Hin >(in_list_singleton ??? Hin) %
355 | #v1 #v2 #IH1 #IH2 #k normalize % #Hin cases (in_list_append_to_or_in_list ???? Hin) -Hin #Hin
356 [ cases (IH1 k) -IH1 #IH1 @IH1 @Hin | cases (IH2 k) -IH2 #IH2 @IH2 @Hin ]
359 lemma fresh_vclose_tm : βu,x.x β FV (Ξ½x.u). //
362 lemma fresh_swap_tm : βz1,z2,u.z1 β FV u β z2 β FV u β swap πΈ z1 z2 Β· u = u.
364 [2: normalize in β’ (?β%β%β?); #x #Hz1 #Hz2 whd in β’ (??%?); >swap_other //
365 [ @(not_to_not β¦ Hz2) | @(not_to_not β¦ Hz1) ] //
367 | #s #v #IH normalize #Hz1 #Hz2 >IH // [@Hz2|@Hz1]
368 | #v1 #v2 #IH1 #IH2 normalize #Hz1 #Hz2
369 >IH1 [| @(not_to_not β¦ Hz2) @in_list_to_in_list_append_l | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_l ]
370 >IH2 // [@(not_to_not β¦ Hz2) @in_list_to_in_list_append_r | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_r ]
374 theorem tm_to_tm2 : βu.tm u β tm2 u.
376 [ #n #Hn cases (not_le_Sn_O n) #Hfalse cases (Hfalse Hn)
378 | #u #v #Hu #Hv @tm_app
379 | #x #s #u #Hu #IHu <(vclose_vopen x u) @tm_lam
381 | #y #Hy <(fresh_swap_tm x y (Ξ½x.u)) /2/ @fresh_vclose_tm ]
385 theorem tm2_to_tm : βu.tm2 u β tm u.
386 #u #pu elim pu /2/ #x #s #v #Hx #Hv #IH %4 @IH //
389 definition PAR β Ξ»x.mk_TM (par x) ?. // qed.
390 definition APP β Ξ»u,v:TM.mk_TM (app u v) ?./2/ qed.
391 definition LAM β Ξ»x,s.Ξ»u:TM.mk_TM (lam x s u) ?./2/ qed.
393 axiom vopen_tm_down : βu,x,k.tm_or_ctx (S k) u β tm_or_ctx k (uβxβ).
394 (* needs true_plus_false
397 [ #n #Hn normalize cases (true_or_false (eqb n O)) #H >H [%2]
398 normalize >(?: leb n O = false) [|cases n in H; // >eqb_n_n #H destruct (H) ]
399 normalize lapply Hn cases n in H; normalize [ #Hfalse destruct (Hfalse) ]
400 #n0 #_ #Hn0 % @le_S_S_to_le //
402 | #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 %3 //
403 | #x0 #s #v #Hv #IH normalize @daemon
408 definition vopen_TM β Ξ»u:CTX.Ξ»x.mk_TM (uβxβ) (vopen_tm_down β¦). @ctx_of_CTX qed.
410 axiom vclose_tm_up : βu,x,k.tm_or_ctx k u β tm_or_ctx (S k) (Ξ½x.u).
412 definition vclose_TM β Ξ»u:TM.Ξ»x.mk_CTX (Ξ½x.u) (vclose_tm_up β¦). @tm_of_TM qed.
414 interpretation "ln wf term variable open" 'open u x = (vopen_TM u x).
415 interpretation "ln wf term variable close" 'nu x u = (vclose_TM u x).
417 theorem tm_alpha : βx,y,s,u.x β FV u β y β FV u β lam x s (uβxβ) = lam y s (uβyβ).
418 #x #y #s #u #Hx #Hy whd in β’ (??%%); @eq_f >nominal_eta // >nominal_eta //
421 theorem TM_ind_plus :
422 (* non si puΓ² dare il principio in modo dipendente (almeno utilizzando tm2)
423 la "prova" purtroppo Γ¨ in Type e non si puΓ² garantire che sia esattamente
424 quella che ci aspetteremmo
426 βP:pretm β Type[0].
427 (βx:πΈ.P (PAR x)) β
428 (βv1,v2:TM.P v1 β P v2 β P (APP v1 v2)) β
430 (βx,s.βv:CTX.x β FV v β x β C β
431 (βy.y β FV v β P (vβyβ)) β P (LAM x s (vβxβ))) β
433 #P #Hpar #Happ #C #Hlam * #u #pu elim (tm_to_tm2 u pu) //
434 [ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β¦) (mk_TM β¦)) /2/
435 | #x #s #v #Hx #pv #IH
436 lapply (p_fresh β¦ (C@FV v)) letin x0 β (N_fresh β¦ (C@FV v)) #Hx0
437 >(?:lam x s (vβxβ) = lam x0 s (vβx0β))
438 [|@tm_alpha // @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r ]
439 @(Hlam x0 s (mk_CTX v ?) ??)
440 [ <(nominal_eta β¦ Hx) @vclose_tm_up @tm2_to_tm @pv //
441 | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r
442 | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_l
448 "hvbox('nominal' u 'return' out 'with'
449 [ 'xpar' ident x β f1
450 | 'xapp' ident v1 ident v2 ident recv1 ident recv2 β f2
451 | 'xlam' β¨ident y # Cβ© ident s ident w ident py1 ident py2 ident recw β f3 ])"
453 for @{ TM_ind_plus $out (Ξ»${ident x}:?.$f1)
454 (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
455 $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident recw}:?.$f3)
458 (* include "basics/jmeq.ma".*)
460 definition subst β (Ξ»u:TM.Ξ»x,v.
461 nominal u return (Ξ»_.TM) with
462 [ xpar x0 β match x == x0 with [ true β v | false β u ]
463 | xapp v1 v2 recv1 recv2 β APP recv1 recv2
464 | xlam β¨y # x::FV vβ© s w py1 py2 recw β LAM y s (recw y py1) ]).
466 lemma fasfd : βs,v. pretm_of_TM (subst (LAM O s (PAR 1)) O v) = pretm_of_TM (LAM O s (PAR 1)).
467 #s #v normalize in β’ (??%?);
470 theorem tm2_ind_plus :
471 (* non si puΓ² dare il principio in modo dipendente (almeno utilizzando tm2) *)
472 βP:pretm β Type[0].
473 (βx:πΈ.P (par x)) β
474 (βv1,v2.tm2 v1 β tm2 v2 β P v1 β P v2 β P (app v1 v2)) β
476 (βx,s,v.x β FV v β x β C β (βy.y β FV v β tm2 (vβyβ)) β
477 (βy.y β FV v β P (vβyβ)) β P (lam x s (vβxβ))) β
479 #P #Hpar #Happ #C #Hlam #u #pu elim pu /2/
481 lapply (p_fresh β¦ (C@FV v)) letin y β (N_fresh β¦ (C@FV v)) #Hy
482 >(?:lam x s (vβxβ) = lam y s (vβyβ)) [| @tm_alpha // @(not_to_not β¦ Hy) @in_list_to_in_list_append_r ]
483 @Hlam /2/ lapply Hy -Hy @not_to_not #Hy
484 [ @in_list_to_in_list_append_r @Hy | @in_list_to_in_list_append_l @Hy ]
487 definition check_tm β
488 Ξ»u.pretm_ind_plus ? (Ξ»_.true) (Ξ»_.false)
489 (Ξ»v1,v2,r1,r2.r1 β§ r2) [ ] (Ξ»x,s,v,pv1,pv2,rv.rv) u.
492 lemma check_tm_complete : βu.tm u β check_tm u = true.
493 #u #pu @(tm2_ind_plus β¦ [ ] β¦ (tm_to_tm2 ? pu)) //
494 [ #v1 #v2 #pv1 #pv2 #IH1 #IH2
495 | #x #s #v #Hx1 #Hx2 #Hv #IH
499 "hvbox('nominal' u 'return' out 'with'
500 [ 'xpar' ident x β f1
501 | 'xapp' ident v1 ident v2 ident pv1 ident pv2 ident recv1 ident recv2 β f2
502 | 'xlam' β¨ident y # Cβ© ident s ident w ident py1 ident py2 ident pw ident recw β f3 ])"
504 for @{ tm2_ind_plus $out (Ξ»${ident x}:?.$f1)
505 (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident pv1}:?.Ξ»${ident pv2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
506 $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident pw}:?.Ξ»${ident recw}:?.$f3)
507 ? (tm_to_tm2 ? $u) }.
509 "hvbox('nominal' u 'with'
510 [ 'xlam' ident x # C ident s ident w β f3 ])"
512 for @{ tm2_ind_plus ???
513 $C (Ξ»${ident x}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.
514 Ξ»${ident pw}:?.Ξ»${ident recw}:?.$f3) $u (tm_to_tm2 ??) }.
518 definition subst β (Ξ»u.Ξ»pu:tm u.Ξ»x,v.
519 nominal pu return (Ξ»_.pretm) with
520 [ xpar x0 β match x == x0 with [ true β v | false β u ]
521 | xapp v1 v2 pv1 pv2 recv1 recv2 β app recv1 recv2
522 | xlam β¨y # x::FV vβ© s w py1 py2 pw recw β lam y s (recw y py1) ]).
524 lemma fasfd : βx,s,u,p1,v. subst (lam x s u) p1 x v = lam x s u.
528 definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,y.
530 (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
531 (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
532 (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
533 u (tm_to_tm2 β¦ pu).
535 definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
537 [ xlam y # (x::FV v) s w ^ ? ].
540 notation > "Ξ ident x. ident T [ident x] β¦ P"
541 with precedence 48 for @{'foo (Ξ»${ident x}.Ξ»${ident T}.$P)}.
543 notation < "Ξ ident x. ident T [ident x] β¦ P"
544 with precedence 48 for @{'foo (Ξ»${ident x}:$Q.Ξ»${ident T}:$R.$P)}.
549 "hvbox('nominal' u 'with'
550 [ 'xpar' ident x β f1
551 | 'xapp' ident v1 ident v2 β f2
552 | 'xlam' ident x # C s w β f3 ])"
554 for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
555 (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
556 $C (Ξ»${ident x}:$Tx.Ξ»${ident s}:$Ts.Ξ»${ident w}:$Tw.Ξ»${ident py1}:$Tpy1.Ξ»${ident py2}:$Tpy2.Ξ»${ident pw}:$Tpw.Ξ»${ident recw}:$Trw.$f3) $u (tm_to_tm2 ??) }.
561 "hvbox('nominal' u 'with'
562 [ 'xpar' ident x ^ f1
563 | 'xapp' ident v1 ident v2 ^ f2 ])"
564 (* | 'xlam' ident x # C s w ^ f3 ]) *)
566 for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
567 (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
568 $C (Ξ»${ident x}:$Tx.Ξ»${ident s}:$Ts.Ξ»${ident w}:$Tw.Ξ»${ident py1}:$Tpy1.Ξ»${ident py2}:$Tpy2.Ξ»${ident pw}:$Tpw.Ξ»${ident recw}:$Trw.$f3) $u (tm_to_tm2 ??) }.
571 "hvbox('nominal' u 'with'
572 [ 'xpar' ident x ^ f1
573 | 'xapp' ident v1 ident v2 ^ f2 ])"
575 for @{ tm2_ind_plus ? (Ξ»${ident x}:?.$f1)
576 (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
577 $C (Ξ»${ident x}:?.Ξ»${ident s}:$Ts.Ξ»${ident w}:$Tw.Ξ»${ident py1}:$Tpy1.Ξ»${ident py2}:$Tpy2.Ξ»${ident pw}:$Tpw.Ξ»${ident recw}:$Trw.$f3) $u (tm_to_tm2 ??) }.
580 definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
582 [ xpar x0 ^ match x == x0 with [ true β v | false β u ]
584 | xlam y # (x::FV v) s w ^ ? ].
587 (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
588 (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
589 (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
590 u (tm_to_tm2 β¦ pu).
594 definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
596 (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
597 (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
598 (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
599 u (tm_to_tm2 β¦ pu).
604 axiom in_Env : πΈ Γ tp β Env β Prop.
605 notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
606 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
610 inductive judg : list tp β tm β tp β Prop β
611 | t_var : βg,n,t.Nth ? n g = Some ? t β judg g (var n) t
612 | t_app : βg,m,n,t,u.judg g m (arr t u) β judg g n t β judg g (app m n) u
613 | t_abs : βg,t,m,u.judg (t::g) m u β judg g (abs t m) (arr t u).
615 definition Env := list (πΈ Γ tp).
617 axiom vclose_env : Env β list tp.
618 axiom vclose_tm : Env β tm β tm.
619 axiom Lam : πΈ β tp β tm β tm.
620 definition Judg β Ξ»G,M,T.judg (vclose_env G) (vclose_tm G M) T.
621 definition dom β Ξ»G:Env.map ?? (fst ??) G.
623 definition sctx β πΈ Γ tm.
624 axiom swap_tm : πΈ β πΈ β tm β tm.
625 definition sctx_app : sctx β πΈ β tm β Ξ»M0,Y.let β©X,Mβͺ β M0 in swap_tm X Y M.
627 axiom in_list : βA:Type[0].A β list A β Prop.
628 interpretation "list membership" 'mem x l = (in_list ? x l).
629 interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
631 axiom in_Env : πΈ Γ tp β Env β Prop.
632 notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
633 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
635 let rec FV M β match M with
637 | app M1 M2 β FV M1@FV M2
641 (* axiom Lookup : πΈ β Env β option tp. *)
643 (* forma alto livello del judgment
644 t_abs* : βG,T,X,M,U.
645 (βY β supp(M).Judg (β©Y,Tβͺ::G) (M[Y]) U) β
646 Judg G (Lam X T (M[X])) (arr T U) *)
648 (* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
650 axiom Judg_ind : βP:Env β tm β tp β Prop.
651 (βX,G,T.β©X,Tβͺ β G β P G (par X) T) β
653 Judg G M (arr T U) β Judg G N T β
654 P G M (arr T U) β P G N T β P G (app M N) U) β
656 (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β Judg (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
657 (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β P (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
658 P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) β
659 βG,M,T.Judg G M T β P G M T.
661 axiom t_par : βX,G,T.β©X,Tβͺ β G β Judg G (par X) T.
662 axiom t_app2 : βG,M,N,T,U.Judg G M (arr T U) β Judg G N T β Judg G (app M N) U.
663 axiom t_Lam : βG,X,M,T,U.Judg (β©X,Tβͺ::G) M U β Judg G (Lam X T M) (arr T U).
665 definition subenv β Ξ»G1,G2.βx.x β G1 β x β G2.
666 interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
668 axiom daemon : βP:Prop.P.
670 theorem weakening : βG1,G2,M,T.G1 β G2 β Judg G1 M T β Judg G2 M T.
671 #G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (βG2.?)
673 [ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
674 | #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
675 [| @IH1 // | @IH2 // ]
676 | #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
677 [ (* trivial property of Lam *) @daemon
678 | (* trivial property of subenv *) @daemon ]
682 (* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e