matita/matita/lib/lambda-delta/reduction/tpr_defs.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 "lambda-delta/substitution/subst_defs.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,T0,T.
  27              tpr V1 V2 → tpr T1 T2 →
  28              ⋆.  𝕓{Abbr} V2 ⊢ ↓[0, 1] T2 ≡ T0 → ↑[0, 1] T0 ≡ T →
  29              tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} 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    'PR T1 T2 = (tpr T1 T2).
  41
  42 (* Basic properties *********************************************************)
  43
  44 lemma tpr_refl: ∀T. T ⇒ T.
  45 #T elim T -T //
  46 #I elim I -I /2/
  47 qed.
  48
  49 (* The basic inversion lemmas ***********************************************)
  50
  51 lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
  52                          ∨∨           T1 = #i
  53                           | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
  54                                       T1 = 𝕓{Abbr} V. T
  55                           | ∃∃V,T.    T ⇒ #i & T1 = 𝕗{Cast} V. T.
  56 #T1 #T2 #H elim H -H T1 T2
  57 [ #k #i #H destruct
  58 | #j #i /2/
  59 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
  60 | #I #V1 #V2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
  61 | #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #i #H destruct
  62 | #V1 #V2 #T1 #T2 #T0 #T #_ #_ #_ #_ #_ #_ #i #H destruct
  63 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #i #H destruct
  64 | #V #T #T1 #T2 #HT1 #HT12 #_ #i #H destruct /3 width=6/
  65 | #V #T1 #T2 #HT12 #_ #i #H destruct /3/
  66 ]
  67 qed.
  68
  69 lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
  70                      ∨∨           T1 = #i
  71                       | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
  72                                   T1 = 𝕓{Abbr} V. T
  73                       | ∃∃V,T.    T ⇒ #i & T1 = 𝕗{Cast} V. T.
  74 /2/ qed.