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