]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/pts_dummy/par_reduction.ma
Many changes
[helm.git] / matita / matita / lib / pts_dummy / par_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/subterms.ma".
13 (*
14 (*
15 inductive T : Type[0] ≝
16   | Sort: nat → T
17   | Rel: nat → T 
18   | App: T → T → T 
19   | Lambda: T → T → T (* type, body *)
20   | Prod: T → T → T (* type, body *)
21   | D: T →T
22 . *)
23
24 (*
25 let rec is_dummy M ≝ 
26 match M with 
27   [D P ⇒ true
28   |_ ⇒ false
29   ]. *)
30   
31 let rec is_lambda M ≝ 
32 match M with 
33   [Lambda P Q ⇒ true
34   |_ ⇒ false
35   ]. 
36
37 (* 
38 theorem is_dummy_to_exists: ∀M. is_dummy M = true → 
39 ∃N. M = D N.
40 #M (cases M) normalize 
41   [1,2: #n #H destruct|3,4,5: #P #Q #H destruct
42   |#N #_ @(ex_intro … N) //
43   ]
44 qed.*)
45
46 theorem is_lambda_to_exists: ∀M. is_lambda M = true → 
47 ∃P,N. M = Lambda P N.
48 #M (cases M) normalize 
49   [1,2,6: #n #H destruct|3,5: #P #Q #H destruct
50   |#P #N #_ @(ex_intro … P) @(ex_intro … N) //
51   ]
52 qed. 
53
54 inductive pr : T →T → Prop ≝
55   | beta: ∀P,M,N,M1,N1. pr M M1 → pr N N1 →
56       pr (App (Lambda P M) N) (M1[0 ≝ N1])
57   | none: ∀M. pr M M
58   | appl: ∀M,M1,N,N1. pr M M1 → pr N N1 → pr (App M N) (App M1 N1)
59   | lam: ∀P,P1,M,M1. pr P P1 → pr M M1 → 
60       pr (Lambda P M) (Lambda P1 M1)
61   | prod: ∀P,P1,M,M1. pr P P1 → pr M M1 → 
62       pr (Prod P M) (Prod P1 M1)
63   | d: ∀M,M1. pr M M1 → pr (D M) (D M1).
64
65 lemma prSort: ∀M,n. pr (Sort n) M → M = Sort n.
66 #M #n #prH (inversion prH)
67   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
68   |//
69   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
70   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
71   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
72   |#M #N #_ #_ #H destruct
73   ]
74 qed.
75
76 lemma prRel: ∀M,n. pr (Rel n) M → M = Rel n.
77 #M #n #prH (inversion prH)
78   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
79   |//
80   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
81   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
82   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
83   |#M #N #_ #_ #H destruct
84   ]
85 qed.
86
87 lemma prD: ∀M,N. pr (D N) M → ∃P.M = D P ∧ pr N P.
88 #M #N #prH (inversion prH)  
89   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct
90   |#M #eqM #_ @(ex_intro … N) /2/ 
91   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
92   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
93   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
94   |#M1 #N1 #pr #_ #H destruct #eqM @(ex_intro … N1) /2/
95   ]
96 qed.
97
98 lemma prApp_not_lambda: 
99 ∀M,N,P. pr (App M N) P → is_lambda M = false →
100   ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
101 #M #N #P #prH (inversion prH)
102   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct #_ #H1 destruct
103   |#M1 #eqM1 #_ #_ @(ex_intro … M) @(ex_intro … N) /3/ 
104   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H #H1 #_ destruct 
105    @(ex_intro … N1) @(ex_intro … N2) /3/ 
106   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
107   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
108   |#M #N #_ #_ #H destruct
109   ]
110 qed. 
111
112 lemma prApp_lambda: 
113 ∀Q,M,N,P. pr (App (Lambda Q M) N) P → 
114   ∃M1,N1. (P = M1[0:=N1] ∧ pr M M1 ∧ pr N N1) ∨
115    (P = (App M1 N1) ∧ pr (Lambda Q M) M1 ∧ pr N N1).
116 #Q #M #N #P #prH (inversion prH)
117   [#R #M #N #M1 #N1 #pr1 #pr2 #_ #_ #H destruct #_ 
118    @(ex_intro … M1) @(ex_intro … N1) /4/ 
119   |#M1 #eqM1 #_ @(ex_intro … (Lambda Q M)) @(ex_intro … N) /4/ 
120   |#M1 #N1 #M2 #N2 #pr1 #pr2 #_ #_ #H destruct #_
121    @(ex_intro … N1) @(ex_intro … N2) /4/ 
122   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
123   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
124   |#M #N #_ #_ #H destruct
125   ]
126 qed. 
127
128 lemma prLambda: ∀M,N,P. pr (Lambda M N) P →
129   ∃M1,N1. (P = Lambda M1 N1 ∧ pr M M1 ∧ pr N N1).
130 #M #N #P #prH (inversion prH)
131   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct 
132   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
133   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
134   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct 
135    @(ex_intro … Q1) @(ex_intro … S1) /3/
136   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
137   |#M #N #_ #_ #H destruct
138   ]
139 qed. 
140
141 lemma prProd: ∀M,N,P. pr (Prod M N) P → 
142   ∃M1,N1. P = Prod M1 N1 ∧ pr M M1 ∧ pr N N1.
143 #M #N #P #prH (inversion prH)
144   [#P #M #N #M1 #N1 #_ #_ #_ #_ #H destruct 
145   |#Q #eqQ #_ @(ex_intro … M) @(ex_intro … N) /3/
146   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
147   |#M #M1 #N #N1 #_ #_ #_ #_ #H destruct
148   |#Q #Q1 #S #S1 #pr1 #pr2 #_ #_ #H #H1 destruct
149    @(ex_intro … Q1) @(ex_intro … S1) /3/
150   |#M #N #_ #_ #H destruct
151   ]
152 qed.
153  
154 let rec full M ≝
155   match M with
156   [ Sort n ⇒ Sort n
157   | Rel n ⇒ Rel n
158   | App P Q ⇒ full_app P (full Q)
159   | Lambda P Q ⇒ Lambda (full P) (full Q)
160   | Prod P Q ⇒ Prod (full P) (full Q)
161   | D P ⇒ D (full P)
162   ]
163 and full_app M N ≝
164   match M with 
165   [ Sort n ⇒ App (Sort n) N
166   | Rel n ⇒ App (Rel n) N
167   | App P Q ⇒ App (full_app P (full Q)) N
168   | Lambda P Q ⇒ (full Q) [0 ≝ N] 
169   | Prod P Q ⇒ App (Prod (full P) (full Q)) N
170   | D P ⇒ App (D (full P)) N
171   ]
172
173
174 lemma pr_lift: ∀N,N1,n. pr N N1 → 
175   ∀k. pr (lift N k n) (lift N1 k n).
176 #N #N1 #n #pr1 (elim pr1)
177   [#P #M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
178    normalize >lift_subst_up @beta; // 
179   |// 
180   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
181    normalize @appl; [@Hind1 |@Hind2]
182   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
183    normalize @lam; [@Hind1 |@Hind2]
184   |#M1 #N1 #M2 #N2 #pr2 #pr3 #Hind1 #Hind2 #k
185    normalize @prod; [@Hind1 |@Hind2]
186   |#M1 #M2 #pr2 #Hind #k normalize @d //
187   ]
188 qed.
189
190 theorem pr_subst: ∀M,M1,N,N1,n. pr M M1 → pr N N1 → 
191   pr M[n≝N] M1[n≝N1].
192 @Telim_size #P (cases P) 
193   [#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prSort … pr1) //
194   |#i #Hind #N #M1 #N1 #n #pr1 #pr2 >(prRel … pr1)
195     (cases (true_or_false (leb i n)))
196     [#lein (cases (le_to_or_lt_eq i n (leb_true_to_le … lein)))
197       [#ltin >(subst_rel1 … ltin) >(subst_rel1 … ltin) //
198       |#eqin >eqin >subst_rel2 >subst_rel2 /2/ 
199       ]
200     |#lefalse (cut (n < i)) [@not_le_to_lt /2/] #ltni
201      >(subst_rel3 … ltni) >(subst_rel3 … ltni) //
202     ]
203   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
204    (cases (true_or_false (is_lambda Q)))
205     [#islambda (cases (is_lambda_to_exists … islambda))
206      #M2 * #N2 #eqQ >eqQ in pr1 #pr3 (cases (prApp_lambda … pr3))
207      #M3 * #N3 * 
208       [* * #eqM1 #pr4 #pr5 >eqM1 
209        >(plus_n_O n) in ⊢ (??%) >subst_lemma @beta;
210         [<plus_n_Sm <plus_n_O @Hind // >eqQ 
211          @(transitive_lt ? (size (Lambda M2 N2))) normalize //
212         |@Hind // normalize // 
213         ]
214       |* * #eqM1 #pr4 #pr5 >eqM1 @appl;  
215         [@Hind // <eqQ normalize // 
216         |@Hind // normalize // 
217         ]
218       ]
219     |#notlambda (cases (prApp_not_lambda … pr1 ?)) //
220      #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1 @appl;
221       [@Hind // normalize // |@Hind // normalize // ]
222     ]
223   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
224    (cases (prLambda … pr1))
225    #N2 * #Q1 * * #eqM1 #pr3 #pr4 >eqM1 @lam;
226     [@Hind // normalize // | @Hind // normalize // ]
227   |#Q #M #Hind #M1 #N #N1 #n #pr1 #pr2
228    (cases (prProd … pr1)) #M2 * #N2 * * #eqM1 #pr3 #pr4 >eqM1
229    @prod; [@Hind // normalize // | @Hind // normalize // ]
230   |#Q #Hind #M1 #N #N1 #n #pr1 #pr2 (cases (prD … pr1))
231    #M2 * #eqM1 #pr1 >eqM1 @d @Hind // normalize // 
232   ]
233 qed.
234  
235 lemma pr_full_app: ∀M,N,N1. pr N N1 → 
236   (∀S.subterm S M → pr S (full S)) →
237   pr (App M N) (full_app M N1).
238 #M (elim M) normalize /2/
239   [#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @Hind1 /3/
240   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @beta /2/
241   |#P #Q #Hind1 #Hind2 #N1 #N2 #prN #H @appl // @prod /2/
242   |#P #Hind #N1 #N2 #prN #H @appl // @d /2/ 
243   ]
244 qed.
245
246 theorem pr_full: ∀M. pr M (full M).
247 @Telim #M (cases M) normalize
248   [// 
249   |//
250   |#M1 #N1 #H @pr_full_app /3/
251   |#M1 #N1 #H normalize /3/
252   |#M1 #N1 #H @prod /2/
253   |#P #H @d /2/
254   ]
255 qed. 
256
257 lemma complete_app: ∀M,N,P.
258   (∀S,P.subterm S (App M N) → pr S P → pr P (full S)) →
259   pr (App M N) P → pr P (full_app M (full N)).
260 #M (elim M) normalize
261   [#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // 
262    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; 
263     [@(subH (Sort n)) // |@subH //]
264   |#n #P #Q #subH #pr1 cases (prApp_not_lambda … pr1 ?) // 
265    #M1 * #N1 * * #eqQ #pr1 #pr2 >eqQ @appl; 
266     [@(subH (Rel n)) // |@subH //]
267   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
268    cases (prApp_not_lambda … prH ?) // 
269    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; 
270     [@Hind1 /3/ |@subH //]
271   |#P #Q #Hind1 #Hind2 #N1 #P2 #subH #prH
272    cases (prApp_lambda … prH) #M2 * #N2 *
273     [* * #eqP2 #pr1 #pr2 >eqP2 @pr_subst /3/
274     |* * #eqP2 #pr1 #pr2 >eqP2 (cases (prLambda … pr1))
275      #M3 * #M4 * * #eqM2 #pr3 #pr4 >eqM2 @beta @subH /2/
276     ]
277   |#P #Q #Hind1 #Hind2 #N1 #N2 #subH #prH
278    cases (prApp_not_lambda … prH ?) // 
279    #M2 * #N2 * * #eqQ #pr1 #pr2 >eqQ @appl; 
280     [@(subH (Prod P Q)) // |@subH //]
281   |#P #Hind #N1 #N2 #subH #pr1
282    cases (prApp_not_lambda … pr1 ?) // 
283    #M1 * #N1 * * #eqQ #pr2 #pr3 >eqQ @appl; 
284     [@(subH (D P) M1) // |@subH //]    
285   ]
286 qed.
287
288 theorem complete: ∀M,N. pr M N → pr N (full M).
289 @Telim #M (cases M) 
290   [#n #Hind #N #prH normalize >(prSort … prH) //
291   |#n #Hind #N #prH normalize >(prRel … prH) //
292   |#M #N #Hind #Q @complete_app 
293    #S #P #subS @Hind //
294   |#P #P1 #Hind #N #Hpr 
295    (cases (prLambda …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
296   |#P #P1 #Hind #N #Hpr 
297    (cases (prProd …Hpr)) #M1 * #N1 * * #eqN >eqN normalize /3/
298   |#N #Hind #P #prH normalize cases (prD … prH) 
299    #Q * #eqP >eqP #prN @d @Hind //
300   ]
301 qed.
302
303 theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
304 pr Q S ∧ pr P S.
305 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
306 qed.
307
308 *)