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/tpss_tpss.ma".
16 include "basic_2/unfold/ltpss_tpss.ma".
18 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
20 (* Advanced properties ******************************************************)
22 (* Main properties **********************************************************)
24 theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
25 L1 [d, e] ▶* L → L [d, e] ▶* L2 → L1 [d, e] ▶* L2.
28 lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
29 L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶* V2 →
30 L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
31 #L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
33 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
37 lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
38 L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
39 0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
40 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
41 >(plus_minus_m_m e 1) // /2 width=1/
44 lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
45 L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶* V2 →
46 L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
47 #L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
49 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
53 lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
54 L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
55 0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
56 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
57 >(plus_minus_m_m d 1) // /2 width=1/
60 fact ltps_conf_aux: ∀K,K1,L1,d1,e1. K1 [d1, e1] ▶ L1 →
61 ∀K2,L2,d2,e2. K2 [d2, e2] ▶ L2 → K1 = K → K2 = K →
62 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
63 #K @(lw_wf_ind … K) -K #K #IH #K1 #L1 #d1 #e1 * -K1 -L1 -d1 -e1
65 | -IH #K1 #I1 #V1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
67 | #K2 #I2 #V2 #H1 #H2 destruct /2 width=3/
68 | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
69 | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct /4 width=3/
71 | #K1 #L1 #I1 #W1 #V1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
72 [ -IH #d2 #e2 #H1 #H2 destruct
73 | -IH #K2 #I2 #V2 #H1 #H2 destruct
74 @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
75 | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
76 elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
77 elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
78 elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
79 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
80 @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
81 [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
82 | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
84 | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
85 elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
86 elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
87 elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
88 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
89 @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
90 [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
91 | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
94 | #K1 #L1 #I1 #W1 #V1 #d1 #e1 #HKL1 #HWV1 #K2 #L2 #d2 #e2 * -K2 -L2 -d2 -e2
95 [ -IH #d2 #e2 #H1 #H2 destruct
96 | -IH #K2 #I2 #V2 #H1 #H2 destruct
97 @ex2_1_intro [2,3: @inj ] /3 width=5/ (**) (* /4 width=5/ is too slow *)
98 | #K2 #L2 #I2 #W2 #V2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
99 elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
100 elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
101 elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
102 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
103 @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
104 [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
105 | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
107 | #K2 #L2 #I2 #W2 #V2 #d2 #e2 #HKL2 #HWV2 #H1 #H2 destruct
108 elim (IH … HKL1 … HKL2 ? ?) -IH [2,4: // |3: skip |5: /2 width=1/ ] -K1 #L #HL1 #HL2
109 elim (ltpss_tps_conf … HWV1 … HL1) #U1 #HWU1 #HVU1
110 elim (ltpss_tps_conf … HWV2 … HL2) #U2 #HWU2 #HVU2
111 elim (tpss_conf_eq … HWU1 … HWU2) -W1 #W #HU1W #HU2W
112 @(ex2_1_intro … (L.ⓑ{I1}W)) (**) (* explicit constructor *)
113 [ @(ltpss_trans_eq … (L1.ⓑ{I1}U1)) /2 width=1/
114 | @(ltpss_trans_eq … (L2.ⓑ{I1}U2)) /2 width=1/
120 lemma ltps_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶ L1 →
121 ∀L2,d2,e2. L0 [d2, e2] ▶ L2 →
122 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
125 axiom ltpss_conf: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
126 ∀L2,d2,e2. L0 [d2, e2] ▶* L2 →
127 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
129 fact ltpss_conf_aux: ∀K1,L1,d1,e1. K1 [d1, e1] ▶* L1 →
130 ∀K2,L2,d2,e2. K2 [d2, e2] ▶* L2 → K1 = K2 →
131 ∃∃L. L1 [d2, e2] ▶* L & L2 [d1, e1] ▶* L.
132 #K1 #L1 #d1 #e1 #H @(ltpss_ind_dx … H) -K1 /2 width=3/
133 #X1 #K1 #HXK1 #HKL1 #IHKL1 #K2 #L2 #d2 #e2 #H @(ltpss_ind_dx … H) -K2
135 lapply (ltpss_strap … HXK1 HKL1) -K1 /2 width=3/
136 | #X2 #K2 #HXK2 #HKL2 #_ #H destruct
137 elim (ltps_conf … HXK1 … HXK2) -X2 #K #HK1 #HK2
138 elim (IHKL1 … HK1 ?) // -K1 #L #HL1 #HKL
139 @(ex2_1_intro … K) //