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 "basics/list2.ma".
21 | Lambda: T → T → T (* type, body *)
22 | Prod: T → T → T (* type, body *)
25 nlet rec lift_aux t k p ≝
28 | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
29 | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
30 | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
31 | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
34 ndefinition lift ≝ λt.λp.lift_aux t 0 p.
36 notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift $n $M}.
37 notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift_aux $n $k $M}.
39 interpretation "Lift" 'Lift n M = (lift M n).
40 interpretation "Lift_aux" 'Lift_aux n k M = (lift_aux M k n).
42 nlet rec subst_aux t k a ≝
45 | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
46 (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
47 | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
48 | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
49 | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
52 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
54 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
55 notation "M [ k ← N]" non associative with precedence 90 for @{'Subst_aux $M $k $N}.
57 interpretation "Subst" 'Subst N M = (subst N M).
58 interpretation "Subst_aux" 'Subst_aux M k N = (subst_aux M k N).
60 (*** properties of lift and subst ***)
62 nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
63 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k);
66 nlemma lift_0: ∀t:T. lift t 0 = t.
67 #t; nelim t; nnormalize; //; nqed.
69 nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
72 nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
75 nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
76 #i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
78 nlemma lift_lift_aux: ∀t.∀i,j.j ≤ i → ∀h,k.
79 lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
80 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
81 napply (leb_elim (S n) k); #Hnk;nnormalize;
82 ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
83 ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?);
84 nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
85 napply le_plus;//;napply not_lt_to_le;/2/;
89 nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
92 nlemma lift_lift_aux2: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
95 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
98 nlemma subst_lift_aux_k: ∀A,B.∀k.
99 subst_aux (lift_aux B k 1) k A = B.
100 #A; #B; nelim B; nnormalize; /2/; #n; #k;
101 napply (leb_elim (S n) k); nnormalize; #Hnk;
102 ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
103 ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
104 ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
105 nnormalize;/2/; napply (not_to_not … Hnk);//;
106 ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
111 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
112 nnormalize; //; nqed.
114 nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
117 nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
120 nlemma subst_rel: ∀A.subst A (Rel O) = A.
121 nnormalize; //; nqed.
123 nlemma subst_rel1: ∀A.∀k,i. i < k →
124 subst_aux (Rel i) k A = Rel i.
125 #A; #k; #i; nnormalize; #ltik;
126 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
128 nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
130 nrewrite > (lt_to_leb_false (S k) k ?); //;
131 nrewrite > (eq_to_eqb_true … (refl …)); //;
134 nlemma subst_rel3: ∀A.∀k,i. k < i →
135 subst_aux (Rel i) k A = Rel (i-1).
136 #A; #k; #i; nnormalize; #ltik;
137 nrewrite > (lt_to_leb_false (S i) k ?); /2/;
138 nrewrite > (not_eq_to_eqb_false i k ?); //;
139 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
142 nlemma lift_subst_aux_ijk: ∀A,B.∀i,j,k.
143 lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
144 #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
145 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
146 ##[nelim (leb (S n) k);
147 ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/;
148 ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/;
150 ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
151 ##[nrewrite > (lt_to_leb_false (S n) k ?);
152 ##[ncut (j+k+i = n+i);##[//;##] #Heq;
153 nrewrite > Heq; nrewrite > (subst_rel2 A ?);
154 nnormalize; napplyS lift_lift_aux;//;
158 ##[napply not_eq_to_le_to_lt;
159 ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
161 ncut (O < n); ##[/2/; ##] #posn;
162 ncut (k ≤ n); ##[/2/; ##] #lekn;
163 nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
164 ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
165 nrewrite > (subst_rel3 A (j+k+i) (n+i) ?);
167 ##|napply le_S_S;/3/; (* /3/;*)
173 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
174 subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k).
175 #A; #B; nelim B; nnormalize; /2/;
176 ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
177 napply eq_f2;/2/; napply Hind2;
178 napplyS (monotonic_le_plus_l 1);//
179 ##|#n; #i; #j; #k; #leij; #ltjk;
180 napply (leb_elim (S n) i); nnormalize; #len;
181 ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
182 ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
184 nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
185 nnormalize; /2/; napply (not_to_not …len);
186 #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
188 ##|napply le_S_S; napply (transitive_le … ltjk);
189 napply le_plus;//; napply not_lt_to_le; /2/;
194 (********************* substitution lemma ***********************)
196 nlemma subst_lemma: ∀A,B,C.∀k,i.
197 subst_aux (subst_aux A i B) (k+i) C =
198 subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
199 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
200 #n; #i; napply (leb_elim (S n) i); #Hle;
201 ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
202 ncut (n ≤ k+i); ##[/2/##] #len;
203 nrewrite > (subst_rel1 C (k+i) n ltn);
204 nrewrite > (le_to_leb_true n (k+i) len);
205 nrewrite > (subst_rel1 … Hle);//;
206 ##|napply (eqb_elim n i); #eqni;
208 nrewrite > (le_to_leb_true i (k+i) ?); //;
209 nrewrite > (subst_rel2 …); nnormalize;
211 napplyS (lift_subst_aux_ijk C B i k O);
212 ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
213 ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
214 nrewrite > (le_to_leb_true n (k+i) ?);
215 ##[nrewrite > (subst_rel3 ? i n ?);//;
216 napply not_eq_to_le_to_lt;
218 ##|napply not_lt_to_le;/2/;
220 ##|napply (transitive_le … nk);//;
223 ##[napply not_eq_to_le_to_lt; ##[/2/]
224 napply (not_lt_to_le … Hle);##]
225 #ltin; ncut (O < n); ##[/2/;##] #posn;
226 napply (eqb_elim (n-1) (k+i)); #H
227 ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
228 nrewrite > (lt_to_leb_false n (k+i) ?);
229 ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?);
231 ##|nrewrite < H; napplyS plus_minus_m_m;//;
233 ##|nrewrite < H; napply (lt_O_n_elim … posn);
237 ##[napply not_eq_to_le_to_lt;
238 ##[napply symmetric_not_eq; napply H;
239 ##|napply (not_lt_to_le … nk);
242 #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
243 ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
244 ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
245 nrewrite > (subst_rel3 ? i (n-1) ?);//;
246 napply (le_to_lt_to_lt … Hlt);//;
247 ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
249 ##|napply (transitive_lt … Hlt);
250 napply (lt_O_n_elim … posn);
255 ncut (∃m:nat. S m = n);
256 ##[napply (lt_O_n_elim … posn); #m;@ m;//;
257 ##|*; #m; #Hm; nrewrite < Hm;
258 nrewrite > (delift ???????);nnormalize;/2/;