matita/matita/contribs/lambda_delta/basic_2/reducibility/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 (* Basic_1: includes: pr0_delta1 *)
  20 inductive tpr: relation term ≝
  21 | tpr_atom : ∀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 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
  26 | tpr_delta: ∀I,V1,V2,T1,T2,T.
  27              tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
  28              tpr (ⓑ{I} V1. T1) (ⓑ{I} 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 (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
  32 | tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
  33 | tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓣV. T1) T2
  34 .
  35
  36 interpretation
  37    "context-free parallel reduction (term)"
  38    'PRed T1 T2 = (tpr T1 T2).
  39
  40 (* Basic properties *********************************************************)
  41
  42 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
  43                                 ⓑ{I} V1. T1 ➡  ⓑ{I} V2. T2.
  44 /2 width=3/ qed.
  45
  46 (* Basic_1: was by definition: pr0_refl *)
  47 lemma tpr_refl: ∀T. T ➡ T.
  48 #T elim T -T //
  49 #I elim I -I /2 width=1/
  50 qed.
  51
  52 (* Basic inversion lemmas ***************************************************)
  53
  54 fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
  55 #U1 #U2 * -U1 -U2
  56 [ //
  57 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
  58 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
  59 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
  60 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
  61 | #V #T #T1 #T2 #_ #_ #k #H destruct
  62 | #V #T1 #T2 #_ #k #H destruct
  63 ]
  64 qed.
  65
  66 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
  67 lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
  68 /2 width=3/ qed-.
  69
  70 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
  71                         (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
  72                                     ⋆.  ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
  73                                     U2 = ⓑ{I} V2. T
  74                         ) ∨
  75                         ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
  76 #U1 #U2 * -U1 -U2
  77 [ #J #I #V #T #H destruct
  78 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
  79 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
  80 | #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct /3 width=7/
  81 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
  82 | #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct /3 width=3/
  83 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
  84 ]
  85 qed.
  86
  87 lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
  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 /2 width=3/ qed-.
  94
  95 (* Basic_1: was pr0_gen_abbr *)
  96 lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
  97                      (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
  98                                  ⋆.  ⓓV2 ⊢ T2 [0, 1] ▶ T &
  99                                  U2 = ⓓV2. T
 100                       ) ∨
 101                       ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
 102 #V1 #T1 #U2 #H
 103 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 104 qed-.
 105
 106 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
 107                         ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
 108                                                U2 = ⓕ{I} V2. T2
 109                          | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 110                                                U0 = ⓛW. T1 &
 111                                                U2 = ⓓV2. T2 & I = Appl
 112                          | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 113                                                ⇧[0,1] V2 ≡ V &
 114                                                U0 = ⓓW1. T1 &
 115                                                U2 = ⓓW2. ⓐV. T2 &
 116                                                I = Appl
 117                          |                     (U0 ➡ U2 ∧ I = Cast).
 118 #U1 #U2 * -U1 -U2
 119 [ #I #J #V #T #H destruct
 120 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=5/
 121 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct /3 width=8/
 122 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
 123 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H destruct /3 width=12/
 124 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
 125 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct /3 width=1/
 126 ]
 127 qed.
 128
 129 lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
 130                      ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
 131                                             U2 = ⓕ{I} V2. T2
 132                       | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 133                                             U0 = ⓛW. T1 &
 134                                             U2 = ⓓV2. T2 & I = Appl
 135                       | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 136                                             ⇧[0,1] V2 ≡ V &
 137                                             U0 = ⓓW1. T1 &
 138                                             U2 = ⓓW2. ⓐV. T2 &
 139                                             I = Appl
 140                       |                     (U0 ➡ U2 ∧ I = Cast).
 141 /2 width=3/ qed-.
 142
 143 (* Basic_1: was pr0_gen_appl *)
 144 lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
 145                      ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
 146                                             U2 = ⓐV2. T2
 147                       | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
 148                                             U0 = ⓛW. T1 &
 149                                             U2 = ⓓV2. T2
 150                       | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
 151                                             ⇧[0,1] V2 ≡ V &
 152                                             U0 = ⓓW1. T1 &
 153                                             U2 = ⓓW2. ⓐV. T2.
 154 #V1 #U0 #U2 #H
 155 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
 156 qed-.
 157
 158 (* Note: the main property of simple terms *)
 159 lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝐒[T1] →
 160                             ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
 161                                      U = ⓐV2. T2.
 162 #V1 #T1 #U #H #HT1
 163 elim (tpr_inv_appl1 … H) -H *
 164 [ /2 width=5/
 165 | #V2 #W #W1 #W2 #_ #_ #H #_ destruct
 166   elim (simple_inv_bind … HT1)
 167 | #V2 #V #W1 #W2 #U1 #U2 #_ #_ #_ #_ #H #_ destruct
 168   elim (simple_inv_bind … HT1)
 169 ]
 170 qed-.
 171
 172 (* Basic_1: was: pr0_gen_cast *)
 173 lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 →
 174                        (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓣV2. T2)
 175                      ∨ T1 ➡ U2.
 176 #V1 #T1 #U2 #H
 177 elim (tpr_inv_flat1 … H) -H * /3 width=5/
 178 [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
 179 | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
 180 ]
 181 qed-.
 182
 183 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
 184                         ∨∨           T1 = #i
 185                          | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
 186                                      T1 = ⓓV. T
 187                          | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
 188 #T1 #T2 * -T1 -T2
 189 [ #I #i #H destruct /2 width=1/
 190 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 191 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 192 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 193 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 194 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
 195 | #V #T1 #T2 #HT12 #i #H destruct /3 width=4/
 196 ]
 197 qed.
 198
 199 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
 200                      ∨∨           T1 = #i
 201                       | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
 202                                   T1 = ⓓV. T
 203                       | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
 204 /2 width=3/ qed-.
 205
 206 (* Basic_1: removed theorems 3:
 207             pr0_subst0_back pr0_subst0_fwd pr0_subst0
 208    Basic_1: removed local theorems: 1: pr0_delta_tau
 209 *)