]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/subst.ma
Many changes
[helm.git] / matita / matita / lib / pts_dummy / subst.ma
1 (*
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.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "pts_dummy/lift.ma".
13 (*
14 let rec subst t k a ≝ 
15   match t with 
16     [ Sort n ⇒ Sort n
17     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
18         (if_then_else T (eqb n k) (lift a 0 n) (Rel (n-1)))
19     | App m n ⇒ App (subst m k a) (subst n k a)
20     | Lambda m n ⇒ Lambda (subst m k a) (subst n (k+1) a)
21     | Prod m n ⇒ Prod (subst m k a) (subst n (k+1) a)
22     | D n ⇒ D (subst n k a)
23     ].
24
25 (* meglio non definire 
26 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
27 notation "M [ N ]" non associative with precedence 90 for @{'Subst $N $M}.
28 *)
29
30 (* interpretation "Subst" 'Subst N M = (subst N M). *)
31 interpretation "Subst" 'Subst1 M k N = (subst M k N).
32
33 (*** properties of subst ***)
34
35 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
36 #A #B (elim B) normalize /2/ #n #k
37 @(leb_elim (S n) k) normalize #Hnk
38   [>(le_to_leb_true ?? Hnk) normalize //
39   |>(lt_to_leb_false (S (n + 1)) k ?) normalize
40     [>(not_eq_to_eqb_false (n+1) k ?) normalize /2/
41     |@le_S (applyS (not_le_to_lt (S n) k Hnk))
42     ]
43   ]
44 qed.
45
46 (*
47 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
48 nnormalize; //; nqed. *)
49
50 lemma subst_sort: ∀A.∀n,k.(Sort n) [k ≝ A] = Sort n.
51 // qed.
52
53 lemma subst_rel: ∀A.(Rel 0) [0 ≝ A] = A.
54 normalize // qed.
55
56 lemma subst_rel1: ∀A.∀k,i. i < k → 
57   (Rel i) [k ≝ A] = Rel i.
58 #A #k #i normalize #ltik >(le_to_leb_true (S i) k) //
59 qed.
60
61 lemma subst_rel2: ∀A.∀k. 
62   (Rel k) [k ≝ A] = lift A 0 k.
63 #A #k normalize >(lt_to_leb_false (S k) k) // >(eq_to_eqb_true … (refl …)) //
64 qed.
65
66 lemma subst_rel3: ∀A.∀k,i. k < i → 
67   (Rel i) [k ≝ A] = Rel (i-1).
68 #A #k #i normalize #ltik >(lt_to_leb_false (S i) k) /2/ 
69 >(not_eq_to_eqb_false i k) // @sym_not_eq @lt_to_not_eq //
70 qed.
71
72 lemma lift_subst_ijk: ∀A,B.∀i,j,k.
73   lift (B [j+k := A]) k i = (lift B k i) [j+k+i ≝ A].
74 #A #B #i #j (elim B) normalize /2/ #n #k
75 @(leb_elim (S n) (j + k)) normalize #Hnjk
76   [(elim (leb (S n) k))
77     [>(subst_rel1 A (j+k+i) n) /2/
78     |>(subst_rel1 A (j+k+i) (n+i)) /2/
79     ]
80   |@(eqb_elim n (j+k)) normalize #Heqnjk 
81     [>(lt_to_leb_false (S n) k);
82       [(cut (j+k+i = n+i)) [//] #Heq
83        >Heq >(subst_rel2 A ?) normalize (applyS lift_lift) //
84       |/2/
85       ]
86     |(cut (j + k < n))
87       [@not_eq_to_le_to_lt;
88         [/2/ |@le_S_S_to_le @not_le_to_lt /2/ ]
89       |#ltjkn
90        (cut (O < n)) [/2/] #posn (cut (k ≤ n)) [/2/] #lekn
91        >(lt_to_leb_false (S (n-1)) k) normalize
92         [>(lt_to_leb_false … (le_S_S … lekn))
93          >(subst_rel3 A (j+k+i) (n+i)); [/3/ |/2/]
94         |@le_S_S; (* /3/; 65 *) (applyS monotonic_pred) @le_plus_b //
95         ]
96      ]
97   ]
98 qed. 
99
100 lemma lift_subst_up: ∀M,N,n,i,j.
101   lift M[i≝N] (i+j) n = (lift M (i+j+1) n)[i≝ (lift N j n)].
102 #M (elim M) 
103   [//
104   |#p #N #n #i #j (cases (true_or_false (leb p i)))
105     [#lepi (cases (le_to_or_lt_eq … (leb_true_to_le … lepi)))
106       [#ltpi >(subst_rel1 … ltpi) 
107        (cut (p < i+j)) [@(lt_to_le_to_lt … ltpi) //] #ltpij
108        >(lift_rel_lt … ltpij); >(lift_rel_lt ?? p ?); 
109         [>subst_rel1 // | @(lt_to_le_to_lt … ltpij) //]
110       |#eqpi >eqpi >subst_rel2 >lift_rel_lt;
111         [>subst_rel2 >(plus_n_O (i+j)) 
112          applyS lift_lift_up 
113         |@(le_to_lt_to_lt ? (i+j)) //
114         ]
115       ]
116     |#lefalse (cut (i < p)) [@not_le_to_lt /2/] #ltip
117      (cut (0 < p)) [@(le_to_lt_to_lt … ltip) //] #posp
118      >(subst_rel3 … ltip) (cases (true_or_false (leb (S p) (i+j+1))))
119       [#Htrue (cut (p < i+j+1)) [@(leb_true_to_le … Htrue)] #Hlt
120        >lift_rel_lt; 
121         [>lift_rel_lt // >(subst_rel3 … ltip) // | @lt_plus_to_minus //]
122       |#Hfalse >lift_rel_ge; 
123         [>lift_rel_ge; 
124           [>subst_rel3; [@eq_f /2/ | @(lt_to_le_to_lt … ltip) //]
125           |@not_lt_to_le @(leb_false_to_not_le … Hfalse)
126           ]
127         |@le_plus_to_minus_r @not_lt_to_le 
128          @(leb_false_to_not_le … Hfalse)
129         ]
130       ]
131     ]
132   |#P #Q #HindP #HindQ #N #n #i #j normalize 
133    @eq_f2; [@HindP |@HindQ ]
134   |#P #Q #HindP #HindQ #N #n #i #j normalize 
135    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
136    <associative_plus @HindQ]
137   |#P #Q #HindP #HindQ #N #n #i #j normalize 
138    @eq_f2; [@HindP |>associative_plus >(commutative_plus j 1)
139    <associative_plus @HindQ]
140   |#P #HindP #N #n #i #j normalize 
141    @eq_f @HindP
142   ]
143 qed.
144
145 lemma lift_subst_up_O: ∀v,t,k,p. (lift t (k+1) p)[O≝lift v k p] = lift t[O≝v] k p.
146 // qed.
147
148 theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
149   (lift B i (S k)) [j ≝ A] = lift B i k.
150 #A #B (elim B) normalize /2/
151   [2,3,4: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
152    @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
153   |5:#T #Hind #i #j #k #leij #lejk @eq_f @Hind //
154   |#n #i #j #k #leij #ltjk @(leb_elim (S n) i) normalize #len
155     [>(le_to_leb_true (S n) j) /2/
156     |>(lt_to_leb_false (S (n+S k)) j);
157       [normalize >(not_eq_to_eqb_false (n+S k) j)normalize 
158        /2/ @(not_to_not …len) #H @(le_plus_to_le_r k) normalize //
159       |@le_S_S @(transitive_le … ltjk) @le_plus // @not_lt_to_le /2/
160       ]
161     ]
162   ]
163 qed.
164      
165 (********************* substitution lemma ***********************)    
166
167 lemma subst_lemma: ∀A,B,C.∀k,i. 
168   (A [i ≝ B]) [k+i ≝ C] = 
169     (A [S (k+i) := C]) [i ≝ B [k ≝ C]].
170 #A #B #C #k (elim A) normalize // (* WOW *)
171 #n #i @(leb_elim (S n) i) #Hle
172   [(cut (n < k+i)) [/2/] #ltn (* lento *) (cut (n ≤ k+i)) [/2/] #len
173    >(subst_rel1 C (k+i) n ltn) >(le_to_leb_true n (k+i) len) >(subst_rel1 … Hle) // 
174   |@(eqb_elim n i) #eqni
175     [>eqni >(le_to_leb_true i (k+i)) // >(subst_rel2 …); 
176      normalize @sym_eq (applyS (lift_subst_ijk C B i k O))
177     |@(leb_elim (S (n-1)) (k+i)) #nk
178       [>(subst_rel1 C (k+i) (n-1) nk) >(le_to_leb_true n (k+i));
179         [>(subst_rel3 ? i n) // @not_eq_to_le_to_lt;
180           [/2/ |@not_lt_to_le /2/]
181         |@(transitive_le … nk) //
182         ]
183       |(cut (i < n)) [@not_eq_to_le_to_lt; [/2/] @(not_lt_to_le … Hle)]
184        #ltin (cut (O < n)) [/2/] #posn
185        @(eqb_elim (n-1) (k+i)) #H
186         [>H >(subst_rel2 C (k+i)) >(lt_to_leb_false n (k+i));
187           [>(eq_to_eqb_true n (S(k+i))); 
188             [normalize |<H (applyS plus_minus_m_m) // ]
189            (generalize in match ltin)
190            <H @(lt_O_n_elim … posn) #m #leim >delift normalize /2/
191           |<H @(lt_O_n_elim … posn) #m normalize //
192           ]
193         |(cut (k+i < n-1))
194           [@not_eq_to_le_to_lt; [@sym_not_eq @H |@(not_lt_to_le … nk)]]
195          #Hlt >(lt_to_leb_false n (k+i));
196           [>(not_eq_to_eqb_false n (S(k+i)));
197             [>(subst_rel3 C (k+i) (n-1) Hlt);
198              >(subst_rel3 ? i (n-1)) // @(le_to_lt_to_lt … Hlt) //
199             |@(not_to_not … H) #Hn >Hn normalize //
200             ]
201           |@(transitive_lt … Hlt) @(lt_O_n_elim … posn) normalize // 
202           ]
203         ]
204       ]
205     ]
206   ] 
207 qed.
208
209 lemma subst_lemma_comm: ∀A,B,C.∀k,i.
210   (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
211 #A #B #C #k #i >commutative_plus >subst_lemma //
212 qed. 
213 *)