2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "lambda/subst.ma".
13 include "basics/list.ma".
16 (*************************** substl *****************************)
18 let rec substl (G:list T) (N:T) : list T ≝
21 | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
25 nlemma substl_cons: ∀A,N.∀G.
26 substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
31 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
34 (****************************************************************)
36 axiom A: nat → nat → Prop.
37 axiom R: nat → nat → nat → Prop.
38 axiom conv: T → T → Prop.
40 inductive TJ: list T → T → T → Prop ≝
41 | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
42 | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
44 TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
45 | prod: ∀G.∀A,B.∀i,j,k. R i j k →
46 TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
48 TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
50 TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
51 | conv: ∀G.∀A,B,C.∀i. conv B C →
52 TJ G A B → TJ G B (Sort i) → TJ G A C
54 TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
56 interpretation "type judgement" 'TJ G A B = (TJ G A B).
58 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
60 (**** definitions ****)
62 inductive Glegal (G: list T) : Prop ≝
63 glegalk : ∀A,B. G ⊢ A : B → Glegal G.
65 inductive Gterm (G: list T) (A:T) : Prop ≝
66 | is_term: ∀B.G ⊢ A:B → Gterm G A
67 | is_type: ∀B.G ⊢ B:A → Gterm G A.
69 inductive Gtype (G: list T) (A:T) : Prop ≝
70 gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
72 inductive Gelement (G:list T) (A:T) : Prop ≝
73 gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
75 inductive Tlegal (A:T) : Prop ≝
76 tlegalk: ∀G. Gterm G A → Tlegal A.
79 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
81 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
83 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
85 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
87 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
91 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
93 #G; #i; #j; #axij; #Gleg; ncases Gleg;
94 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
97 theorem start_lemma1: ∀G.∀i,j.
98 A i j → Glegal G → G ⊢ Sort i: Sort j.
99 #G #i #j #axij #Gleg (cases Gleg)
100 #A #B #tjAB (elim tjAB) /2/
103 theorem start_rel: ∀G.∀A.∀C.∀n,i,q.
104 G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
105 #G #A #C #n #i #p #tjC #tjn
106 (applyS (weak G (Rel n))) //. (* bello *)
108 nrewrite > (plus_n_O i);
109 nrewrite > (plus_n_Sm i O);
110 nrewrite < (lift_lift A 1 i);
111 nrewrite > (plus_n_O n); nrewrite > (plus_n_Sm n O);
112 applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
115 theorem start_lemma2: ∀G.
116 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
117 #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
118 [#i #j #axij #p normalize #abs @False_ind @(absurd … abs) //
119 |#G #A #i #tjA #Hind #m (cases m) /2/
120 #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
121 |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
122 /2/ #p #Hle @start_rel // @Hind1 @le_S_S_to_le @Hle
127 nlet rec TJm G D on D : Prop ≝
130 | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
133 nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
134 #G; #D; #A; *; //; nqed.
136 ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
137 ∀G. Glegal G → TJm G D → TJ G A B.
138 #D; #A; #B; #tjAB; nelim tjAB;
141 ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
146 ntheorem substitution_tj:
147 ∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
148 TJ G (subst N M) (subst N B).
150 napply (TJ_inv2 (A::G) M B);
152 ##|#G; #A; #N; #tjA; #Hind; #Heq;
154 ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
156 ##|nnormalize; #E; #A; #B; #i; #j; #k;
157 #Ax; #tjA; #tjB; #Hind1; #_;
158 #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
160 ##|nnormalize; napplyS weak;
165 axiom conv_subst: ∀P,Q,N,i.conv P Q → conv P[i := N] Q[i := N].
167 theorem substitution_tj:
168 ∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A →
169 ((substl D N)@G) ⊢ M[|D| := N]: B[|D| := N].
170 #E #A #B #M #tjMB (elim tjMB)
171 [normalize #i #j #k #G #D #N (cases D)
172 [normalize #isnil destruct
173 |#P #L normalize #isnil destruct
175 |#G #A1 #i #tjA #Hind #G1 #D (cases D)
176 [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
177 (normalize in Heq) destruct /2/
178 |#H #L #N1 #Heq (normalize in Heq)
179 #tjN1 normalize destruct; (applyS start) /2/
181 |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
183 [#Heq destruct #tjN //
184 |#H #L #Heq #tjN1 destruct;
185 (* napplyS weak non va *)
186 (cut (S (length T L) = (length T L)+0+1)) [//]
187 #Hee (applyS weak) /2/
189 |#G #P #Q #i #j #k #Ax #tjP #tjQ #Hind1 #Hind2
190 #G1 #D #N #Heq #tjN normalize @(prod … Ax);
192 |(cut (S (length T D) = (length T D)+1)) [//]
193 #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
195 |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
196 #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
197 >(plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?))
198 >(subst_lemma R S N ? 0) (applyS app) /2/
199 |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
200 #G1 #D #N #Heq #tjN normalize
202 [normalize in Hind2 /2/
203 |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
204 generalize in match (Hind1 G1 (P::D) N ? tjN);
205 [#H (normalize in H) (applyS H) | normalize // ]
207 |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
209 @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 //
210 |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
211 #G1 #D #N #Heq #tjN @dummy /2/
215 (* weakening lemma: special case *)
216 axiom tj_weak_1: ∀G,t,u. G ⊢ t : u → ∀w. w :: G ⊢ lift t 0 1 : lift u 0 1.
219 (* thinning lemma: special case *)
220 axiom tj_thin_1: ∀w,G,t,u. w :: G ⊢ lift t 0 1 : lift u 0 1 → G ⊢ t : u.