matita/matita/contribs/lambda/paths/labeled_st_computation.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 "paths/standard_trace.ma".
  16 include "paths/labeled_sequential_computation.ma".
  17 include "paths/labeled_st_reduction.ma".
  18
  19 (* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************)
  20
  21 (* Note: lstar shuld be replaced by l_sreds *)
  22 definition pl_sts: trace → relation subterms ≝ lstar … pl_st.
  23
  24 interpretation "path-labeled standard reduction"
  25     'StdStar F p G = (pl_sts p F G).
  26
  27 notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )"
  28    non associative with precedence 45
  29    for @{ 'StdStar $F $p $G }.
  30
  31 lemma pl_sts_fwd_pl_sreds: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ⇓F1 ↦*[s] ⇓F2.
  32 #s #F1 #F2 #H @(lstar_ind_r ????????? H) -s -F2 //
  33 #p #s #F #F2 #_ #HF2 #IHF1
  34 lapply (pl_st_fwd_pl_sred … HF2) -HF2 /2 width=3/
  35 qed-.
  36
  37 lemma pl_sts_refl: reflexive … (pl_sts (◊)).
  38 //
  39 qed.
  40
  41 lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2.
  42 /2 width=3/
  43 qed-.
  44
  45 lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2.
  46 /2 width=3/
  47 qed-.
  48
  49 lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2.
  50 /2 width=1/
  51 qed.
  52
  53 lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2.
  54 /2 width=5 by lstar_inv_nil/
  55 qed-.
  56
  57 lemma pl_sts_inv_cons: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ∀q,r. q::r = s →
  58                        ∃∃F. F1 Ⓡ↦[q] F & F Ⓡ↦*[r] F2.
  59 /2 width=3 by lstar_inv_cons/
  60 qed-.
  61
  62 lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2.
  63 /2 width=1 by lstar_inv_step/
  64 qed-.
  65
  66 lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| →
  67                       ∃∃p,r,F. p::r = s & F1 Ⓡ↦[p] F & F Ⓡ↦*[r] F2.
  68 /2 width=1 by lstar_inv_pos/
  69 qed-.
  70
  71 lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
  72 /2 width=1/
  73 qed.
  74
  75 lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s).
  76 /3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/
  77 qed-.
  78
  79 lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s).
  80 /2 width=1/
  81 qed.
  82
  83 theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s).
  84 /3 width=7 by lstar_singlevalued, pl_st_mono/
  85 qed-.
  86
  87 theorem pl_sts_trans: ltransitive … pl_sts.
  88 /2 width=3 by lstar_ltransitive/
  89 qed-.
  90
  91 theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
  92 #s elim s -s // #p1 * //
  93 #p2 #s #IHs #F1 #F2 #H
  94 elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
  95 elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
  96 lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
  97 qed-.
  98
  99 axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
 100                                  ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
 101                                  is_standard (s@(p::◊)) →
 102                                  ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
 103
 104 theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
 105                                      ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
 106 #s #M1 #M2 #H @(lstar_ind_r ????????? H) -s -M2 /2 width=3/
 107 #p #s #M #M2 #_ #HM2 #IHM1 #Hsp
 108 lapply (is_standard_fwd_append_sn … Hsp) #Hs
 109 elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
 110 elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
 111 lapply (pl_sts_step_dx … HM1 … HF2) -F
 112 #H @(ex2_intro … F2) // (**) (* auto needs some help here *)
 113 qed-.