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/relocation/cpy_lift.ma".
17 (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
19 (* Main properties **********************************************************)
21 theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 →
22 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 →
23 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶×[d1, e1] T.
24 #G #L #T0 #T1 #d1 #e1 #H elim H -G -L -T0 -T1 -d1 -e1
25 [ /2 width=3 by ex2_intro/
26 | #I1 #G #L #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #T2 #d2 #e2 #H
27 elim (cpy_inv_lref1 … H) -H
28 [ #HX destruct /3 width=7 by cpy_subst, ex2_intro/
29 | -Hd1 -Hde1 * #I2 #K2 #V2 #_ #_ #HLK2 #HVT2
30 lapply (ldrop_mono … HLK1 … HLK2) -HLK1 -HLK2 #H destruct
31 >(lift_mono … HVT1 … HVT2) -HVT1 -HVT2 /2 width=3 by ex2_intro/
33 | #a #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
34 elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
35 lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
36 elim (IHV01 … HV02) -V0 #V #HV1 #HV2
37 elim (IHT01 … HT02) -T0 #T #HT1 #HT2
38 lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
39 lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
40 | #I #G #L #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
41 elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
42 elim (IHV01 … HV02) -V0
43 elim (IHT01 … HT02) -T0 /3 width=5 by cpy_flat, ex2_intro/
47 theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 →
48 ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 →
49 (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
50 ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶×[d1, e1] T.
51 #G #L1 #T0 #T1 #d1 #e1 #H elim H -G -L1 -T0 -T1 -d1 -e1
52 [ /2 width=3 by ex2_intro/
53 | #I1 #G #L1 #K1 #V1 #T1 #i0 #d1 #e1 #Hd1 #Hde1 #HLK1 #HVT1 #L2 #T2 #d2 #e2 #H1 #H2
54 elim (cpy_inv_lref1 … H1) -H1
55 [ #H destruct /3 width=7 by cpy_subst, ex2_intro/
56 | -HLK1 -HVT1 * #I2 #K2 #V2 #Hd2 #Hde2 #_ #_ elim H2 -H2 #Hded
58 lapply (transitive_le … Hded Hd2) -Hded -Hd2 #H
59 lapply (lt_to_le_to_lt … Hde1 H) -Hde1 -H #H
60 elim (lt_refl_false … H)
62 lapply (transitive_le … Hded Hd1) -Hded -Hd1 #H
63 lapply (lt_to_le_to_lt … Hde2 H) -Hde2 -H #H
64 elim (lt_refl_false … H)
67 | #a #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
68 elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
69 elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
70 elim (IHT01 … HT02) -T0
72 lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V) ?) -HT1 /2 width=1 by lsuby_succ/
73 lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
74 | -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H
75 /3 width=1 by monotonic_le_plus_l, or_intror, or_introl/
77 | #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
78 elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
79 elim (IHV01 … HV02 H) -V0
80 elim (IHT01 … HT02 H) -T0 -H /3 width=5 by cpy_flat, ex2_intro/
84 (* Note: the constant 1 comes from cpy_subst *)
85 theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 →
86 ∀T2. ⦃G, L⦄ ⊢ T0 ▶×[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2.
87 #G #L #T1 #T0 #d #e #H elim H -G -L -T1 -T0 -d -e
88 [ #I #G #L #d #e #T2 #H #He
89 elim (cpy_inv_atom1 … H) -H
91 | * #J #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct
92 lapply (lt_to_le_to_lt … (d+e) Hide2 ?) /2 width=5 by cpy_subst, monotonic_lt_plus_r/
94 | #I #G #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He
95 lapply (cpy_weak … HVT2 0 (i +1) ? ?) -HVT2 /2 width=1 by le_S_S/ #HVT2
96 <(cpy_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=5 by cpy_subst/
97 | #a #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
98 elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
99 lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
100 lapply (IHT10 … HT02 He) -T0 #HT12
101 lapply (lsuby_cpy_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /3 width=1 by cpy_bind, lsuby_succ/
102 | #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
103 elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpy_flat/
107 theorem cpy_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 →
108 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 →
109 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2.
110 #G #L #T1 #T0 #d1 #e1 #H elim H -G -L -T1 -T0 -d1 -e1
111 [ /2 width=3 by ex2_intro/
112 | #I #G #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
113 lapply (transitive_le … Hde2d1 Hdi1) -Hde2d1 #Hde2i1
114 lapply (cpy_weak … HWT2 0 (i1 + 1) ? ?) -HWT2 normalize /2 width=1 by le_S/ -Hde2i1 #HWT2
115 <(cpy_inv_lift1_eq … HWT2 … HVW) -HWT2 /3 width=9 by cpy_subst, ex2_intro/
116 | #a #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
117 elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
118 lapply (lsuby_cpy_trans … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
119 elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
120 elim (IHT10 … HT02 ?) -T0 /2 width=1 by le_S_S/ #T #HT1 #HT2
121 lapply (lsuby_cpy_trans … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1 by lsuby_succ/
122 lapply (lsuby_cpy_trans … HT2 (L. ⓑ{I} V2) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
123 | #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
124 elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
125 elim (IHV10 … HV02) -V0 //
126 elim (IHT10 … HT02) -T0 /3 width=6 by cpy_flat, ex2_intro/