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