]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/broken_lib/binding/ln.ma
0.99.3 -> 0.99.4
[helm.git] / matita / matita / broken_lib / binding / ln.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basics/lists/list.ma".
16 include "basics/deqsets.ma".
17 include "binding/names.ma".
18 include "binding/fp.ma".
19
20 axiom alpha : Nset.
21 notation "𝔸" non associative with precedence 90 for @{'alphabet}.
22 interpretation "set of names" 'alphabet = alpha.
23
24 inductive tp : Type[0] β‰ 
25 | top : tp
26 | arr : tp β†’ tp β†’ tp.
27 inductive pretm : Type[0] β‰ 
28 | var : nat β†’ pretm
29 | par :  π”Έ β†’ pretm
30 | abs : tp β†’ pretm β†’ pretm
31 | app : pretm β†’ pretm β†’ pretm.
32
33 let rec Nth T n (l:list T) on n β‰ 
34   match l with 
35   [ nil β‡’ None ?
36   | cons hd tl β‡’ match n with
37     [ O β‡’ Some ? hd
38     | S n0 β‡’ Nth T n0 tl ] ].
39
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.  
46
47 definition vopen_var β‰ Ξ»n,x,k.match eqb n k with
48  [ true β‡’ par x
49  | false β‡’ match leb n k with
50    [ true β‡’ var n
51    | false β‡’ var (pred n) ] ].
52
53 let rec vopen_tm_aux u x k β‰ match u with
54   [ var n β‡’ vopen_var n x k
55   | par x0 β‡’ u
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.
59
60 let rec FV u β‰ match u with 
61   [ par x β‡’ [x]
62   | app v1 v2 β‡’ FV v1@FV v2
63   | abs s v β‡’ FV v
64   | _ β‡’ [ ] ].  
65
66 definition lam β‰ Ξ»x,s,u.abs s (vclose_tm u x).
67
68 let rec Pi_map_tm p u on u β‰ match u with
69 [ par x β‡’ par (p x)
70 | var _ β‡’ u
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) ].
73
74 interpretation "permutation of tm" 'middot p x = (Pi_map_tm p x).
75
76 notation "hvbox(u⌈xβŒ‰)"
77   with precedence 45
78   for @{ 'open $u $x }.
79
80 (*
81 notation "hvbox(u⌈xβŒ‰)"
82   with precedence 45
83   for @{ 'open $u $x }.
84 notation "❴ u β΅ x" non associative with precedence 90 for @{ 'open $u $x }.
85 *)
86 interpretation "ln term variable open" 'open u x = (vopen_tm u x).
87 notation < "hvbox(Ξ½ x break . u)"
88  with precedence 20
89 for @{'nu $x $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).
93
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) 
97 | _ β‡’ O ].
98
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. 
101
102 theorem nat_rect_Type0_1 : βˆ€n:nat.βˆ€P:nat β†’ Type[0]. 
103 (βˆ€m.(βˆ€p. p < m β†’ P p) β†’ P m) β†’ P n.
104 #n #P #H 
105 cut (βˆ€q:nat. q β‰€ n β†’ P q) /2/
106 (elim n) 
107  [#q #HleO (* applica male *) 
108     @(le_n_O_rect_Type0 ? HleO)
109     @H #p #ltpO cases (?:False) /2/ (* 3 *)
110  |#p #Hind #q #HleS 
111     @H #a #lta @Hind @le_S_S_to_le /2/
112  ]
113 qed.
114
115 lemma leb_false_to_lt : βˆ€n,m. leb n m = false β†’ m < n.
116 #n elim n
117 [ #m normalize #H destruct(H)
118 | #n0 #IH * // #m normalize #H @le_S_S @IH // ]
119 qed.
120
121 lemma nominal_eta_aux : βˆ€x,u.x βˆ‰ FV u β†’ βˆ€k.vclose_tm_aux (vopen_tm_aux u x k) x k = u.
122 #x #u elim u
123 [ #n #_ #k normalize cases (decidable_eq_nat n k) #Hnk
124   [ >Hnk >eqb_n_n normalize >(\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 #Hy >(\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 ]
136 qed.
137
138 corollary nominal_eta : βˆ€x,u.x βˆ‰ FV u β†’ (Ξ½x.u⌈xβŒ‰) = u.
139 #x #u #Hu @nominal_eta_aux //
140 qed.
141
142 lemma eq_height_vopen_aux : βˆ€v,x,k.tm_height (vopen_tm_aux v x k) = tm_height v.
143 #v #x elim v
144 [ #n #k normalize cases (eqb n k) // cases (leb n k) //
145 | #u #k %
146 | #s #u #IH #k normalize >IH %
147 | #u1 #u2 #IH1 #IH2 #k normalize >IH1 >IH2 % ]
148 qed.
149
150 corollary eq_height_vopen : βˆ€v,x.tm_height (v⌈xβŒ‰) = tm_height v.
151 #v #x @eq_height_vopen_aux
152 qed.
153
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)) β†’ 
159    βˆ€C:list π”Έ.
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 ??)
163 #m cases m
164 [ #_ * /2/
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 (max ??))
167     [ #H @H @Hfalse|*:skip] ] ]
168 -m #m #IH * /2/
169 [ #s #v whd in βŠ’ (?%?β†’?); #Hv
170   lapply (p_fresh β€¦ (C@FV v)) letin y β‰ (N_fresh β€¦ (C@FV v)) #Hy
171   >(?:abs s v = lam y s (v⌈yβŒ‰))
172   [| whd in βŠ’ (???%); >nominal_eta // @(not_to_not β€¦ Hy) @in_list_to_in_list_append_r ] 
173   @Hlam
174   [ @(not_to_not β€¦ Hy) @in_list_to_in_list_append_r
175   | @(not_to_not β€¦ Hy) @in_list_to_in_list_append_l ]
176   @IH [| @Hv | >eq_height_vopen % ]
177 | #v1 #v2 whd in βŠ’ (?%?β†’?); #Hv @Happ
178   [ @IH [| @Hv | @le_max_1 ] | @IH [| @Hv | @le_max_2 ] ] ]
179 qed.
180
181 corollary pretm_ind_plus :
182  βˆ€P:pretm β†’ Type[0].
183    (βˆ€x:𝔸.P (par x)) β†’ 
184    (βˆ€n:β„•.P (var n)) β†’ 
185    (βˆ€v1,v2. P v1 β†’ P v2 β†’ P (app v1 v2)) β†’ 
186    βˆ€C:list π”Έ.
187    (βˆ€x,s,v.x βˆ‰ FV v β†’ x βˆ‰ C β†’ P (v⌈xβŒ‰) β†’ P (lam x s (v⌈xβŒ‰))) β†’
188  βˆ€u.P u.
189 #P #Hpar #Hvar #Happ #C #Hlam #u @pretm_ind_plus_aux /2/
190 qed.
191
192 (* maps a permutation to a list of terms *)
193 definition Pi_map_list : (𝔸 β†’ π”Έ) β†’ list π”Έ β†’ list π”Έ β‰ map π”Έ π”Έ .
194
195 (* interpretation "permutation of name list" 'middot p x = (Pi_map_list p x).*)
196
197 (*
198 inductive tm : pretm β†’ Prop β‰ 
199 | tm_par : βˆ€x:𝔸.tm (par x)
200 | tm_app : βˆ€u,v.tm u β†’ tm v β†’ tm (app u v)
201 | tm_lam : βˆ€x,s,u.tm u β†’ tm (lam x s u).
202
203 inductive ctx_aux : nat β†’ pretm β†’ Prop β‰ 
204 | ctx_var : βˆ€n,k.n < k β†’ ctx_aux k (var n)
205 | ctx_par : βˆ€x,k.ctx_aux k (par x)
206 | ctx_app : βˆ€u,v,k.ctx_aux k u β†’ ctx_aux k v β†’ ctx_aux k (app u v)
207 (* Γ¨ sostituibile da ctx_lam ? *)
208 | ctx_abs : βˆ€s,u.ctx_aux (S k) u β†’ ctx_aux k (abs s u).
209 *)
210
211 inductive tm_or_ctx (k:nat) : pretm β†’ Type[0] β‰ 
212 | toc_var : βˆ€n.n < k β†’ tm_or_ctx k (var n)
213 | toc_par : βˆ€x.tm_or_ctx k (par x)
214 | toc_app : βˆ€u,v.tm_or_ctx k u β†’ tm_or_ctx k v β†’ tm_or_ctx k (app u v)
215 | toc_lam : βˆ€x,s,u.tm_or_ctx k u β†’ tm_or_ctx k (lam x s u).
216
217 definition tm β‰ Ξ»t.tm_or_ctx O t.
218 definition ctx β‰ Ξ»t.tm_or_ctx 1 t.
219
220 definition check_tm β‰ Ξ»u,k.
221   pretm_ind_plus ?
222   (Ξ»_.true)
223   (Ξ»n.leb (S n) k)
224   (Ξ»v1,v2,rv1,rv2.rv1 βˆ§ rv2)
225   [] (Ξ»x,s,v,px,pC,rv.rv)
226   u.
227
228 axiom pretm_ind_plus_app : βˆ€P,u,v,C,H1,H2,H3,H4.
229   pretm_ind_plus P H1 H2 H3 C H4 (app u v) = 
230     H3 u v (pretm_ind_plus P H1 H2 H3 C H4 u) (pretm_ind_plus P H1 H2 H3 C H4 v).
231
232 axiom pretm_ind_plus_lam : βˆ€P,x,s,u,C,px,pC,H1,H2,H3,H4.
233   pretm_ind_plus P H1 H2 H3 C H4 (lam x s (u⌈xβŒ‰)) = 
234     H4 x s u px pC (pretm_ind_plus P H1 H2 H3 C H4 (u⌈xβŒ‰)).
235
236 record TM : Type[0] β‰ {
237   pretm_of_TM :> pretm;
238   tm_of_TM : check_tm pretm_of_TM O = true
239 }.
240
241 record CTX : Type[0] β‰ {
242   pretm_of_CTX :> pretm;
243   ctx_of_CTX : check_tm pretm_of_CTX 1 = true
244 }.
245
246 inductive tm2 : pretm β†’ Type[0] β‰ 
247 | tm_par : βˆ€x.tm2 (par x)
248 | tm_app : βˆ€u,v.tm2 u β†’ tm2 v β†’ tm2 (app u v)
249 | tm_lam : βˆ€x,s,u.x βˆ‰ FV u β†’ (βˆ€y.y βˆ‰ FV u β†’ tm2 (u⌈yβŒ‰)) β†’ tm2 (lam x s (u⌈xβŒ‰)).
250
251 (*
252 inductive tm' : pretm β†’ Prop β‰ 
253 | tm_par : βˆ€x.tm' (par x)
254 | tm_app : βˆ€u,v.tm' u β†’ tm' v β†’ tm' (app u v)
255 | tm_lam : βˆ€x,s,u,C.x βˆ‰ FV u β†’ x βˆ‰ C β†’ (βˆ€y.y βˆ‰ FV u β†’ tm' (❴u❡y)) β†’ tm' (lam x s (❴u❡x)).
256 *)
257
258 lemma pi_vclose_tm : 
259   βˆ€z1,z2,x,u.swap π”Έ z1 z2Β·(Ξ½x.u) = (Ξ½ swap ? z1 z2 x.swap π”Έ z1 z2 Β· u).
260 #z1 #z2 #x #u
261 change with (vclose_tm_aux ???) in match (vclose_tm ??);
262 change with (vclose_tm_aux ???) in βŠ’ (???%); lapply O elim u normalize //
263 [ #n #k cases (leb k n) normalize %
264 | #x0 #k cases (true_or_false (x0==z1)) #H1 >H1 normalize
265   [ cases (true_or_false (x0==x)) #H2 >H2 normalize
266     [ <(\P H2) >H1 normalize >(\b (refl ? z2)) %
267     | >H1 normalize cases (true_or_false (x==z1)) #H3 >H3 normalize
268       [ >(\P H3) in H2; >H1 #Hfalse destruct (Hfalse)
269       | cases (true_or_false (x==z2)) #H4 >H4 normalize
270         [ cases (true_or_false (z2==z1)) #H5 >H5 normalize //
271           >(\P H5) in H4; >H3 #Hfalse destruct (Hfalse)
272         | >(\bf ?) // @sym_not_eq @(\Pf H4) ]
273       ]
274     ]
275   | cases (true_or_false (x0==x)) #H2 >H2 normalize
276     [ <(\P H2) >H1 normalize >(\b (refl ??)) %
277     | >H1 normalize cases (true_or_false (x==z1)) #H3 >H3 normalize
278       [ cases (true_or_false (x0==z2)) #H4 >H4 normalize 
279         [ cases (true_or_false (z1==z2)) #H5 >H5 normalize //
280           <(\P H5) in H4; <(\P H3) >H2 #Hfalse destruct (Hfalse)
281         | >H4 % ]
282       | cases (true_or_false (x0==z2)) #H4 >H4 normalize
283         [ cases (true_or_false (x==z2)) #H5 >H5 normalize 
284           [ <(\P H5) in H4; >H2 #Hfalse destruct (Hfalse)
285           | >(\bf ?) // @sym_not_eq @(\Pf H3) ]
286         | cases (true_or_false (x==z2)) #H5 >H5 normalize
287           [ >H1 %
288           | >H2 % ]
289         ]
290       ]
291     ]
292   ]
293 ]
294 qed.
295
296 lemma pi_vopen_tm : 
297   βˆ€z1,z2,x,u.swap π”Έ z1 z2Β·(u⌈xβŒ‰) = (swap π”Έ z1 z2 Β· u⌈swap π”Έ z1 z2 xβŒ‰).
298 #z1 #z2 #x #u
299 change with (vopen_tm_aux ???) in match (vopen_tm ??);
300 change with (vopen_tm_aux ???) in βŠ’ (???%); lapply O elim u normalize //
301 #n #k cases (true_or_false (eqb n k)) #H1 >H1 normalize //
302 cases (true_or_false (leb n k)) #H2 >H2 normalize //
303 qed.
304
305 lemma pi_lam : 
306   βˆ€z1,z2,x,s,u.swap π”Έ z1 z2 Β· lam x s u = lam (swap π”Έ z1 z2 x) s (swap π”Έ z1 z2 Β· u).
307 #z1 #z2 #x #s #u whd in βŠ’ (???%); <(pi_vclose_tm β€¦) %
308 qed.
309
310 lemma eqv_FV : βˆ€z1,z2,u.FV (swap π”Έ z1 z2 Β· u) = Pi_map_list (swap π”Έ z1 z2) (FV u).
311 #z1 #z2 #u elim u //
312 [ #s #v normalize //
313 | #v1 #v2 normalize /2/ ]
314 qed.
315
316 lemma swap_inv_tm : βˆ€z1,z2,u.swap π”Έ z1 z2 Β· (swap π”Έ z1 z2 Β· u) = u.
317 #z1 #z2 #u elim u [1,3,4:normalize //]
318 #x whd in βŠ’ (??%?); >swap_inv %
319 qed.
320
321 lemma eqv_in_list : βˆ€x,l,z1,z2.x βˆˆ l β†’ swap π”Έ z1 z2 x βˆˆ Pi_map_list (swap π”Έ z1 z2) l.
322 #x #l #z1 #z2 #Hin elim Hin
323 [ #x0 #l0 %
324 | #x1 #x2 #l0 #Hin #IH %2 @IH ]
325 qed.
326
327 lemma eqv_tm2 : βˆ€u.tm2 u β†’ βˆ€z1,z2.tm2 ((swap ? z1 z2)Β·u).
328 #u #Hu #z1 #z2 letin p β‰ (swap ? z1 z2) elim Hu /2/
329 #x #s #v #Hx #Hv #IH >pi_lam >pi_vopen_tm %3
330 [ @(not_to_not β€¦ Hx) -Hx #Hx
331   <(swap_inv ? z1 z2 x) <(swap_inv_tm z1 z2 v) >eqv_FV @eqv_in_list //
332 | #y #Hy <(swap_inv ? z1 z2 y)
333   <pi_vopen_tm @IH @(not_to_not β€¦ Hy) -Hy #Hy <(swap_inv ? z1 z2 y)
334   >eqv_FV @eqv_in_list //
335 ]
336 qed.
337
338 lemma vclose_vopen_aux : βˆ€x,u,k.vopen_tm_aux (vclose_tm_aux u x k) x k = u.
339 #x #u elim u normalize //
340 [ #n #k cases (true_or_false (leb k n)) #H >H whd in βŠ’ (??%?);
341   [ cases (true_or_false (eqb (S n) k)) #H1 >H1
342     [ <(eqb_true_to_eq β€¦ H1) in H; #H lapply (leb_true_to_le β€¦ H) -H #H
343       cases (le_to_not_lt β€¦ H) -H #H cases (H ?) %
344     | whd in βŠ’ (??%?); >lt_to_leb_false // @le_S_S /2/ ]
345   | cases (true_or_false (eqb n k)) #H1 >H1 normalize
346     [ >(eqb_true_to_eq β€¦ H1) in H; #H lapply (leb_false_to_not_le β€¦ H) -H
347       * #H cases (H ?) %
348     | >le_to_leb_true // @not_lt_to_le % #H2 >le_to_leb_true in H;
349       [ #H destruct (H) | /2/ ]
350     ]
351   ]
352 | #x0 #k cases (true_or_false (x0==x)) #H1 >H1 normalize // >(\P H1) >eqb_n_n % ]
353 qed.      
354
355 lemma vclose_vopen : βˆ€x,u.((Ξ½x.u)⌈xβŒ‰) = u. #x #u @vclose_vopen_aux
356 qed.
357
358 (*
359 theorem tm_to_tm : βˆ€t.tm' t β†’ tm t.
360 #t #H elim H
361 *)
362
363 lemma in_list_singleton : βˆ€T.βˆ€t1,t2:T.t1 βˆˆ [t2] β†’ t1 = t2.
364 #T #t1 #t2 #H @(in_list_inv_ind ??? H) /2/
365 qed.
366
367 lemma fresh_vclose_tm_aux : βˆ€u,x,k.x βˆ‰ FV (vclose_tm_aux u x k).
368 #u #x elim u //
369 [ #n #k normalize cases (leb k n) normalize //
370 | #x0 #k normalize cases (true_or_false (x0==x)) #H >H normalize //
371   lapply (\Pf H) @not_to_not #Hin >(in_list_singleton ??? Hin) %
372 | #v1 #v2 #IH1 #IH2 #k normalize % #Hin cases (in_list_append_to_or_in_list ???? Hin) /2/ ]
373 qed.
374
375 lemma fresh_vclose_tm : βˆ€u,x.x βˆ‰ FV (Ξ½x.u). //
376 qed.
377
378 lemma check_tm_true_to_toc : βˆ€u,k.check_tm u k = true β†’ tm_or_ctx k u.
379 #u @(pretm_ind_plus ???? [ ] ? u)
380 [ #x #k #_ %2
381 | #n #k change with (leb (S n) k) in βŠ’ (??%?β†’?); #H % @leb_true_to_le //
382 | #v1 #v2 #rv1 #rv2 #k change with (pretm_ind_plus ???????) in βŠ’ (??%?β†’?);
383   >pretm_ind_plus_app #H cases (andb_true ?? H) -H #Hv1 #Hv2 %3
384   [ @rv1 @Hv1 | @rv2 @Hv2 ]
385 | #x #s #v #Hx #_ #rv #k change with (pretm_ind_plus ???????) in βŠ’ (??%?β†’?); 
386   >pretm_ind_plus_lam // #Hv %4 @rv @Hv ]
387 qed.
388
389 lemma toc_to_check_tm_true : βˆ€u,k.tm_or_ctx k u β†’ check_tm u k = true.
390 #u #k #Hu elim Hu //
391 [ #n #Hn change with (leb (S n) k) in βŠ’ (??%?); @le_to_leb_true @Hn
392 | #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 change with (pretm_ind_plus ???????) in βŠ’ (??%?);
393   >pretm_ind_plus_app change with (check_tm v1 k βˆ§ check_tm v2 k) in βŠ’ (??%?); /2/
394 | #x #s #v #Hv #IH <(vclose_vopen x v) change with (pretm_ind_plus ???????) in βŠ’ (??%?);
395   >pretm_ind_plus_lam [| // | @fresh_vclose_tm ] >(vclose_vopen x v) @IH ]
396 qed.
397
398 lemma fresh_swap_tm : βˆ€z1,z2,u.z1 βˆ‰ FV u β†’ z2 βˆ‰ FV u β†’ swap π”Έ z1 z2 Β· u = u.
399 #z1 #z2 #u elim u
400 [2: normalize in βŠ’ (?β†’%β†’%β†’?); #x #Hz1 #Hz2 whd in βŠ’ (??%?); >swap_other //
401   [ @(not_to_not β€¦ Hz2) | @(not_to_not β€¦ Hz1) ] //
402 |1: //
403 | #s #v #IH normalize #Hz1 #Hz2 >IH // [@Hz2|@Hz1]
404 | #v1 #v2 #IH1 #IH2 normalize #Hz1 #Hz2
405   >IH1 [| @(not_to_not β€¦ Hz2) @in_list_to_in_list_append_l | @(not_to_not β€¦ Hz1) @in_list_to_in_list_append_l ]
406   >IH2 // [@(not_to_not β€¦ Hz2) @in_list_to_in_list_append_r | @(not_to_not β€¦ Hz1) @in_list_to_in_list_append_r ]
407 ]
408 qed.
409
410 theorem tm_to_tm2 : βˆ€u.tm u β†’ tm2 u.
411 #t #Ht elim Ht
412 [ #n #Hn cases (not_le_Sn_O n) #Hfalse cases (Hfalse Hn)
413 | @tm_par
414 | #u #v #Hu #Hv @tm_app
415 | #x #s #u #Hu #IHu <(vclose_vopen x u) @tm_lam
416   [ @fresh_vclose_tm
417   | #y #Hy <(fresh_swap_tm x y (Ξ½x.u)) /2/ @fresh_vclose_tm ]
418 ]
419 qed.
420
421 theorem tm2_to_tm : βˆ€u.tm2 u β†’ tm u.
422 #u #pu elim pu /2/ #x #s #v #Hx #Hv #IH %4 @IH //
423 qed.
424
425 (* define PAR APP LAM *)
426 definition PAR β‰ Ξ»x.mk_TM (par x) ?. // qed.
427 definition APP β‰ Ξ»u,v:TM.mk_TM (app u v) ?.
428 change with (pretm_ind_plus ???????) in match (check_tm ??); >pretm_ind_plus_app
429 change with (check_tm ??) in match (pretm_ind_plus ???????); change with (check_tm ??) in match (pretm_ind_plus ???????) in βŠ’ (??(??%)?);
430 @andb_elim >(tm_of_TM u) >(tm_of_TM v) % qed.
431 definition LAM β‰ Ξ»x,s.Ξ»u:TM.mk_TM (lam x s u) ?.
432 change with (pretm_ind_plus ???????) in match (check_tm ??); <(vclose_vopen x u)
433 >pretm_ind_plus_lam [| // | @fresh_vclose_tm ]
434 change with (check_tm ??) in match (pretm_ind_plus ???????); >vclose_vopen
435 @(tm_of_TM u) qed.
436
437 axiom vopen_tm_down : βˆ€u,x,k.tm_or_ctx (S k) u β†’ tm_or_ctx k (u⌈xβŒ‰).
438 (* needs true_plus_false
439
440 #u #x #k #Hu elim Hu
441 [ #n #Hn normalize cases (true_or_false (eqb n O)) #H >H [%2]
442   normalize >(?: leb n O = false) [|cases n in H; // >eqb_n_n #H destruct (H) ]
443   normalize lapply Hn cases n in H; normalize [ #Hfalse destruct (Hfalse) ]
444   #n0 #_ #Hn0 % @le_S_S_to_le //
445 | #x0 %2
446 | #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 %3 //
447 | #x0 #s #v #Hv #IH normalize @daemon
448 ]
449 qed.
450 *)
451
452 definition vopen_TM β‰ Ξ»u:CTX.Ξ»x.mk_TM (u⌈xβŒ‰) ?.
453 @toc_to_check_tm_true @vopen_tm_down @check_tm_true_to_toc @ctx_of_CTX qed.
454
455 axiom vclose_tm_up : βˆ€u,x,k.tm_or_ctx k u β†’ tm_or_ctx (S k) (Ξ½x.u).
456
457 definition vclose_TM β‰ Ξ»u:TM.Ξ»x.mk_CTX (Ξ½x.u) ?. 
458 @toc_to_check_tm_true @vclose_tm_up @check_tm_true_to_toc @tm_of_TM qed.
459
460 interpretation "ln wf term variable open" 'open u x = (vopen_TM u x).
461 interpretation "ln wf term variable close" 'nu x u = (vclose_TM u x).
462
463 theorem tm_alpha : βˆ€x,y,s,u.x βˆ‰ FV u β†’ y βˆ‰ FV u β†’ lam x s (u⌈xβŒ‰) = lam y s (u⌈yβŒ‰).
464 #x #y #s #u #Hx #Hy whd in βŠ’ (??%%); @eq_f >nominal_eta // >nominal_eta //
465 qed.
466
467 lemma TM_to_tm2 : βˆ€u:TM.tm2 u.
468 #u @tm_to_tm2 @check_tm_true_to_toc @tm_of_TM qed.
469
470 theorem TM_ind_plus_weak : 
471  βˆ€P:pretm β†’ Type[0].
472    (βˆ€x:𝔸.P (PAR x)) β†’ 
473    (βˆ€v1,v2:TM.P v1 β†’ P v2 β†’ P (APP v1 v2)) β†’ 
474    βˆ€C:list π”Έ.
475    (βˆ€x,s.βˆ€v:CTX.x βˆ‰ FV v β†’ x βˆ‰ C β†’ 
476      (βˆ€y.y βˆ‰ FV v β†’ P (v⌈yβŒ‰)) β†’ P (LAM x s (v⌈xβŒ‰))) β†’
477  βˆ€u:TM.P u.
478 #P #Hpar #Happ #C #Hlam #u elim (TM_to_tm2 u) //
479 [ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β€¦) (mk_TM β€¦) IH1 IH2)
480   @toc_to_check_tm_true @tm2_to_tm //
481 | #x #s #v #Hx #pv #IH
482   lapply (p_fresh β€¦ (C@FV v)) letin x0 β‰ (N_fresh β€¦ (C@FV v)) #Hx0
483   >(?:lam x s (v⌈xβŒ‰) = lam x0 s (v⌈x0βŒ‰))
484   [|@tm_alpha // @(not_to_not β€¦ Hx0) @in_list_to_in_list_append_r ]
485   @(Hlam x0 s (mk_CTX v ?) ??)
486   [ <(nominal_eta β€¦ Hx) @toc_to_check_tm_true @vclose_tm_up @tm2_to_tm @pv //
487   | @(not_to_not β€¦ Hx0) @in_list_to_in_list_append_r
488   | @(not_to_not β€¦ Hx0) @in_list_to_in_list_append_l
489   | @IH ]
490 ]
491 qed.
492
493 lemma eq_mk_TM : βˆ€u,v.u = v β†’ βˆ€pu,pv.mk_TM u pu = mk_TM v pv.
494 #u #v #Heq >Heq #pu #pv %
495 qed.
496
497 lemma eq_P : βˆ€T:Type[0].βˆ€t1,t2:T.t1 = t2 β†’ βˆ€P:T β†’ Type[0].P t1 β†’ P t2. // qed.
498
499 theorem TM_ind_plus :
500  βˆ€P:TM β†’ Type[0].
501    (βˆ€x:𝔸.P (PAR x)) β†’ 
502    (βˆ€v1,v2:TM.P v1 β†’ P v2 β†’ P (APP v1 v2)) β†’ 
503    βˆ€C:list π”Έ.
504    (βˆ€x,s.βˆ€v:CTX.x βˆ‰ FV v β†’ x βˆ‰ C β†’ 
505      (βˆ€y.y βˆ‰ FV v β†’ P (v⌈yβŒ‰)) β†’ P (LAM x s (v⌈xβŒ‰))) β†’
506  βˆ€u:TM.P u.
507 #P #Hpar #Happ #C #Hlam * #u #pu
508 >(?:mk_TM u pu = 
509     mk_TM u (toc_to_check_tm_true β€¦ (tm2_to_tm β€¦ (tm_to_tm2 β€¦ (check_tm_true_to_toc β€¦ pu))))) [|%]
510 elim (tm_to_tm2 u ?) //
511 [ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β€¦) (mk_TM β€¦) IH1 IH2)
512 | #x #s #v #Hx #pv #IH
513   lapply (p_fresh β€¦ (C@FV v)) letin x0 β‰ (N_fresh β€¦ (C@FV v)) #Hx0
514   lapply (Hlam x0 s (mk_CTX v ?) ???) 
515   [2: @(not_to_not β€¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_l @Hx0
516   |4: @toc_to_check_tm_true <(nominal_eta x v) // @vclose_tm_up @tm2_to_tm @pv // 
517   | #y #Hy whd in match (vopen_TM ??);
518     >(?:mk_TM (v⌈yβŒ‰) ? = mk_TM (v⌈yβŒ‰) (toc_to_check_tm_true (v⌈yβŒ‰) O (tm2_to_tm (v⌈yβŒ‰) (pv y Hy))))
519     [@IH|%]
520   | @(not_to_not β€¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_r @Hx0 
521   | @eq_P @eq_mk_TM whd in match (vopen_TM ??); @tm_alpha // @(not_to_not β€¦ Hx0) @in_list_to_in_list_append_r ]
522 ]
523 qed.
524
525 notation 
526 "hvbox('nominal' u 'return' out 'with' 
527        [ 'xpar' ident x β‡’ f1 
528        | 'xapp' ident v1 ident v2 ident recv1 ident recv2 β‡’ f2 
529        | 'xlam' β¨ident y # C❩ ident s ident w ident py1 ident py2 ident recw β‡’ f3 ])"
530 with precedence 48 
531 for @{ TM_ind_plus $out (Ξ»${ident x}:?.$f1)
532        (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
533        $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident recw}:?.$f3)
534        $u }.
535        
536 (* include "basics/jmeq.ma".*)
537
538 definition subst β‰ (Ξ»u:TM.Ξ»x,v.
539   nominal u return (Ξ»_.TM) with 
540   [ xpar x0 β‡’ match x == x0 with [ true β‡’ v | false β‡’ PAR x0 ]  (* u instead of PAR x0 does not work, u stays the same at every rec call! *)
541   | xapp v1 v2 recv1 recv2 β‡’ APP recv1 recv2
542   | xlam β¨y # x::FV v❩ s w py1 py2 recw β‡’ LAM y s (recw y py1) ]).
543   
544 lemma subst_def : βˆ€u,x,v.subst u x v =
545   nominal u return (Ξ»_.TM) with 
546   [ xpar x0 β‡’ match x == x0 with [ true β‡’ v | false β‡’ PAR x0 ]
547   | xapp v1 v2 recv1 recv2 β‡’ APP recv1 recv2
548   | xlam β¨y # x::FV v❩ s w py1 py2 recw β‡’ LAM y s (recw y py1) ]. //
549 qed.
550
551 axiom TM_ind_plus_LAM : 
552   βˆ€x,s,u,out,f1,f2,C,f3,Hx1,Hx2.
553   TM_ind_plus out f1 f2 C f3 (LAM x s (u⌈xβŒ‰)) = 
554   f3 x s u Hx1 Hx2 (Ξ»y,Hy.TM_ind_plus ? f1 f2 C f3 ?).
555   
556 axiom TM_ind_plus_APP : 
557   βˆ€u1,u2,out,f1,f2,C,f3.
558   TM_ind_plus out f1 f2 C f3 (APP u1 u2) = 
559   f2 u1 u2 (TM_ind_plus out f1 f2 C f3 ?) (TM_ind_plus out f1 f2 C f3 ?).
560   
561 lemma eq_mk_CTX : βˆ€u,v.u = v β†’ βˆ€pu,pv.mk_CTX u pu = mk_CTX v pv.
562 #u #v #Heq >Heq #pu #pv %
563 qed.
564
565 lemma vclose_vopen_TM : βˆ€x.βˆ€u:TM.((Ξ½x.u)⌈xβŒ‰) = u.
566 #x * #u #pu @eq_mk_TM @vclose_vopen qed.
567
568 lemma nominal_eta_CTX : βˆ€x.βˆ€u:CTX.x βˆ‰ FV u β†’ (Ξ½x.(u⌈xβŒ‰)) = u.
569 #x * #u #pu #Hx @eq_mk_CTX @nominal_eta // qed. 
570
571 theorem TM_alpha : βˆ€x,y,s.βˆ€u:CTX.x βˆ‰ FV u β†’ y βˆ‰ FV u β†’ LAM x s (u⌈xβŒ‰) = LAM y s (u⌈yβŒ‰).
572 #x #y #s #u #Hx #Hy @eq_mk_TM @tm_alpha // qed.
573
574 axiom in_vopen_CTX : βˆ€x,y.βˆ€v:CTX.x βˆˆ FV (v⌈yβŒ‰) β†’ x = y βˆ¨ x βˆˆ FV v.
575
576 theorem subst_fresh : βˆ€u,v:TM.βˆ€x.x βˆ‰ FV u β†’ subst u x v = u.
577 #u #v #x @(TM_ind_plus β€¦ (x::FV v) β€¦ u)
578 [ #x0 normalize in βŠ’ (%β†’?); #Hx normalize in βŠ’ (??%?);
579   >(\bf ?) [| @(not_to_not β€¦ Hx) #Heq >Heq % ] %
580 | #u1 #u2 #IH1 #IH2 normalize in βŠ’ (%β†’?); #Hx
581   >subst_def >TM_ind_plus_APP @eq_mk_TM @eq_f2 @eq_f
582   [ <subst_def @IH1 @(not_to_not β€¦ Hx) @in_list_to_in_list_append_l
583   | <subst_def @IH2 @(not_to_not β€¦ Hx) @in_list_to_in_list_append_r ]
584 | #x0 #s #v0 #Hx0 #HC #IH #Hx >subst_def >TM_ind_plus_LAM [|@HC|@Hx0]
585   @eq_f <subst_def @IH // @(not_to_not β€¦ Hx) -Hx #Hx
586   change with (FV (Ξ½x0.(v0⌈x0βŒ‰))) in βŠ’ (???%); >nominal_eta_CTX //
587   cases (in_vopen_CTX β€¦ Hx) // #Heq >Heq in HC; * #HC @False_ind @HC %
588 ]
589 qed.
590
591 example subst_LAM_same : βˆ€x,s,u,v. subst (LAM x s u) x v = LAM x s u.
592 #x #s #u #v >subst_def <(vclose_vopen_TM x u)
593 lapply (p_fresh β€¦ (FV (Ξ½x.u)@x::FV v)) letin x0 β‰ (N_fresh β€¦ (FV (Ξ½x.u)@x::FV v)) #Hx0
594 >(TM_alpha x x0)
595 [| @(not_to_not β€¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_l @Hx0 | @fresh_vclose_tm ]
596 >TM_ind_plus_LAM [| @(not_to_not β€¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_r @Hx0 | @(not_to_not β€¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_l @Hx0 ]
597 @eq_f change with (subst ((Ξ½x.u)⌈x0βŒ‰) x v) in βŠ’ (??%?); @subst_fresh
598 @(not_to_not β€¦ Hx0) #Hx0' cases (in_vopen_CTX β€¦ Hx0') 
599 [ #Heq >Heq @in_list_to_in_list_append_r %
600 | #Hfalse @False_ind cases (fresh_vclose_tm u x) #H @H @Hfalse ]
601 qed.
602
603 (*
604 notation > "Ξ› ident x. ident T [ident x] β†¦ P"
605   with precedence 48 for @{'foo (Ξ»${ident x}.Ξ»${ident T}.$P)}.
606
607 notation < "Ξ› ident x. ident T [ident x] β†¦ P"
608   with precedence 48 for @{'foo (Ξ»${ident x}:$Q.Ξ»${ident T}:$R.$P)}.
609 *)
610
611 (*
612 notation 
613 "hvbox('nominal' u 'with' 
614        [ 'xpar' ident x β‡’ f1 
615        | 'xapp' ident v1 ident v2  β‡’ f2
616        | 'xlam' ident x # C s w β‡’ f3 ])"
617 with precedence 48 
618 for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1) 
619  (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
620  $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 ??) }.
621 *)
622
623 (*
624 notation 
625 "hvbox('nominal' u 'with' 
626        [ 'xpar' ident x ^ f1 
627        | 'xapp' ident v1 ident v2 ^ f2 ])"
628 (*       | 'xlam' ident x # C s w ^ f3 ]) *)
629 with precedence 48 
630 for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1) 
631  (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
632  $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 ??) }.
633 *)
634 notation 
635 "hvbox('nominal' u 'with' 
636        [ 'xpar' ident x ^ f1 
637        | 'xapp' ident v1 ident v2 ^ f2 ])"
638 with precedence 48 
639 for @{ tm2_ind_plus ? (Ξ»${ident x}:?.$f1) 
640  (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
641  $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 ??) }.
642
643 axiom in_Env : π”Έ Γ— tp β†’ Env β†’ Prop.
644 notation "X β—ƒ G" non associative with precedence 45 for @{'lefttriangle $X $G}.
645 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
646
647
648
649 inductive judg : list tp β†’ tm β†’ tp β†’ Prop β‰ 
650 | t_var : βˆ€g,n,t.Nth ? n g = Some ? t β†’ judg g (var n) t
651 | t_app : βˆ€g,m,n,t,u.judg g m (arr t u) β†’ judg g n t β†’ judg g (app m n) u
652 | t_abs : βˆ€g,t,m,u.judg (t::g) m u β†’ judg g (abs t m) (arr t u).
653
654 definition Env := list (𝔸 Γ— tp).
655
656 axiom vclose_env : Env β†’ list tp.
657 axiom vclose_tm : Env β†’ tm β†’ tm.
658 axiom Lam : π”Έ β†’ tp β†’ tm β†’ tm.
659 definition Judg β‰ Ξ»G,M,T.judg (vclose_env G) (vclose_tm G M) T.
660 definition dom β‰ Ξ»G:Env.map ?? (fst ??) G.
661
662 definition sctx β‰ π”Έ Γ— tm.
663 axiom swap_tm : π”Έ β†’ π”Έ β†’ tm β†’ tm.
664 definition sctx_app : sctx β†’ π”Έ β†’ tm β‰ Ξ»M0,Y.let βŒ©X,MβŒͺ β‰ M0 in swap_tm X Y M.
665
666 axiom in_list : βˆ€A:Type[0].A β†’ list A β†’ Prop.
667 interpretation "list membership" 'mem x l = (in_list ? x l).
668 interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
669
670 axiom in_Env : π”Έ Γ— tp β†’ Env β†’ Prop.
671 notation "X β—ƒ G" non associative with precedence 45 for @{'lefttriangle $X $G}.
672 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
673
674 (* axiom Lookup : π”Έ β†’ Env β†’ option tp. *)
675
676 (* forma alto livello del judgment
677    t_abs* : βˆ€G,T,X,M,U.
678             (βˆ€Y βˆ‰ supp(M).Judg (〈Y,TβŒͺ::G) (M[Y]) U) β†’ 
679             Judg G (Lam X T (M[X])) (arr T U) *)
680
681 (* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
682
683 axiom Judg_ind : βˆ€P:Env β†’ tm β†’ tp β†’ Prop.
684   (βˆ€X,G,T.〈X,TβŒͺ β—ƒ G β†’ P G (par X) T) β†’ 
685   (βˆ€G,M,N,T,U.
686     Judg G M (arr T U) β†’ Judg G N T β†’ 
687     P G M (arr T U) β†’ P G N T β†’ P G (app M N) U) β†’ 
688   (βˆ€G,T1,T2,X,M1.
689     (βˆ€Y.Y βˆ‰ (FV (Lam X T1 (sctx_app M1 X))) β†’ Judg (〈Y,T1βŒͺ::G) (sctx_app M1 Y) T2) β†’
690     (βˆ€Y.Y βˆ‰ (FV (Lam X T1 (sctx_app M1 X))) β†’ P (〈Y,T1βŒͺ::G) (sctx_app M1 Y) T2) β†’ 
691     P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) β†’ 
692   βˆ€G,M,T.Judg G M T β†’ P G M T.
693
694 axiom t_par : βˆ€X,G,T.〈X,TβŒͺ β—ƒ G β†’ Judg G (par X) T.
695 axiom t_app2 : βˆ€G,M,N,T,U.Judg G M (arr T U) β†’ Judg G N T β†’ Judg G (app M N) U.
696 axiom t_Lam : βˆ€G,X,M,T,U.Judg (〈X,TβŒͺ::G) M U β†’ Judg G (Lam X T M) (arr T U).
697
698 definition subenv β‰ Ξ»G1,G2.βˆ€x.x β—ƒ G1 β†’ x β—ƒ G2.
699 interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
700
701 axiom daemon : βˆ€P:Prop.P.
702
703 theorem weakening : βˆ€G1,G2,M,T.G1 βŠ† G2 β†’ Judg G1 M T β†’ Judg G2 M T.
704 #G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (βˆ€G2.?)
705 @(Judg_ind β€¦ HJ)
706 [ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
707 | #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
708   [| @IH1 // | @IH2 // ]
709 | #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH 
710   [ (* trivial property of Lam *) @daemon 
711   | (* trivial property of subenv *) @daemon ]
712 ]
713 qed.
714
715 (* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e
716    ricorsione *)