matita/matita/contribs/lambdadelta/basic_2/etc_2A1/cpr/tpr.etc

   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 notation "hvbox( T1 ➡ break term 46 T2 )"
  16    non associative with precedence 45
  17    for @{ 'PRed $T1 $T2 }.
  18
  19 include "basic_2/substitution/tps.ma".
  20
  21 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
  22
  23 (* Basic_1: includes: pr0_delta1 *)
  24 inductive tpr: relation term ≝
  25 | tpr_atom : ∀I. tpr (⓪{I}) (⓪{I})
  26 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
  27              tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
  28 | tpr_beta : ∀a,V1,V2,W,T1,T2.
  29              tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
  30 | tpr_delta: ∀a,I,V1,V2,T1,T,T2.
  31              tpr V1 V2 → tpr T1 T → ⋆. ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 →
  32              tpr (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
  33 | tpr_theta: ∀a,V,V1,V2,W1,W2,T1,T2.
  34              tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
  35              tpr (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV. T2)
  36 | tpr_zeta : ∀V,T1,T,T2. tpr T1 T → ⇧[0, 1] T2 ≡ T → tpr (+ⓓV. T1) T2
  37 | tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓝV. T1) T2
  38 .
  39
  40 interpretation
  41    "context-free parallel reduction (term)"
  42    'PRed T1 T2 = (tpr T1 T2).
  43
  44 (* Basic properties *********************************************************)
  45
  46 lemma tpr_bind: ∀a,I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 → ⓑ{a,I} V1. T1 ➡ ⓑ{a,I} V2. T2.
  47 /2 width=3/ qed.
  48
  49 (* Basic_1: was by definition: pr0_refl *)
  50 lemma tpr_refl: reflexive … tpr.
  51 #T elim T -T //
  52 #I elim I -I /2 width=1/
  53 qed.
  54
  55 (* Basic inversion lemmas ***************************************************)
  56
  57 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
  58 #U1 #U2 * -U1 -U2
  59 [ //
  60 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
  61 | #a #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
  62 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #k #H destruct
  63 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
  64 | #V #T1 #T #T2 #_ #_ #k #H destruct
  65 | #V #T1 #T2 #_ #k #H destruct
  66 ]
  67 qed.
  68
  69 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
  70 lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
  71 /2 width=3/ qed-.
  72
  73 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀a,I,V1,T1. U1 = ⓑ{a,I} V1. T1 →
  74                         (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
  75                                     ⋆.  ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
  76                                     U2 = ⓑ{a,I} V2. T2
  77                         ) ∨
  78                         ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true & I = Abbr.
  79 #U1 #U2 * -U1 -U2
  80 [ #J #a #I #V #T #H destruct
  81 | #I1 #V1 #V2 #T1 #T2 #_ #_ #a #I #V #T #H destruct
  82 | #b #V1 #V2 #W #T1 #T2 #_ #_ #a #I #V #T #H destruct
  83 | #b #I1 #V1 #V2 #T1 #T #T2 #HV12 #HT1 #HT2 #a #I0 #V0 #T0 #H destruct /3 width=7/
  84 | #b #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #a #I0 #V0 #T0 #H destruct
  85 | #V #T1 #T #T2 #HT1 #HT2 #a #I0 #V0 #T0 #H destruct /3 width=3/
  86 | #V #T1 #T2 #_ #a #I0 #V0 #T0 #H destruct
  87 ]
  88 qed.
  89
  90 lemma tpr_inv_bind1: ∀V1,T1,U2,a,I. ⓑ{a,I} V1. T1 ➡ U2 →
  91                      (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
  92                                  ⋆.  ⓑ{I} V2 ⊢ T ▶ [0, 1] T2 &
  93                                  U2 = ⓑ{a,I} V2. T2
  94                      ) ∨
  95                      ∃∃T. T1 ➡ T & ⇧[0,1] U2 ≡ T & a = true & I = Abbr.
  96 /2 width=3/ qed-.
  97
  98 (* Basic_1: was pr0_gen_abbr *)
  99 lemma tpr_inv_abbr1: ∀a,V1,T1,U2. ⓓ{a}V1. T1 ➡ U2 →
 100                      (∃∃V2,T,T2. V1 ➡ V2 & T1 ➡ T &
 101                                  ⋆.  ⓓV2 ⊢ T ▶ [0, 1] T2 &
 102                                  U2 = ⓓ{a}V2. T2
 103                       ) ∨
 104                       ∃∃T. T1 ➡ T & ⇧[0, 1] U2 ≡ T & a = true.
 105 #a #V1 #T1 #U2 #H
 106 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 107 qed-.
 108
 109 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
 110                         ∨∨ ∃∃V2,T2.              V1 ➡ V2 & U0 ➡ T2 &
 111                                                  U2 = ⓕ{I} V2. T2
 112                          | ∃∃a,V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 113                                                  U0 = ⓛ{a}W. T1 &
 114                                                  U2 = ⓓ{a}V2. T2 & I = Appl
 115                          | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 116                                                  ⇧[0,1] V2 ≡ V &
 117                                                  U0 = ⓓ{a}W1. T1 &
 118                                                  U2 = ⓓ{a}W2. ⓐV. T2 &
 119                                                  I = Appl
 120                          |                       (U0 ➡ U2 ∧ I = Cast).
 121 #U1 #U2 * -U1 -U2
 122 [ #I #J #V #T #H destruct
 123 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
 124 | #a #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=9/
 125 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #J #V0 #T0 #H destruct
 126 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=13/
 127 | #V #T1 #T #T2 #_ #_ #J #V0 #T0 #H destruct
 128 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
 129 ]
 130 qed.
 131
 132 lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
 133                      ∨∨ ∃∃V2,T2.              V1 ➡ V2 & U0 ➡ T2 &
 134                                               U2 = ⓕ{I} V2. T2
 135                       | ∃∃a,V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 136                                               U0 = ⓛ{a}W. T1 &
 137                                               U2 = ⓓ{a}V2. T2 & I = Appl
 138                       | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 139                                               ⇧[0,1] V2 ≡ V &
 140                                               U0 = ⓓ{a}W1. T1 &
 141                                               U2 = ⓓ{a}W2. ⓐV. T2 &
 142                                               I = Appl
 143                       |                       (U0 ➡ U2 ∧ I = Cast).
 144 /2 width=3/ qed-.
 145
 146 (* Basic_1: was pr0_gen_appl *)
 147 lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
 148                      ∨∨ ∃∃V2,T2.              V1 ➡ V2 & U0 ➡ T2 &
 149                                               U2 = ⓐV2. T2
 150                       | ∃∃a,V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 151                                               U0 = ⓛ{a}W. T1 &
 152                                               U2 = ⓓ{a}V2. T2
 153                       | ∃∃a,V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 154                                               ⇧[0,1] V2 ≡ V &
 155                                               U0 = ⓓ{a}W1. T1 &
 156                                               U2 = ⓓ{a}W2. ⓐV. T2.
 157 #V1 #U0 #U2 #H
 158 elim (tpr_inv_flat1 … H) -H *
 159 /3 width=5/ /3 width=9/ /3 width=13/
 160 #_ #H destruct
 161 qed-.
 162
 163 (* Note: the main property of simple terms *)
 164 lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒⦃T1⦄ →
 165                             ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
 166                                      U = ⓐV2. T2.
 167 #V1 #T1 #U #H #HT1
 168 elim (tpr_inv_appl1 … H) -H *
 169 [ /2 width=5/
 170 | #a #V2 #W #W1 #W2 #_ #_ #H #_ destruct
 171   elim (simple_inv_bind … HT1)
 172 | #a #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
 173   elim (simple_inv_bind … HT1)
 174 ]
 175 qed-.
 176
 177 (* Basic_1: was: pr0_gen_cast *)
 178 lemma tpr_inv_cast1: ∀V1,T1,U2. ⓝV1. T1 ➡ U2 →
 179                        (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓝV2. T2)
 180                      ∨ T1 ➡ U2.
 181 #V1 #T1 #U2 #H
 182 elim (tpr_inv_flat1 … H) -H * /3 width=5/ #a #V2 #W #W1 #W2
 183 [ #_ #_ #_ #_ #H destruct
 184 | #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
 185 ]
 186 qed-.
 187
 188 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
 189                         ∨∨        T1 = #i
 190                          | ∃∃V,T. T ➡ #(i+1) & T1 = +ⓓV. T
 191                          | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 192 #T1 #T2 * -T1 -T2
 193 [ #I #i #H destruct /2 width=1/
 194 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 195 | #a #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 196 | #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #i #H destruct
 197 | #a #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 198 | #V #T1 #T #T2 #HT1 #HT2 #i #H destruct
 199   lapply (lift_inv_lref1_ge … HT2 ?) -HT2 // #H destruct /3 width=4/
 200 | #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
 201 ]
 202 qed.
 203
 204 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
 205                      ∨∨        T1 = #i
 206                       | ∃∃V,T. T ➡ #(i+1) & T1 = +ⓓV. T
 207                       | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 208 /2 width=3/ qed-.
 209
 210 (* Basic forward lemmas *****************************************************)
 211
 212 lemma tpr_fwd_bind1_minus: ∀I,V1,T1,T. -ⓑ{I}V1.T1 ➡ T → ∀b.
 213                            ∃∃V2,T2. ⓑ{b,I}V1.T1 ➡ ⓑ{b,I}V2.T2 &
 214                                     T = -ⓑ{I}V2.T2.
 215 #I #V1 #T1 #T #H #b elim (tpr_inv_bind1 … H) -H *
 216 [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct /3 width=4/
 217 | #T2 #_ #_ #H destruct
 218 ]
 219 qed-.
 220
 221 lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
 222                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
 223 #L1 @(lenv_ind_dx … L1) -L1 normalize
 224 [ #T1 #T #HT1
 225   @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
 226 | #I #L1 #V1 #IH #T1 #X
 227   >shift_append_assoc normalize #H
 228   elim (tpr_inv_bind1 … H) -H *
 229   [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct
 230     elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct
 231     elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct
 232     >append_length >HL1 >HL2 -L1 -L
 233     @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
 234   | #T #_ #_ #H destruct
 235   ]
 236 ]
 237 qed-.
 238
 239 (* Basic_1: removed theorems 3:
 240             pr0_subst0_back pr0_subst0_fwd pr0_subst0
 241 *)
 242 (* Basic_1: removed local theorems: 1: pr0_delta_tau *)