notation "hvbox(a break β b)" non associative with precedence 45
for @{ 'mem $a $b }.
+notation "hvbox(a break β b)" non associative with precedence 45
+for @{ 'notmem $a $b }.
+
notation "hvbox(a break β¬ b)" non associative with precedence 45
for @{ 'overlaps $a $b }. (* \between *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/lists/list.ma".
+
+axiom alpha : Type[0].
+notation "πΈ" non associative with precedence 90 for @{'alphabet}.
+interpretation "set of names" 'alphabet = alpha.
+
+inductive tp : Type[0] β
+| top : tp
+| arr : tp β tp β tp.
+inductive tm : Type[0] β
+| var : nat β tm
+| par : πΈ β tm
+| abs : tp β tm β tm
+| app : tm β tm β tm.
+
+let rec Nth T n (l:list T) on n β
+ match l with
+ [ nil β None ?
+ | cons hd tl β match n with
+ [ O β Some ? hd
+ | S n0 β Nth T n0 tl ] ].
+
+inductive judg : list tp β tm β tp β Prop β
+| t_var : βg,n,t.Nth ? n g = Some ? t β judg g (var n) t
+| t_app : βg,m,n,t,u.judg g m (arr t u) β judg g n t β judg g (app m n) u
+| t_abs : βg,t,m,u.judg (t::g) m u β judg g (abs t m) (arr t u).
+
+definition Env := list (πΈ Γ tp).
+
+axiom vclose_env : Env β list tp.
+axiom vclose_tm : Env β tm β tm.
+axiom Lam : πΈ β tp β tm β tm.
+definition Judg β Ξ»G,M,T.judg (vclose_env G) (vclose_tm G M) T.
+definition dom β Ξ»G:Env.map ?? (fst ??) G.
+
+definition sctx β πΈ Γ tm.
+axiom swap_tm : πΈ β πΈ β tm β tm.
+definition sctx_app : sctx β πΈ β tm β Ξ»M0,Y.let β©X,Mβͺ β M0 in swap_tm X Y M.
+
+axiom in_list : βA:Type[0].A β list A β Prop.
+interpretation "list membership" 'mem x l = (in_list ? x l).
+interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
+
+axiom in_Env : πΈ Γ tp β Env β Prop.
+notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
+interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
+
+let rec FV M β match M with
+ [ par X β [X]
+ | app M1 M2 β FV M1@FV M2
+ | abs T M0 β FV M0
+ | _ β [ ] ].
+
+(* axiom Lookup : πΈ β Env β option tp. *)
+
+(* forma alto livello del judgment
+ t_abs* : βG,T,X,M,U.
+ (βY β supp(M).Judg (β©Y,Tβͺ::G) (M[Y]) U) β
+ Judg G (Lam X T (M[X])) (arr T U) *)
+
+(* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
+
+axiom Judg_ind : βP:Env β tm β tp β Prop.
+ (βX,G,T.β©X,Tβͺ β G β P G (par X) T) β
+ (βG,M,N,T,U.
+ Judg G M (arr T U) β Judg G N T β
+ P G M (arr T U) β P G N T β P G (app M N) U) β
+ (βG,T1,T2,X,M1.
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β Judg (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β P (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) β
+ βG,M,T.Judg G M T β P G M T.
+
+axiom t_par : βX,G,T.β©X,Tβͺ β G β Judg G (par X) T.
+axiom t_app2 : βG,M,N,T,U.Judg G M (arr T U) β Judg G N T β Judg G (app M N) U.
+axiom t_Lam : βG,X,M,T,U.Judg (β©X,Tβͺ::G) M U β Judg G (Lam X T M) (arr T U).
+
+definition subenv β Ξ»G1,G2.βx.x β G1 β x β G2.
+interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
+
+axiom daemon : βP:Prop.P.
+
+theorem weakening : βG1,G2,M,T.G1 β G2 β Judg G1 M T β Judg G2 M T.
+#G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (βG2.?)
+@(Judg_ind β¦ HJ)
+[ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
+| #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
+ [| @IH1 // | @IH2 // ]
+| #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
+ [ (* trivial property of Lam *) @daemon
+ | (* trivial property of subenv *) @daemon ]
+]
+qed.
+
+(* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e
+ ricorsione *)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "binding/names.ma".
+
+(* permutations *)
+definition finite_perm : βX:Nset.(X β X) β Prop β
+ Ξ»X,f.injective X X f β§ surjective X X f β§ βl.βx.x β l β f x = x.
+
+(* maps a permutation to a list of parameters *)
+definition Pi_list : βX:Nset.(X β X) β list X β list X β
+ Ξ»X,p,xl.map ?? (Ξ»x.p x) xl.
+
+interpretation "permutation of X list" 'middot p x = (Pi_list p x).
+
+definition swap : βN:Nset.N β N β N β N β
+ Ξ»N,u,v,x.match (x == u) with
+ [true β v
+ |false β match (x == v) with
+ [true β u
+ |false β x]].
+
+axiom swap_right : βN,x,y.swap N x y y = x.
+(*
+#N x y;nnormalize;nrewrite > (p_eqb3 ? y y β¦);//;
+nlapply (refl ? (y β x));ncases (y β x) in β’ (???% β %);nnormalize;//;
+#H1;napply p_eqb1;//;
+nqed.
+*)
+
+axiom swap_left : βN,x,y.swap N x y x = y.
+(*
+#N x y;nnormalize;nrewrite > (p_eqb3 ? x x β¦);//;
+nqed.
+*)
+
+axiom swap_other : βN,x,y,z.x β z β y β z β swap N x y z = z.
+(*
+#N x y z H1 H2;nnormalize;nrewrite > (p_eqb4 β¦);
+##[nrewrite > (p_eqb4 β¦);//;@;ncases H2;/2/;
+##|@;ncases H1;/2/
+##]
+nqed.
+*)
+
+axiom swap_inv : βN,x,y,z.swap N x y (swap N x y z) = z.
+(*
+#N x y z;nlapply (refl ? (x β z));ncases (x β z) in β’ (???% β ?);#H1
+##[nrewrite > (p_eqb1 β¦ H1);nrewrite > (swap_left β¦);//;
+##|nlapply (refl ? (y β z));ncases (y β z) in β’ (???% β ?);#H2
+ ##[nrewrite > (p_eqb1 β¦ H2);nrewrite > (swap_right β¦);//;
+ ##|nrewrite > (swap_other β¦) in β’ (??(????%)?);/2/;
+ nrewrite > (swap_other β¦);/2/;
+ ##]
+##]
+nqed.
+*)
+
+axiom swap_fp : βN,x1,x2.finite_perm ? (swap N x1 x2).
+(*
+#N x1 x2;@
+##[@
+ ##[nwhd;#xa xb;nnormalize;nlapply (refl ? (xa β x1));
+ ncases (xa β x1) in β’ (???% β %);#H1
+ ##[nrewrite > (p_eqb1 β¦ H1);nlapply (refl ? (xb β x1));
+ ncases (xb β x1) in β’ (???% β %);#H2
+ ##[nrewrite > (p_eqb1 β¦ H2);//
+ ##|nlapply (refl ? (xb β x2));
+ ncases (xb β x2) in β’ (???% β %);#H3
+ ##[nnormalize;#H4;nrewrite > H4 in H3;
+ #H3;nrewrite > H3 in H2;#H2;ndestruct (H2)
+ ##|nnormalize;#H4;nrewrite > H4 in H3;
+ nrewrite > (p_eqb3 β¦);//;#H5;ndestruct (H5)
+ ##]
+ ##]
+ ##|nlapply (refl ? (xa β x2));
+ ncases (xa β x2) in β’ (???% β %);#H2
+ ##[nrewrite > (p_eqb1 β¦ H2);nlapply (refl ? (xb β x1));
+ ncases (xb β x1) in β’ (???% β %);#H3
+ ##[nnormalize;#H4;nrewrite > H4 in H3;
+ #H3;nrewrite > (p_eqb1 β¦ H3);@
+ ##|nnormalize;nlapply (refl ? (xb β x2));
+ ncases (xb β x2) in β’ (???% β %);#H4
+ ##[nrewrite > (p_eqb1 β¦ H4);//
+ ##|nnormalize;#H5;nrewrite > H5 in H3;
+ nrewrite > (p_eqb3 β¦);//;#H6;ndestruct (H6);
+ ##]
+ ##]
+ ##|nnormalize;nlapply (refl ? (xb β x1));
+ ncases (xb β x1) in β’ (???% β %);#H3
+ ##[nnormalize;#H4;nrewrite > H4 in H2;nrewrite > (p_eqb3 β¦);//;
+ #H5;ndestruct (H5)
+ ##|nlapply (refl ? (xb β x2));
+ ncases (xb β x2) in β’ (???% β %);#H4
+ ##[nnormalize;#H5;nrewrite > H5 in H1;nrewrite > (p_eqb3 β¦);//;
+ #H6;ndestruct (H6)
+ ##|nnormalize;//
+ ##]
+ ##]
+ ##]
+ ##]
+ ##|nwhd;#z;nnormalize;nlapply (refl ? (z β x1));
+ ncases (z β x1) in β’ (???% β %);#H1
+ ##[nlapply (refl ? (z β x2));
+ ncases (z β x2) in β’ (???% β %);#H2
+ ##[@ z;nrewrite > H1;nrewrite > H2;napply p_eqb1;//
+ ##|@ x2;nrewrite > (p_eqb4 β¦);
+ ##[nrewrite > (p_eqb3 β¦);//;
+ nnormalize;napply p_eqb1;//
+ ##|nrewrite < (p_eqb1 β¦ H1);@;#H3;nrewrite > H3 in H2;
+ nrewrite > (p_eqb3 β¦);//;#H2;ndestruct (H2)
+ ##]
+ ##]
+ ##|nlapply (refl ? (z β x2));
+ ncases (z β x2) in β’ (???% β %);#H2
+ ##[@ x1;nrewrite > (p_eqb3 β¦);//;
+ napply p_eqb1;nnormalize;//
+ ##|@ z;nrewrite > H1;nrewrite > H2;@;
+ ##]
+ ##]
+ ##]
+##|@ [x1;x2];#x0 H1;nrewrite > (swap_other β¦)
+ ##[@
+ ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;/2/;
+ ##|@;#H2;nrewrite > H2 in H1;*;#H3;napply H3;//;
+ ##]
+##]
+nqed.
+*)
+
+axiom inj_swap : βN,u,v.injective ?? (swap N u v).
+(*
+#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
+nqed.
+*)
+
+axiom surj_swap : βN,u,v.surjective ?? (swap N u v).
+(*
+#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
+nqed.
+*)
+
+axiom finite_swap : βN,u,v.βl.βx.x β l β swap N u v x = x.
+(*
+#N u v;ncases (swap_fp N u v);*;#H1 H2 H3;//;
+nqed.
+*)
+
+(* swaps two lists of parameters
+definition Pi_swap_list : βxl,xl':list X.X β X β
+ Ξ»xl,xl',x.foldr2 ??? (Ξ»u,v,r.swap ? u v r) x xl xl'.
+
+nlemma fp_swap_list :
+ βxl,xl'.finite_perm ? (Pi_swap_list xl xl').
+#xl xl';@
+##[@;
+ ##[ngeneralize in match xl';nelim xl
+ ##[nnormalize;//;
+ ##|#x0 xl0;#IH xl'';nelim xl''
+ ##[nnormalize;//
+ ##|#x1 xl1 IH1 y0 y1;nchange in β’ (??%% β ?) with (swap ????);
+ #H1;nlapply (inj_swap β¦ H1);#H2;
+ nlapply (IH β¦ H2);//
+ ##]
+ ##]
+ ##|ngeneralize in match xl';nelim xl
+ ##[nnormalize;#_;#z;@z;@
+ ##|#x' xl0 IH xl'';nelim xl''
+ ##[nnormalize;#z;@z;@
+ ##|#x1 xl1 IH1 z;
+ nchange in β’ (??(Ξ»_.???%)) with (swap ????);
+ ncases (surj_swap X x' x1 z);#x2 H1;
+ ncases (IH xl1 x2);#x3 H2;@ x3;
+ nrewrite < H2;napply H1
+ ##]
+ ##]
+ ##]
+##|ngeneralize in match xl';nelim xl
+ ##[#;@ [];#;@
+ ##|#x0 xl0 IH xl'';ncases xl''
+ ##[@ [];#;@
+ ##|#x1 xl1;ncases (IH xl1);#xl2 H1;
+ ncases (finite_swap X x0 x1);#xl3 H2;
+ @ (xl2@xl3);#x2 H3;
+ nchange in β’ (??%?) with (swap ????);
+ nrewrite > (H1 β¦);
+ ##[nrewrite > (H2 β¦);//;@;#H4;ncases H3;#H5;napply H5;
+ napply in_list_to_in_list_append_r;//
+ ##|@;#H4;ncases H3;#H5;napply H5;
+ napply in_list_to_in_list_append_l;//
+ ##]
+ ##]
+ ##]
+##]
+nqed.
+
+(* the 'reverse' swap of lists of parameters
+ composing Pi_swap_list and Pi_swap_list_r yields the identity function
+ (see the Pi_swap_list_inv lemma) *)
+ndefinition Pi_swap_list_r : βxl,xl':list X. Pi β
+ Ξ»xl,xl',x.foldl2 ??? (Ξ»r,u,v.swap ? u v r ) x xl xl'.
+
+nlemma fp_swap_list_r :
+ βxl,xl'.finite_perm ? (Pi_swap_list_r xl xl').
+#xl xl';@
+##[@;
+ ##[ngeneralize in match xl';nelim xl
+ ##[nnormalize;//;
+ ##|#x0 xl0;#IH xl'';nelim xl''
+ ##[nnormalize;//
+ ##|#x1 xl1 IH1 y0 y1;nwhd in β’ (??%% β ?);
+ #H1;nlapply (IH β¦ H1);#H2;
+ napply (inj_swap β¦ H2);
+ ##]
+ ##]
+ ##|ngeneralize in match xl';nelim xl
+ ##[nnormalize;#_;#z;@z;@
+ ##|#x' xl0 IH xl'';nelim xl''
+ ##[nnormalize;#z;@z;@
+ ##|#x1 xl1 IH1 z;nwhd in β’ (??(Ξ»_.???%));
+ ncases (IH xl1 z);#x2 H1;
+ ncases (surj_swap X x' x1 x2);#x3 H2;
+ @ x3;nrewrite < H2;napply H1;
+ ##]
+ ##]
+ ##]
+##|ngeneralize in match xl';nelim xl
+ ##[#;@ [];#;@
+ ##|#x0 xl0 IH xl'';ncases xl''
+ ##[@ [];#;@
+ ##|#x1 xl1;
+ ncases (IH xl1);#xl2 H1;
+ ncases (finite_swap X x0 x1);#xl3 H2;
+ @ (xl2@xl3);#x2 H3;nwhd in β’ (??%?);
+ nrewrite > (H2 β¦);
+ ##[nrewrite > (H1 β¦);//;@;#H4;ncases H3;#H5;napply H5;
+ napply in_list_to_in_list_append_l;//
+ ##|@;#H4;ncases H3;#H5;napply H5;
+ napply in_list_to_in_list_append_r;//
+ ##]
+ ##]
+ ##]
+##]
+nqed.
+
+nlemma Pi_swap_list_inv :
+ βxl1,xl2,x.
+ Pi_swap_list xl1 xl2 (Pi_swap_list_r xl1 xl2 x) = x.
+#xl;nelim xl
+##[#;@
+##|#x1 xl1 IH xl';ncases xl'
+ ##[#;@
+ ##|#x2 xl2;#x;
+ nchange in β’ (??%?) with
+ (swap ??? (Pi_swap_list ??
+ (Pi_swap_list_r ?? (swap ????))));
+ nrewrite > (IH xl2 ?);napply swap_inv;
+ ##]
+##]
+nqed.
+
+nlemma Pi_swap_list_fresh :
+ βx,xl1,xl2.x β xl1 β x β xl2 β Pi_swap_list xl1 xl2 x = x.
+#x xl1;nelim xl1
+##[#;@
+##|#x3 xl3 IH xl2' H1;ncases xl2'
+ ##[#;@
+ ##|#x4 xl4 H2;ncut (x β xl3 β§ x β xl4);
+ ##[@
+ ##[@;#H3;ncases H1;#H4;napply H4;/2/;
+ ##|@;#H3;ncases H2;#H4;napply H4;/2/
+ ##]
+ ##] *; #H1' H2';
+ nchange in β’ (??%?) with (swap ????);
+ nrewrite > (swap_other β¦)
+ ##[napply IH;//;
+ ##|nchange in β’ (?(???%)) with (Pi_swap_list ???);
+ nrewrite > (IH β¦);//;@;#H3;ncases H2;#H4;napply H4;//;
+ ##|nchange in β’ (?(???%)) with (Pi_swap_list ???);
+ nrewrite > (IH β¦);//;@;#H3;ncases H1;#H4;napply H4;//
+ ##]
+ ##]
+##]
+nqed.
+*)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/lists/list.ma".
+include "basics/deqsets.ma".
+include "binding/names.ma".
+include "binding/fp.ma".
+
+axiom alpha : Nset.
+notation "πΈ" non associative with precedence 90 for @{'alphabet}.
+interpretation "set of names" 'alphabet = alpha.
+
+inductive tp : Type[0] β
+| top : tp
+| arr : tp β tp β tp.
+inductive pretm : Type[0] β
+| var : nat β pretm
+| par : πΈ β pretm
+| abs : tp β pretm β pretm
+| app : pretm β pretm β pretm.
+
+let rec Nth T n (l:list T) on n β
+ match l with
+ [ nil β None ?
+ | cons hd tl β match n with
+ [ O β Some ? hd
+ | S n0 β Nth T n0 tl ] ].
+
+let rec vclose_tm_aux u x k β match u with
+ [ var n β if (leb k n) then var (S n) else u
+ | par x0 β if (x0 == x) then (var k) else u
+ | app v1 v2 β app (vclose_tm_aux v1 x k) (vclose_tm_aux v2 x k)
+ | abs s v β abs s (vclose_tm_aux v x (S k)) ].
+definition vclose_tm β Ξ»u,x.vclose_tm_aux u x O.
+
+definition vopen_var β Ξ»n,x,k.match eqb n k with
+ [ true β par x
+ | false β match leb n k with
+ [ true β var n
+ | false β var (pred n) ] ].
+
+let rec vopen_tm_aux u x k β match u with
+ [ var n β vopen_var n x k
+ | par x0 β u
+ | app v1 v2 β app (vopen_tm_aux v1 x k) (vopen_tm_aux v2 x k)
+ | abs s v β abs s (vopen_tm_aux v x (S k)) ].
+definition vopen_tm β Ξ»u,x.vopen_tm_aux u x O.
+
+let rec FV u β match u with
+ [ par x β [x]
+ | app v1 v2 β FV v1@FV v2
+ | abs s v β FV v
+ | _ β [ ] ].
+
+definition lam β Ξ»x,s,u.abs s (vclose_tm u x).
+
+let rec Pi_map_tm p u on u β match u with
+[ par x β par (p x)
+| var _ β u
+| app v1 v2 β app (Pi_map_tm p v1) (Pi_map_tm p v2)
+| abs s v β abs s (Pi_map_tm p v) ].
+
+interpretation "permutation of tm" 'middot p x = (Pi_map_tm p x).
+
+notation "hvbox(uβxβ)"
+ with precedence 45
+ for @{ 'open $u $x }.
+
+(*
+notation "hvbox(uβxβ)"
+ with precedence 45
+ for @{ 'open $u $x }.
+notation "β΄ u β΅ x" non associative with precedence 90 for @{ 'open $u $x }.
+*)
+interpretation "ln term variable open" 'open u x = (vopen_tm u x).
+notation < "hvbox(Ξ½ x break . u)"
+ with precedence 20
+for @{'nu $x $u }.
+notation > "Ξ½ list1 x sep , . term 19 u" with precedence 20
+ for ${ fold right @{$u} rec acc @{'nu $x $acc)} }.
+interpretation "ln term variable close" 'nu x u = (vclose_tm u x).
+
+let rec tm_height u β match u with
+[ app v1 v2 β S (max (tm_height v1) (tm_height v2))
+| abs s v β S (tm_height v)
+| _ β O ].
+
+theorem le_n_O_rect_Type0 : βn:nat. n β€ O β βP: nat βType[0]. P O β P n.
+#n (cases n) // #a #abs cases (?:False) /2/ qed.
+
+theorem nat_rect_Type0_1 : βn:nat.βP:nat β Type[0].
+(βm.(βp. p < m β P p) β P m) β P n.
+#n #P #H
+cut (βq:nat. q β€ n β P q) /2/
+(elim n)
+ [#q #HleO (* applica male *)
+ @(le_n_O_rect_Type0 ? HleO)
+ @H #p #ltpO cases (?:False) /2/ (* 3 *)
+ |#p #Hind #q #HleS
+ @H #a #lta @Hind @le_S_S_to_le /2/
+ ]
+qed.
+
+lemma leb_false_to_lt : βn,m. leb n m = false β m < n.
+#n elim n
+[ #m normalize #H destruct(H)
+| #n0 #IH * // #m normalize #H @le_S_S @IH // ]
+qed.
+
+lemma nominal_eta_aux : βx,u.x β FV u β βk.vclose_tm_aux (vopen_tm_aux u x k) x k = u.
+#x #u elim u
+[ #n #_ #k normalize cases (decidable_eq_nat n k) #Hnk
+ [ >Hnk >eqb_n_n normalize >(\b ?) //
+ | >(not_eq_to_eqb_false β¦ Hnk) normalize cases (true_or_false (leb n k)) #Hleb
+ [ >Hleb normalize >(?:leb k n = false) //
+ @lt_to_leb_false @not_eq_to_le_to_lt /2/
+ | >Hleb normalize >(?:leb k (pred n) = true) normalize
+ [ cases (leb_false_to_lt β¦ Hleb) //
+ | @le_to_leb_true cases (leb_false_to_lt β¦ Hleb) normalize /2/ ] ] ]
+| #y normalize #Hy >(\bf ?) // @(not_to_not β¦ Hy) //
+| #s #v #IH normalize #Hv #k >IH // @Hv
+| #v1 #v2 #IH1 #IH2 normalize #Hv1v2 #k
+ >IH1 [ >IH2 // | @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_l ]
+ @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_r ]
+qed.
+
+corollary nominal_eta : βx,u.x β FV u β (Ξ½x.uβxβ) = u.
+#x #u #Hu @nominal_eta_aux //
+qed.
+
+lemma eq_height_vopen_aux : βv,x,k.tm_height (vopen_tm_aux v x k) = tm_height v.
+#v #x elim v
+[ #n #k normalize cases (eqb n k) // cases (leb n k) //
+| #u #k %
+| #s #u #IH #k normalize >IH %
+| #u1 #u2 #IH1 #IH2 #k normalize >IH1 >IH2 % ]
+qed.
+
+corollary eq_height_vopen : βv,x.tm_height (vβxβ) = tm_height v.
+#v #x @eq_height_vopen_aux
+qed.
+
+theorem pretm_ind_plus_aux :
+ βP:pretm β Type[0].
+ (βx:πΈ.P (par x)) β
+ (βn:β.P (var n)) β
+ (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
+ βC:list πΈ.
+ (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
+ βn,u.tm_height u β€ n β P u.
+#P #Hpar #Hvar #Happ #C #Hlam #n change with ((Ξ»n.?) n); @(nat_rect_Type0_1 n ??)
+#m cases m
+[ #_ * /2/
+ [ normalize #s #v #Hfalse cases (?:False) cases (not_le_Sn_O (tm_height v)) /2/
+ | #v1 #v2 whd in β’ (?%?β?); #Hfalse cases (?:False) cases (not_le_Sn_O (max ??))
+ [ #H @H @Hfalse|*:skip] ] ]
+-m #m #IH * /2/
+[ #s #v whd in β’ (?%?β?); #Hv
+ lapply (p_fresh β¦ (C@FV v)) letin y β (N_fresh β¦ (C@FV v)) #Hy
+ >(?:abs s v = lam y s (vβyβ))
+ [| whd in β’ (???%); >nominal_eta // @(not_to_not β¦ Hy) @in_list_to_in_list_append_r ]
+ @Hlam
+ [ @(not_to_not β¦ Hy) @in_list_to_in_list_append_r
+ | @(not_to_not β¦ Hy) @in_list_to_in_list_append_l ]
+ @IH [| @Hv | >eq_height_vopen % ]
+| #v1 #v2 whd in β’ (?%?β?); #Hv @Happ
+ [ @IH [| @Hv | @le_max_1 ] | @IH [| @Hv | @le_max_2 ] ] ]
+qed.
+
+corollary pretm_ind_plus :
+ βP:pretm β Type[0].
+ (βx:πΈ.P (par x)) β
+ (βn:β.P (var n)) β
+ (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
+ βC:list πΈ.
+ (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
+ βu.P u.
+#P #Hpar #Hvar #Happ #C #Hlam #u @pretm_ind_plus_aux /2/
+qed.
+
+(* maps a permutation to a list of terms *)
+definition Pi_map_list : (πΈ β πΈ) β list πΈ β list πΈ β map πΈ πΈ .
+
+(* interpretation "permutation of name list" 'middot p x = (Pi_map_list p x).*)
+
+(*
+inductive tm : pretm β Prop β
+| tm_par : βx:πΈ.tm (par x)
+| tm_app : βu,v.tm u β tm v β tm (app u v)
+| tm_lam : βx,s,u.tm u β tm (lam x s u).
+
+inductive ctx_aux : nat β pretm β Prop β
+| ctx_var : βn,k.n < k β ctx_aux k (var n)
+| ctx_par : βx,k.ctx_aux k (par x)
+| ctx_app : βu,v,k.ctx_aux k u β ctx_aux k v β ctx_aux k (app u v)
+(* Γ¨ sostituibile da ctx_lam ? *)
+| ctx_abs : βs,u.ctx_aux (S k) u β ctx_aux k (abs s u).
+*)
+
+inductive tm_or_ctx (k:nat) : pretm β Type[0] β
+| toc_var : βn.n < k β tm_or_ctx k (var n)
+| toc_par : βx.tm_or_ctx k (par x)
+| toc_app : βu,v.tm_or_ctx k u β tm_or_ctx k v β tm_or_ctx k (app u v)
+| toc_lam : βx,s,u.tm_or_ctx k u β tm_or_ctx k (lam x s u).
+
+definition tm β Ξ»t.tm_or_ctx O t.
+definition ctx β Ξ»t.tm_or_ctx 1 t.
+
+definition check_tm β Ξ»u,k.
+ pretm_ind_plus ?
+ (Ξ»_.true)
+ (Ξ»n.leb (S n) k)
+ (Ξ»v1,v2,rv1,rv2.rv1 β§ rv2)
+ [] (Ξ»x,s,v,px,pC,rv.rv)
+ u.
+
+axiom pretm_ind_plus_app : βP,u,v,C,H1,H2,H3,H4.
+ pretm_ind_plus P H1 H2 H3 C H4 (app u v) =
+ H3 u v (pretm_ind_plus P H1 H2 H3 C H4 u) (pretm_ind_plus P H1 H2 H3 C H4 v).
+
+axiom pretm_ind_plus_lam : βP,x,s,u,C,px,pC,H1,H2,H3,H4.
+ pretm_ind_plus P H1 H2 H3 C H4 (lam x s (uβxβ)) =
+ H4 x s u px pC (pretm_ind_plus P H1 H2 H3 C H4 (uβxβ)).
+
+record TM : Type[0] β {
+ pretm_of_TM :> pretm;
+ tm_of_TM : check_tm pretm_of_TM O = true
+}.
+
+record CTX : Type[0] β {
+ pretm_of_CTX :> pretm;
+ ctx_of_CTX : check_tm pretm_of_CTX 1 = true
+}.
+
+inductive tm2 : pretm β Type[0] β
+| tm_par : βx.tm2 (par x)
+| tm_app : βu,v.tm2 u β tm2 v β tm2 (app u v)
+| tm_lam : βx,s,u.x β FV u β (βy.y β FV u β tm2 (uβyβ)) β tm2 (lam x s (uβxβ)).
+
+(*
+inductive tm' : pretm β Prop β
+| tm_par : βx.tm' (par x)
+| tm_app : βu,v.tm' u β tm' v β tm' (app u v)
+| tm_lam : βx,s,u,C.x β FV u β x β C β (βy.y β FV u β tm' (β΄uβ΅y)) β tm' (lam x s (β΄uβ΅x)).
+*)
+
+lemma pi_vclose_tm :
+ βz1,z2,x,u.swap πΈ z1 z2Β·(Ξ½x.u) = (Ξ½ swap ? z1 z2 x.swap πΈ z1 z2 Β· u).
+#z1 #z2 #x #u
+change with (vclose_tm_aux ???) in match (vclose_tm ??);
+change with (vclose_tm_aux ???) in β’ (???%); lapply O elim u normalize //
+[ #n #k cases (leb k n) normalize %
+| #x0 #k cases (true_or_false (x0==z1)) #H1 >H1 normalize
+ [ cases (true_or_false (x0==x)) #H2 >H2 normalize
+ [ <(\P H2) >H1 normalize >(\b (refl ? z2)) %
+ | >H1 normalize cases (true_or_false (x==z1)) #H3 >H3 normalize
+ [ >(\P H3) in H2; >H1 #Hfalse destruct (Hfalse)
+ | cases (true_or_false (x==z2)) #H4 >H4 normalize
+ [ cases (true_or_false (z2==z1)) #H5 >H5 normalize //
+ >(\P H5) in H4; >H3 #Hfalse destruct (Hfalse)
+ | >(\bf ?) // @sym_not_eq @(\Pf H4) ]
+ ]
+ ]
+ | cases (true_or_false (x0==x)) #H2 >H2 normalize
+ [ <(\P H2) >H1 normalize >(\b (refl ??)) %
+ | >H1 normalize cases (true_or_false (x==z1)) #H3 >H3 normalize
+ [ cases (true_or_false (x0==z2)) #H4 >H4 normalize
+ [ cases (true_or_false (z1==z2)) #H5 >H5 normalize //
+ <(\P H5) in H4; <(\P H3) >H2 #Hfalse destruct (Hfalse)
+ | >H4 % ]
+ | cases (true_or_false (x0==z2)) #H4 >H4 normalize
+ [ cases (true_or_false (x==z2)) #H5 >H5 normalize
+ [ <(\P H5) in H4; >H2 #Hfalse destruct (Hfalse)
+ | >(\bf ?) // @sym_not_eq @(\Pf H3) ]
+ | cases (true_or_false (x==z2)) #H5 >H5 normalize
+ [ >H1 %
+ | >H2 % ]
+ ]
+ ]
+ ]
+ ]
+]
+qed.
+
+lemma pi_vopen_tm :
+ βz1,z2,x,u.swap πΈ z1 z2Β·(uβxβ) = (swap πΈ z1 z2 Β· uβswap πΈ z1 z2 xβ).
+#z1 #z2 #x #u
+change with (vopen_tm_aux ???) in match (vopen_tm ??);
+change with (vopen_tm_aux ???) in β’ (???%); lapply O elim u normalize //
+#n #k cases (true_or_false (eqb n k)) #H1 >H1 normalize //
+cases (true_or_false (leb n k)) #H2 >H2 normalize //
+qed.
+
+lemma pi_lam :
+ βz1,z2,x,s,u.swap πΈ z1 z2 Β· lam x s u = lam (swap πΈ z1 z2 x) s (swap πΈ z1 z2 Β· u).
+#z1 #z2 #x #s #u whd in β’ (???%); <(pi_vclose_tm β¦) %
+qed.
+
+lemma eqv_FV : βz1,z2,u.FV (swap πΈ z1 z2 Β· u) = Pi_map_list (swap πΈ z1 z2) (FV u).
+#z1 #z2 #u elim u //
+[ #s #v normalize //
+| #v1 #v2 normalize /2/ ]
+qed.
+
+lemma swap_inv_tm : βz1,z2,u.swap πΈ z1 z2 Β· (swap πΈ z1 z2 Β· u) = u.
+#z1 #z2 #u elim u [1,3,4:normalize //]
+#x whd in β’ (??%?); >swap_inv %
+qed.
+
+lemma eqv_in_list : βx,l,z1,z2.x β l β swap πΈ z1 z2 x β Pi_map_list (swap πΈ z1 z2) l.
+#x #l #z1 #z2 #Hin elim Hin
+[ #x0 #l0 %
+| #x1 #x2 #l0 #Hin #IH %2 @IH ]
+qed.
+
+lemma eqv_tm2 : βu.tm2 u β βz1,z2.tm2 ((swap ? z1 z2)Β·u).
+#u #Hu #z1 #z2 letin p β (swap ? z1 z2) elim Hu /2/
+#x #s #v #Hx #Hv #IH >pi_lam >pi_vopen_tm %3
+[ @(not_to_not β¦ Hx) -Hx #Hx
+ <(swap_inv ? z1 z2 x) <(swap_inv_tm z1 z2 v) >eqv_FV @eqv_in_list //
+| #y #Hy <(swap_inv ? z1 z2 y)
+ <pi_vopen_tm @IH @(not_to_not β¦ Hy) -Hy #Hy <(swap_inv ? z1 z2 y)
+ >eqv_FV @eqv_in_list //
+]
+qed.
+
+lemma vclose_vopen_aux : βx,u,k.vopen_tm_aux (vclose_tm_aux u x k) x k = u.
+#x #u elim u normalize //
+[ #n #k cases (true_or_false (leb k n)) #H >H whd in β’ (??%?);
+ [ cases (true_or_false (eqb (S n) k)) #H1 >H1
+ [ <(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_true_to_le β¦ H) -H #H
+ cases (le_to_not_lt β¦ H) -H #H cases (H ?) %
+ | whd in β’ (??%?); >lt_to_leb_false // @le_S_S /2/ ]
+ | cases (true_or_false (eqb n k)) #H1 >H1 normalize
+ [ >(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_false_to_not_le β¦ H) -H
+ * #H cases (H ?) %
+ | >le_to_leb_true // @not_lt_to_le % #H2 >le_to_leb_true in H;
+ [ #H destruct (H) | /2/ ]
+ ]
+ ]
+| #x0 #k cases (true_or_false (x0==x)) #H1 >H1 normalize // >(\P H1) >eqb_n_n % ]
+qed.
+
+lemma vclose_vopen : βx,u.((Ξ½x.u)βxβ) = u. #x #u @vclose_vopen_aux
+qed.
+
+(*
+theorem tm_to_tm : βt.tm' t β tm t.
+#t #H elim H
+*)
+
+lemma in_list_singleton : βT.βt1,t2:T.t1 β [t2] β t1 = t2.
+#T #t1 #t2 #H @(in_list_inv_ind ??? H) /2/
+qed.
+
+lemma fresh_vclose_tm_aux : βu,x,k.x β FV (vclose_tm_aux u x k).
+#u #x elim u //
+[ #n #k normalize cases (leb k n) normalize //
+| #x0 #k normalize cases (true_or_false (x0==x)) #H >H normalize //
+ lapply (\Pf H) @not_to_not #Hin >(in_list_singleton ??? Hin) %
+| #v1 #v2 #IH1 #IH2 #k normalize % #Hin cases (in_list_append_to_or_in_list ???? Hin) /2/ ]
+qed.
+
+lemma fresh_vclose_tm : βu,x.x β FV (Ξ½x.u). //
+qed.
+
+lemma check_tm_true_to_toc : βu,k.check_tm u k = true β tm_or_ctx k u.
+#u @(pretm_ind_plus ???? [ ] ? u)
+[ #x #k #_ %2
+| #n #k change with (leb (S n) k) in β’ (??%?β?); #H % @leb_true_to_le //
+| #v1 #v2 #rv1 #rv2 #k change with (pretm_ind_plus ???????) in β’ (??%?β?);
+ >pretm_ind_plus_app #H cases (andb_true ?? H) -H #Hv1 #Hv2 %3
+ [ @rv1 @Hv1 | @rv2 @Hv2 ]
+| #x #s #v #Hx #_ #rv #k change with (pretm_ind_plus ???????) in β’ (??%?β?);
+ >pretm_ind_plus_lam // #Hv %4 @rv @Hv ]
+qed.
+
+lemma toc_to_check_tm_true : βu,k.tm_or_ctx k u β check_tm u k = true.
+#u #k #Hu elim Hu //
+[ #n #Hn change with (leb (S n) k) in β’ (??%?); @le_to_leb_true @Hn
+| #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 change with (pretm_ind_plus ???????) in β’ (??%?);
+ >pretm_ind_plus_app change with (check_tm v1 k β§ check_tm v2 k) in β’ (??%?); /2/
+| #x #s #v #Hv #IH <(vclose_vopen x v) change with (pretm_ind_plus ???????) in β’ (??%?);
+ >pretm_ind_plus_lam [| // | @fresh_vclose_tm ] >(vclose_vopen x v) @IH ]
+qed.
+
+lemma fresh_swap_tm : βz1,z2,u.z1 β FV u β z2 β FV u β swap πΈ z1 z2 Β· u = u.
+#z1 #z2 #u elim u
+[2: normalize in β’ (?β%β%β?); #x #Hz1 #Hz2 whd in β’ (??%?); >swap_other //
+ [ @(not_to_not β¦ Hz2) | @(not_to_not β¦ Hz1) ] //
+|1: //
+| #s #v #IH normalize #Hz1 #Hz2 >IH // [@Hz2|@Hz1]
+| #v1 #v2 #IH1 #IH2 normalize #Hz1 #Hz2
+ >IH1 [| @(not_to_not β¦ Hz2) @in_list_to_in_list_append_l | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_l ]
+ >IH2 // [@(not_to_not β¦ Hz2) @in_list_to_in_list_append_r | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_r ]
+]
+qed.
+
+theorem tm_to_tm2 : βu.tm u β tm2 u.
+#t #Ht elim Ht
+[ #n #Hn cases (not_le_Sn_O n) #Hfalse cases (Hfalse Hn)
+| @tm_par
+| #u #v #Hu #Hv @tm_app
+| #x #s #u #Hu #IHu <(vclose_vopen x u) @tm_lam
+ [ @fresh_vclose_tm
+ | #y #Hy <(fresh_swap_tm x y (Ξ½x.u)) /2/ @fresh_vclose_tm ]
+]
+qed.
+
+theorem tm2_to_tm : βu.tm2 u β tm u.
+#u #pu elim pu /2/ #x #s #v #Hx #Hv #IH %4 @IH //
+qed.
+
+(* define PAR APP LAM *)
+definition PAR β Ξ»x.mk_TM (par x) ?. // qed.
+definition APP β Ξ»u,v:TM.mk_TM (app u v) ?.
+change with (pretm_ind_plus ???????) in match (check_tm ??); >pretm_ind_plus_app
+change with (check_tm ??) in match (pretm_ind_plus ???????); change with (check_tm ??) in match (pretm_ind_plus ???????) in β’ (??(??%)?);
+@andb_elim >(tm_of_TM u) >(tm_of_TM v) % qed.
+definition LAM β Ξ»x,s.Ξ»u:TM.mk_TM (lam x s u) ?.
+change with (pretm_ind_plus ???????) in match (check_tm ??); <(vclose_vopen x u)
+>pretm_ind_plus_lam [| // | @fresh_vclose_tm ]
+change with (check_tm ??) in match (pretm_ind_plus ???????); >vclose_vopen
+@(tm_of_TM u) qed.
+
+axiom vopen_tm_down : βu,x,k.tm_or_ctx (S k) u β tm_or_ctx k (uβxβ).
+(* needs true_plus_false
+
+#u #x #k #Hu elim Hu
+[ #n #Hn normalize cases (true_or_false (eqb n O)) #H >H [%2]
+ normalize >(?: leb n O = false) [|cases n in H; // >eqb_n_n #H destruct (H) ]
+ normalize lapply Hn cases n in H; normalize [ #Hfalse destruct (Hfalse) ]
+ #n0 #_ #Hn0 % @le_S_S_to_le //
+| #x0 %2
+| #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 %3 //
+| #x0 #s #v #Hv #IH normalize @daemon
+]
+qed.
+*)
+
+definition vopen_TM β Ξ»u:CTX.Ξ»x.mk_TM (uβxβ) ?.
+@toc_to_check_tm_true @vopen_tm_down @check_tm_true_to_toc @ctx_of_CTX qed.
+
+axiom vclose_tm_up : βu,x,k.tm_or_ctx k u β tm_or_ctx (S k) (Ξ½x.u).
+
+definition vclose_TM β Ξ»u:TM.Ξ»x.mk_CTX (Ξ½x.u) ?.
+@toc_to_check_tm_true @vclose_tm_up @check_tm_true_to_toc @tm_of_TM qed.
+
+interpretation "ln wf term variable open" 'open u x = (vopen_TM u x).
+interpretation "ln wf term variable close" 'nu x u = (vclose_TM u x).
+
+theorem tm_alpha : βx,y,s,u.x β FV u β y β FV u β lam x s (uβxβ) = lam y s (uβyβ).
+#x #y #s #u #Hx #Hy whd in β’ (??%%); @eq_f >nominal_eta // >nominal_eta //
+qed.
+
+lemma TM_to_tm2 : βu:TM.tm2 u.
+#u @tm_to_tm2 @check_tm_true_to_toc @tm_of_TM qed.
+
+theorem TM_ind_plus_weak :
+ βP:pretm β Type[0].
+ (βx:πΈ.P (PAR x)) β
+ (βv1,v2:TM.P v1 β P v2 β P (APP v1 v2)) β
+ βC:list πΈ.
+ (βx,s.βv:CTX.x β FV v β x β C β
+ (βy.y β FV v β P (vβyβ)) β P (LAM x s (vβxβ))) β
+ βu:TM.P u.
+#P #Hpar #Happ #C #Hlam #u elim (TM_to_tm2 u) //
+[ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β¦) (mk_TM β¦) IH1 IH2)
+ @toc_to_check_tm_true @tm2_to_tm //
+| #x #s #v #Hx #pv #IH
+ lapply (p_fresh β¦ (C@FV v)) letin x0 β (N_fresh β¦ (C@FV v)) #Hx0
+ >(?:lam x s (vβxβ) = lam x0 s (vβx0β))
+ [|@tm_alpha // @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r ]
+ @(Hlam x0 s (mk_CTX v ?) ??)
+ [ <(nominal_eta β¦ Hx) @toc_to_check_tm_true @vclose_tm_up @tm2_to_tm @pv //
+ | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r
+ | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_l
+ | @IH ]
+]
+qed.
+
+lemma eq_mk_TM : βu,v.u = v β βpu,pv.mk_TM u pu = mk_TM v pv.
+#u #v #Heq >Heq #pu #pv %
+qed.
+
+lemma eq_P : βT:Type[0].βt1,t2:T.t1 = t2 β βP:T β Type[0].P t1 β P t2. // qed.
+
+theorem TM_ind_plus :
+ βP:TM β Type[0].
+ (βx:πΈ.P (PAR x)) β
+ (βv1,v2:TM.P v1 β P v2 β P (APP v1 v2)) β
+ βC:list πΈ.
+ (βx,s.βv:CTX.x β FV v β x β C β
+ (βy.y β FV v β P (vβyβ)) β P (LAM x s (vβxβ))) β
+ βu:TM.P u.
+#P #Hpar #Happ #C #Hlam * #u #pu
+>(?:mk_TM u pu =
+ mk_TM u (toc_to_check_tm_true β¦ (tm2_to_tm β¦ (tm_to_tm2 β¦ (check_tm_true_to_toc β¦ pu))))) [|%]
+elim (tm_to_tm2 u ?) //
+[ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β¦) (mk_TM β¦) IH1 IH2)
+| #x #s #v #Hx #pv #IH
+ lapply (p_fresh β¦ (C@FV v)) letin x0 β (N_fresh β¦ (C@FV v)) #Hx0
+ lapply (Hlam x0 s (mk_CTX v ?) ???)
+ [2: @(not_to_not β¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_l @Hx0
+ |4: @toc_to_check_tm_true <(nominal_eta x v) // @vclose_tm_up @tm2_to_tm @pv //
+ | #y #Hy whd in match (vopen_TM ??);
+ >(?:mk_TM (vβyβ) ? = mk_TM (vβyβ) (toc_to_check_tm_true (vβyβ) O (tm2_to_tm (vβyβ) (pv y Hy))))
+ [@IH|%]
+ | @(not_to_not β¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_r @Hx0
+ | @eq_P @eq_mk_TM whd in match (vopen_TM ??); @tm_alpha // @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r ]
+]
+qed.
+
+notation
+"hvbox('nominal' u 'return' out 'with'
+ [ 'xpar' ident x β f1
+ | 'xapp' ident v1 ident v2 ident recv1 ident recv2 β f2
+ | 'xlam' β¨ident y # Cβ© ident s ident w ident py1 ident py2 ident recw β f3 ])"
+with precedence 48
+for @{ TM_ind_plus $out (Ξ»${ident x}:?.$f1)
+ (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
+ $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident recw}:?.$f3)
+ $u }.
+
+(* include "basics/jmeq.ma".*)
+
+definition subst β (Ξ»u:TM.Ξ»x,v.
+ nominal u return (Ξ»_.TM) with
+ [ 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! *)
+ | xapp v1 v2 recv1 recv2 β APP recv1 recv2
+ | xlam β¨y # x::FV vβ© s w py1 py2 recw β LAM y s (recw y py1) ]).
+
+lemma subst_def : βu,x,v.subst u x v =
+ nominal u return (Ξ»_.TM) with
+ [ xpar x0 β match x == x0 with [ true β v | false β PAR x0 ]
+ | xapp v1 v2 recv1 recv2 β APP recv1 recv2
+ | xlam β¨y # x::FV vβ© s w py1 py2 recw β LAM y s (recw y py1) ]. //
+qed.
+
+axiom TM_ind_plus_LAM :
+ βx,s,u,out,f1,f2,C,f3,Hx1,Hx2.
+ TM_ind_plus out f1 f2 C f3 (LAM x s (uβxβ)) =
+ f3 x s u Hx1 Hx2 (Ξ»y,Hy.TM_ind_plus ? f1 f2 C f3 ?).
+
+axiom TM_ind_plus_APP :
+ βu1,u2,out,f1,f2,C,f3.
+ TM_ind_plus out f1 f2 C f3 (APP u1 u2) =
+ f2 u1 u2 (TM_ind_plus out f1 f2 C f3 ?) (TM_ind_plus out f1 f2 C f3 ?).
+
+lemma eq_mk_CTX : βu,v.u = v β βpu,pv.mk_CTX u pu = mk_CTX v pv.
+#u #v #Heq >Heq #pu #pv %
+qed.
+
+lemma vclose_vopen_TM : βx.βu:TM.((Ξ½x.u)βxβ) = u.
+#x * #u #pu @eq_mk_TM @vclose_vopen qed.
+
+lemma nominal_eta_CTX : βx.βu:CTX.x β FV u β (Ξ½x.(uβxβ)) = u.
+#x * #u #pu #Hx @eq_mk_CTX @nominal_eta // qed.
+
+theorem TM_alpha : βx,y,s.βu:CTX.x β FV u β y β FV u β LAM x s (uβxβ) = LAM y s (uβyβ).
+#x #y #s #u #Hx #Hy @eq_mk_TM @tm_alpha // qed.
+
+axiom in_vopen_CTX : βx,y.βv:CTX.x β FV (vβyβ) β x = y β¨ x β FV v.
+
+theorem subst_fresh : βu,v:TM.βx.x β FV u β subst u x v = u.
+#u #v #x @(TM_ind_plus β¦ (x::FV v) β¦ u)
+[ #x0 normalize in β’ (%β?); #Hx normalize in β’ (??%?);
+ >(\bf ?) [| @(not_to_not β¦ Hx) #Heq >Heq % ] %
+| #u1 #u2 #IH1 #IH2 normalize in β’ (%β?); #Hx
+ >subst_def >TM_ind_plus_APP @eq_mk_TM @eq_f2 @eq_f
+ [ <subst_def @IH1 @(not_to_not β¦ Hx) @in_list_to_in_list_append_l
+ | <subst_def @IH2 @(not_to_not β¦ Hx) @in_list_to_in_list_append_r ]
+| #x0 #s #v0 #Hx0 #HC #IH #Hx >subst_def >TM_ind_plus_LAM [|@HC|@Hx0]
+ @eq_f <subst_def @IH // @(not_to_not β¦ Hx) -Hx #Hx
+ change with (FV (Ξ½x0.(v0βx0β))) in β’ (???%); >nominal_eta_CTX //
+ cases (in_vopen_CTX β¦ Hx) // #Heq >Heq in HC; * #HC @False_ind @HC %
+]
+qed.
+
+example subst_LAM_same : βx,s,u,v. subst (LAM x s u) x v = LAM x s u.
+#x #s #u #v >subst_def <(vclose_vopen_TM x u)
+lapply (p_fresh β¦ (FV (Ξ½x.u)@x::FV v)) letin x0 β (N_fresh β¦ (FV (Ξ½x.u)@x::FV v)) #Hx0
+>(TM_alpha x x0)
+[| @(not_to_not β¦ Hx0) -Hx0 #Hx0 @in_list_to_in_list_append_l @Hx0 | @fresh_vclose_tm ]
+>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 ]
+@eq_f change with (subst ((Ξ½x.u)βx0β) x v) in β’ (??%?); @subst_fresh
+@(not_to_not β¦ Hx0) #Hx0' cases (in_vopen_CTX β¦ Hx0')
+[ #Heq >Heq @in_list_to_in_list_append_r %
+| #Hfalse @False_ind cases (fresh_vclose_tm u x) #H @H @Hfalse ]
+qed.
+
+(*
+notation > "Ξ ident x. ident T [ident x] β¦ P"
+ with precedence 48 for @{'foo (Ξ»${ident x}.Ξ»${ident T}.$P)}.
+
+notation < "Ξ ident x. ident T [ident x] β¦ P"
+ with precedence 48 for @{'foo (Ξ»${ident x}:$Q.Ξ»${ident T}:$R.$P)}.
+*)
+
+(*
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x β f1
+ | 'xapp' ident v1 ident v2 β f2
+ | 'xlam' ident x # C s w β f3 ])"
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+*)
+
+(*
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x ^ f1
+ | 'xapp' ident v1 ident v2 ^ f2 ])"
+(* | 'xlam' ident x # C s w ^ f3 ]) *)
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+*)
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x ^ f1
+ | 'xapp' ident v1 ident v2 ^ f2 ])"
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:?.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+
+axiom in_Env : πΈ Γ tp β Env β Prop.
+notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
+interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
+
+
+
+inductive judg : list tp β tm β tp β Prop β
+| t_var : βg,n,t.Nth ? n g = Some ? t β judg g (var n) t
+| t_app : βg,m,n,t,u.judg g m (arr t u) β judg g n t β judg g (app m n) u
+| t_abs : βg,t,m,u.judg (t::g) m u β judg g (abs t m) (arr t u).
+
+definition Env := list (πΈ Γ tp).
+
+axiom vclose_env : Env β list tp.
+axiom vclose_tm : Env β tm β tm.
+axiom Lam : πΈ β tp β tm β tm.
+definition Judg β Ξ»G,M,T.judg (vclose_env G) (vclose_tm G M) T.
+definition dom β Ξ»G:Env.map ?? (fst ??) G.
+
+definition sctx β πΈ Γ tm.
+axiom swap_tm : πΈ β πΈ β tm β tm.
+definition sctx_app : sctx β πΈ β tm β Ξ»M0,Y.let β©X,Mβͺ β M0 in swap_tm X Y M.
+
+axiom in_list : βA:Type[0].A β list A β Prop.
+interpretation "list membership" 'mem x l = (in_list ? x l).
+interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
+
+axiom in_Env : πΈ Γ tp β Env β Prop.
+notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
+interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
+
+(* axiom Lookup : πΈ β Env β option tp. *)
+
+(* forma alto livello del judgment
+ t_abs* : βG,T,X,M,U.
+ (βY β supp(M).Judg (β©Y,Tβͺ::G) (M[Y]) U) β
+ Judg G (Lam X T (M[X])) (arr T U) *)
+
+(* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
+
+axiom Judg_ind : βP:Env β tm β tp β Prop.
+ (βX,G,T.β©X,Tβͺ β G β P G (par X) T) β
+ (βG,M,N,T,U.
+ Judg G M (arr T U) β Judg G N T β
+ P G M (arr T U) β P G N T β P G (app M N) U) β
+ (βG,T1,T2,X,M1.
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β Judg (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β P (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) β
+ βG,M,T.Judg G M T β P G M T.
+
+axiom t_par : βX,G,T.β©X,Tβͺ β G β Judg G (par X) T.
+axiom t_app2 : βG,M,N,T,U.Judg G M (arr T U) β Judg G N T β Judg G (app M N) U.
+axiom t_Lam : βG,X,M,T,U.Judg (β©X,Tβͺ::G) M U β Judg G (Lam X T M) (arr T U).
+
+definition subenv β Ξ»G1,G2.βx.x β G1 β x β G2.
+interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
+
+axiom daemon : βP:Prop.P.
+
+theorem weakening : βG1,G2,M,T.G1 β G2 β Judg G1 M T β Judg G2 M T.
+#G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (βG2.?)
+@(Judg_ind β¦ HJ)
+[ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
+| #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
+ [| @IH1 // | @IH2 // ]
+| #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
+ [ (* trivial property of Lam *) @daemon
+ | (* trivial property of subenv *) @daemon ]
+]
+qed.
+
+(* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e
+ ricorsione *)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/lists/list.ma".
+include "basics/deqsets.ma".
+include "binding/names.ma".
+include "binding/fp.ma".
+
+definition alpha : Nset β X. check alpha
+notation "πΈ" non associative with precedence 90 for @{'alphabet}.
+interpretation "set of names" 'alphabet = alpha.
+
+inductive tp : Type[0] β
+| top : tp
+| arr : tp β tp β tp.
+inductive pretm : Type[0] β
+| var : nat β pretm
+| par : πΈ β pretm
+| abs : tp β pretm β pretm
+| app : pretm β pretm β pretm.
+
+let rec Nth T n (l:list T) on n β
+ match l with
+ [ nil β None ?
+ | cons hd tl β match n with
+ [ O β Some ? hd
+ | S n0 β Nth T n0 tl ] ].
+
+let rec vclose_tm_aux u x k β match u with
+ [ var n β if (leb k n) then var (S n) else u
+ | par x0 β if (x0 == x) then (var k) else u
+ | app v1 v2 β app (vclose_tm_aux v1 x k) (vclose_tm_aux v2 x k)
+ | abs s v β abs s (vclose_tm_aux v x (S k)) ].
+definition vclose_tm β Ξ»u,x.vclose_tm_aux u x O.
+
+definition vopen_var β Ξ»n,x,k.match eqb n k with
+ [ true β par x
+ | false β match leb n k with
+ [ true β var n
+ | false β var (pred n) ] ].
+
+let rec vopen_tm_aux u x k β match u with
+ [ var n β vopen_var n x k
+ | par x0 β u
+ | app v1 v2 β app (vopen_tm_aux v1 x k) (vopen_tm_aux v2 x k)
+ | abs s v β abs s (vopen_tm_aux v x (S k)) ].
+definition vopen_tm β Ξ»u,x.vopen_tm_aux u x O.
+
+let rec FV u β match u with
+ [ par x β [x]
+ | app v1 v2 β FV v1@FV v2
+ | abs s v β FV v
+ | _ β [ ] ].
+
+definition lam β Ξ»x,s,u.abs s (vclose_tm u x).
+
+let rec Pi_map_tm p u on u β match u with
+[ par x β par (p x)
+| var _ β u
+| app v1 v2 β app (Pi_map_tm p v1) (Pi_map_tm p v2)
+| abs s v β abs s (Pi_map_tm p v) ].
+
+interpretation "permutation of tm" 'middot p x = (Pi_map_tm p x).
+
+notation "hvbox(uβxβ)"
+ with precedence 45
+ for @{ 'open $u $x }.
+
+(*
+notation "hvbox(uβxβ)"
+ with precedence 45
+ for @{ 'open $u $x }.
+notation "β΄ u β΅ x" non associative with precedence 90 for @{ 'open $u $x }.
+*)
+interpretation "ln term variable open" 'open u x = (vopen_tm u x).
+notation < "hvbox(Ξ½ x break . u)"
+ with precedence 20
+for @{'nu $x $u }.
+notation > "Ξ½ list1 x sep , . term 19 u" with precedence 20
+ for ${ fold right @{$u} rec acc @{'nu $x $acc)} }.
+interpretation "ln term variable close" 'nu x u = (vclose_tm u x).
+
+let rec tm_height u β match u with
+[ app v1 v2 β S (max (tm_height v1) (tm_height v2))
+| abs s v β S (tm_height v)
+| _ β O ].
+
+theorem le_n_O_rect_Type0 : βn:nat. n β€ O β βP: nat βType[0]. P O β P n.
+#n (cases n) // #a #abs cases (?:False) /2/ qed.
+
+theorem nat_rect_Type0_1 : βn:nat.βP:nat β Type[0].
+(βm.(βp. p < m β P p) β P m) β P n.
+#n #P #H
+cut (βq:nat. q β€ n β P q) /2/
+(elim n)
+ [#q #HleO (* applica male *)
+ @(le_n_O_rect_Type0 ? HleO)
+ @H #p #ltpO cases (?:False) /2/ (* 3 *)
+ |#p #Hind #q #HleS
+ @H #a #lta @Hind @le_S_S_to_le /2/
+ ]
+qed.
+
+lemma leb_false_to_lt : βn,m. leb n m = false β m < n.
+#n elim n
+[ #m normalize #H destruct(H)
+| #n0 #IH * // #m normalize #H @le_S_S @IH // ]
+qed.
+
+lemma nominal_eta_aux : βx,u.x β FV u β βk.vclose_tm_aux (vopen_tm_aux u x k) x k = u.
+#x #u elim u
+[ #n #_ #k normalize cases (decidable_eq_nat n k) #Hnk
+ [ >Hnk >eqb_n_n whd in β’ (??%?); >(\b ?) //
+ | >(not_eq_to_eqb_false β¦ Hnk) normalize cases (true_or_false (leb n k)) #Hleb
+ [ >Hleb normalize >(?:leb k n = false) //
+ @lt_to_leb_false @not_eq_to_le_to_lt /2/
+ | >Hleb normalize >(?:leb k (pred n) = true) normalize
+ [ cases (leb_false_to_lt β¦ Hleb) //
+ | @le_to_leb_true cases (leb_false_to_lt β¦ Hleb) normalize /2/ ] ] ]
+| #y normalize in β’ (%β?β?); #Hy whd in β’ (?β??%?); >(\bf ?) // @(not_to_not β¦ Hy) //
+| #s #v #IH normalize #Hv #k >IH // @Hv
+| #v1 #v2 #IH1 #IH2 normalize #Hv1v2 #k
+ >IH1 [ >IH2 // | @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_l ]
+ @(not_to_not β¦ Hv1v2) @in_list_to_in_list_append_r ]
+qed.
+
+corollary nominal_eta : βx,u.x β FV u β (Ξ½x.uβxβ) = u.
+#x #u #Hu @nominal_eta_aux //
+qed.
+
+lemma eq_height_vopen_aux : βv,x,k.tm_height (vopen_tm_aux v x k) = tm_height v.
+#v #x elim v
+[ #n #k normalize cases (eqb n k) // cases (leb n k) //
+| #u #k %
+| #s #u #IH #k normalize >IH %
+| #u1 #u2 #IH1 #IH2 #k normalize >IH1 >IH2 % ]
+qed.
+
+corollary eq_height_vopen : βv,x.tm_height (vβxβ) = tm_height v.
+#v #x @eq_height_vopen_aux
+qed.
+
+theorem pretm_ind_plus_aux :
+ βP:pretm β Type[0].
+ (βx:πΈ.P (par x)) β
+ (βn:β.P (var n)) β
+ (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
+ βC:list πΈ.
+ (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
+ βn,u.tm_height u β€ n β P u.
+#P #Hpar #Hvar #Happ #C #Hlam #n change with ((Ξ»n.?) n); @(nat_rect_Type0_1 n ??)
+#m cases m
+[ #_ * /2/
+ [ normalize #s #v #Hfalse cases (?:False) cases (not_le_Sn_O (tm_height v)) /2/
+ | #v1 #v2 whd in β’ (?%?β?); #Hfalse cases (?:False) cases (not_le_Sn_O (S (max ??))) /2/ ] ]
+-m #m #IH * /2/
+[ #s #v whd in β’ (?%?β?); #Hv
+ lapply (p_fresh β¦ (C@FV v)) letin y β (N_fresh β¦ (C@FV v)) #Hy
+ >(?:abs s v = lam y s (vβyβ))
+ [| whd in β’ (???%); >nominal_eta // @(not_to_not β¦ Hy) @in_list_to_in_list_append_r ]
+ @Hlam
+ [ @(not_to_not β¦ Hy) @in_list_to_in_list_append_r
+ | @(not_to_not β¦ Hy) @in_list_to_in_list_append_l ]
+ @IH [| @Hv | >eq_height_vopen % ]
+| #v1 #v2 whd in β’ (?%?β?); #Hv @Happ
+ [ @IH [| @Hv | // ] | @IH [| @Hv | // ] ] ]
+qed.
+
+corollary pretm_ind_plus :
+ βP:pretm β Type[0].
+ (βx:πΈ.P (par x)) β
+ (βn:β.P (var n)) β
+ (βv1,v2. P v1 β P v2 β P (app v1 v2)) β
+ βC:list πΈ.
+ (βx,s,v.x β FV v β x β C β P (vβxβ) β P (lam x s (vβxβ))) β
+ βu.P u.
+#P #Hpar #Hvar #Happ #C #Hlam #u @pretm_ind_plus_aux /2/
+qed.
+
+(* maps a permutation to a list of terms *)
+definition Pi_map_list : (πΈ β πΈ) β list πΈ β list πΈ β map πΈ πΈ .
+
+(* interpretation "permutation of name list" 'middot p x = (Pi_map_list p x).*)
+
+(*
+inductive tm : pretm β Prop β
+| tm_par : βx:πΈ.tm (par x)
+| tm_app : βu,v.tm u β tm v β tm (app u v)
+| tm_lam : βx,s,u.tm u β tm (lam x s u).
+
+inductive ctx_aux : nat β pretm β Prop β
+| ctx_var : βn,k.n < k β ctx_aux k (var n)
+| ctx_par : βx,k.ctx_aux k (par x)
+| ctx_app : βu,v,k.ctx_aux k u β ctx_aux k v β ctx_aux k (app u v)
+(* Γ¨ sostituibile da ctx_lam ? *)
+| ctx_abs : βs,u.ctx_aux (S k) u β ctx_aux k (abs s u).
+*)
+
+inductive tm_or_ctx (k:nat) : pretm β Type[0] β
+| toc_var : βn.n < k β tm_or_ctx k (var n)
+| toc_par : βx.tm_or_ctx k (par x)
+| toc_app : βu,v.tm_or_ctx k u β tm_or_ctx k v β tm_or_ctx k (app u v)
+| toc_lam : βx,s,u.tm_or_ctx k u β tm_or_ctx k (lam x s u).
+
+definition tm β Ξ»t.tm_or_ctx O t.
+definition ctx β Ξ»t.tm_or_ctx 1 t.
+
+record TM : Type[0] β {
+ pretm_of_TM :> pretm;
+ tm_of_TM : tm pretm_of_TM
+}.
+
+record CTX : Type[0] β {
+ pretm_of_CTX :> pretm;
+ ctx_of_CTX : ctx pretm_of_CTX
+}.
+
+inductive tm2 : pretm β Type[0] β
+| tm_par : βx.tm2 (par x)
+| tm_app : βu,v.tm2 u β tm2 v β tm2 (app u v)
+| tm_lam : βx,s,u.x β FV u β (βy.y β FV u β tm2 (uβyβ)) β tm2 (lam x s (uβxβ)).
+
+(*
+inductive tm' : pretm β Prop β
+| tm_par : βx.tm' (par x)
+| tm_app : βu,v.tm' u β tm' v β tm' (app u v)
+| tm_lam : βx,s,u,C.x β FV u β x β C β (βy.y β FV u β tm' (β΄uβ΅y)) β tm' (lam x s (β΄uβ΅x)).
+*)
+
+axiom swap_inj : βN.βz1,z2,x,y.swap N z1 z2 x = swap N z1 z2 y β x = y.
+
+lemma pi_vclose_tm :
+ βz1,z2,x,u.swap πΈ z1 z2Β·(Ξ½x.u) = (Ξ½ swap ? z1 z2 x.swap πΈ z1 z2 Β· u).
+#z1 #z2 #x #u
+change with (vclose_tm_aux ???) in match (vclose_tm ??);
+change with (vclose_tm_aux ???) in β’ (???%); lapply O elim u
+[3:whd in β’ (?β?β(?β ??%%)β?β??%%); //
+|4:whd in β’ (?β?β(?β??%%)β(?β??%%)β?β??%%); //
+| #n #k whd in β’ (??(??%)%); cases (leb k n) normalize %
+| #x0 #k cases (true_or_false (x0==z1)) #H1 >H1 whd in β’ (??%%);
+ [ cases (true_or_false (x0==x)) #H2 >H2 whd in β’ (??(??%)%);
+ [ <(\P H2) >H1 whd in β’ (??(??%)%); >(\b ?) // >(\b ?) //
+ | >H2 whd in match (swap ????); >H1
+ whd in match (if false then var k else ?);
+ whd in match (if true then z2 else ?); >(\bf ?)
+ [ >(\P H1) >swap_left %
+ | <(swap_inv ? z1 z2 z2) in β’ (?(??%?)); % #H3
+ lapply (swap_inj β¦ H3) >swap_right #H4 <H4 in H2; >H1 #H destruct (H) ]
+ ]
+ | >(?:(swap ? z1 z2 x0 == swap ? z1 z2 x) = (x0 == x))
+ [| cases (true_or_false (x0==x)) #H2 >H2
+ [ >(\P H2) @(\b ?) %
+ | @(\bf ?) % #H >(swap_inj β¦ H) in H2; >(\b ?) // #H0 destruct (H0) ] ]
+ cases (true_or_false (x0==x)) #H2 >H2 whd in β’ (??(??%)%);
+ [ <(\P H2) >H1 >(\b (refl ??)) %
+ | >H1 >H2 % ]
+ ]
+ ]
+qed.
+
+lemma pi_vopen_tm :
+ βz1,z2,x,u.swap πΈ z1 z2Β·(uβxβ) = (swap πΈ z1 z2 Β· uβswap πΈ z1 z2 xβ).
+#z1 #z2 #x #u
+change with (vopen_tm_aux ???) in match (vopen_tm ??);
+change with (vopen_tm_aux ???) in β’ (???%); lapply O elim u //
+[2: #s #v whd in β’ ((?β??%%)β?β??%%); //
+|3: #v1 #v2 whd in β’ ((?β??%%)β(?β??%%)β?β??%%); /2/ ]
+#n #k whd in β’ (??(??%)%); cases (true_or_false (eqb n k)) #H1 >H1 //
+cases (true_or_false (leb n k)) #H2 >H2 normalize //
+qed.
+
+lemma pi_lam :
+ βz1,z2,x,s,u.swap πΈ z1 z2 Β· lam x s u = lam (swap πΈ z1 z2 x) s (swap πΈ z1 z2 Β· u).
+#z1 #z2 #x #s #u whd in β’ (???%); <(pi_vclose_tm β¦) %
+qed.
+
+lemma eqv_FV : βz1,z2,u.FV (swap πΈ z1 z2 Β· u) = Pi_map_list (swap πΈ z1 z2) (FV u).
+#z1 #z2 #u elim u //
+[ #s #v #H @H
+| #v1 #v2 whd in β’ (??%%β??%%β??%%); #H1 #H2 >H1 >H2
+ whd in β’ (???(????%)); /2/ ]
+qed.
+
+lemma swap_inv_tm : βz1,z2,u.swap πΈ z1 z2 Β· (swap πΈ z1 z2 Β· u) = u.
+#z1 #z2 #u elim u
+[1: #n %
+|3: #s #v whd in β’ (?β??%%); //
+|4: #v1 #v2 #Hv1 #Hv2 whd in β’ (??%%); // ]
+#x whd in β’ (??%?); >swap_inv %
+qed.
+
+lemma eqv_in_list : βx,l,z1,z2.x β l β swap πΈ z1 z2 x β Pi_map_list (swap πΈ z1 z2) l.
+#x #l #z1 #z2 #Hin elim Hin
+[ #x0 #l0 %
+| #x1 #x2 #l0 #Hin #IH %2 @IH ]
+qed.
+
+lemma eqv_tm2 : βu.tm2 u β βz1,z2.tm2 ((swap ? z1 z2)Β·u).
+#u #Hu #z1 #z2 letin p β (swap ? z1 z2) elim Hu /2/
+#x #s #v #Hx #Hv #IH >pi_lam >pi_vopen_tm %3
+[ @(not_to_not β¦ Hx) -Hx #Hx
+ <(swap_inv ? z1 z2 x) <(swap_inv_tm z1 z2 v) >eqv_FV @eqv_in_list //
+| #y #Hy <(swap_inv ? z1 z2 y)
+ <pi_vopen_tm @IH @(not_to_not β¦ Hy) -Hy #Hy <(swap_inv ? z1 z2 y)
+ >eqv_FV @eqv_in_list //
+]
+qed.
+
+lemma vclose_vopen_aux : βx,u,k.vopen_tm_aux (vclose_tm_aux u x k) x k = u.
+#x #u elim u [1,3,4:normalize //]
+[ #n #k cases (true_or_false (leb k n)) #H >H whd in β’ (??%?);
+ [ cases (true_or_false (eqb (S n) k)) #H1 >H1
+ [ <(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_true_to_le β¦ H) -H #H
+ cases (le_to_not_lt β¦ H) -H #H cases (H ?) %
+ | whd in β’ (??%?); >lt_to_leb_false // @le_S_S /2/ ]
+ | cases (true_or_false (eqb n k)) #H1 >H1 normalize
+ [ >(eqb_true_to_eq β¦ H1) in H; #H lapply (leb_false_to_not_le β¦ H) -H
+ * #H cases (H ?) %
+ | >le_to_leb_true // @not_lt_to_le % #H2 >le_to_leb_true in H;
+ [ #H destruct (H) | /2/ ]
+ ]
+ ]
+| #x0 #k whd in β’ (??(?%??)?); cases (true_or_false (x0==x))
+ #H1 >H1 normalize // >(\P H1) >eqb_n_n % ]
+qed.
+
+lemma vclose_vopen : βx,u.((Ξ½x.u)βxβ) = u. #x #u @vclose_vopen_aux
+qed.
+
+(*
+theorem tm_to_tm : βt.tm' t β tm t.
+#t #H elim H
+*)
+
+lemma in_list_singleton : βT.βt1,t2:T.t1 β [t2] β t1 = t2.
+#T #t1 #t2 #H @(in_list_inv_ind ??? H) /2/
+qed.
+
+lemma fresh_vclose_tm_aux : βu,x,k.x β FV (vclose_tm_aux u x k).
+#u #x elim u //
+[ #n #k normalize cases (leb k n) normalize //
+| #x0 #k whd in β’ (?(???(?%))); cases (true_or_false (x0==x)) #H >H normalize //
+ lapply (\Pf H) @not_to_not #Hin >(in_list_singleton ??? Hin) %
+| #v1 #v2 #IH1 #IH2 #k normalize % #Hin cases (in_list_append_to_or_in_list ???? Hin) -Hin #Hin
+ [ cases (IH1 k) -IH1 #IH1 @IH1 @Hin | cases (IH2 k) -IH2 #IH2 @IH2 @Hin ]
+qed.
+
+lemma fresh_vclose_tm : βu,x.x β FV (Ξ½x.u). //
+qed.
+
+lemma fresh_swap_tm : βz1,z2,u.z1 β FV u β z2 β FV u β swap πΈ z1 z2 Β· u = u.
+#z1 #z2 #u elim u
+[2: normalize in β’ (?β%β%β?); #x #Hz1 #Hz2 whd in β’ (??%?); >swap_other //
+ [ @(not_to_not β¦ Hz2) | @(not_to_not β¦ Hz1) ] //
+|1: //
+| #s #v #IH normalize #Hz1 #Hz2 >IH // [@Hz2|@Hz1]
+| #v1 #v2 #IH1 #IH2 normalize #Hz1 #Hz2
+ >IH1 [| @(not_to_not β¦ Hz2) @in_list_to_in_list_append_l | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_l ]
+ >IH2 // [@(not_to_not β¦ Hz2) @in_list_to_in_list_append_r | @(not_to_not β¦ Hz1) @in_list_to_in_list_append_r ]
+]
+qed.
+
+theorem tm_to_tm2 : βu.tm u β tm2 u.
+#t #Ht elim Ht
+[ #n #Hn cases (not_le_Sn_O n) #Hfalse cases (Hfalse Hn)
+| @tm_par
+| #u #v #Hu #Hv @tm_app
+| #x #s #u #Hu #IHu <(vclose_vopen x u) @tm_lam
+ [ @fresh_vclose_tm
+ | #y #Hy <(fresh_swap_tm x y (Ξ½x.u)) /2/ @fresh_vclose_tm ]
+]
+qed.
+
+theorem tm2_to_tm : βu.tm2 u β tm u.
+#u #pu elim pu /2/ #x #s #v #Hx #Hv #IH %4 @IH //
+qed.
+
+definition PAR β Ξ»x.mk_TM (par x) ?. // qed.
+definition APP β Ξ»u,v:TM.mk_TM (app u v) ?./2/ qed.
+definition LAM β Ξ»x,s.Ξ»u:TM.mk_TM (lam x s u) ?./2/ qed.
+
+axiom vopen_tm_down : βu,x,k.tm_or_ctx (S k) u β tm_or_ctx k (uβxβ).
+(* needs true_plus_false
+
+#u #x #k #Hu elim Hu
+[ #n #Hn normalize cases (true_or_false (eqb n O)) #H >H [%2]
+ normalize >(?: leb n O = false) [|cases n in H; // >eqb_n_n #H destruct (H) ]
+ normalize lapply Hn cases n in H; normalize [ #Hfalse destruct (Hfalse) ]
+ #n0 #_ #Hn0 % @le_S_S_to_le //
+| #x0 %2
+| #v1 #v2 #Hv1 #Hv2 #IH1 #IH2 %3 //
+| #x0 #s #v #Hv #IH normalize @daemon
+]
+qed.
+*)
+
+definition vopen_TM β Ξ»u:CTX.Ξ»x.mk_TM (uβxβ) (vopen_tm_down β¦). @ctx_of_CTX qed.
+
+axiom vclose_tm_up : βu,x,k.tm_or_ctx k u β tm_or_ctx (S k) (Ξ½x.u).
+
+definition vclose_TM β Ξ»u:TM.Ξ»x.mk_CTX (Ξ½x.u) (vclose_tm_up β¦). @tm_of_TM qed.
+
+interpretation "ln wf term variable open" 'open u x = (vopen_TM u x).
+interpretation "ln wf term variable close" 'nu x u = (vclose_TM u x).
+
+theorem tm_alpha : βx,y,s,u.x β FV u β y β FV u β lam x s (uβxβ) = lam y s (uβyβ).
+#x #y #s #u #Hx #Hy whd in β’ (??%%); @eq_f >nominal_eta // >nominal_eta //
+qed.
+
+theorem TM_ind_plus :
+(* non si puΓ² dare il principio in modo dipendente (almeno utilizzando tm2)
+ la "prova" purtroppo Γ¨ in Type e non si puΓ² garantire che sia esattamente
+ quella che ci aspetteremmo
+ *)
+ βP:pretm β Type[0].
+ (βx:πΈ.P (PAR x)) β
+ (βv1,v2:TM.P v1 β P v2 β P (APP v1 v2)) β
+ βC:list πΈ.
+ (βx,s.βv:CTX.x β FV v β x β C β
+ (βy.y β FV v β P (vβyβ)) β P (LAM x s (vβxβ))) β
+ βu:TM.P u.
+#P #Hpar #Happ #C #Hlam * #u #pu elim (tm_to_tm2 u pu) //
+[ #v1 #v2 #pv1 #pv2 #IH1 #IH2 @(Happ (mk_TM β¦) (mk_TM β¦)) /2/
+| #x #s #v #Hx #pv #IH
+ lapply (p_fresh β¦ (C@FV v)) letin x0 β (N_fresh β¦ (C@FV v)) #Hx0
+ >(?:lam x s (vβxβ) = lam x0 s (vβx0β))
+ [|@tm_alpha // @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r ]
+ @(Hlam x0 s (mk_CTX v ?) ??)
+ [ <(nominal_eta β¦ Hx) @vclose_tm_up @tm2_to_tm @pv //
+ | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_r
+ | @(not_to_not β¦ Hx0) @in_list_to_in_list_append_l
+ | @IH ]
+]
+qed.
+
+notation
+"hvbox('nominal' u 'return' out 'with'
+ [ 'xpar' ident x β f1
+ | 'xapp' ident v1 ident v2 ident recv1 ident recv2 β f2
+ | 'xlam' β¨ident y # Cβ© ident s ident w ident py1 ident py2 ident recw β f3 ])"
+with precedence 48
+for @{ TM_ind_plus $out (Ξ»${ident x}:?.$f1)
+ (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
+ $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident recw}:?.$f3)
+ $u }.
+
+(* include "basics/jmeq.ma".*)
+
+definition subst β (Ξ»u:TM.Ξ»x,v.
+ nominal u return (Ξ»_.TM) with
+ [ xpar x0 β match x == x0 with [ true β v | false β u ]
+ | xapp v1 v2 recv1 recv2 β APP recv1 recv2
+ | xlam β¨y # x::FV vβ© s w py1 py2 recw β LAM y s (recw y py1) ]).
+
+lemma fasfd : βs,v. pretm_of_TM (subst (LAM O s (PAR 1)) O v) = pretm_of_TM (LAM O s (PAR 1)).
+#s #v normalize in β’ (??%?);
+
+
+theorem tm2_ind_plus :
+(* non si puΓ² dare il principio in modo dipendente (almeno utilizzando tm2) *)
+ βP:pretm β Type[0].
+ (βx:πΈ.P (par x)) β
+ (βv1,v2.tm2 v1 β tm2 v2 β P v1 β P v2 β P (app v1 v2)) β
+ βC:list πΈ.
+ (βx,s,v.x β FV v β x β C β (βy.y β FV v β tm2 (vβyβ)) β
+ (βy.y β FV v β P (vβyβ)) β P (lam x s (vβxβ))) β
+ βu.tm2 u β P u.
+#P #Hpar #Happ #C #Hlam #u #pu elim pu /2/
+#x #s #v #px #pv #IH
+lapply (p_fresh β¦ (C@FV v)) letin y β (N_fresh β¦ (C@FV v)) #Hy
+>(?:lam x s (vβxβ) = lam y s (vβyβ)) [| @tm_alpha // @(not_to_not β¦ Hy) @in_list_to_in_list_append_r ]
+@Hlam /2/ lapply Hy -Hy @not_to_not #Hy
+[ @in_list_to_in_list_append_r @Hy | @in_list_to_in_list_append_l @Hy ]
+qed.
+
+definition check_tm β
+ Ξ»u.pretm_ind_plus ? (Ξ»_.true) (Ξ»_.false)
+ (Ξ»v1,v2,r1,r2.r1 β§ r2) [ ] (Ξ»x,s,v,pv1,pv2,rv.rv) u.
+
+(*
+lemma check_tm_complete : βu.tm u β check_tm u = true.
+#u #pu @(tm2_ind_plus β¦ [ ] β¦ (tm_to_tm2 ? pu)) //
+[ #v1 #v2 #pv1 #pv2 #IH1 #IH2
+| #x #s #v #Hx1 #Hx2 #Hv #IH
+*)
+
+notation
+"hvbox('nominal' u 'return' out 'with'
+ [ 'xpar' ident x β f1
+ | 'xapp' ident v1 ident v2 ident pv1 ident pv2 ident recv1 ident recv2 β f2
+ | 'xlam' β¨ident y # Cβ© ident s ident w ident py1 ident py2 ident pw ident recw β f3 ])"
+with precedence 48
+for @{ tm2_ind_plus $out (Ξ»${ident x}:?.$f1)
+ (Ξ»${ident v1}:?.Ξ»${ident v2}:?.Ξ»${ident pv1}:?.Ξ»${ident pv2}:?.Ξ»${ident recv1}:?.Ξ»${ident recv2}:?.$f2)
+ $C (Ξ»${ident y}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.Ξ»${ident pw}:?.Ξ»${ident recw}:?.$f3)
+ ? (tm_to_tm2 ? $u) }.
+(* notation
+"hvbox('nominal' u 'with'
+ [ 'xlam' ident x # C ident s ident w β f3 ])"
+with precedence 48
+for @{ tm2_ind_plus ???
+ $C (Ξ»${ident x}:?.Ξ»${ident s}:?.Ξ»${ident w}:?.Ξ»${ident py1}:?.Ξ»${ident py2}:?.
+ Ξ»${ident pw}:?.Ξ»${ident recw}:?.$f3) $u (tm_to_tm2 ??) }.
+*)
+
+
+definition subst β (Ξ»u.Ξ»pu:tm u.Ξ»x,v.
+ nominal pu return (Ξ»_.pretm) with
+ [ xpar x0 β match x == x0 with [ true β v | false β u ]
+ | xapp v1 v2 pv1 pv2 recv1 recv2 β app recv1 recv2
+ | xlam β¨y # x::FV vβ© s w py1 py2 pw recw β lam y s (recw y py1) ]).
+
+lemma fasfd : βx,s,u,p1,v. subst (lam x s u) p1 x v = lam x s u.
+#x #s #u #p1 #v
+
+
+definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,y.
+ tm2_ind_plus ?
+ (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
+ (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
+ (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
+ u (tm_to_tm2 β¦ pu).
+check subst
+definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
+ nominal u with
+ [ xlam y # (x::FV v) s w ^ ? ].
+
+(*
+notation > "Ξ ident x. ident T [ident x] β¦ P"
+ with precedence 48 for @{'foo (Ξ»${ident x}.Ξ»${ident T}.$P)}.
+
+notation < "Ξ ident x. ident T [ident x] β¦ P"
+ with precedence 48 for @{'foo (Ξ»${ident x}:$Q.Ξ»${ident T}:$R.$P)}.
+*)
+
+(*
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x β f1
+ | 'xapp' ident v1 ident v2 β f2
+ | 'xlam' ident x # C s w β f3 ])"
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+*)
+
+(*
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x ^ f1
+ | 'xapp' ident v1 ident v2 ^ f2 ])"
+(* | 'xlam' ident x # C s w ^ f3 ]) *)
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:$Tx.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+*)
+notation
+"hvbox('nominal' u 'with'
+ [ 'xpar' ident x ^ f1
+ | 'xapp' ident v1 ident v2 ^ f2 ])"
+with precedence 48
+for @{ tm2_ind_plus ? (Ξ»${ident x}:?.$f1)
+ (Ξ»${ident v1}:$Tv1.Ξ»${ident v2}:$Tv2.Ξ»${ident pv1}:$Tpv1.Ξ»${ident pv2}:$Tpv2.Ξ»${ident recv1}:$Trv1.Ξ»${ident recv2}:$Trv2.$f2)
+ $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 ??) }.
+
+
+definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
+ nominal u with
+ [ xpar x0 ^ match x == x0 with [ true β v | false β u ]
+ | xapp v1 v2 ^ ? ].
+ | xlam y # (x::FV v) s w ^ ? ].
+
+
+ (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
+ (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
+ (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
+ u (tm_to_tm2 β¦ pu).
+
+
+*)
+definition subst β Ξ»u.Ξ»pu:tm u.Ξ»x,v.
+ tm2_ind_plus ?
+ (* par x0 *) (Ξ»x0.match x == x0 with [ true β v | false β u ])
+ (* app v1 v2 *) (Ξ»v1,v2,pv1,pv2,recv1,recv2.app recv1 recv2)
+ (* lam y#(x::FV v) s w *) (x::FV v) (Ξ»y,s,w,py1,py2,pw,recw.lam y s (recw y py1))
+ u (tm_to_tm2 β¦ pu).
+
+check subst
+
+
+axiom in_Env : πΈ Γ tp β Env β Prop.
+notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
+interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
+
+
+
+inductive judg : list tp β tm β tp β Prop β
+| t_var : βg,n,t.Nth ? n g = Some ? t β judg g (var n) t
+| t_app : βg,m,n,t,u.judg g m (arr t u) β judg g n t β judg g (app m n) u
+| t_abs : βg,t,m,u.judg (t::g) m u β judg g (abs t m) (arr t u).
+
+definition Env := list (πΈ Γ tp).
+
+axiom vclose_env : Env β list tp.
+axiom vclose_tm : Env β tm β tm.
+axiom Lam : πΈ β tp β tm β tm.
+definition Judg β Ξ»G,M,T.judg (vclose_env G) (vclose_tm G M) T.
+definition dom β Ξ»G:Env.map ?? (fst ??) G.
+
+definition sctx β πΈ Γ tm.
+axiom swap_tm : πΈ β πΈ β tm β tm.
+definition sctx_app : sctx β πΈ β tm β Ξ»M0,Y.let β©X,Mβͺ β M0 in swap_tm X Y M.
+
+axiom in_list : βA:Type[0].A β list A β Prop.
+interpretation "list membership" 'mem x l = (in_list ? x l).
+interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
+
+axiom in_Env : πΈ Γ tp β Env β Prop.
+notation "X β G" non associative with precedence 45 for @{'lefttriangle $X $G}.
+interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
+
+let rec FV M β match M with
+ [ par X β [X]
+ | app M1 M2 β FV M1@FV M2
+ | abs T M0 β FV M0
+ | _ β [ ] ].
+
+(* axiom Lookup : πΈ β Env β option tp. *)
+
+(* forma alto livello del judgment
+ t_abs* : βG,T,X,M,U.
+ (βY β supp(M).Judg (β©Y,Tβͺ::G) (M[Y]) U) β
+ Judg G (Lam X T (M[X])) (arr T U) *)
+
+(* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
+
+axiom Judg_ind : βP:Env β tm β tp β Prop.
+ (βX,G,T.β©X,Tβͺ β G β P G (par X) T) β
+ (βG,M,N,T,U.
+ Judg G M (arr T U) β Judg G N T β
+ P G M (arr T U) β P G N T β P G (app M N) U) β
+ (βG,T1,T2,X,M1.
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β Judg (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ (βY.Y β (FV (Lam X T1 (sctx_app M1 X))) β P (β©Y,T1βͺ::G) (sctx_app M1 Y) T2) β
+ P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) β
+ βG,M,T.Judg G M T β P G M T.
+
+axiom t_par : βX,G,T.β©X,Tβͺ β G β Judg G (par X) T.
+axiom t_app2 : βG,M,N,T,U.Judg G M (arr T U) β Judg G N T β Judg G (app M N) U.
+axiom t_Lam : βG,X,M,T,U.Judg (β©X,Tβͺ::G) M U β Judg G (Lam X T M) (arr T U).
+
+definition subenv β Ξ»G1,G2.βx.x β G1 β x β G2.
+interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
+
+axiom daemon : βP:Prop.P.
+
+theorem weakening : βG1,G2,M,T.G1 β G2 β Judg G1 M T β Judg G2 M T.
+#G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (βG2.?)
+@(Judg_ind β¦ HJ)
+[ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
+| #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
+ [| @IH1 // | @IH2 // ]
+| #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
+ [ (* trivial property of Lam *) @daemon
+ | (* trivial property of subenv *) @daemon ]
+]
+qed.
+
+(* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e
+ ricorsione *)
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basics/logic.ma".
+include "basics/lists/in.ma".
+include "basics/types.ma".
+
+(*interpretation "list membership" 'mem x l = (in_list ? x l).*)
+
+record Nset : Type[1] β
+{
+ (* carrier is specified as a coercion: when an object X of type Nset is
+ given, but something of type Type is expected, Matita will insert a
+ hidden coercion: the user sees "X", but really means "carrier X" *)
+ carrier :> DeqSet;
+ N_fresh : list carrier β carrier;
+ p_fresh : βl.N_fresh l β l
+}.
+
+definition maxlist β
+ Ξ»l.foldr ?? (Ξ»x,acc.max x acc) 0 l.
+
+definition natfresh β Ξ»l.S (maxlist l).
+
+lemma le_max_1 : βx,y.x β€ max x y. /2/
+qed.
+
+lemma le_max_2 : βx,y.y β€ max x y. /2/
+qed.
+
+lemma le_maxlist : βl,x.x β l β x β€ maxlist l.
+#l elim l
+[#x #Hx @False_ind cases (not_in_list_nil ? x) #H1 /2/
+|#y #tl #IH #x #H1 change with (max ??) in β’ (??%);
+ cases (in_list_cons_case ???? H1);#H2;
+ [ >H2 @le_max_1
+ | whd in β’ (??%); lapply (refl ? (leb y (maxlist tl)));
+ cases (leb y (maxlist tl)) in β’ (???% β %);#H3
+ [ @IH //
+ | lapply (IH ? H2) #H4
+ lapply (leb_false_to_not_le β¦ H3) #H5
+ lapply (not_le_to_lt β¦ H5) #H6
+ @(transitive_le β¦ H4)
+ @(transitive_le β¦ H6) %2 %
+ ]
+ ]
+]
+qed.
+
+(* prove freshness for nat *)
+lemma lt_l_natfresh_l : βl,x.x β l β x < natfresh l.
+#l #x #H1 @le_S_S /2/
+qed.
+
+(*naxiom p_Xfresh : βl.βx:Xcarr.x β l β x β ntm (Xfresh l) β§ x β ntp (Xfresh l).*)
+lemma p_natfresh : βl.natfresh l β l.
+#l % #H1 lapply (lt_l_natfresh_l β¦ H1) #H2
+cases (lt_to_not_eq β¦ H2) #H3 @H3 %
+qed.
+
+include "basics/finset.ma".
+
+definition X : Nset β mk_Nset DeqNat β¦.
+[ @natfresh
+| @p_natfresh
+]
+qed.
\ No newline at end of file
projects / helm.git / commitdiff