tpr_tpr.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 "lambda-delta/substitution/lift_weight.ma".
  13 include "lambda-delta/reduction/tpr_main.ma".
  14
  15 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
  16
  17 (* Confluence lemmas ********************************************************)
  18
  19 lemma tpr_conf_sort_sort: ∀k1. ∃∃T0. ⋆k1 ⇒ T0 & ⋆k1 ⇒ T0.
  20 /2/ qed.
  21
  22 lemma tpr_conf_lref_lref: ∀i1. ∃∃T0. #i1 ⇒ T0 & #i1 ⇒ T0.
  23 /2/ qed.
  24
  25 lemma tpr_conf_bind_bind:
  26    ∀I1,V11,V12,T11,T12,V22,T22. (
  27       ∀T1. #T1 < #V11 + #T11 + 1 →
  28       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  29       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
  30    ) →
  31    V11 ⇒ V12 → T11 ⇒ T12 →
  32    V11 ⇒ V22 → T11 ⇒ T22 →
  33    ∃∃T0. 𝕓{I1} V12. T12 ⇒ T0 & 𝕓{I1} V22. T22 ⇒ T0.
  34 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
  35 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
  36 elim (IH … HT1 … HT2) -HT1 HT2 IH /3 width=5/
  37 qed.
  38
  39 lemma tpr_conf_bind_zeta:
  40    ∀V11,V12,T11,T12,T22,T20. (
  41       ∀T1. #T1 < #V11 + #T11 +1 →
  42       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  43       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
  44    ) →
  45    V11 ⇒ V12 → T22 ⇒ T20 → T11 ⇒ T12 → ↑[O, 1] T22 ≡ T11 →
  46    ∃∃T0. 𝕓{Abbr} V12. T12 ⇒ T0 & T20 ⇒ T0.
  47 #V11 #V12 #T11 #T12 #T22 #T20 #IH #HV112 #HT202 #HT112 #HT
  48 elim (tpr_inv_lift … HT112 … HT) -HT112 #T #HT12 #HT22
  49 lapply (tw_lift … HT) -HT #HT
  50 elim (IH … HT202 … HT22) -HT202 HT22 IH /3/
  51 qed.
  52
  53 lemma tpr_conf_flat_flat:
  54    ∀I1,V11,V12,T11,T12,V22,T22. (
  55       ∀T1. #T1 < #V11 + #T11 + 1 →
  56       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  57       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
  58    ) →
  59    V11 ⇒ V12 → T11 ⇒ T12 →
  60    V11 ⇒ V22 → T11 ⇒ T22 →
  61    ∃∃T0. 𝕗{I1} V12. T12 ⇒ T0 & 𝕗{I1} V22. T22 ⇒ T0.
  62 #I1 #V11 #V12 #T11 #T12 #V22 #T22 #IH #HV1 #HT1 #HV2 #HT2
  63 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV1 #HV2
  64 elim (IH … HT1 … HT2) -HT1 HT2 /3 width=5/
  65 qed.
  66
  67 lemma tpr_conf_flat_beta:
  68    ∀V11,V12,T12,V22,W2,T21,T22. (
  69       ∀T1. #T1 < #V11 + (#W2 + #T21 + 1) + 1 →
  70       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  71       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
  72    ) →
  73    V11 ⇒ V12 → V11 ⇒ V22 →
  74    T21 ⇒ T22 → 𝕓{Abst} W2. T21 ⇒ T12 →
  75    ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} V22. T22 ⇒ T0.
  76 #V11 #V12 #T12 #V22 #W2 #T21 #T22 #IH #HV1 #HV2 #HT1 #HT2
  77 elim (tpr_inv_abst1 … HT2) -HT2 #W1 #T1 #HW21 #HT21 #H destruct -T12;
  78 elim (IH … HV1 … HV2) -HV1 HV2 // #V #HV12 #HV22
  79 elim (IH … HT21 … HT1) -HT21 HT1 IH /3 width=5/
  80 qed.
  81 (*
  82 lemma tpr_conf_flat_theta:
  83    ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
  84       ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
  85       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  86       ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
  87    ) →
  88    V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
  89    W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
  90    ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
  91 *)
  92
  93 (* Confluence ***************************************************************)
  94 (*
  95 lemma tpr_conf_aux:
  96    ∀T. (
  97       ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
  98       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
  99          ) →
 100    ∀U1,T1,T2. U1 ⇒ T1 → U1 ⇒ T2 → U1 = T →
 101    ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
 102 #T #IH  #U1 #T1 #T2 * -U1 T1
 103 [ #k1 #H1 #H2 destruct -T;
 104   lapply (tpr_inv_sort1 … H1) -H1
 105 (* case 1: sort, sort *)
 106   #H1 destruct -T2 //
 107 | #i1 #H1 #H2 destruct -T;
 108   lapply (tpr_inv_lref1 … H1) -H1
 109 (* case 2: lref, lref *)
 110   #H1 destruct -T2 //
 111 | #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 #H1 #H2 destruct -T;
 112   lapply (tpr_inv_bind1 … H1) -H1
 113   [
 114
 115 theorem tpr_conf: ∀T,T1,T2. T ⇒ T1 → T ⇒ T2 →
 116                  ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
 117 #T @(tw_wf_ind … T) -T /3 width=6/
 118 qed.
 119 *)
 120 lemma tpr_conf_aux:
 121    ∀T. (
 122       ∀T1. #T1 < #T → ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
 123       ∃∃T0. T3 ⇒ T0 & T4 ⇒ T0
 124          ) →
 125    ∀U1,T1,U2,T2. U1 ⇒ T1 → U2 ⇒ T2 →
 126    U1 = T → U2 = T →
 127    ∃∃T0. T1 ⇒ T0 & T2 ⇒ T0.
 128 #T #IH  #U1 #T1 #U2 #T2
 129 * -U1 T1
 130 [ #k1 * -U2 T2
 131 (* case 1: sort, sort *)
 132   [ #k2 #H1 #H2 destruct -T k2 //
 133 (* case 2: sort, lref (excluded) *)
 134   | #i2 #H1 #H2 destruct
 135 (* case 3: sort, bind (excluded) *)
 136   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 137 (* case 4: sort, flat (excluded) *)
 138   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 139 (* case 5: sort, beta (excluded) *)
 140   | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
 141 (* case 6: sort, delta (excluded) *)
 142   | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
 143 (* case 7: sort, theta (excluded) *)
 144   | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
 145 (* case 8: sort, zeta (excluded) *)
 146   | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
 147 (* case 9: sort, tau (excluded) *)
 148   | #V2 #T21 #T22 #_ #H1 #H2 destruct
 149   ]
 150 | #i1 * -U2 T2
 151 (* case 10: lref, sort (excluded) broken *)
 152   [ #k2 #H1 #H2 destruct
 153 (* case 11: lref, sort (excluded) *)
 154   | #i2 #H1 #H2 destruct -T i2 //
 155 (* case 12: lref, bind (excluded) *)
 156   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 157 (* case 13: lref, flat (excluded) *)
 158   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 159 (* case 14: lref, beta (excluded) *)
 160   | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
 161 (* case 15: lref, delta (excluded) *)
 162   | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
 163 (* case 16: lref, theta (excluded) *)
 164   | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
 165 (* case 17: lref, zeta (excluded) *)
 166   | #V2 #T21 #T22 #T20 #_ #_ #H1 #H2 destruct
 167 (* case 18: lref, tau (excluded) *)
 168   | #V2 #T21 #T22 #_ #H1 #H2 destruct
 169   ]
 170 | #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
 171 (* case 19: bind, sort (excluded) *)
 172   [ #k2 #H1 #H2 destruct
 173 (* case 20: bind, lref (excluded) *)
 174   | #i2 #H1 #H2 destruct
 175 (* case 21: bind, bind *)
 176   | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
 177     destruct -T I2 V21 T21 /3 width=7/
 178 (* case 22: bind, flat (excluded) *)
 179   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 180 (* case 23: bind, beta (excluded) *)
 181   | #V21 #V22 #W2 #T21 #T22 #_ #_ #H1 #H2 destruct
 182 (* case 24: bind, delta (excluded) *)
 183   | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
 184 (* case 25: bind, theta (excluded) *)
 185   | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #_ #_ #_ #_ #H1 #H2 destruct
 186 (* case 26: bind, zeta *)
 187   | #V2 #T21 #T22 #T20 #HT212 #HT220 #H1 #H2
 188     destruct -I1 V2 T21 T /3 width=8/
 189 (* case 27: bind, tau (excluded) *)
 190   | #V2 #T21 #T22 #_ #H1 #H2 destruct
 191   ]
 192 | #I1 #V11 #V12 #T11 #T12 #HV112 #HT112 * -U2 T2
 193 (* case 28: flat, sort (excluded) *)
 194   [ #k2 #H1 #H2 destruct
 195 (* case 29: flat, lref (excluded) *)
 196   | #i2 #H1 #H2 destruct
 197 (* case 30: flat, bind (excluded) *)
 198   | #I2 #V21 #V22 #T21 #T22 #_ #_ #H1 #H2 destruct
 199 (* case 31: flat, flat *)
 200   | #I2 #V21 #V22 #T21 #T22 #HV212 #HT212 #H1 #H2
 201     destruct -T I2 V21 T21 /3 width=7/
 202 (* case 32: flat, beta *)
 203   | #V21 #V22 #W2 #T21 #T22 #HV212 #HT212 #H1 #H2
 204     destruct -I1 V21 T11 T /3 width=8/ (**) (* slow *)
 205 (* case 33: flat, delta (excluded) *)
 206   | #V21 #V22 #T21 #T22 #T20 #_ #_ #_ #H1 #H2 destruct
 207 (* case 34: flat, theta *)
 208   | #V2 #V21 #V22 #W21 #W22 #T21 #T22 #H212 #HV222 #HW212 #HT212 #H1 #H2
 209     destruct -I1 V21 T11 T //
 210
 211 lemma tpr_conf_flat_theta:
 212    ∀V11,V12,T12,V2,V22,W21,W22,T21,T22. (
 213       ∀T1. #T1 < #V11 + (#W21 + #T21 + 1) + 1 →
 214       ∀T3,T4. T1 ⇒ T3 → T1 ⇒ T4 →
 215       ∃∃T0. T3 ⇒ T0 & T4 ⇒T0
 216    ) →
 217    V11 ⇒ V12 → V11 ⇒ V22 → ↑[O,1] V22 ≡ V2 →
 218    W21 ⇒ W22 → T21 ⇒ T22 →  𝕓{Abbr} W21. T21 ⇒ T12 →
 219    ∃∃T0. 𝕗{Appl} V12. T12 ⇒ T0 & 𝕓{Abbr} W22. 𝕗{Appl} V2. T22 ⇒T0.
 220