matita/matita/contribs/lambda-delta/Basic-2/reduction/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 "Basic-2/substitution/tps.ma".
  13
  14 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
  15
  16 inductive tpr: term → term → Prop ≝
  17 | tpr_sort : ∀k. tpr (⋆k) (⋆k)
  18 | tpr_lref : ∀i. tpr (#i) (#i)
  19 | tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
  20              tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
  21 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
  22              tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
  23 | tpr_beta : ∀V1,V2,W,T1,T2.
  24              tpr V1 V2 → tpr T1 T2 →
  25              tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
  26 | tpr_delta: ∀V1,V2,T1,T2,T.
  27              tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T →
  28              tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
  29 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
  30              tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
  31              tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
  32 | tpr_zeta : ∀V,T,T1,T2. ↑[0,1] T1 ≡ T → tpr T1 T2 →
  33              tpr (𝕚{Abbr} V. T) T2
  34 | tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (𝕚{Cast} V. T1) T2
  35 .
  36
  37 interpretation
  38    "context-free parallel reduction (term)"
  39    'PRed T1 T2 = (tpr T1 T2).
  40
  41 (* Basic properties *********************************************************)
  42
  43 lemma tpr_refl: ∀T. T ⇒ T.
  44 #T elim T -T //
  45 #I elim I -I /2/
  46 qed.
  47
  48 (* Basic inversion lemmas ***************************************************)
  49
  50 lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
  51 #U1 #U2 * -U1 U2
  52 [ #k0 #k #H destruct -k0 //
  53 | #i #k #H destruct
  54 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
  55 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
  56 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
  57 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
  58 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
  59 | #V #T #T1 #T2 #_ #_ #k #H destruct
  60 | #V #T1 #T2 #_ #k #H destruct
  61 ]
  62 qed.
  63
  64 lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k.
  65 /2/ qed.
  66
  67 lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
  68 #U1 #U2 * -U1 U2
  69 [ #k #i #H destruct
  70 | #j #i #H destruct -j //
  71 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
  72 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
  73 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
  74 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
  75 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
  76 | #V #T #T1 #T2 #_ #_ #i #H destruct
  77 | #V #T1 #T2 #_ #i #H destruct
  78 ]
  79 qed.
  80
  81 lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
  82 /2/ qed.
  83
  84 lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 →
  85                          ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
  86                           | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
  87                                        ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
  88                                        U2 = 𝕚{Abbr} V2. T
  89                           | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
  90 #U1 #U2 * -U1 U2
  91 [ #k #V #T #H destruct
  92 | #i #V #T #H destruct
  93 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
  94 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
  95 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
  96 | #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
  97 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
  98 | #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
  99 | #V #T1 #T2 #_ #V0 #T0 #H destruct
 100 ]
 101 qed.
 102
 103 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
 104                      ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
 105                       | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
 106                                    ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
 107                                    U2 = 𝕚{Abbr} V2. T
 108                       | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
 109 /2/ qed.
 110
 111 lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
 112                          ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
 113 #U1 #U2 * -U1 U2
 114 [ #k #V #T #H destruct
 115 | #i #V #T #H destruct
 116 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
 117 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 118 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
 119 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
 120 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
 121 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
 122 | #V #T1 #T2 #_ #V0 #T0 #H destruct
 123 ]
 124 qed.
 125
 126 lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
 127                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
 128 /2/ qed.
 129
 130 lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
 131                      ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2
 132                       | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
 133                                    ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
 134                                    U2 = 𝕚{Abbr} V2. T & I = Abbr
 135                       | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
 136 #V1 #T1 #U2 * #H
 137 [ elim (tpr_inv_abbr1 … H) -H * /3 width=7/
 138 | /3/
 139 ]
 140 qed.
 141
 142 lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
 143                          ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
 144                                                 U2 = 𝕚{Appl} V2. T2
 145                           | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
 146                                                 U0 = 𝕚{Abst} W. T1 &
 147                                                 U2 = 𝕓{Abbr} V2. T2
 148                           | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
 149                                                 ↑[0,1] V2 ≡ V &
 150                                                 U0 = 𝕚{Abbr} W1. T1 &
 151                                                 U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
 152 #U1 #U2 * -U1 U2
 153 [ #k #V #T #H destruct
 154 | #i #V #T #H destruct
 155 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 156 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
 157 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
 158 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
 159 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
 160   destruct -V1 T0 /3 width=12/
 161 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
 162 | #V #T1 #T2 #_ #V0 #T0 #H destruct
 163 ]
 164 qed.
 165
 166 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕚{Appl} V1. U0 ⇒ U2 →
 167                      ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
 168                                             U2 = 𝕚{Appl} V2. T2
 169                       | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
 170                                             U0 = 𝕚{Abst} W. T1 &
 171                                             U2 = 𝕓{Abbr} V2. T2
 172                       | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
 173                                             ↑[0,1] V2 ≡ V &
 174                                             U0 = 𝕚{Abbr} W1. T1 &
 175                                             U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
 176 /2/ qed.
 177
 178 lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 →
 179                            (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
 180                          ∨ T1 ⇒ U2.
 181 #U1 #U2 * -U1 U2
 182 [ #k #V #T #H destruct
 183 | #i #V #T #H destruct
 184 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 185 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
 186 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
 187 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
 188 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
 189 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
 190 | #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
 191 ]
 192 qed.
 193
 194 lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕚{Cast} V1. T1 ⇒ U2 →
 195                        (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
 196                      ∨ T1 ⇒ U2.
 197 /2/ qed.
 198
 199 lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
 200                      ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
 201                                             U2 = 𝕗{I} V2. T2
 202                       | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
 203                                             U0 = 𝕚{Abst} W. T1 &
 204                                             U2 = 𝕓{Abbr} V2. T2 & I = Appl
 205                       | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
 206                                             ↑[0,1] V2 ≡ V &
 207                                             U0 = 𝕚{Abbr} W1. T1 &
 208                                             U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2 &
 209                                             I = Appl
 210                       |                     (U0 ⇒ U2 ∧ I = Cast).
 211 #V1 #U0 #U2 * #H
 212 [ elim (tpr_inv_appl1 … H) -H * /3 width=12/
 213 | elim (tpr_inv_cast1 … H) -H [1: *] /3 width=5/
 214 ]
 215 qed.
 216
 217 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
 218                          ∨∨           T1 = #i
 219                           | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
 220                                       T1 = 𝕚{Abbr} V. T
 221                           | ∃∃V,T.    T ⇒ #i & T1 = 𝕚{Cast} V. T.
 222 #T1 #T2 * -T1 T2
 223 [ #k #i #H destruct
 224 | #j #i /2/
 225 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 226 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 227 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 228 | #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 229 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 230 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
 231 | #V #T1 #T2 #HT12 #i #H destruct /3/
 232 ]
 233 qed.
 234
 235 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
 236                      ∨∨           T1 = #i
 237                       | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
 238                                   T1 = 𝕓{Abbr} V. T
 239                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕗{Cast} V. T.
 240 /2/ qed.