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 "pts_dummy/par_reduction.ma".
13 include "basics/star.ma".
16 inductive T : Type[0] ≝
20 | Lambda: T → T → T (* type, body *)
21 | Prod: T → T → T (* type, body *)
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 | d: ∀M,M1. red M M1 → red (D M) (D M1).
35 lemma red_to_pr: ∀M,N. red M N → pr M N.
36 #M #N #redMN (elim redMN) /2/
39 lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
40 #M #P #redMP (inversion redMP)
41 [#P1 #M1 #N1 #eqH destruct
42 |2,3,4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
43 |#Q1 #M1 #red1 #_ #eqH destruct #eqP @(ex_intro … M1) /2/
47 lemma red_lambda : ∀M,N,P. red (Lambda M N) P →
48 (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨
49 (∃N1. P = (Lambda M N1) ∧ red N N1).
50 #M #N #P #redMNP (inversion redMNP)
51 [#P1 #M1 #N1 #eqH destruct
52 |2,3,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
53 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
54 (@(ex_intro … M1)) % //
55 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
56 (@(ex_intro … N1)) % //
57 |#Q1 #M1 #red1 #_ #eqH destruct
61 lemma red_prod : ∀M,N,P. red (Prod M N) P →
62 (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
63 (∃N1. P = (Prod M N1) ∧ red N N1).
64 #M #N #P #redMNP (inversion redMNP)
65 [#P1 #M1 #N1 #eqH destruct
66 |2,3,4,5:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
67 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
68 (@(ex_intro … M1)) % //
69 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
70 (@(ex_intro … N1)) % //
71 |#Q1 #M1 #red1 #_ #eqH destruct
75 lemma red_app : ∀M,N,P. red (App M N) P →
76 (∃M1,N1. M = (Lambda M1 N1) ∧ P = N1[0:=N]) ∨
77 (∃M1. P = (App M1 N) ∧ red M M1) ∨
78 (∃N1. P = (App M N1) ∧ red N N1).
79 #M #N #P #redMNP (inversion redMNP)
80 [#P1 #M1 #N1 #eqH destruct #eqP %1 %1
81 @(ex_intro … P1) @(ex_intro … M1) % //
82 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
83 (@(ex_intro … M1)) % //
84 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
85 (@(ex_intro … N1)) % //
86 |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
87 |#Q1 #M1 #red1 #_ #eqH destruct
91 definition reduct ≝ λn,m. red m n.
93 definition SN ≝ WF ? reduct.
95 definition NF ≝ λM. ∀N. ¬ (reduct N M).
97 theorem NF_to_SN: ∀M. NF M → SN M.
98 #M #nfM % #a #red @False_ind /2/
101 lemma NF_Sort: ∀i. NF (Sort i).
102 #i #N % #redN (inversion redN)
103 [1: #P #N #M #H destruct
104 |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct
105 |#M #N #_ #_ #H destruct
109 lemma NF_Rel: ∀i. NF (Rel i).
110 #i #N % #redN (inversion redN)
111 [1: #P #N #M #H destruct
112 |2,3,4,5,6,7: #N #M #P #_ #_ #H destruct
113 |#M #N #_ #_ #H destruct
117 lemma red_subst : ∀N,M,M1,i. red M M1 → red M[i≝N] M1[i≝N].
118 #N @Telim_size #P (cases P)
119 [1,2:#j #Hind #M1 #i #r1 @False_ind /2/
120 |#P #Q #Hind #M1 #i #r1 (cases (red_app … r1))
122 [* #M2 * #N2 * #eqP #eqM1 >eqP normalize
123 >eqM1 >(plus_n_O i) >(subst_lemma N2) <(plus_n_O i)
124 (cut (i+1 =S i)) [//] #Hcut >Hcut @rbeta
125 |* #M2 * #eqM1 #rP >eqM1 normalize @rappl @Hind /2/
127 |* #N2 * #eqM1 #rQ >eqM1 normalize @rappr @Hind /2/
129 |#P #Q #Hind #M1 #i #r1 (cases (red_lambda …r1))
130 [* #P1 * #eqM1 #redP >eqM1 normalize @rlaml @Hind /2/
131 |* #Q1 * #eqM1 #redP >eqM1 normalize @rlamr @Hind /2/
133 |#P #Q #Hind #M1 #i #r1 (cases (red_prod …r1))
134 [* #P1 * #eqM1 #redP >eqM1 normalize @rprodl @Hind /2/
135 |* #P1 * #eqM1 #redP >eqM1 normalize @rprodr @Hind /2/
137 |#P #Hind #M1 #i #r1 (cases (red_d …r1))
138 #P1 * #eqM1 #redP >eqM1 normalize @d @Hind /2/
142 lemma red_lift: ∀N,N1,n. red N N1 → ∀k. red (lift N k n) (lift N1 k n).
143 #N #N1 #n #r1 (elim r1) normalize /2/
147 lemma star_appl: ∀M,M1,N. star … red M M1 →
148 star … red (App M N) (App M1 N).
149 #M #M1 #N #star1 (elim star1) //
150 #B #C #starMB #redBC #H @(inj … H) /2/
153 lemma star_appr: ∀M,N,N1. star … red N N1 →
154 star … red (App M N) (App M N1).
155 #M #N #N1 #star1 (elim star1) //
156 #B #C #starMB #redBC #H @(inj … H) /2/
159 lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
160 star … red (App M N) (App M1 N1).
161 #M #M1 #N #N1 #redM #redN @(trans_star ??? (App M1 N)) /2/
164 lemma star_laml: ∀M,M1,N. star … red M M1 →
165 star … red (Lambda M N) (Lambda M1 N).
166 #M #M1 #N #star1 (elim star1) //
167 #B #C #starMB #redBC #H @(inj … H) /2/
170 lemma star_lamr: ∀M,N,N1. star … red N N1 →
171 star … red (Lambda M N) (Lambda M N1).
172 #M #N #N1 #star1 (elim star1) //
173 #B #C #starMB #redBC #H @(inj … H) /2/
176 lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
177 star … red (Lambda M N) (Lambda M1 N1).
178 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Lambda M1 N)) /2/
181 lemma star_prodl: ∀M,M1,N. star … red M M1 →
182 star … red (Prod M N) (Prod M1 N).
183 #M #M1 #N #star1 (elim star1) //
184 #B #C #starMB #redBC #H @(inj … H) /2/
187 lemma star_prodr: ∀M,N,N1. star … red N N1 →
188 star … red (Prod M N) (Prod M N1).
189 #M #N #N1 #star1 (elim star1) //
190 #B #C #starMB #redBC #H @(inj … H) /2/
193 lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 →
194 star … red (Prod M N) (Prod M1 N1).
195 #M #M1 #N #N1 #redM #redN @(trans_star ??? (Prod M1 N)) /2/
198 lemma star_d: ∀M,M1. star … red M M1 →
199 star … red (D M) (D M1).
200 #M #M1 #redM (elim redM) // #B #C #starMB #redBC #H @(inj … H) /2/
203 lemma red_subst1 : ∀M,N,N1,i. red N N1 →
204 (star … red) M[i≝N] M[i≝N1].
207 |#i #P #Q #n #r1 (cases (true_or_false (leb i n)))
208 [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
209 [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
210 |#eqin >eqin >subst_rel2 >subst_rel2 @R_to_star /2/
212 |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
213 >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
215 |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_app /2/
216 |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_lam /2/
217 |#P #Q #Hind1 #Hind2 #M1 #N1 #i #r1 normalize @star_prod /2/
218 |#P #Hind #M #N #i #r1 normalize @star_d /2/
222 lemma SN_d : ∀M. SN M → SN (D M).
223 #M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd))
224 #Q * #eqa #redbQ >eqa @Hind //
227 lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
228 #N * #b #H #M #red @H //.
231 lemma SN_star: ∀M,N. (star … red) N M → SN N → SN M.
232 #M #N #rstar (elim rstar) //
233 #Q #P #HbQ #redQP #snNQ #snN @(SN_step …redQP) /2/
236 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
237 ∃M1.subterm N1 M1 ∧ red M M1.
238 #M #N #subN (elim subN) /4/
239 (* trsansitive case *)
240 #P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
241 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
245 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
246 ∃M1.subterm N1 M1 ∧ red M M1.
248 lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
249 #M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN
250 (cases (sub_red … subNM ? redN)) #M1 *
251 #subN1M1 #redMM1 @(HindM … redMM1) //
254 lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
255 #M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
256 lapply (H Hstar) #Hstari (elim Hstari) //
257 #M #N #_ #subNM #snM @(SN_subterm …subNM) //
260 definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
262 definition SH ≝ WF ? shrink.
264 lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
265 #M #snM (elim snM) #M
266 #snM #HindM #N #subNM (cases (star_case ???? subNM))
269 [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
270 #subN1M1 #redMM1 @(HindM M1) /2/
271 |#subN1 @(HindM N) /2/
276 theorem SN_to_SH: ∀N. SN N → SH N.
277 #N #snN (elim snN) (@Telim_size)
278 #b #Hsize #snb #Hind % #a * /2/ #subab @Hsize;
280 [#c #subac @size_subterm //
281 |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
283 |@SN_step @(SN_subterm_star b);
284 [% /2/ |@TC_to_star @subab] % @snb
285 |#a1 #reda1 cases(sub_star_red b a ?? reda1);
286 [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]
290 lemma SH_to_SN: ∀N. SH N → SN N.
291 @WF_antimonotonic /2/ qed.
293 lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
294 #N #snN (elim snN) #P #shP #HindP #M #snM
295 (* for M we proceed by induction on SH *)
296 (lapply (SN_to_SH ? snM)) #shM (elim shM)
297 #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH))
298 [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
300 |* #S * #eqa #redQS >eqa @(HindQ S) /2/
304 lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M).
305 #N #snN (elim snN) #P #shP #HindP #M #snM (elim snM)
306 #Q #snQ #HindQ % #a #redH (cases (red_prod … redH))
307 [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
309 |* #S * #eqa #redQS >eqa @(HindQ S) /2/
313 lemma SN_subst: ∀i,N,M.SN M[i ≝ N] → SN M.
314 #i #N (cut (∀P.SN P → ∀M.P=M[i ≝ N] → SN M));
315 [#P #H (elim H) #Q #snQ #Hind #M #eqM % #M1 #redM
316 @(Hind M1[i:=N]) // >eqM /2/
317 |#Hcut #M #snM @(Hcut … snM) //
321 lemma SN_DAPP: ∀N,M. SN (App M N) → SN (App (D M) N).
322 cut (∀P. SN P → ∀M,N. P = App M N → SN (App (D M) N)); [|/2/]
323 #P #snP (elim snP) #Q #snQ #Hind
324 #M #N #eqQ % #A #rA (cases (red_app … rA))
327 [* #M1 * #N1 * #eqH destruct
328 |* #M1 * #eqH destruct #eqA >eqA @SN_d % @snQ
330 |* #M1 * #eqA #red1 (cases (red_d …red1))
331 #M2 * #eqM1 #r2 >eqA >eqM1 @(Hind (App M2 N)) /2/
333 |* #M2 * #eqA >eqA #r2 @(Hind (App M M2)) /2/
337 lemma SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
338 SN M[0:=N] → SN (App (Lambda P M) N).
339 #P #snP (elim snP) #A #snA #HindA
340 #N #snN (elim snN) #B #snB #HindB
341 #M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM
342 (generalize in match snM1) (elim shM)
343 #C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
345 [* #M2 * #N2 * #eqlam destruct #eqQ //
346 |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam))
347 [* #M3 * #eqM2 #r2 >eqM2 @HindA // % /2/
348 |* #M3 * #eqM2 #r2 >eqM2 @HindC;
349 [%1 // |@(SN_step … snC1) /2/]
352 |* #M2 * #eqQ #r2 >eqQ @HindB // @(SN_star … snC1)