matita/matita/lib/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 "lambda/paths/standard_trace.ma".
  16 include "lambda/paths/labeled_sequential_computation.ma".
  17 include "lambda/paths/labeled_st_reduction.ma".
  18
  19 include "lambda/notation/relations/stdstar_3.ma".
  20
  21 include "lambda/xoa/ex_2_3.ma".
  22
  23 (* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************)
  24
  25 (* Note: lstar shuld be replaced by l_sreds *)
  26 definition pl_sts: trace → relation subterms ≝ lstar … pl_st.
  27
  28 interpretation "path-labeled standard reduction"
  29     'StdStar F p G = (pl_sts p F 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_inv_empty: ∀s,M1,F2. {⊥}⇑M1 Ⓡ↦*[s] F2 → ◊ = s ∧ {⊥}⇑M1 = F2.
  48 #s #M1 #F2 #H @(lstar_ind_r … s F2 H) -s -F2 /2 width=1/ #p #s #F #F2 #_ #HF2 * #_ #H
  49 elim (pl_st_inv_empty … HF2 … H)
  50 qed-.
  51
  52 lemma pl_sts_refl: reflexive … (pl_sts (◊)).
  53 //
  54 qed.
  55
  56 lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2.
  57 /2 width=3/
  58 qed-.
  59
  60 lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2.
  61 /2 width=3/
  62 qed-.
  63
  64 lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2.
  65 /2 width=1/
  66 qed.
  67
  68 lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2.
  69 /2 width=5 by lstar_inv_nil/
  70 qed-.
  71
  72 lemma pl_sts_inv_cons: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ∀q,r. q::r = s →
  73                        ∃∃F. F1 Ⓡ↦[q] F & F Ⓡ↦*[r] F2.
  74 /2 width=3 by lstar_inv_cons/
  75 qed-.
  76
  77 lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2.
  78 /2 width=1 by lstar_inv_step/
  79 qed-.
  80
  81 lemma pl_sts_inv_pos: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → 0 < |s| →
  82                       ∃∃p,r,F. p::r = s & F1 Ⓡ↦[p] F & F Ⓡ↦*[r] F2.
  83 /2 width=1 by lstar_inv_pos/
  84 qed-.
  85
  86 lemma pl_sts_inv_rc_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 → ∀r. rc:::r = s →
  87                              ∃∃b1,T1. T1 Ⓡ↦*[r] T2 & {b1}𝛌.T1 = F1.
  88 #b2 #s #F1 #T2 #H @(lstar_ind_l … s F1 H) -s -F1
  89 [ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=4/
  90 | #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
  91   elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
  92   elim (pl_st_inv_rc … HF1 … Hp) -HF1 -p #b1 #T1 #T #HT1 #HF1 #HF destruct
  93   elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
  94   #b0 #T0 #HT02 #H destruct
  95   lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=4/
  96 ]
  97 qed-.
  98
  99 lemma pl_sts_inv_sn_appl_dx: ∀b2,s,F1,V2,T2. F1 Ⓡ↦*[s] {b2}@V2.T2 → ∀r. sn:::r = s →
 100                              ∃∃b1,V1,T1. V1 Ⓡ↦*[r] V2 & {b1}@V1.T1 = F1.
 101 #b2 #s #F1 #V2 #T2 #H @(lstar_ind_l … s F1 H) -s -F1
 102 [ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=5/
 103 | #p #s #F1 #F #HF1 #_ #IHF2 #r #H -b2
 104   elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
 105   elim (pl_st_inv_sn … HF1 … Hp) -HF1 -p #b1 #V1 #V #T1 #HV1 #HF1 #HF destruct
 106   elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
 107   #b0 #V0 #T0 #HV02 #H destruct
 108   lapply (pl_sts_step_sn … HV1 … HV02) -V /2 width=5/
 109 ]
 110 qed-.
 111
 112 lemma pl_sts_inv_dx_appl_dx: ∀b,s,F1,V,T2. F1 Ⓡ↦*[s] {b}@V.T2 → ∀r. dx:::r = s →
 113                              ∃∃T1. T1 Ⓡ↦*[r] T2 & {b}@V.T1 = F1.
 114 #b #s #F1 #V #T2 #H @(lstar_ind_l … s F1 H) -s -F1
 115 [ #r #H lapply (map_cons_inv_nil … r H) -H #H destruct /2 width=3/
 116 | #p #s #F1 #F #HF1 #_ #IHF2 #r #H
 117   elim (map_cons_inv_cons … r H) -H #q #r0 #Hp #Hs #Hr
 118   elim (pl_st_inv_dx … HF1 … Hp) -HF1 -p #b0 #V0 #T1 #T #HT1 #HF1 #HF destruct
 119   elim (IHF2 …) -IHF2 [3: // |2: skip ] (**) (* simplify line *)
 120   #T0 #HT02 #H destruct
 121   lapply (pl_sts_step_sn … HT1 … HT02) -T /2 width=3/
 122 ]
 123 qed-.
 124
 125 lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
 126 /2 width=1/
 127 qed.
 128
 129 lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s).
 130 /3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/
 131 qed-.
 132
 133 lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s).
 134 /2 width=1/
 135 qed.
 136
 137 theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s).
 138 /3 width=7 by lstar_singlevalued, pl_st_mono/
 139 qed-.
 140
 141 theorem pl_sts_trans: ltransitive … pl_sts.
 142 /2 width=3 by lstar_ltransitive/
 143 qed-.
 144
 145 lemma pl_sts_inv_trans: inv_ltransitive … pl_sts.
 146 /2 width=3 by lstar_inv_ltransitive/
 147 qed-.
 148
 149 lemma pl_sts_fwd_dx_sn_appl_dx: ∀b2,s,r,F1,V2,T2. F1 Ⓡ↦*[(dx:::s)@(sn:::r)] {b2}@V2.T2 →
 150                                 ∃∃b1,V1,T1,T0. V1 Ⓡ↦*[r] V2 & T1 Ⓡ↦*[s] T0 & {b1}@V1.T1 = F1.
 151 #b2 #s #r #F1 #V2 #T2 #H
 152 elim (pl_sts_inv_trans … H) -H #F #HF1 #H
 153 elim (pl_sts_inv_sn_appl_dx … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 154 #b #V #T #HV2 #H destruct
 155 elim (pl_sts_inv_dx_appl_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
 156 #T1 #HT1 #H destruct /2 width=7/
 157 qed-.
 158
 159 theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
 160 #s elim s -s // #p1 * //
 161 #p2 #s #IHs #F1 #F2 #H
 162 elim (pl_sts_inv_cons … H …) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
 163 elim (pl_sts_inv_cons … H …) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
 164 lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
 165 qed-.
 166
 167 lemma pl_sts_fwd_abst_dx: ∀b2,s,F1,T2. F1 Ⓡ↦*[s] {b2}𝛌.T2 →
 168                           ∃∃r1,r2. is_whd r1 & r1@rc:::r2 = s.
 169 #b2 #s #F1 #T2 #H
 170 lapply (pl_sts_fwd_is_standard … H)
 171 @(lstar_ind_l … s F1 H) -s -F1
 172 [ #_ @(ex2_2_intro … ◊ ◊) // (**) (* auto needs some help here *)
 173 | #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
 174   lapply (is_standard_fwd_cons … Hs) #H
 175   elim (IHF1 …) // -IHF1 -H #r1 #r2 #Hr1 #H destruct
 176   elim (in_whd_or_in_inner p) #Hp
 177   [ -Hs -F1 -F -T2 -b2
 178     @(ex2_2_intro … (p::r1) r2) // /2 width=1/ (**) (* auto needs some help here *)
 179   | lapply (is_standard_fwd_append_sn (p::r1) ? Hs) -Hs #H
 180     lapply (is_standard_fwd_in_inner … H ?) -H // #H
 181     lapply (is_whd_is_inner_inv … Hr1 ?) -Hr1 // -H #H destruct
 182     elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp
 183 (* case 1: dx *)
 184     [ -IHq
 185       elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
 186       #b #T #_ #HT -T2
 187       elim (pl_st_inv_dx … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
 188       #c #V #T1 #T0 #_ #_ #HT0 -q -T1 -F1 destruct
 189 (* case 2: rc *)
 190     | destruct -F1 -F -T2 -b2
 191       @(ex2_2_intro … ◊ (q::r2)) // (**) (* auto needs some help here *)
 192 (* case 3: sn *)
 193     | elim (pl_sts_inv_rc_abst_dx … HF2 …) -b2 [3: // |2: skip ] (**) (* simplify line *)
 194       #b #T #_ #HT -T2
 195       elim (pl_st_inv_sn … HF1 …) -HF1 [3: // |2: skip ] (**) (* simplify line *)
 196       #c #V1 #V #T0 #_ #_ #HT0 -c -q -V1 -F1 destruct
 197     ]
 198   ]
 199 ]
 200 qed-.
 201
 202 lemma pl_sts_fwd_appl_dx: ∀b2,s,F1,V2,T2. F1 Ⓡ↦*[s] {b2}@V2.T2 →
 203                           ∃∃r1,r2,r3. is_whd r1 & is_inner r2 &
 204                                       r1@(dx:::r2)@sn:::r3 = s.
 205 #b2 #s #F1 #V2 #T2 #H
 206 lapply (pl_sts_fwd_is_standard … H)
 207 @(lstar_ind_l … s F1 H) -s -F1
 208 [ #_ @(ex3_3_intro … ◊ ◊ ◊) // (**) (* auto needs some help here *)
 209 | #p #s #F1 #F #HF1 #HF2 #IHF1 #Hs
 210   lapply (is_standard_fwd_cons … Hs) #H
 211   elim (IHF1 …) // -IHF1 -H #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
 212   elim (in_whd_or_in_inner p) #Hp
 213   [ -Hs -F1 -F -V2 -T2 -b2
 214     @(ex3_3_intro … (p::r1) r2 r3) // /2 width=1/ (**) (* auto needs some help here *)
 215   | lapply (is_standard_fwd_append_sn (p::r1) ? Hs) -Hs #H
 216     lapply (is_standard_fwd_in_inner … H ?) -H // #H
 217     lapply (is_whd_is_inner_inv … Hr1 ?) -Hr1 // -H #H destruct
 218     elim (in_inner_inv … Hp) -Hp * #q [3: #IHq ] #Hp
 219 (* case 1: dx *)
 220     [ destruct -F1 -F -V2 -T2 -b2
 221       @(ex3_3_intro … ◊ (q::r2) r3) // /2 width=1/ (**) (* auto needs some help here *)
 222 (* case 2: rc *)
 223     | -Hr2
 224       elim (pl_sts_fwd_dx_sn_appl_dx … HF2) -b2 #b #V #T #T0 #_ #_ #HT -V2 -T2 -T0
 225       elim (pl_st_inv_rc … HF1 … Hp) -HF1 #c #V0 #T0 #_ #_ #HT0 -c -V0 -q -F1 destruct
 226 (* case 3: sn *)
 227     | -Hr2
 228       elim (pl_sts_fwd_dx_sn_appl_dx … HF2) -b2 #b #V #T #T0 #_ #HT0 #HT -V2 -T2
 229       elim (pl_st_inv_sn … HF1 … Hp) -HF1 #c #V1 #V0 #T1 #_ #_ #H -c -V1 -F1 destruct -V
 230       elim (pl_sts_inv_empty … HT0) -HT0 #H #_ -T0 -T1 destruct
 231       @(ex3_3_intro … ◊ ◊ (q::r3)) // (**) (* auto needs some help here *)
 232     ]
 233   ]
 234 ]
 235 qed-.
 236
 237 lemma pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
 238                                  ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
 239                                  is_standard (s@(p::◊)) →
 240                                  ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
 241 #p #M #M2 #H elim H -p -M -M2
 242 [ #B #A #F #HF #s #M1 #HM1 #Hs
 243   lapply (is_standard_fwd_is_whd … Hs) -Hs // #Hs
 244   elim (pl_sts_inv_pl_sreds … HM1 Hs) -HM1 -Hs #M #_ #H -s -M1 destruct
 245   >carrier_boolean in HF; #H destruct normalize /2 width=3/
 246 | #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
 247   elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
 248   elim (pl_sts_fwd_abst_dx … HM1) #r1 #r2 #Hr1 #H destruct
 249   elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
 250   elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
 251   >associative_append in Hs; #Hs
 252   lapply (is_standard_fwd_append_dx … Hs) -r1
 253   <(map_cons_append … r2 (p::◊)) #H
 254   lapply (is_standard_inv_compatible_rc … H) -H #Hp
 255   elim (pl_sts_inv_rc_abst_dx … HT …) -HT [3: // |2: skip ] #b0 #T0 #HT02 #H (**) (* simplify line *)
 256   elim (boolean_inv_abst … (sym_eq … H)) -H #A0 #_ #H #_ -b0 -M0 destruct
 257   elim (IHA12 … HT02 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
 258   @(ex2_intro … ({⊥}𝛌.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
 259 | #p #B1 #B2 #A #_ #IHB12 #F #HF #s #M1 #HM1 #Hs
 260   elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
 261   elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #_ #H destruct
 262   elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
 263   elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
 264   >associative_append in Hs; #Hs
 265   lapply (is_standard_fwd_append_dx … Hs) -r1
 266   >associative_append #Hs
 267   lapply (is_standard_fwd_append_dx … Hs) -Hs
 268   <(map_cons_append … r3 (p::◊)) #H
 269   lapply (is_standard_inv_compatible_sn … H) -H #Hp
 270   elim (pl_sts_fwd_dx_sn_appl_dx … HT) -HT #b0 #V0 #T0 #T1 #HV0 #_ #H -T1 -r2
 271   elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #H #_ #_ -b0 -M0 -T0 destruct
 272   elim (IHB12 … HV0 …) // -r3 -B0 -IHB12 #G2 #HG2 #H
 273   @(ex2_intro … ({⊥}@G2.{⊥}⇕T)) normalize // /2 width=1/ (**) (* auto needs some help here *)
 274 | #p #B #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
 275   elim (carrier_inv_appl … HF) -HF #b #V #T #HV #HT #HF destruct
 276   elim (pl_sts_fwd_appl_dx … HM1) #r1 #r2 #r3 #Hr1 #Hr2 #H destruct
 277   elim (pl_sts_inv_trans … HM1) -HM1 #F0 #HM1 #HT
 278   elim (pl_sts_inv_pl_sreds … HM1 …) // #M0 #_ #H -M1 -Hr1 destruct
 279   >associative_append in Hs; #Hs
 280   lapply (is_standard_fwd_append_dx … Hs) -r1
 281   >associative_append #Hs
 282   elim (list_inv … r3)
 283   [ #H destruct
 284     elim (in_whd_or_in_inner p) #Hp
 285     [ lapply (is_standard_fwd_is_whd … Hs) -Hs /2 width=1/ -Hp #Hs
 286       lapply (is_whd_inv_dx … Hs) -Hs #H
 287       lapply (is_whd_is_inner_inv … Hr2) -Hr2 // -H #H destruct
 288       lapply (pl_sts_inv_nil … HT ?) -HT // #H
 289       elim (boolean_inv_appl … H) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
 290       elim (IHA12 … A0 …) -IHA12 [3,5,6: // |2,4: skip ] (* simplify line *)
 291       #F2 #HF2 #H
 292       @(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
 293     | <(map_cons_append … r2 (p::◊)) in Hs; #H
 294       lapply (is_standard_inv_compatible_dx … H ?) -H /3 width=1/ -Hp #Hp
 295       >append_nil in HT; #HT
 296       elim (pl_sts_inv_dx_appl_dx … HT …) -HT [3: // |2: skip ] (* simplify line *)
 297       #T0 #HT0 #H
 298       elim (boolean_inv_appl … (sym_eq … H)) -H #B0 #A0 #_ #_ #H #_ -M0 -B0 destruct
 299       elim (IHA12 … HT0 …) // -r2 -A0 -IHA12 #F2 #HF2 #H
 300       @(ex2_intro … ({b}@V.F2)) normalize // /2 width=1/ (**) (* auto needs some help here *)
 301     ]
 302   | -IHA12 -Hr2 -M0 * #q #r #H destruct
 303     lapply (is_standard_fwd_append_dx … Hs) -r2 #Hs
 304     lapply (is_standard_fwd_sle … Hs) -r #H
 305     elim (sle_inv_sn … H …) -H [3: // |2: skip ] (**) (* simplify line *)
 306     #q0 #_ #H destruct
 307   ]
 308 ]
 309 qed-.
 310
 311 theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
 312                                      ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
 313 #s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 /2 width=3/
 314 #p #s #M #M2 #_ #HM2 #IHM1 #Hsp
 315 lapply (is_standard_fwd_append_sn … Hsp) #Hs
 316 elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
 317 elim (pl_sred_is_standard_pl_st … HM2 … HM1 …) -HM2 // -M -Hsp #F2 #HF2 #HFM2
 318 lapply (pl_sts_step_dx … HM1 … HF2) -F
 319 #H @(ex2_intro … F2) // (**) (* auto needs some help here *)
 320 qed-.