1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "PTS/subst.ma".
17 (*************************** substl *****************************)
19 nlet rec substl (G:list T) (N:T) : list T ≝
22 | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
26 nlemma substl_cons: ∀A,N.∀G.
27 substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
30 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
34 (****************************************************************)
36 naxiom A: nat → nat → Prop.
37 naxiom R: nat → nat → nat → Prop.
38 naxiom conv: T → T → Prop.
40 nlemma mah: ∀A,i. lift A i = lift_aux A 0 i.
45 ninductive TJ: list T → T → T → Prop ≝
46 | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
47 | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 1)
49 TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1)
50 | prod: ∀G.∀A,B.∀i,j,k. R i j k →
51 TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
53 TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst a B)
55 TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
56 | conv: ∀G.∀A,B,C.∀i. conv B C →
57 TJ G A B → TJ G B (Sort i) → TJ G A C.
59 notation "hvbox(G break ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
60 interpretation "type judgement" 'TJ G A B = (TJ G A B).
62 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
64 (**** definitions ****)
66 ninductive Glegal (G: list T) : Prop ≝
67 glegalk : ∀A,B. G ⊢ A : B → Glegal G.
69 ninductive Gterm (G: list T) (A:T) : Prop ≝
70 | is_term: ∀B.G ⊢ A:B → Gterm G A
71 | is_type: ∀B.G ⊢ B:A → Gterm G A.
73 ninductive Gtype (G: list T) (A:T) : Prop ≝
74 gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
76 ninductive Gelement (G:list T) (A:T) : Prop ≝
77 gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
79 ninductive Tlegal (A:T) : Prop ≝
80 tlegalk: ∀G. Gterm G A → Tlegal A.
83 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
85 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
87 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
89 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
91 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
95 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
97 #G; #i; #j; #axij; #Gleg; ncases Gleg;
98 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
101 ntheorem start_lemma1: ∀G.∀i,j.
102 A i j → Glegal G → G ⊢ Sort i: Sort j.
103 #G; #i; #j; #axij; #Gleg; ncases Gleg;
104 #A; #B; #tjAB; nelim tjAB; /2/;
107 ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
108 G ⊢ C: Sort q → G ⊢ Rel n: lift A i → (C::G) ⊢ Rel (S n): lift A (S i).
109 #G; #A; #C; #n; #i; #p; #tjC; #tjn;
110 napplyS (weak G (Rel n));//. (* bello *)
112 nrewrite > (plus_n_O i);
113 nrewrite > (plus_n_Sm i O);
114 nrewrite < (lift_lift A 1 i);
115 nrewrite > (plus_n_O n); nrewrite > (plus_n_Sm n O);
116 applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
119 ntheorem start_lemma2: ∀G.
120 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) (S n).
121 #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
122 ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
123 napply (absurd … abs); //;
124 ##|#G; #A; #i; #tjA; #Hind; #m; ncases m; /2/;
125 #p; #Hle; napply start_rel; //; napply Hind;
126 napply le_S_S_to_le; napply Hle;
127 ##|#G; #A; #B; #C; #i; #tjAB; #tjC; #Hind1; #_; #m; ncases m;
128 /2/; #p; #Hle; napply start_rel; //;
129 napply Hind1; napply le_S_S_to_le; napply Hle;
134 nlet rec TJm G D on D : Prop ≝
137 | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
140 nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
141 #G; #D; #A; *; //; nqed.
143 ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
144 ∀G. Glegal G → TJm G D → TJ G A B.
145 #D; #A; #B; #tjAB; nelim tjAB;
148 ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
153 ntheorem substitution_tj:
154 ∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
155 TJ G (subst N M) (subst N B).
157 napply (TJ_inv2 (A::G) M B);
159 ##|#G; #A; #N; #tjA; #Hind; #Heq;
161 ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
163 ##|nnormalize; #E; #A; #B; #i; #j; #k;
164 #Ax; #tjA; #tjB; #Hind1; #_;
165 #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
167 ##|nnormalize; napplyS weak;
171 ntheorem substitution_tj:
172 ∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A →
173 ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N].
174 #E; #A; #B; #M; #tjMB; nelim tjMB;
175 ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D;
176 ##[nnormalize; #isnil; ndestruct;
177 ##|#P; #L; nnormalize; #isnil; ndestruct;
179 ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D;
181 nrewrite > (delift (lift N O) A1 O O O ??); //;
182 nnormalize in Heq; ndestruct;/2/;
183 ##|#H; #L; #N1; #Heq; nnormalize in Heq;
184 #tjN1; nnormalize; ndestruct;
185 (* napplyS start non va *)
186 ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
189 ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
190 #G1; #D; #N; ncases D; nnormalize;
191 ##[#Heq; ndestruct; #tjN; //;
194 (* napplyS weak non va *)
195 ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq;
198 ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
199 #G1; #D; #N; #Heq; #tjN; nnormalize;
202 ##|ncheck (Hind2 G1 (P::D) N ? tjN).
203 ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
205 napply (Hind2 ? (P::D));//;
207 ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
208 #G1; #D; #N; #Heq; #tjN; nnormalize;
209 nlapply (subst_lemma R S N (length ? D) 0); #sl;
210 nrewrite < (plus_n_O ?) in sl; #sl;
212 napply app; nnormalize in Hind1;/2/;
218 ntheorem substitution_tj:
219 ∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A →
221 TJ ((substl D N)@G) (subst_aux M k N) (subst_aux B k N).
222 #E; #A; #B; #M; #tjMB; nelim tjMB;
223 ##[nnormalize; (* /3/; *)
224 ##|#G; #A1; #i; #tjA; #Hind;
226 ##[#N; #Heq; #tjN; #k; nnormalize in ⊢ (% → ?); #kO;
228 nrewrite > (delift (lift N O) A1 O O O ??); //;
229 nnormalize in Heq; ndestruct;/2/;
230 ##|#H; #L; #N1; #Heq; nnormalize in Heq;
231 #tjN1; #k; #len; nnormalize in len;
233 nnormalize; ndestruct;
235 ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
237 nrewrite < (lift_subst_aux_k N1 H (length T L) O);
238 nrewrite < (plus_n_O (length T L));
239 napply (start (substl L N1@G1) (subst_aux H (length T L) N1) i ?).