]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy_new/reduction.ma
almost there
[helm.git] / matita / matita / lib / pts_dummy_new / reduction.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_new/par_reduction.ma".
13 include "basics/star.ma".
14
15 (*
16 inductive T : Type[0] ≝
17   | Sort: nat → T
18   | Rel: nat → T 
19   | App: T → T → T 
20   | Lambda: T → T → T (* type, body *)
21   | Prod: T → T → T (* type, body *)
22   | D: T →T
23 . *)
24
25 inductive red : T →T → Prop ≝
26   | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
27   | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
28   | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1)
29   | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
30   | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
31   | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
32   | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
33   | dl: ∀M,M1,N. red M M1 → red (D M N) (D M1 N)
34   | dr: ∀M,N,N1. red N N1 → red (D M N) (D M N1).
35
36 lemma red_to_pr: ∀M,N. red M N → pr M N.
37 #M #N #redMN (elim redMN) /2/
38 qed.
39
40 lemma red_d : ∀M,N,P. red (D M N) P → 
41   (∃M1. P = D M1 N ∧ red M M1) ∨
42   (∃N1. P = D M N1 ∧ red N N1).
43 #M #N #P #redMP (inversion redMP)
44   [#P1 #M1 #N1 #eqH destruct
45   |2,3,4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
46   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP 
47    %1 @(ex_intro … M1) /2/
48   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP 
49    %2 @(ex_intro … N1) /2/
50   ]
51 qed.
52
53 lemma red_lambda : ∀M,N,P. red (Lambda M N) P →
54  (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨
55  (∃N1. P = (Lambda M N1) ∧ red N N1).
56 #M #N #P #redMNP (inversion redMNP)
57   [#P1 #M1 #N1 #eqH destruct
58   |2,3,6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
59   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 
60    (@(ex_intro … M1)) % //
61   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
62    (@(ex_intro … N1)) % //
63   ]
64 qed.
65   
66 lemma red_prod : ∀M,N,P. red (Prod M N) P →
67  (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
68  (∃N1. P = (Prod M N1) ∧ red N N1).
69 #M #N #P #redMNP (inversion redMNP)
70   [#P1 #M1 #N1 #eqH destruct
71   |2,3,4,5,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
72   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
73    (@(ex_intro … M1)) % //
74   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 
75    (@(ex_intro … N1)) % //
76   ]
77 qed.
78
79 lemma red_app : ∀M,N,P. red (App M N) P →
80  (∃M1,N1. M =  (Lambda M1 N1) ∧ P = N1[0:=N]) ∨
81  (∃M1. P = (App M1 N) ∧ red M M1) ∨
82  (∃N1. P = (App M N1) ∧ red N N1).
83 #M #N #P #redMNP (inversion redMNP)
84   [#P1 #M1 #N1 #eqH destruct #eqP %1 %1 
85    @(ex_intro … P1) @(ex_intro … M1) % //
86   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
87    (@(ex_intro … M1)) % //
88   |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2 
89    (@(ex_intro … N1)) % //
90   |4,5,6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
91   ]
92 qed.
93
94 definition reduct ≝ λn,m. red m n.
95
96 definition SN : T → Prop ≝ WF ? reduct.
97
98 definition NF : T → Prop ≝ λM. ∀N. ¬ (reduct N M).
99
100 theorem NF_to_SN: ∀M. NF M → SN M.
101 #M #nfM % #a #red @False_ind /2/
102 qed.
103
104 lemma NF_Sort: ∀i. NF (Sort i).
105 #i #N % #redN (inversion redN) 
106   [1: #P #N #M #H destruct
107   |2,3,4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
108   ]
109 qed.
110
111 lemma NF_Rel: ∀i. NF (Rel i).
112 #i #N % #redN (inversion redN) 
113   [1: #P #N #M #H destruct
114   |2,3,4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
115   ]
116 qed.
117
118 lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
119 #N @Telim_size #P (cases P) 
120   [1,2:#j #Hind #M1 #i #r1 @False_ind /2/
121   |#P #Q #Hind #M1 #i #r1 (cases (red_app … r1))
122     [*
123       [* #M2 * #N2 * #eqP #eqM1 >eqP normalize
124        >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i)
125        (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta
126       |* #M2 * #eqM1 #rP >eqM1 normalize @rappl @Hind /2/
127       ]
128     |* #N2 * #eqM1 #rQ >eqM1 normalize @rappr @Hind /2/
129     ] 
130   |#P #Q #Hind #M1 #i #r1 (cases (red_lambda …r1)) 
131     [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/
132     |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/
133     ]
134   |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1))
135     [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/
136     |* #P1 * #eqM1 #redP >eqM1 normalize @rprodr @Hind /2/
137     ]
138   |#P #Q #Hind #M1 #i #r1 (cases (red_d …r1))
139     [* #P1 * #eqM1 #redP >eqM1 normalize @dl @Hind /2/
140     |* #P1 * #eqM1 #redP >eqM1 normalize @dr @Hind /2/
141     ]
142 qed.
143
144 lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n).
145 #N #N1 #n #r1 (elim r1) normalize /2/
146 qed.
147
148 (* star red *)
149 lemma star_appl: ∀M,M1,N. star … red M M1 → 
150   star … red (App M N) (App M1 N).
151 #M #M1 #N #star1 (elim star1) //
152 #B #C #starMB #redBC #H /3 width=3/ 
153 qed.
154   
155 lemma star_appr: ∀M,N,N1. star … red N N1 →
156   star … red (App M N) (App M N1).
157 #M #N #N1 #star1 (elim star1) // 
158 #B #C #starMB #redBC #H /3 width=3/
159 qed.
160  
161 lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
162   star … red (App M N) (App M1 N1).
163 #M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/
164 qed.
165
166 lemma star_laml: ∀M,M1,N. star … red M M1 → 
167   star … red (Lambda M N) (Lambda M1 N).
168 #M #M1 #N #star1 (elim star1) //
169 #B #C #starMB #redBC #H /3 width=3/ 
170 qed.
171   
172 lemma star_lamr: ∀M,N,N1. star … red N N1 →
173   star … red (Lambda M N) (Lambda M N1).
174 #M #N #N1 #star1 (elim star1) //
175 #B #C #starMB #redBC #H /3 width=3/
176 qed.
177  
178 lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
179   star … red (Lambda M N) (Lambda M1 N1).
180 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/
181 qed.
182
183 lemma star_prodl: ∀M,M1,N. star … red M M1 → 
184   star … red (Prod M N) (Prod M1 N).
185 #M #M1 #N #star1 (elim star1) //
186 #B #C #starMB #redBC #H /3 width=3/
187 qed.
188   
189 lemma star_prodr: ∀M,N,N1. star … red N N1 →
190   star … red (Prod M N) (Prod M N1).
191 #M #N #N1 #star1 (elim star1) //
192 #B #C #starMB #redBC #H /3 width=3/
193 qed.
194  
195 lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
196   star … red (Prod M N) (Prod M1 N1).
197 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/
198 qed.
199
200 lemma star_dl: ∀M,M1,N. star … red M M1 → 
201   star … red (D M N) (D M1 N).
202 #M #M1 #N #star1 (elim star1) //
203 #B #C #starMB #redBC #H /3 width=3/
204 qed.
205   
206 lemma star_dr: ∀M,N,N1. star … red N N1 →
207   star … red (D M N) (D M N1).
208 #M #N #N1 #star1 (elim star1) //
209 #B #C #starMB #redBC #H /3 width=3/
210 qed.
211
212 lemma star_d: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
213   star … red (D M N) (D M1 N1).
214 #M #M1 #N #N1 #redM #redN @(trans_star ??? (D M1 N)) /2/
215 qed.
216
217 lemma red_subst1 : ∀M,N,N1,i. red N N1 → 
218  (star … red) M[i≝N] M[i≝N1].
219 #M (elim M)
220   [// 
221   |#i #P #Q #n #r1 (cases (true_or_false (leb i n)))
222     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
223       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
224       |#eqin >eqin >subst_rel2 >subst_rel2 @R_to_star /2/
225       ]
226     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
227      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
228     ]
229   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/ 
230   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/
231   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/
232   |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_d /2/
233   ]
234 qed. 
235
236 lemma SN_d : ∀M. SN M → ∀N. SN N → SN (D M N). 
237 #M #snM (elim snM) #b #H #Hind 
238 #N #snN (elim snN) #c #H1 #Hind1 % #a #redd 
239 (cases (red_d … redd))
240   [* #Q * #eqa #redbQ >eqa @Hind // % /2/
241   |* #Q * #eqa #redbQ >eqa @Hind1 //
242   ]
243 qed. 
244
245 lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
246 #N * #b #H #M #red @H //.
247 qed. 
248
249 lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M.
250 #M #N #rstar (elim rstar) //
251 #Q #P #HbQ  #redQP #snNQ #snN @(SN_step …redQP) /2/
252 qed. 
253
254 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 → 
255 ∃M1.subterm N1 M1 ∧ red M M1.
256 #M #N #subN (elim subN) /4/
257 (* trsansitive case *)
258 #P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
259 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
260 @(ex_intro … C) /3/
261 qed.
262
263 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 → 
264 ∃M1.subterm N1 M1 ∧ red M M1.
265   
266 lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
267 #M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN 
268 (cases (sub_red … subNM ? redN)) #M1 *
269 #subN1M1 #redMM1 @(HindM … redMM1) //
270 qed.
271
272 lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
273 #M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
274 lapply (H Hstar) #Hstari (elim Hstari) //
275 #M #N #_ #subNM #snM @(SN_subterm …subNM) //
276 qed.
277
278 definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
279
280 definition SH ≝ WF ? shrink.
281
282 lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
283 #M #snM (elim snM) #M 
284 #snM #HindM #N #subNM (cases (star_case ???? subNM))
285   [#eqNM >eqNM % /2/
286   |#subsNM % #N1 *
287     [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
288      #subN1M1 #redMM1 @(HindM M1) /2/
289     |#subN1 @(HindM N) /2/ 
290     ]
291   ]
292 qed.
293
294 theorem SN_to_SH: ∀N. SN N → SH N.
295 #N #snN (elim snN) (@Telim_size) 
296 #b #Hsize #snb #Hind % #a * /2/ #subab @Hsize; 
297   [(elim subab) 
298     [#c #subac @size_subterm // 
299     |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
300     ]    
301   |@SN_step @(SN_subterm_star b); 
302     [% /2/ |@TC_to_star @subab] % @snb
303   |#a1 #reda1 cases(sub_star_red b a ?? reda1);
304     [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]  
305   ]
306 qed.
307
308 lemma SH_to_SN: ∀N. SH N → SN N.
309 @WF_antimonotonic /2/ qed.
310
311 lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
312 #N #snN (elim snN) #P #shP #HindP #M #snM 
313 (* for M we proceed by induction on SH *)
314 (lapply (SN_to_SH ? snM)) #shM (elim shM)
315 #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH))
316   [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // 
317    @SH_to_SN % /2/ 
318   |* #S * #eqa #redQS >eqa @(HindQ S) /2/
319   ]
320 qed. 
321  
322 lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M).
323 #N #snN (elim snN) #P #shP #HindP #M #snM (elim snM)
324 #Q #snQ #HindQ % #a #redH (cases (red_prod … redH))
325   [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) // 
326    % /2/ 
327   |* #S * #eqa #redQS >eqa @(HindQ S) /2/
328   ]
329 qed.
330
331 lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M.
332 #i #N (cut (∀P.SN P → ∀M.P=M[i ≝ N] → SN M)); 
333   [#P #H (elim H) #Q #snQ #Hind #M #eqM % #M1 #redM 
334    @(Hind M1[i:=N]) // >eqM /2/
335   |#Hcut #M #snM @(Hcut … snM) //
336 qed.
337
338 (*
339 lemma SN_DAPP: ∀N,M. SN (App M N) → SN (App (D M) N).
340 cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/]
341 #P #snP (elim snP) #Q #snQ #Hind
342 #M #N #eqQ % #A #rA (cases (red_app … rA))
343   [* 
344     [*
345       [* #M1 * #N1 * #eqH destruct
346       |* #M1 * #eqH destruct #eqA >eqA @SN_d % @snQ
347       ]
348     |* #M1 * #eqA #red1 (cases (red_d …red1))
349      #M2 * #eqM1 #r2 >eqA >eqM1 @(Hind (App M2 N)) /2/
350     ]
351   |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/
352   ]
353 qed. *)
354
355 lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
356   SN M[0:=N] → SN (App (Lambda P M) N).
357 #P #snP (elim snP) #A #snA #HindA
358 #N #snN (elim snN) #B #snB #HindB
359 #M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM 
360 generalize in match snM1; elim shM
361 #C #shC #HindC #snC1 % #Q #redQ cases (red_app … redQ);
362   [*
363     [* #M2 * #N2 * #eqlam destruct #eqQ //
364     |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam))
365       [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/
366       |* #M3 * #eqM2 #r2 >eqM2 @HindC; 
367         [%1 // |@(SN_step … snC1) /2/]
368       ]
369     ]
370   |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1) 
371    @red_subst1 //
372   ]
373 qed.
374
375
376
377