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 elim (IHV01 … HV02) -IHV01 -HV02 #V #HV1 #HV2
36 elim (IHT01 … HT02) -T0 #T #HT1 #HT2
37 lapply (lsuby_cpy_trans … HT1 (L.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
38 lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V2) ?) -HT2
39 /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 [ -Hd1 -Hde2 | -Hd2 -Hde1 ]
57 [ elim (ylt_yle_false … Hde1) -Hde1 /2 width=3 by yle_trans/
58 | elim (ylt_yle_false … Hde2) -Hde2 /2 width=3 by yle_trans/
61 | #a #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
62 elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
63 elim (IHV01 … HV02 H) -IHV01 -HV02 #V #HV1 #HV2
64 elim (IHT01 … HT02) -T0
66 lapply (lsuby_cpy_trans … HT1 (L2.ⓑ{I}V1) ?) -HT1 /2 width=1 by lsuby_succ/
67 lapply (lsuby_cpy_trans … HT2 (L1.ⓑ{I}V2) ?) -HT2 /3 width=5 by cpy_bind, lsuby_succ, ex2_intro/
68 | -HV1 -HV2 elim H -H /3 width=1 by yle_succ, or_introl, or_intror/
70 | #I #G #L1 #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #L2 #X #d2 #e2 #HX #H
71 elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
72 elim (IHV01 … HV02 H) -V0
73 elim (IHT01 … HT02 H) -T0 -H /3 width=5 by cpy_flat, ex2_intro/
77 (* Note: the constant 1 comes from cpy_subst *)
78 theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 →
79 ∀T2. ⦃G, L⦄ ⊢ T0 ▶×[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2.
80 #G #L #T1 #T0 #d #e #H elim H -G -L -T1 -T0 -d -e
81 [ #I #G #L #d #e #T2 #H #He
82 elim (cpy_inv_atom1 … H) -H
84 | * #J #K #V #i #Hd2i #Hide2 #HLK #HVT2 #H destruct
85 lapply (ylt_yle_trans … (d+e) … Hide2) /2 width=5 by cpy_subst, monotonic_yle_plus_dx/
87 | #I #G #L #K #V #V2 #i #d #e #Hdi #Hide #HLK #HVW #T2 #HVT2 #He
88 lapply (cpy_weak … HVT2 0 (i+1) ? ?) -HVT2 /3 width=1 by yle_plus_dx2_trans, yle_succ/
89 >yplus_inj #HVT2 <(cpy_inv_lift1_eq … HVW … HVT2) -HVT2 /2 width=5 by cpy_subst/
90 | #a #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
91 elim (cpy_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
92 lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
93 lapply (IHT10 … HT02 He) -T0 /3 width=1 by cpy_bind/
94 | #I #G #L #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
95 elim (cpy_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpy_flat/
99 theorem cpy_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 →
100 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 →
101 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2.
102 #G #L #T1 #T0 #d1 #e1 #H elim H -G -L -T1 -T0 -d1 -e1
103 [ /2 width=3 by ex2_intro/
104 | #I #G #L #K #V #W #i1 #d1 #e1 #Hdi1 #Hide1 #HLK #HVW #T2 #d2 #e2 #HWT2 #Hde2d1
105 lapply (yle_trans … Hde2d1 … Hdi1) -Hde2d1 #Hde2i1
106 lapply (cpy_weak … HWT2 0 (i1+1) ? ?) -HWT2 /3 width=1 by yle_succ, yle_pred_sn/ -Hde2i1
107 >yplus_inj #HWT2 <(cpy_inv_lift1_eq … HVW … HWT2) -HWT2 /3 width=9 by cpy_subst, ex2_intro/
108 | #a #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
109 elim (cpy_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
110 lapply (lsuby_cpy_trans … HT02 (L.ⓑ{I}V1) ?) -HT02 /2 width=1 by lsuby_succ/ #HT02
111 elim (IHV10 … HV02) -IHV10 -HV02 // #V
112 elim (IHT10 … HT02) -T0 /2 width=1 by yle_succ/ #T #HT1 #HT2
113 lapply (lsuby_cpy_trans … HT2 (L.ⓑ{I}V) ?) -HT2 /3 width=6 by cpy_bind, lsuby_succ, ex2_intro/
114 | #I #G #L #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
115 elim (cpy_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
116 elim (IHV10 … HV02) -V0 //
117 elim (IHT10 … HT02) -T0 /3 width=6 by cpy_flat, ex2_intro/