1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "paths/standard_trace.ma".
16 include "paths/labeled_sequential_computation.ma".
17 include "paths/labeled_st_reduction.ma".
19 (* PATH-LABELED STANDARD COMPUTATION (MULTISTEP) ****************************)
21 (* Note: lstar shuld be replaced by l_sreds *)
22 definition pl_sts: trace → relation subterms ≝ lstar … pl_st.
24 interpretation "path-labeled standard reduction"
25 'StdStar F p G = (pl_sts p F G).
27 notation "hvbox( F break Ⓡ ↦* [ term 46 p ] break term 46 G )"
28 non associative with precedence 45
29 for @{ 'StdStar $F $p $G }.
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/
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/
47 lemma pl_sts_refl: reflexive … (pl_sts (◊)).
51 lemma pl_sts_step_sn: ∀p,F1,F. F1 Ⓡ↦[p] F → ∀s,F2. F Ⓡ↦*[s] F2 → F1 Ⓡ↦*[p::s] F2.
55 lemma pl_sts_step_dx: ∀s,F1,F. F1 Ⓡ↦*[s] F → ∀p,F2. F Ⓡ↦[p] F2 → F1 Ⓡ↦*[s@p::◊] F2.
59 lemma pl_sts_step_rc: ∀p,F1,F2. F1 Ⓡ↦[p] F2 → F1 Ⓡ↦*[p::◊] F2.
63 lemma pl_sts_inv_nil: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → ◊ = s → F1 = F2.
64 /2 width=5 by lstar_inv_nil/
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/
72 lemma pl_sts_inv_step_rc: ∀p,F1,F2. F1 Ⓡ↦*[p::◊] F2 → F1 Ⓡ↦[p] F2.
73 /2 width=1 by lstar_inv_step/
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/
81 lemma pl_sts_lift: ∀s. sliftable (pl_sts s).
85 lemma pl_sts_inv_lift: ∀s. sdeliftable_sn (pl_sts s).
86 /3 width=3 by lstar_sdeliftable_sn, pl_st_inv_lift/
89 lemma pl_sts_dsubst: ∀s. sdsubstable_f_dx … (booleanized ⊥) (pl_sts s).
93 theorem pl_sts_mono: ∀s. singlevalued … (pl_sts s).
94 /3 width=7 by lstar_singlevalued, pl_st_mono/
97 theorem pl_sts_trans: ltransitive … pl_sts.
98 /2 width=3 by lstar_ltransitive/
101 theorem pl_sts_fwd_is_standard: ∀s,F1,F2. F1 Ⓡ↦*[s] F2 → is_standard s.
102 #s elim s -s // #p1 * //
103 #p2 #s #IHs #F1 #F2 #H
104 elim (pl_sts_inv_cons … H ???) -H [4: // |2,3: skip ] #F3 #HF13 #H (**) (* simplify line *)
105 elim (pl_sts_inv_cons … H ???) [2: // |3,4: skip ] #F4 #HF34 #_ (**) (* simplify line *)
106 lapply (pl_st_fwd_sle … HF13 … HF34) -F1 -F4 /3 width=3/
109 axiom pl_sred_is_standard_pl_st: ∀p,M,M2. M ↦[p] M2 → ∀F. ⇓F = M →
110 ∀s,M1.{⊤}⇑ M1 Ⓡ↦*[s] F →
111 is_standard (s@(p::◊)) →
112 ∃∃F2. F Ⓡ↦[p] F2 & ⇓F2 = M2.
114 #p #M #M2 #H elim H -p -M -M2
115 [ #B #A #F #HF #s #M1 #HM1 #Hs
116 lapply (is_standard_fwd_is_whd … Hs) -Hs // #Hs
117 elim (pl_sts_inv_pl_sreds … HM1 Hs) -HM1 -Hs #M #_ #H -s -M1 destruct
118 >carrier_boolean in HF; #H destruct normalize /2 width=3/
119 | #p #A1 #A2 #_ #IHA12 #F #HF #s #M1 #HM1 #Hs
120 elim (carrier_inv_abst … HF) -HF #b #T #HT #HF destruct
122 elim (carrier_inv_appl … HF) -HF #b1 #V #G #HV #HG #HF
125 theorem pl_sreds_is_standard_pl_sts: ∀s,M1,M2. M1 ↦*[s] M2 → is_standard s →
126 ∃∃F2. {⊤}⇑ M1 Ⓡ↦*[s] F2 & ⇓F2 = M2.
127 #s #M1 #M2 #H @(lstar_ind_r … s M2 H) -s -M2 /2 width=3/
128 #p #s #M #M2 #_ #HM2 #IHM1 #Hsp
129 lapply (is_standard_fwd_append_sn … Hsp) #Hs
130 elim (IHM1 Hs) -IHM1 -Hs #F #HM1 #H
131 elim (pl_sred_is_standard_pl_st … HM2 … HM1 ?) -HM2 // -M -Hsp #F2 #HF2 #HFM2
132 lapply (pl_sts_step_dx … HM1 … HF2) -F
133 #H @(ex2_intro … F2) // (**) (* auto needs some help here *)