matita/matita/contribs/lambda/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 "size.ma".
  16 include "labelled_sequential_reduction.ma".
  17
  18 (* PARALLEL REDUCTION (SINGLE STEP) *****************************************)
  19
  20 (* Note: the application "(A B)" is represented by "@B.A"
  21          as for labelled sequential reduction
  22 *)
  23 inductive pred: relation term ≝
  24 | pred_vref: ∀i. pred (#i) (#i)
  25 | pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C)
  26 | pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C)
  27 | pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C)
  28 .
  29
  30 interpretation "parallel reduction"
  31     'ParRed M N = (pred M N).
  32
  33 notation "hvbox( M break ⥤ break term 46 N )"
  34    non associative with precedence 45
  35    for @{ 'ParRed $M $N }.
  36
  37 lemma pred_refl: reflexive … pred.
  38 #M elim M -M // /2 width=1/
  39 qed.
  40
  41 lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N.
  42 #M #N * -M -N //
  43 [ #A #C #_ #i #H destruct
  44 | #B #D #A #C #_ #_ #i #H destruct
  45 | #B #D #A #C #_ #_ #i #H destruct
  46 ]
  47 qed-.
  48
  49 lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M →
  50                      ∃∃C. A ⥤ C & 𝛌.C = N.
  51 #M #N * -M -N
  52 [ #i #A0 #H destruct
  53 | #A #C #HAC #A0 #H destruct /2 width=3/
  54 | #B #D #A #C #_ #_ #A0 #H destruct
  55 | #B #D #A #C #_ #_ #A0 #H destruct
  56 ]
  57 qed-.
  58
  59 lemma pred_inv_appl: ∀M,N. M ⥤ N → ∀B,A. @B.A = M →
  60                      (∃∃D,C. B ⥤ D & A ⥤ C & @D.C = N) ∨
  61                      ∃∃A0,D,C0. B ⥤ D & A0 ⥤ C0 & 𝛌.A0 = A & [⬐D]C0 = N.
  62 #M #N * -M -N
  63 [ #i #B0 #A0 #H destruct
  64 | #A #C #_ #B0 #A0 #H destruct
  65 | #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=5/
  66 | #B #D #A #C #HBD #HAC #B0 #A0 #H destruct /3 width=7/
  67 ]
  68 qed-.
  69
  70 lemma pred_lift: liftable pred.
  71 #h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/
  72 #D #D #A #C #_ #_ #IHBD #IHAC #d <dsubst_lift_le // /2 width=1/
  73 qed.
  74
  75 lemma pred_inv_lift: deliftable pred.
  76 #h #N1 #N2 #H elim H -N1 -N2 /2 width=3/
  77 [ #C1 #C2 #_ #IHC12 #d #M1 #H
  78   elim (lift_inv_abst … H) -H #A1 #HAC1 #H
  79   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
  80   @(ex2_1_intro … (𝛌.A2)) // /2 width=1/
  81 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
  82   elim (lift_inv_appl … H) -H #B1 #A1 #HBD1 #HAC1 #H
  83   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
  84   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
  85   @(ex2_1_intro … (@B2.A2)) // /2 width=1/
  86 | #D1 #D2 #C1 #C2 #_ #_ #IHD12 #IHC12 #d #M1 #H
  87   elim (lift_inv_appl … H) -H #B1 #M #HBD1 #HM #H1
  88   elim (lift_inv_abst … HM) -HM #A1 #HAC1 #H
  89   elim (IHD12 … HBD1) -D1 #B2 #HB12 #HBD2
  90   elim (IHC12 … HAC1) -C1 #A2 #HA12 #HAC2 destruct
  91   @(ex2_1_intro … ([⬐B2]A2)) /2 width=1/
  92 ]
  93 qed-.
  94
  95 lemma pred_dsubst: dsubstable pred.
  96 #N1 #N2 #HN12 #M1 #M2 #H elim H -M1 -M2
  97 [ #i #d elim (lt_or_eq_or_gt i d) #Hid
  98   [ >(dsubst_vref_lt … Hid) >(dsubst_vref_lt … Hid) //
  99   | destruct >dsubst_vref_eq >dsubst_vref_eq /2 width=1/
 100   | >(dsubst_vref_gt … Hid) >(dsubst_vref_gt … Hid) //
 101   ]
 102 | normalize /2 width=1/
 103 | normalize /2 width=1/
 104 | normalize #B #D #A #C #_ #_ #IHBD #IHAC #d
 105   >dsubst_dsubst_ge // /2 width=1/
 106 ]
 107 qed.
 108
 109 lemma pred_conf1_vref: ∀i. confluent1 … pred (#i).
 110 #i #M1 #H1 #M2 #H2
 111 <(pred_inv_vref … H1) -H1 [3: // |2: skip ] (**) (* simplify line *)
 112 <(pred_inv_vref … H2) -H2 [3: // |2: skip ] (**) (* simplify line *)
 113 /2 width=3/
 114 qed-.
 115
 116 lemma pred_conf1_abst: ∀A. confluent1 … pred A → confluent1 … pred (𝛌.A).
 117 #A #IH #M1 #H1 #M2 #H2
 118 elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #A1 #HA1 #H destruct (**) (* simplify line *)
 119 elim (pred_inv_abst … H2 ??) -H2 [3: // |2: skip ] #A2 #HA2 #H destruct (**) (* simplify line *)
 120 elim (IH … HA1 … HA2) -A /3 width=3/
 121 qed-.
 122
 123 lemma pred_conf1_appl_beta: ∀B,B1,B2,C,C2,M1.
 124                             (∀M0. |M0| < |B|+|𝛌.C|+1 → confluent1 ? pred M0) → (**) (* ? needed in place of … *)
 125                             B ⥤ B1 → B ⥤ B2 → 𝛌.C ⥤ M1 → C ⥤ C2 →
 126                             ∃∃M. @B1.M1 ⥤ M & [⬐B2]C2 ⥤ M.
 127 #B #B1 #B2 #C #C2 #M1 #IH #HB1 #HB2 #H1 #HC2
 128 elim (pred_inv_abst … H1 ??) -H1 [3: // |2: skip ] #C1 #HC1 #H destruct (**) (* simplify line *)
 129 elim (IH B … HB1 … HB2) -HB1 -HB2 //
 130 elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
 131 qed-.
 132
 133 theorem pred_conf: confluent … pred.
 134 #M @(f_ind … size … M) -M #n #IH * normalize
 135 [ /2 width=3 by pred_conf1_vref/
 136 | /3 width=4 by pred_conf1_abst/
 137 | #B #A #H #M1 #H1 #M2 #H2 destruct
 138   elim (pred_inv_appl … H1 ???) -H1 [5: // |2,3: skip ] * (**) (* simplify line *)
 139   elim (pred_inv_appl … H2 ???) -H2 [5,10: // |2,3,7,8: skip ] * (**) (* simplify line *)
 140   [ #B2 #A2 #HB2 #HA2 #H2 #B1 #A1 #HB1 #HA1 #H1 destruct
 141     elim (IH A … HA1 … HA2) -HA1 -HA2 //
 142     elim (IH B … HB1 … HB2) // -A -B /3 width=5/
 143   | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #B1 #N #HB1 #H #HM1 destruct
 144     @(pred_conf1_appl_beta … IH) // (**) (* /2 width=7 by pred_conf1_appl_beta/ does not work *)
 145   | #B2 #N #B2 #H #HM2 #C #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
 146     @ex2_1_commute @(pred_conf1_appl_beta … IH) //
 147   | #C #B2 #C2 #HB2 #HC2 #H2 #HM2 #C0 #B1 #C1 #HB1 #HC1 #H1 #HM1 destruct
 148     elim (IH B … HB1 … HB2) -HB1 -HB2 //
 149     elim (IH C … HC1 … HC2) normalize // -B -C /3 width=5/
 150   ]
 151 ]
 152 qed-.
 153
 154 lemma lsred_pred: ∀p,M,N. M ⇀[p] N → M ⥤ N.
 155 #p #M #N #H elim H -p -M -N /2 width=1/
 156 qed.