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 "basic_2/unfold/ltpss_ltpss.ma".
16 include "basic_2/unfold/ltpsss_tpss.ma".
18 (* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
20 (* Advanced properties ******************************************************)
22 lemma ltpsss_strip: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
23 ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
24 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶** L.
27 lemma ltpsss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
28 ∀T2,U2. L1 ⊢ T2 [d, e] ▶* U2 → L0 ⊢ T2 [d, e] ▶* U2.
29 #L0 #L1 #d #e #H @(ltpsss_ind … H) -L1
31 | #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
32 lapply (ltpss_tpss_trans_eq … HTU2 … HL1) -HL1 -HTU2 /2 width=1/
36 lemma ltpsss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ▶** L1 →
37 ∀T2,U2. L1 ⊢ T2 [d, e] ▶ U2 → L0 ⊢ T2 [d, e] ▶* U2.
40 lemma ltpsss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶* T2 →
41 ∀L2,ds,es. L1 [ds, es] ▶** L2 →
42 ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
43 #L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpsss_ind … H) -L2
45 | -HT12 #L #L2 #HL1 #HL2 * #T #HT1 #HT2
46 lapply (ltpsss_strap1 … HL1 HL2) -HL1 #HL12
47 elim (ltpss_tpss_conf … HT1 … HL2) -L #T0 #HT10 #HT0
48 lapply (ltpsss_tpss_trans_eq … HL12 … HT0) -HL12 -HT0 #HT0
49 lapply (tpss_trans_eq … HT2 HT0) -T /2 width=3/
53 lemma ltpsss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
54 ∀L2,ds,es. L1 [ds, es] ▶** L2 →
55 ∃∃T. L2 ⊢ T1 [d, e] ▶* T & L1 ⊢ T2 [ds, es] ▶* T.
58 (* Advanced forward lemmas **************************************************)
60 lemma ltpsss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶** L2 →
61 ∃∃K2,V2. K1 [0, e - 1] ▶** K2 &
62 K1 ⊢ V1 [0, e - 1] ▶* V2 &
64 #e #K1 #I #V1 #L2 #He #H @(ltpsss_ind … H) -L2
66 | #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
67 elim (ltpss_inv_tpss21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
68 lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
69 lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
73 lemma ltpsss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶** L2 →
74 ∃∃K2,V2. K1 [d - 1, e] ▶** K2 &
75 K1 ⊢ V1 [d - 1, e] ▶* V2 &
77 #d #e #K1 #I #V1 #L2 #Hd #H @(ltpsss_ind … H) -L2
79 | #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
80 elim (ltpss_inv_tpss11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
81 lapply (ltpss_tpss_trans_eq … HV2 … HK2) -HV2 #HV2
82 lapply (ltpsss_tpss_trans_eq … HK1 … HV2) -HV2 /3 width=5/
86 lemma ltpsss_fwd_tpss22: ∀I,L1,K2,V2,e. L1 [0, e] ▶** K2. ⓑ{I} V2 → 0 < e →
87 ∃∃K1,V1. K1 [0, e - 1] ▶** K2 &
88 K1 ⊢ V1 [0, e - 1] ▶* V2 &
90 #I #L1 #K2 #V2 #e #H #He @(ltpsss_ind_dx … H) -L1
92 | #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
93 elim (ltpss_inv_tpss22 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
94 lapply (tpss_trans_eq … HV1 HV2) -V #HV12
95 lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
99 lemma ltpsss_inv_tpss12: ∀I,L1,K2,V2,d,e. L1 [d, e] ▶** K2. ⓑ{I} V2 → 0 < d →
100 ∃∃K1,V1. K1 [d - 1, e] ▶** K2 &
101 K1 ⊢ V1 [d - 1, e] ▶* V2 &
103 #I #L1 #K2 #V2 #d #e #H #Hd @(ltpsss_ind_dx … H) -L1
105 | #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct
106 elim (ltpss_inv_tpss12 … HL1 ?) -HL1 // #K1 #V1 #HK1 #HV1 #H destruct
107 lapply (tpss_trans_eq … HV1 HV2) -V #HV12
108 lapply (ltpss_tpss_trans_eq … HV12 … HK1) -HV12 /3 width=5/
112 (* Main properties **********************************************************)
114 theorem ltpsss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶** L1 →
115 ∀L2,d2,e2. L0 [d2, e2] ▶** L2 →
116 ∃∃L. L1 [d2, e2] ▶** L & L2 [d1, e1] ▶** L.
119 theorem ltpsss_trans_eq: ∀L1,L,L2,d,e.
120 L1 [d, e] ▶** L → L [d, e] ▶** L2 → L1 [d, e] ▶** L2.
123 lemma ltpsss_tpss2: ∀L1,L2,I,V1,V2,e.
124 L1 [0, e] ▶** L2 → L2 ⊢ V1 [0, e] ▶* V2 →
125 L1. ⓑ{I} V1 [0, e + 1] ▶** L2. ⓑ{I} V2.
126 #L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
128 | #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
132 lemma ltpsss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
133 L1 [0, e - 1] ▶** L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
134 0 < e → L1. ⓑ{I} V1 [0, e] ▶** L2. ⓑ{I} V2.
135 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
136 >(plus_minus_m_m e 1) // /2 width=1/
139 lemma ltpsss_tpss1: ∀L1,L2,I,V1,V2,d,e.
140 L1 [d, e] ▶** L2 → L2 ⊢ V1 [d, e] ▶* V2 →
141 L1. ⓑ{I} V1 [d + 1, e] ▶** L2. ⓑ{I} V2.
142 #L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
144 | #V #V2 #_ #HV2 #IHV @(ltpsss_trans_eq … IHV) /2 width=1/
148 lemma ltpsss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
149 L1 [d - 1, e] ▶** L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
150 0 < d → L1. ⓑ{I} V1 [d, e] ▶** L2. ⓑ{I} V2.
151 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
152 >(plus_minus_m_m d 1) // /2 width=1/