]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/lambda/terms/parallel_reduction.ma
- cprs and cnx on the way
[helm.git] / matita / matita / lib / lambda / terms / parallel_reduction.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "lambda/terms/size.ma".
16 include "lambda/terms/sequential_reduction.ma".
17
18 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
19
20 (* Note: the application "(A B)" is represented by "@B.A"
21          as for sequential reduction
22 *)
23 inductive pred: relation term ≝
24 | pred_vref: ∀i. pred (#i) (#i)
25 | pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2) 
26 | pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2)
27 | pred_beta: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.𝛌.A1) ([↙B2]A2)
28 .
29
30 interpretation "parallel reduction"
31     'ParRed M N = (pred M N).
32
33 lemma pred_refl: reflexive … pred.
34 #M elim M -M // /2 width=1/
35 qed.
36
37 lemma pred_inv_vref: ∀M,N. M ⤇ N → ∀i. #i = M → #i = N.
38 #M #N * -M -N //
39 [ #A1 #A2 #_ #i #H destruct
40 | #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
41 | #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
42 ]
43 qed-.
44
45 lemma pred_inv_abst: ∀M,N. M ⤇ N → ∀A. 𝛌.A = M →
46                      ∃∃C. A ⤇ C & 𝛌.C = N.
47 #M #N * -M -N
48 [ #i #A0 #H destruct
49 | #A1 #A2 #HA12 #A0 #H destruct /2 width=3/
50 | #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
51 | #B1 #B2 #A1 #A2 #_ #_ #A0 #H destruct
52 ]
53 qed-.
54
55 lemma pred_inv_appl: ∀M,N. M ⤇ N → ∀B,A. @B.A = M →
56                      (∃∃D,C. B ⤇ D & A ⤇ C & @D.C = N) ∨
57                      ∃∃A0,D,C0. B ⤇ D & A0 ⤇ C0 & 𝛌.A0 = A & [↙D]C0 = N.
58 #M #N * -M -N
59 [ #i #B0 #A0 #H destruct
60 | #A1 #A2 #_ #B0 #A0 #H destruct
61 | #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=5/
62 | #B1 #B2 #A1 #A2 #HB12 #HA12 #B0 #A0 #H destruct /3 width=7/
63 ]
64 qed-.
65
66 lemma pred_lift: liftable pred.
67 #h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
68 #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d <dsubst_lift_le // /2 width=1/
69 qed.
70
71 lemma pred_inv_lift: deliftable_sn pred.
72 #h #N1 #N2 #H elim H -N1 -N2 /2 width=3/
73 [ #C1 #C2 #_ #IHC12 #d #M1 #H
74   elim (lift_inv_abst … H) -H #A1 #HAC1 #H
75   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
76   @(ex2_intro … (𝛌.A2)) // /2 width=1/
77 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
78   elim (lift_inv_appl … H) -H #B1 #A1 #HBD1 #HAC1 #H
79   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
80   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
81   @(ex2_intro … (@B2.A2)) // /2 width=1/
82 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
83   elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
84   elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
85   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
86   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
87   @(ex2_intro … ([↙B2]A2)) /2 width=1/
88 ]
89 qed-.
90
91 lemma pred_dsubst: dsubstable pred.
92 #N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
93 [ #i #d elim (lt_or_eq_or_gt i d) #Hid
94   [ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
95   | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/
96   | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
97   ]
98 | normalize /2 width=1/
99 | normalize /2 width=1/
100 | normalize #B1 #B2 #A1 #A2 #_ #_ #IHB12 #IHC12 #d
101   >dsubst_dsubst_ge // /2 width=1/
102 ]
103 qed.
104
105 lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
106 #i #M1 #H1 #M2 #H2
107 <(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
108 <(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
109 /2 width=3/
110 qed-.
111
112 lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
113 #A #IH #M1 #H1 #M2 #H2
114 elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
115 elim (pred_inv_abst … H2 …) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
116 elim (IH … HA1 … HA2) -A /3 width=3/
117 qed-.
118
119 lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
120                             (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
121                             B ⤇ B1 → B ⤇ B2 → 𝛌.C ⤇ M1 → C ⤇ C2 →
122                             ∃∃M. @B1.M1 ⤇ M & [↙B2]C2 ⤇ M.
123 #B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
124 elim (pred_inv_abst … H1 …) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
125 elim (IH B … HB1 … HB2) -HB1 -HB2 //
126 elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
127 qed-.
128
129 theorem pred_conf: confluent … pred.
130 #M @(f_ind … size … M) -M #n #IH * normalize
131 [ /2 width=3 by pred_conf1_vref/
132 | /3 width=4 by pred_conf1_abst/
133 | #B #A #H #M1 #H1 #M2 #H2 destruct
134   elim (pred_inv_appl … H1 …) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
135   elim (pred_inv_appl … H2 …) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *) 
136   [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
137     elim (IH A … HA1 … HA2) -HA1 -HA2 //
138     elim (IH B … HB1 … HB2) // -A -B /3 width=5/
139   | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct
140     @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *)
141   | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
142     @ex2_commute @(pred_conf1_appl_beta … IH) //
143   | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
144     elim (IH B … HB1 … HB2) -HB1 -HB2 //
145     elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
146   ]
147 ]
148 qed-.
149
150 lemma sred_pred: ∀M,N. M ↦ N → M ⤇ N.
151 #M #N #H elim H -M -N /2 width=1/
152 qed.