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 "lambda/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 | rdapp: ∀M,N. red (App (D M) N) (D (App M N))
28 | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N))
29 | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
30 | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1)
31 | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
32 | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
33 | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
34 | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
35 | d: ∀M,M1. red M M1 → red (D M) (D M1).
37 lemma red_to_pr: ∀M,N. red M N → pr M N.
38 #M #N #redMN (elim redMN) /2/
41 lemma red_d : ∀M,P. red (D M) P → ∃N. P = D N ∧ red M N.
42 #M #P #redMP (inversion redMP)
43 [#P1 #M1 #N1 #eqH destruct
44 |#M1 #N1 #eqH destruct
45 |#M1 #N1 #eqH destruct
46 |4,5,6,7,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
47 |#Q1 #M1 #red1 #_ #eqH destruct #eqP @(ex_intro … M1) /2/
51 lemma red_lambda : ∀M,N,P. red (Lambda M N) P →
52 (∃M1. P = (Lambda M1 N) ∧ red M M1) ∨
53 (∃N1. P = (Lambda M N1) ∧ red N N1) ∨
54 (∃Q. N = D Q ∧ P = D (Lambda M Q)).
55 #M #N #P #redMNP (inversion redMNP)
56 [#P1 #M1 #N1 #eqH destruct
57 |#M1 #N1 #eqH destruct
58 |#M1 #N1 #eqH destruct #eqP %2 (@(ex_intro … N1)) % //
59 |4,5,8,9:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
60 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %1
61 (@(ex_intro … M1)) % //
62 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1 %2
63 (@(ex_intro … N1)) % //
64 |#Q1 #M1 #red1 #_ #eqH destruct
68 lemma red_prod : ∀M,N,P. red (Prod M N) P →
69 (∃M1. P = (Prod M1 N) ∧ red M M1) ∨
70 (∃N1. P = (Prod M N1) ∧ red N N1).
71 #M #N #P #redMNP (inversion redMNP)
72 [#P1 #M1 #N1 #eqH destruct
73 |2,3: #M1 #N1 #eqH destruct
74 |4,5,6,7:#Q1 #Q2 #N1 #red1 #_ #eqH destruct
75 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %1
76 (@(ex_intro … M1)) % //
77 |#Q1 #M1 #N1 #red1 #_ #eqH destruct #eqP %2
78 (@(ex_intro … N1)) % //
79 |#Q1 #M1 #red1 #_ #eqH destruct
83 definition reduct ≝ λn,m. red m n.
85 definition SN ≝ WF ? reduct.
87 definition NF ≝ λM. ∀N. ¬ (reduct N M).
89 theorem NF_to_SN: ∀M. NF M → SN M.
90 #M #nfM % #a #red @False_ind /2/
93 lemma NF_Sort: ∀i. NF (Sort i).
94 #i #N % #redN (inversion redN)
95 [1: #P #N #M #H destruct
96 |2,3 :#N #M #H destruct
97 |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
98 |#M #N #_ #_ #H destruct
102 lemma NF_Rel: ∀i. NF (Rel i).
103 #i #N % #redN (inversion redN)
104 [1: #P #N #M #H destruct
105 |2,3 :#N #M #H destruct
106 |4,5,6,7,8,9: #N #M #P #_ #_ #H destruct
107 |#M #N #_ #_ #H destruct
111 lemma SN_d : ∀M. SN M → SN (D M).
112 #M #snM (elim snM) #b #H #Hind % #a #redd (cases (red_d … redd))
113 #Q * #eqa #redbQ >eqa @Hind //
116 lemma SN_step: ∀N. SN N → ∀M. reduct M N → SN M.
117 #N * #b #H #M #red @H //.
120 lemma sub_red: ∀M,N.subterm N M → ∀N1.red N N1 →
121 ∃M1.subterm N1 M1 ∧ red M M1.
122 #M #N #subN (elim subN) /4/
123 (* trsansitive case *)
124 #P #Q #S #subPQ #subQS #H1 #H2 #A #redP (cases (H1 ? redP))
125 #B * #subA #redQ (cases (H2 ? redQ)) #C * #subBC #redSC
129 axiom sub_star_red: ∀M,N.(star … subterm) N M → ∀N1.red N N1 →
130 ∃M1.subterm N1 M1 ∧ red M M1.
132 lemma SN_subterm: ∀M. SN M → ∀N.subterm N M → SN N.
133 #M #snM (elim snM) #M #snM #HindM #N #subNM % #N1 #redN
134 (cases (sub_red … subNM ? redN)) #M1 *
135 #subN1M1 #redMM1 @(HindM … redMM1) //
138 lemma SN_subterm_star: ∀M. SN M → ∀N.(star … subterm N M) → SN N.
139 #M #snM #N #Hstar (cases (star_inv T subterm M N)) #_ #H
140 lapply (H Hstar) #Hstari (elim Hstari) //
141 #M #N #_ #subNM #snM @(SN_subterm …subNM) //
144 definition shrink ≝ λN,M. reduct N M ∨ (TC … subterm) N M.
146 definition SH ≝ WF ? shrink.
148 lemma SH_subterm: ∀M. SH M → ∀N.(star … subterm) N M → SH N.
149 #M #snM (elim snM) #M
150 #snM #HindM #N #subNM (cases (star_case ???? subNM))
153 [#redN (cases (sub_star_red … subNM ? redN)) #M1 *
154 #subN1M1 #redMM1 @(HindM M1) /2/
155 |#subN1 @(HindM N) /2/
160 theorem SN_to_SH: ∀N. SN N → SH N.
161 #N #snN (elim snN) (@Telim_size)
162 #b #Hsize #snb #Hind % #a * /2/ #subab @Hsize;
164 [#c #subac @size_subterm //
165 |#b #c #subab #subbc #sab @(transitive_lt … sab) @size_subterm //
167 |@SN_step @(SN_subterm_star b);
168 [% /2/ |@TC_to_star @subab] % @snb
169 |#a1 #reda1 cases(sub_star_red b a ?? reda1);
170 [#a2 * #suba1 #redba2 @(SH_subterm a2) /2/ |/2/ ]
174 lemma SH_to_SN: ∀N. SH N → SN N.
175 @WF_antimonotonic /2/ qed.
177 lemma SN_Lambda: ∀N.SN N → ∀M.SN M → SN (Lambda N M).
178 #N #snN (elim snN) #P #shP #HindP #M #snM
179 (* for M we proceed by induction on SH *)
180 (lapply (SN_to_SH ? snM)) #shM (elim shM)
181 #Q #shQ #HindQ % #a #redH (cases (red_lambda … redH))
183 [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
185 |* #S * #eqa #redQS >eqa @(HindQ S) /2/
187 |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
192 lemma SH_Lambda: ∀N.SH N → ∀M.SH M → SN (Lambda N M).
193 #N #snN (elim snN) #P #snP #HindP #M #snM (elim snM)
194 #Q #snQ #HindQ % #a #redH (cases (red_lambda … redH))
196 [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) /2/
198 |* #S * #eqa #redQS >eqa @(HindQ S) /2/
200 |* #S * #eqQ #eqa >eqa @SN_d @(HindQ S) /3/
204 lemma SN_Prod: ∀N.SN N → ∀M.SN M → SN (Prod N M).
205 #N #snN (elim snN) #P #shP #HindP #M #snM (elim snM)
206 #Q #snQ #HindQ % #a #redH (cases (red_prod … redH))
207 [* #S * #eqa #redPS >eqa @(HindP S ? Q ?) //
209 |* #S * #eqa #redQS >eqa @(HindQ S) /2/