]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/PTS/subst.ma
5282e86baa5465c7e14e4eccaadd99dcf80b1eb6
[helm.git] / helm / software / matita / nlibrary / PTS / subst.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basics/list2.ma".
16
17 ninductive T : Type ≝
18   | Sort: nat → T
19   | Rel: nat → T 
20   | App: T → T → T 
21   | Lambda: T → T → T (* type, body *)
22   | Prod: T → T → T (* type, body *)
23 .
24
25 nlet rec lift t k p ≝
26   match t with 
27     [ Sort n ⇒ Sort n
28     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
29     | App m n ⇒ App (lift m k p) (lift n k p)
30     | Lambda m n ⇒ Lambda (lift m k p) (lift n (k+1) p)
31     | Prod m n ⇒ Prod (lift m k p) (lift n (k+1) p)
32     ].
33
34 (* 
35 ndefinition lift ≝ λt.λp.lift_aux t 0 p.*)
36
37 notation "↑ \sup n ( M )" non associative with precedence 70 for @{'Lift O $M}.
38 notation "↑ \sub k \sup n ( M )" non associative with precedence 70 for @{'Lift $n $k $M}.
39
40 (* interpretation "Lift" 'Lift n M = (lift M n). *)
41 interpretation "Lift" 'Lift n k M = (lift M k n).
42
43 nlet rec subst t k a ≝ 
44   match t with 
45     [ Sort n ⇒ Sort n
46     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
47         (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
48     | App m n ⇒ App (subst m k a) (subst n k a)
49     | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
50     | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
51     ].
52
53 (* meglio non definire 
54 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
55 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
56 *)
57
58 notation "M [ k ← N]" non associative with precedence 90 for @{'Subst $M $k $N}.
59
60 (* interpretation "Subst" 'Subst N M = (subst N M). *)
61 interpretation "Subst" 'Subst M k N = (subst M k N).
62
63 (*** properties of lift and subst ***)
64
65 nlemma lift_0: ∀t:T.∀k. lift t k 0 = t.
66 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k); 
67 nnormalize;//;nqed.
68
69 (* nlemma lift_0: ∀t:T. lift t 0 = t.
70 #t; nelim t; nnormalize; //; nqed. *)
71
72 nlemma lift_sort: ∀i,k,n. lift (Sort i) k n = Sort i.
73 //; nqed.
74
75 nlemma lift_rel: ∀i,n. lift (Rel i) 0 n = Rel (i+n).
76 //; nqed.
77
78 nlemma lift_rel1: ∀i.lift (Rel i) 0 1 = Rel (S i).
79 #i; nchange with (lift (Rel i) 0 1 = Rel (1 + i)); //; nqed.
80
81 nlemma lift_lift: ∀t.∀i,j.j ≤ i  → ∀h,k. 
82   lift (lift t k i) (j+k) h = lift t k (i+h).
83 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
84 napply (leb_elim (S n) k); #Hnk;nnormalize;
85   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
86   ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); 
87      nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
88      napply le_plus;//;napply not_lt_to_le;/2/;
89   ##]
90 nqed.
91
92 nlemma lift_lift1: ∀t.∀i,j,k. 
93   lift(lift t k j) k i = lift t k (j+i).
94 #t;/3/; nqed.
95
96 nlemma lift_lift2: ∀t.∀i,j,k. 
97   lift (lift t k j) (j+k) i = lift t k (j+i).
98 #t; /2/; nqed.
99
100 (*
101 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
102 nnormalize; //; nqed. *)
103
104 nlemma subst_lift_k: ∀A,B.∀k. subst (lift B k 1) k A = B.
105 #A; #B; nelim B; nnormalize; /2/; #n; #k;
106 napply (leb_elim (S n) k); nnormalize; #Hnk;
107   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
108   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
109       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
110          nnormalize;/2/; napply (not_to_not … Hnk);//;
111       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
112       ##]
113   ##]
114 nqed.
115
116 (*
117 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
118 nnormalize; //; nqed. *)
119
120 nlemma subst_sort: ∀A.∀n,k. subst (Sort n) k A = Sort n.
121 //; nqed.
122
123 nlemma subst_rel: ∀A.subst (Rel 0) 0 A = A.
124 nnormalize; //; nqed.
125
126 nlemma subst_rel1: ∀A.∀k,i. i < k → 
127   subst (Rel i) k A = Rel i.
128 #A; #k; #i; nnormalize; #ltik;
129 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
130
131 nlemma subst_rel2: ∀A.∀k. 
132   subst (Rel k) k A = lift A 0 k.
133 #A; #k; nnormalize; 
134 nrewrite > (lt_to_leb_false (S k) k ?); //; 
135 nrewrite > (eq_to_eqb_true … (refl …)); //;
136 nqed.
137
138 nlemma subst_rel3: ∀A.∀k,i. k < i → 
139   subst (Rel i) k A = Rel (i-1).
140 #A; #k; #i; nnormalize; #ltik;
141 nrewrite > (lt_to_leb_false (S i) k ?); /2/; 
142 nrewrite > (not_eq_to_eqb_false i k ?); //;
143 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
144 nqed.
145
146 nlemma lift_subst_ijk: ∀A,B.∀i,j,k.
147   lift (subst B (j+k) A) k i = subst (lift B k i) (j+k+i) A.
148 #A; #B; #i; #j; nelim B; nnormalize; /2/; #n; #k;
149 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
150   ##[nelim (leb (S n) k);
151     ##[nrewrite > (subst_rel1 A (j+k+i) n ?);/2/;
152     ##|nrewrite > (subst_rel1 A (j+k+i) (n+i) ?);/2/;
153     ##]
154   ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
155     ##[nrewrite > (lt_to_leb_false (S n) k ?);
156        ##[ncut (j+k+i = n+i);##[//;##] #Heq;
157           nrewrite > Heq; nrewrite > (subst_rel2 A ?);
158           nnormalize; napplyS lift_lift;//;
159        ##|/2/;
160        ##]
161     ##|ncut (j + k < n);
162       ##[napply not_eq_to_le_to_lt;
163         ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
164       ##|#ltjkn;
165          ncut (O < n); ##[/2/; ##] #posn;
166          ncut (k ≤ n); ##[/2/; ##] #lekn;
167          nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
168           ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
169              nrewrite > (subst_rel3 A (j+k+i) (n+i) ?);
170               ##[/3/; ##|/2/; ##]
171           ##|napply le_S_S;/3/;  (* /3/;*)
172           ##]
173      ##]
174   ##]
175 nqed. 
176
177 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
178   subst (lift B i (S k)) j A = (lift B i k).
179 #A; #B; nelim B; nnormalize; /2/;
180    ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
181       napply eq_f2; /2/; napply Hind2;
182       napplyS (monotonic_le_plus_l 1);//
183    ##|#n; #i; #j; #k; #leij; #ltjk;
184       napply (leb_elim (S n) i); nnormalize; #len;
185       ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
186       ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
187         ##[nnormalize; 
188            nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
189            nnormalize; /2/; napply (not_to_not …len);
190            #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
191            nnormalize; //; 
192         ##|napply le_S_S; napply (transitive_le … ltjk);
193            napply le_plus;//; napply not_lt_to_le; /2/;
194         ##]
195     ##]
196 nqed.
197      
198 (********************* substitution lemma ***********************)    
199
200 nlemma subst_lemma: ∀A,B,C.∀k,i. 
201   subst (subst A i B) (k+i) C = 
202     subst (subst A (S (k+i)) C) i (subst B k C).
203 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
204 #n; #i; napply (leb_elim (S n) i); #Hle;
205   ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
206      ncut (n ≤ k+i); ##[/2/##] #len;
207      nrewrite > (subst_rel1 C (k+i) n ltn);
208      nrewrite > (le_to_leb_true n (k+i) len);
209      nrewrite > (subst_rel1 … Hle);//;
210   ##|napply (eqb_elim n i); #eqni;
211     ##[nrewrite > eqni; 
212        nrewrite > (le_to_leb_true i (k+i) ?); //;
213        nrewrite > (subst_rel2 …); nnormalize; 
214        napply sym_eq; 
215        napplyS (lift_subst_ijk C B i k O);
216     ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
217       ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
218          nrewrite > (le_to_leb_true n (k+i) ?);
219         ##[nrewrite > (subst_rel3 ? i n ?);//;
220            napply not_eq_to_le_to_lt;
221             ##[/2/;
222             ##|napply not_lt_to_le;/2/;
223             ##]
224         ##|napply (transitive_le … nk);//;
225         ##]
226       ##|ncut (i < n);
227         ##[napply not_eq_to_le_to_lt; ##[/2/]
228            napply (not_lt_to_le … Hle);##]
229          #ltin; ncut (O < n); ##[/2/;##] #posn;
230          napply (eqb_elim (n-1) (k+i)); #H
231          ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
232             nrewrite > (lt_to_leb_false n (k+i) ?);
233             ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); 
234               ##[nnormalize;
235               ##|nrewrite < H; napplyS plus_minus_m_m;//;
236               ##]
237             ##|nrewrite < H; napply (lt_O_n_elim … posn);
238                #m; nnormalize;//;
239             ##]
240          ##|ncut (k+i < n-1);
241             ##[napply not_eq_to_le_to_lt;
242               ##[napply symmetric_not_eq; napply H;
243               ##|napply (not_lt_to_le … nk);
244               ##]
245             ##]
246             #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
247             ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
248               ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
249                  nrewrite > (subst_rel3 ? i (n-1) ?);//;
250                  napply (le_to_lt_to_lt … Hlt);//;
251               ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
252               ##]
253             ##|napply (transitive_lt … Hlt);
254                napply (lt_O_n_elim … posn);
255                #m; nnormalize;//;
256             ##]
257           ##]
258           nrewrite <H;
259           ncut (∃m:nat. S m = n);
260           ##[napply (lt_O_n_elim … posn); #m;@ m;//;
261             ##|*; #m; #Hm; nrewrite < Hm;
262                nrewrite > (delift ???????);nnormalize;/2/;
263           ##]
264 nqed.
265   
266
267
268