1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/lists/list.ma".
17 axiom alpha : Type[0].
18 notation "𝔸" non associative with precedence 90 for @{'alphabet}.
19 interpretation "set of names" 'alphabet = alpha.
21 inductive tp : Type[0] ≝
24 inductive tm : Type[0] ≝
30 let rec Nth T n (l:list T) on n ≝
33 | cons hd tl ⇒ match n with
35 | S n0 ⇒ Nth T n0 tl ] ].
37 inductive judg : list tp → tm → tp → Prop ≝
38 | t_var : ∀g,n,t.Nth ? n g = Some ? t → judg g (var n) t
39 | t_app : ∀g,m,n,t,u.judg g m (arr t u) → judg g n t → judg g (app m n) u
40 | t_abs : ∀g,t,m,u.judg (t::g) m u → judg g (abs t m) (arr t u).
42 definition Env := list (𝔸 × tp).
44 axiom vclose_env : Env → list tp.
45 axiom vclose_tm : Env → tm → tm.
46 axiom Lam : 𝔸 → tp → tm → tm.
47 definition Judg ≝ λG,M,T.judg (vclose_env G) (vclose_tm G M) T.
48 definition dom ≝ λG:Env.map ?? (fst ??) G.
50 definition sctx ≝ 𝔸 × tm.
51 axiom swap_tm : 𝔸 → 𝔸 → tm → tm.
52 definition sctx_app : sctx → 𝔸 → tm ≝ λM0,Y.let 〈X,M〉 ≝ M0 in swap_tm X Y M.
54 axiom in_list : ∀A:Type[0].A → list A → Prop.
55 interpretation "list membership" 'mem x l = (in_list ? x l).
56 interpretation "list non-membership" 'notmem x l = (Not (in_list ? x l)).
58 axiom in_Env : 𝔸 × tp → Env → Prop.
59 notation "X ◃ G" non associative with precedence 45 for @{'lefttriangle $X $G}.
60 interpretation "Env membership" 'lefttriangle x l = (in_Env x l).
62 let rec FV M ≝ match M with
64 | app M1 M2 ⇒ FV M1@FV M2
68 (* axiom Lookup : 𝔸 → Env → option tp. *)
70 (* forma alto livello del judgment
72 (∀Y ∉ supp(M).Judg (〈Y,T〉::G) (M[Y]) U) →
73 Judg G (Lam X T (M[X])) (arr T U) *)
75 (* prima dimostrare, poi perfezionare gli assiomi, poi dimostrarli *)
77 axiom Judg_ind : ∀P:Env → tm → tp → Prop.
78 (∀X,G,T.〈X,T〉 ◃ G → P G (par X) T) →
80 Judg G M (arr T U) → Judg G N T →
81 P G M (arr T U) → P G N T → P G (app M N) U) →
83 (∀Y.Y ∉ (FV (Lam X T1 (sctx_app M1 X))) → Judg (〈Y,T1〉::G) (sctx_app M1 Y) T2) →
84 (∀Y.Y ∉ (FV (Lam X T1 (sctx_app M1 X))) → P (〈Y,T1〉::G) (sctx_app M1 Y) T2) →
85 P G (Lam X T1 (sctx_app M1 X)) (arr T1 T2)) →
86 ∀G,M,T.Judg G M T → P G M T.
88 axiom t_par : ∀X,G,T.〈X,T〉 ◃ G → Judg G (par X) T.
89 axiom t_app2 : ∀G,M,N,T,U.Judg G M (arr T U) → Judg G N T → Judg G (app M N) U.
90 axiom t_Lam : ∀G,X,M,T,U.Judg (〈X,T〉::G) M U → Judg G (Lam X T M) (arr T U).
92 definition subenv ≝ λG1,G2.∀x.x ◃ G1 → x ◃ G2.
93 interpretation "subenv" 'subseteq G1 G2 = (subenv G1 G2).
95 axiom daemon : ∀P:Prop.P.
97 theorem weakening : ∀G1,G2,M,T.G1 ⊆ G2 → Judg G1 M T → Judg G2 M T.
98 #G1 #G2 #M #T #Hsub #HJ lapply Hsub lapply G2 -G2 change with (∀G2.?)
100 [ #X #G #T0 #Hin #G2 #Hsub @t_par @Hsub //
101 | #G #M0 #N #T0 #U #HM0 #HN #IH1 #IH2 #G2 #Hsub @t_app2
102 [| @IH1 // | @IH2 // ]
103 | #G #T1 #T2 #X #M1 #HM1 #IH #G2 #Hsub @t_Lam @IH
104 [ (* trivial property of Lam *) @daemon
105 | (* trivial property of subenv *) @daemon ]
109 (* Serve un tipo Tm per i termini localmente chiusi e i suoi principi di induzione e