matita/matita/contribs/lambdadelta/basic_2/reducibility/xpr.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/static/ssta.ma".
  16 include "basic_2/reducibility/cpr.ma".
  17
  18 lemma arith1: ∀x,y,z,w. z < y → x + (y + w) - z = x + y - z + w.
  19 #x #y #z #w #H <le_plus_minus_comm // /3 width=1 by lt_to_le, le_plus_a/
  20 qed-.
  21
  22 (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************)
  23
  24 notation "hvbox( ⦃term 46 h, break term 46 L⦄ ⊢ break term 46 T1 ➡ break [ term 46 g ] break term 46 T2 )"
  25    non associative with precedence 45
  26    for @{ 'XPRed $h $g $L $T1 $T2 }.
  27
  28 inductive xpr (h) (g): lenv → relation term ≝
  29 | xpr_cpr : ∀I,L,U2. L ⊢ ⓪{I} ➡ U2 → xpr h g L (⓪{I}) U2
  30 | xpr_ssta: ∀I,L,U2,l. ⦃h, L⦄ ⊢ ⓪{I} •[g] ⦃l+1, U2⦄ → xpr h g L (⓪{I}) U2
  31 | xpr_bind: ∀a,I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g (L.ⓑ{I}V2) T1 T2 →
  32             L ⊢ ⓑ{a,I}V2.T2 ➡ U2 → xpr h g L (ⓑ{a,I}V1.T1) U2
  33 | xpr_flat: ∀I,L,V1,V2,T1,T2,U2. xpr h g L V1 V2 → xpr h g L T1 T2 →
  34             L ⊢ ⓕ{I}V2.T2 ➡ U2 → xpr h g L (ⓕ{I}V1.T1) U2
  35 .
  36
  37 interpretation
  38    "context-sensitive extended parallel reduction (term)"
  39    'XPRed h g L T1 T2 = (xpr h g L T1 T2).
  40
  41 (* Basic properties *********************************************************)
  42
  43 (* Note: this is "∀h,g,L. reflexive … (xpr h g L)" *)
  44 lemma xpr_refl: ∀h,g,T,L. ⦃h, L⦄ ⊢ T ➡[g] T.
  45 #h #g #T elim T -T /2 width=1/ * /2 width=5/
  46 qed.
  47
  48 lemma cpr_xpr: ∀h,g,T1,L,T2. L ⊢ T1 ➡ T2 → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
  49 #h #g #T1 elim T1 -T1 /2 width=1/ * /2 width=5/
  50 qed.
  51
  52 lemma ssta_xpr: ∀h,g,T1,L,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ⦃h, L⦄ ⊢ T1 ➡[g] T2.
  53 #h #g #T1 elim T1 -T1 /2 width=2/ * [|*]
  54 [ #a #I #V1 #T1 #_ #IHT1 #L #X #l #H
  55   elim (ssta_inv_bind1 … H) -H #T2 #HT12 #H destruct /3 width=5/
  56 | #V1 #T1 #_ #IHT1 #L #X #l #H
  57   elim (ssta_inv_appl1 … H) -H #T2 #HT12 #H destruct /3 width=5/
  58 | #V1 #T1 #_ #IHT1 #L #X #l #H
  59   lapply (ssta_inv_cast1 … H) -H /3 width=5/
  60 ]
  61 qed.
  62
  63 include "basic_2/substitution/lift_lift.ma".
  64 include "basic_2/substitution/fsup.ma".
  65 include "basic_2/unfold/ltpss_dx_ldrop.ma".
  66