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_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
  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: ∀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 (𝕔{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_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
  44                              𝕓{I} V1. T1 ⇒  𝕓{I} V2. T2.
  45 /2/ qed.
  46
  47 lemma tpr_refl: ∀T. T ⇒ T.
  48 #T elim T -T //
  49 #I elim I -I /2/
  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 lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ⇒ U2 → U2 = 𝕒{I}.
  67 /2/ qed.
  68
  69 fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
  70                         (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
  71                                     ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
  72                                     U2 = 𝕓{I} V2. T
  73                         ) ∨
  74                         ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
  75 #U1 #U2 * -U1 U2
  76 [ #J #I #V #T #H destruct
  77 | #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
  78 | #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
  79 | #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
  80 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
  81 | #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
  82 | #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
  83 ]
  84 qed.
  85
  86 lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
  87                      (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
  88                                  ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
  89                                  U2 = 𝕓{I} V2. T
  90                      ) ∨
  91                      ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
  92 /2/ qed.
  93
  94 lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
  95                      (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
  96                                  ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
  97                                  U2 = 𝕓{Abbr} V2. T
  98                       ) ∨
  99                       ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
 100 #V1 #T1 #U2 #H
 101 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 102 qed.
 103
 104 fact tpr_inv_flat1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
 105                         ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
 106                                                U2 = 𝕗{I} V2. T2
 107                          | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
 108                                                U0 = 𝕔{Abst} W. T1 &
 109                                                U2 = 𝕔{Abbr} V2. T2 & I = Appl
 110                          | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
 111                                                ↑[0,1] V2 ≡ V &
 112                                                U0 = 𝕔{Abbr} W1. T1 &
 113                                                U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
 114                                                I = Appl
 115                          |                     (U0 ⇒ U2 ∧ I = Cast).
 116 #U1 #U2 * -U1 U2
 117 [ #I #J #V #T #H destruct
 118 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -I V1 T1 /3 width=5/
 119 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #J #V #T #H destruct -J V1 T /3 width=8/
 120 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #J #V0 #T0 #H destruct
 121 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #J #V0 #T0 #H
 122   destruct -J V1 T0 /3 width=12/
 123 | #V #T #T1 #T2 #_ #_ #J #V0 #T0 #H destruct
 124 | #V #T1 #T2 #HT12 #J #V0 #T0 #H destruct -J V T1 /3/
 125 ]
 126 qed.
 127
 128 lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ⇒ U2 →
 129                      ∨∨ ∃∃V2,T2.            V1 ⇒ V2 & U0 ⇒ T2 &
 130                                             U2 = 𝕗{I} V2. T2
 131                       | ∃∃V2,W,T1,T2.       V1 ⇒ V2 & T1 ⇒ T2 &
 132                                             U0 = 𝕔{Abst} W. T1 &
 133                                             U2 = 𝕔{Abbr} V2. T2 & I = Appl
 134                       | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
 135                                             ↑[0,1] V2 ≡ V &
 136                                             U0 = 𝕔{Abbr} W1. T1 &
 137                                             U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
 138                                             I = Appl
 139                       |                     (U0 ⇒ U2 ∧ I = Cast).
 140 /2/ qed.
 141
 142 lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ⇒ U2 →
 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 #V1 #U0 #U2 #H
 153 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
 154 qed.
 155
 156 lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ⇒ U2 →
 157                        (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Cast} V2. T2)
 158                      ∨ T1 ⇒ U2.
 159 #V1 #T1 #U2 #H
 160 elim (tpr_inv_flat1 … H) -H * /3 width=5/
 161 [ #V2 #W #W1 #W2 #_ #_ #_ #_ #H destruct
 162 | #V2 #W #W1 #W2 #T2 #U1 #_ #_ #_ #_ #_ #_ #H destruct
 163 ]
 164 qed.
 165
 166 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
 167                         ∨∨           T1 = #i
 168                          | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
 169                                      T1 = 𝕔{Abbr} V. T
 170                          | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
 171 #T1 #T2 * -T1 T2
 172 [ #I #i #H destruct /2/
 173 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 174 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
 175 | #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 176 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 177 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
 178 | #V #T1 #T2 #HT12 #i #H destruct /3/
 179 ]
 180 qed.
 181
 182 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
 183                      ∨∨           T1 = #i
 184                       | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
 185                                   T1 = 𝕔{Abbr} V. T
 186                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕔{Cast} V. T.
 187 /2/ qed.