matita/matita/lib/lambda-delta/reduction/cpr.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/reduction/tpr.ma".
  13
  14 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
  15
  16 definition cpr: lenv → term → term → Prop ≝
  17    λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2.
  18
  19 interpretation
  20    "context-sensitive parallel reduction (term)"
  21    'PRed L T1 T2 = (cpr L T1 T2).
  22
  23 (* Basic properties *********************************************************)
  24
  25 lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
  26 /2/ qed.
  27
  28 lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
  29 /3 width=5/ qed.
  30
  31 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
  32 /2/ qed.
  33
  34 (* NOTE: new property *)
  35 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
  36                 L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
  37 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
  38 qed.
  39
  40 lemma cpr_delta: ∀L,K,V1,V2,V,i.
  41                  ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫ V2 →
  42                  ↑[0, i + 1] V2 ≡ V → L ⊢ #i ⇒ V.
  43 #L #K #V1 #V2 #V #i #HLK #HV12 #HV2
  44 @ex2_1_intro [2: // | skip ] /3 width=8/ (**) (* /4/ is too slow *)
  45 qed.
  46
  47 lemma cpr_cast: ∀L,V,T1,T2.
  48                 L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{Cast} V. T1 ⇒ T2.
  49 #L #V #T1 #T2 * /3/
  50 qed.
  51
  52 (* Basic inversion lemmas ***************************************************)