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_cpy.ma".
16 include "basic_2/substitution/cpys_lift.ma".
18 (* CONTEXT-SENSITIVE EXTENDED MULTIPLE SUBSTITUTION FOR TERMS ***************)
20 (* Advanced inversion lemmas ************************************************)
22 lemma cpys_inv_SO2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶*×[d, 1] T2 → ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2.
23 #G #L #T1 #T2 #d #H @(cpys_ind … H) -T2 /2 width=3 by cpy_trans_ge/
26 (* Advanced properties ******************************************************)
28 lemma cpys_strip_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 →
29 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 →
30 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T.
31 normalize /3 width=3 by cpy_conf_eq, TC_strip1/ qed-.
33 lemma cpys_strip_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 →
34 ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 →
35 (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
36 ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T.
37 normalize /3 width=3 by cpy_conf_neq, TC_strip1/ qed-.
39 lemma cpys_strap1_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 →
40 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 → d2 + e2 ≤ d1 →
41 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2.
42 normalize /3 width=3 by cpy_trans_down, TC_strap1/ qed.
44 lemma cpys_strap2_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶×[d1, e1] T0 →
45 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 →
46 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶×[d1, e1] T2.
47 normalize /3 width=3 by cpy_trans_down, TC_strap2/ qed-.
49 lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
50 ∀i. d ≤ i → i ≤ d + e →
51 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d, i - d] T & ⦃G, L⦄ ⊢ T ▶*×[i, d + e - i] T2.
52 #G #L #T1 #T2 #d #e #H #i #Hdi #Hide @(cpys_ind … H) -T2
53 [ /2 width=3 by ex2_intro/
54 | #T #T2 #_ #HT12 * #T3 #HT13 #HT3
55 elim (cpy_split_up … HT12 … Hdi Hide) -HT12 -Hide #T0 #HT0 #HT02
56 elim (cpys_strap1_down … HT3 … HT0 ?) -T /3 width=5 by cpys_strap1, ex2_intro/
57 >commutative_plus /2 width=1 by le_minus_to_plus_r/
61 lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
62 ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
63 d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
64 ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
66 #G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
67 elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
68 lapply (cpys_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1 by le_minus_to_plus_r/ ] -Hddt -Hdtde #HU1
69 lapply (cpys_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct
70 elim (cpys_inv_lift1_ge … HU2 … HLK … HTU1) -HU2 -HLK -HTU1 // <minus_plus_m_m /2 width=3 by ex2_intro/
73 (* Main properties **********************************************************)
75 theorem cpys_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶*×[d1, e1] T1 →
76 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 →
77 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶*×[d1, e1] T.
78 normalize /3 width=3 by cpy_conf_eq, TC_confluent2/ qed-.
80 theorem cpys_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶*×[d1, e1] T1 →
81 ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶*×[d2, e2] T2 →
82 (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
83 ∃∃T. ⦃G, L2⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L1⦄ ⊢ T2 ▶*×[d1, e1] T.
84 normalize /3 width=3 by cpy_conf_neq, TC_confluent2/ qed-.
86 theorem cpys_trans_eq: ∀G,L,T1,T,T2,d,e.
87 ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T → ⦃G, L⦄ ⊢ T ▶*×[d, e] T2 →
88 ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2.
89 normalize /2 width=3 by trans_TC/ qed-.
91 theorem cpys_trans_down: ∀G,L,T1,T0,d1,e1. ⦃G, L⦄ ⊢ T1 ▶*×[d1, e1] T0 →
92 ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶*×[d2, e2] T2 → d2 + e2 ≤ d1 →
93 ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[d2, e2] T & ⦃G, L⦄ ⊢ T ▶*×[d1, e1] T2.
94 normalize /3 width=3 by cpy_trans_down, TC_transitive2/ qed-.