(* *)
(**************************************************************************)
-include "size.ma".
-include "labelled_sequential_reduction.ma".
+include "length.ma".
+include "labeled_sequential_reduction.ma".
(* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
| pred_vref: ∀i. pred (#i) (#i)
| pred_abst: ∀A1,A2. pred A1 A2 → pred (𝛌.A1) (𝛌.A2)
| pred_appl: ∀B1,B2,A1,A2. pred B1 B2 → pred A1 A2 → pred (@B1.A1) (@B2.A2)
-| pred_beta: â\88\80B1,B2,A1,A2. pred B1 B2 â\86\92 pred A1 A2 â\86\92 pred (@B1.ð\9d\9b\8c.A1) ([â¬\90B2]A2)
+| pred_beta: â\88\80B1,B2,A1,A2. pred B1 B2 â\86\92 pred A1 A2 â\86\92 pred (@B1.ð\9d\9b\8c.A1) ([â\86\99B2]A2)
.
interpretation "parallel reduction"
'ParRed M N = (pred M N).
-notation "hvbox( M break ⥤ break term 46 N )"
+notation "hvbox( M ⤇ break term 46 N )"
non associative with precedence 45
for @{ 'ParRed $M $N }.
#M elim M -M // /2 width=1/
qed.
-lemma pred_inv_vref: â\88\80M,N. M ⥤ N → ∀i. #i = M → #i = N.
+lemma pred_inv_vref: â\88\80M,N. M â¤\87 N → ∀i. #i = M → #i = N.
#M #N * -M -N //
[ #A1 #A2 #_ #i #H destruct
| #B1 #B2 #A1 #A2 #_ #_ #i #H destruct
]
qed-.
-lemma pred_inv_abst: â\88\80M,N. M ⥤ N → ∀A. 𝛌.A = M →
- â\88\83â\88\83C. A ⥤ C & 𝛌.C = N.
+lemma pred_inv_abst: â\88\80M,N. M â¤\87 N → ∀A. 𝛌.A = M →
+ â\88\83â\88\83C. A â¤\87 C & 𝛌.C = N.
#M #N * -M -N
[ #i #A0 #H destruct
| #A1 #A2 #HA12 #A0 #H destruct /2 width=3/
]
qed-.
-lemma pred_inv_appl: â\88\80M,N. M ⥤ N → ∀B,A. @B.A = M →
- (â\88\83â\88\83D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨
- â\88\83â\88\83A0,D,C0. B ⥤ D & A0 ⥤ C0 & ð\9d\9b\8c.A0 = A & [â¬\90D]C0 = N.
+lemma pred_inv_appl: â\88\80M,N. M â¤\87 N → ∀B,A. @B.A = M →
+ (â\88\83â\88\83D,C. B â¤\87 D & A â¤\87 C & @D.C = N) ∨
+ â\88\83â\88\83A0,D,C0. B â¤\87 D & A0 â¤\87 C0 & ð\9d\9b\8c.A0 = A & [â\86\99D]C0 = N.
#M #N * -M -N
[ #i #B0 #A0 #H destruct
| #A1 #A2 #_ #B0 #A0 #H destruct
elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
- @(ex2_intro â\80¦ ([â¬\90B2]A2)) /2 width=1/
+ @(ex2_intro â\80¦ ([â\86\99B2]A2)) /2 width=1/
]
qed-.
lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
(∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
- B ⥤ B1 â\86\92 B ⥤ B2 â\86\92 ð\9d\9b\8c.C ⥤ M1 â\86\92 C ⥤ C2 →
- â\88\83â\88\83M. @B1.M1 ⥤ M & [â¬\90B2]C2 ⥤ M.
+ B â¤\87 B1 â\86\92 B â¤\87 B2 â\86\92 ð\9d\9b\8c.C â¤\87 M1 â\86\92 C â¤\87 C2 →
+ â\88\83â\88\83M. @B1.M1 â¤\87 M & [â\86\99B2]C2 â¤\87 M.
#B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
elim (IH B … HB1 … HB2) -HB1 -HB2 //
qed-.
theorem pred_conf: confluent … pred.
-#M @(f_ind … size … M) -M #n #IH * normalize
+#M @(f_ind … length … M) -M #n #IH * normalize
[ /2 width=3 by pred_conf1_vref/
| /3 width=4 by pred_conf1_abst/
| #B #A #H #M1 #H1 #M2 #H2 destruct
]
qed-.
-lemma lsred_pred: â\88\80p,M,N. M â\87\80[p] N â\86\92 M ⥤ N.
+lemma lsred_pred: â\88\80p,M,N. M â\86¦[p] N â\86\92 M â¤\87 N.
#p #M #N #H elim H -p -M -N /2 width=1/
qed.