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 … s F2 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_inv_pl_sreds: ∀s,M1,F2. {⊤}⇑M1 Ⓡ↦*[s] F2 → is_whd s →
  38                            ∃∃M2. M1 ↦*[s] M2 & {⊤}⇑M2 = F2.
  39 #s #M1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 /2 width=3/
  40 #p #s #F #F2 #_ #HF2 #IHF #H
  41 elim (is_whd_inv_append … H) -H #Hs * #Hp #_
  42 elim (IHF Hs) -IHF -Hs #M #HM #H destruct
  43 elim (pl_st_inv_pl_sred … HF2) -HF2 // -Hp #M2 #HM2 #H
  44 lapply (pl_sreds_step_dx … HM … HM2) -M /2 width=3/
  45 qed-.
  46
  47 lemma pl_sts_refl: reflexive … (pl_sts (◊)).
  48 //
  49 qed.
  50
  51 lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2.
  52 /2 width=3/
  53 qed-.
  54
  55 lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2.
  56 /2 width=3/
  57 qed-.
  58
  59 lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2.
  60 /2 width=1/
  61 qed.
  62
  63 lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2.
  64 /2 width=5 by lstar_inv_nil/
  65 qed-.
  66
  67 lemma pl_sts_inv_cons: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ∀q,r. q::r = s →
  68                        ∃∃F. F1 Ⓡ↦[q] F & F Ⓡ↦*[r] F2.
  69 /2 width=3 by lstar_inv_cons/
  70 qed-.
  71
  72 lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2.
  73 /2 width=1 by lstar_inv_step/
  74 qed-.
  75
  76 lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| →
  77                       ∃∃p,r,F. p::r = s & F1 Ⓡ↦[p] F & F Ⓡ↦*[r] F2.
  78 /2 width=1 by lstar_inv_pos/
  79 qed-.
  80
  81 lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. rc:::r = s →
  82                              ∃∃b1,T1. T1 Ⓡ↦*[r] T2 & {b1}𝛌.T1 = F1.
  83 #b2 #s #F1 #T2 #H @(lstar_ind_l … s F1 H) -s -F1
  84 [ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=4/
  85 | #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
  86   elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
  87   elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct
  88   elim (IHF2 ??) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
  89   #b0 #T0 #HT02 #H destruct
  90   lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/
  91 ]
  92 qed-.
  93
  94 lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
  95 /2 width=1/
  96 qed.
  97
  98 lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s).
  99 /3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/
 100 qed-.
 101
 102 lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s).
 103 /2 width=1/
 104 qed.
 105
 106 theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s).
 107 /3 width=7 by lstar_singlevalued, pl_st_mono/
 108 qed-.
 109
 110 theorem pl_sts_trans: ltransitive … pl_sts.
 111 /2 width=3 by lstar_ltransitive/
 112 qed-.
 113
 114 theorem pl_sts_inv_trans: inv_ltransitive … pl_sts.
 115 /2 width=3 by lstar_inv_ltransitive/
 116 qed-.
 117
 118 theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
 119 #s elim s -s // #p1 * //
 120 #p2 #s #IHs #F1 #F2 #H
 121 elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
 122 elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
 123 lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
 124 qed-.
 125
 126 lemma pl_sts_fwd_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
 127                           (∃r2. rc:::r2 = s) ∨ ∃∃r1,r2. r1@◊::rc:::r2 = s.
 128 #b2 #s #F1 #T2 #H
 129 lapply (pl_sts_fwd_is_standard … H)
 130 @(lstar_ind_l … s F1 H) -s -F1
 131 [ #_ @or_introl @(ex_intro … ◊) // (**) (* auto needs some help here *)
 132 | * [ | * #p ] #s #F1 #F #HF1 #HF #IHF #Hs
 133   lapply (is_standard_fwd_cons … Hs) #H
 134   elim (IHF H) -IHF -H * [2,4,6,8: #r1 ] #r2 #H destruct
 135 (* case 1: ◊, @ *)
 136   [ -Hs -F1 -F -T2 -b2
 137     @or_intror @(ex1_2_intro … (◊::r1) r2) // (**) (* auto needs some help here *)
 138 (* case 2: rc, @ *)
 139   | -F1 -F -T2 -b2
 140     lapply (is_standard_fwd_sle … Hs) -Hs #H
 141     lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
 142 (* case 3: sn, @ *)
 143   | -F1 -F -T2 -b2
 144     lapply (is_standard_fwd_sle … Hs) -Hs #H
 145     lapply (sle_nil_inv_in_whd … H) -H * #H #_ destruct
 146 (* case 4: dx, @ *)
 147   | -Hs -F1 -F -T2 -b2
 148     @or_intror @(ex1_2_intro … ((dx::p)::r1) r2) // (**) (* auto needs some help here *)
 149 (* case 5: ◊, no @ *)
 150   | -Hs -F1 -F -T2 -b2
 151     @or_intror @(ex1_2_intro … ◊ r2) // (**) (* auto needs some help here *)
 152 (* case 6, rc, no @ *)
 153   | -Hs -F1 -F -T2 -b2
 154     @or_introl @(ex_intro … (p::r2)) // (**) (* auto needs some help here *)
 155 (* case 7: sn, no @ *)
 156   | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
 157     #b #T #_ #HT -Hs -T2
 158     elim (pl_st_inv_sn … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
 159     #c #V1 #V #T0 #_ #_ #HT0 -c -V1 -F1 destruct
 160 (* case 8: dx, no @ *)
 161   | elim (pl_sts_inv_rc_abst_dx … HF ??) -b2 [3: // |2: skip ] (**) (* simplify line *)
 162     #b #T #_ #HT -Hs -T2
 163     elim (pl_st_inv_dx … HF1 ??) -HF1 [3: // |2: skip ] (**) (* simplify line *)
 164     #c #V #T1 #T0 #_ #_ #HT0 -T1 -F1 destruct
 165   ]
 166 ]
 167 qed-.
 168
 169 lemma pl_sts_fwd_abst_dx_is_whd: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
 170                                  ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s.
 171 #b2 #s #F1 #T2 #H
 172 lapply (pl_sts_fwd_is_standard … H)
 173 elim (pl_sts_fwd_abst_dx … H) -b2 -F1 -T2 * [ | #r1 ] #r2 #Hs destruct
 174 [ #_ @(ex2_2_intro … ◊ r2) //
 175 | <(associative_append … r1 (◊::◊) (rc:::r2)) #Hs
 176   lapply (is_standard_fwd_append_sn … Hs) -Hs #H
 177   lapply (is_standard_fwd_is_whd … H) -H // /4 width=4/
 178 ]
 179 qed-.
 180
 181 axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
 182                                  ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
 183                                  is_standard (s@(p::◊)) →
 184                                  ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
 185 (*
 186 #p #M #M2 #H elim H -p -M -M2
 187 [ #B #A #F #HF #s #M1 #HM1 #Hs
 188   lapply (is_standard_fwd_is_whd … Hs) -Hs // #Hs
 189   elim (pl_sts_inv_pl_sreds … HM1 Hs) -HM1 -Hs #M #_ #H -s -M1 destruct
 190   >carrier_boolean in HF; #H destruct normalize /2 width=3/
 191 | #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
 192   elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
 193   elim (pl_sts_fwd_abst_dx_is_whd … HM1) #r1 #r2 #Hr1 #H destruct
 194   elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
 195   elim (pl_sts_inv_pl_sreds … HM1 ?) // #M0 #_ #H -M1 -Hr1 destruct
 196   elim (pl_sts_inv_rc_abst_dx … HT ??) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
 197   elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct
 198   >associative_append in Hs; #Hs
 199   lapply (is_standard_fwd_append_dx … Hs) -r1
 200   <(map_cons_append … r2 (p::◊)) #H
 201   lapply (is_standard_inv_compatible_rc … H) -H #H
 202   elim (IHA12 … HT02 ?) // -r2 -A0 -IHA12 #F2 #HF2 #H
 203   @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
 204 (*
 205   elim (carrier_inv_appl … HF) -HF #b1 #V #G #HV #HG #HF
 206 *)
 207 *)
 208 theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
 209                                      ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
 210 #s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 /2 width=3/
 211 #p #s #M #M2 #_ #HM2 #IHM1 #Hsp
 212 lapply (is_standard_fwd_append_sn … Hsp) #Hs
 213 elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
 214 elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
 215 lapply (pl_sts_step_dx … HM1 … HF2) -F
 216 #H @(ex2_intro … F2) // (**) (* auto needs some help here *)
 217 qed-.