matita/matita/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 *)