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 "ground_2/steps/rtc_ist_shift.ma".
16 include "ground_2/steps/rtc_ist_plus.ma".
17 include "ground_2/steps/rtc_ist_max.ma".
18 include "basic_2/notation/relations/pty_6.ma".
19 include "basic_2/rt_transition/cpg.ma".
21 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
23 definition cpt (h) (G) (L) (n): relation2 term term ≝
24 λT1,T2. ∃∃c. 𝐓⦃n,c⦄ & ⦃G,L⦄ ⊢ T1 ⬈[eq …,c,h] T2.
27 "t-bound context-sensitive parallel t-transition (term)"
28 'PTy h n G L T1 T2 = (cpt h G L n T1 T2).
30 (* Basic properties *********************************************************)
32 lemma cpt_ess (h) (G) (L):
33 ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
34 /2 width=3 by cpg_ess, ex2_intro/ qed.
36 lemma cpt_delta (h) (n) (G) (K):
37 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
38 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆[h,n] W2.
40 /3 width=5 by cpg_delta, ex2_intro/
43 lemma cpt_ell (h) (n) (G) (K):
44 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
45 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆[h,↑n] W2.
47 /3 width=5 by cpg_ell, ex2_intro, ist_succ/
50 lemma cpt_lref (h) (n) (G) (K):
51 ∀T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T → ∀U. ⇧*[1] T ≘ U →
52 ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆[h,n] U.
54 /3 width=5 by cpg_lref, ex2_intro/
57 lemma cpt_bind (h) (n) (G) (L):
58 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 →
59 ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] ⓑ{p,I}V2.T2.
60 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #I #T1 #T2 *
61 /3 width=5 by cpg_bind, ist_max_O1, ex2_intro/
64 lemma cpt_appl (h) (n) (G) (L):
65 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
66 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] ⓐV2.T2.
67 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #T1 #T2 *
68 /3 width=5 by ist_max_O1, cpg_appl, ex2_intro/
71 lemma cpt_cast (h) (n) (G) (L):
72 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 →
73 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆[h,n] ⓝU2.T2.
74 #h #n #G #L #U1 #U2 * #cU #HcU #HU12 #T1 #T2 *
75 /3 width=6 by cpg_cast, ex2_intro/
78 lemma cpt_ee (h) (n) (G) (L):
79 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 → ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆[h,↑n] U2.
81 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
84 (* Basic properties *********************************************************)
86 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
87 /3 width=3 by cpg_refl, ex2_intro/ qed.
89 (* Basic inversion lemmas ***************************************************)
91 lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
92 ∀X2. ⦃G,L⦄ ⊢ ⓪{J} ⬆[h,n] X2 →
93 ∨∨ ∧∧ X2 = ⓪{J} & n = 0
94 | ∃∃s. X2 = ⋆(⫯[h]s) & J = Sort s & n =1
95 | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1 & J = LRef 0
96 | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & J = LRef 0 & n = ↑m
97 | ∃∃I,K,T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I} & J = LRef (↑i).
98 #h #n #J #G #L #X2 * #c #Hc #H
99 elim (cpg_inv_atom1 … H) -H *
100 [ #H1 #H2 destruct /3 width=1 by or5_intro0, conj/
101 | #s #H1 #H2 #H3 destruct /3 width=3 by or5_intro1, ex3_intro/
102 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
103 /4 width=6 by or5_intro2, ex4_3_intro, ex2_intro/
104 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct
105 elim (ist_inv_plus_SO_dx … H3) -H3 [| // ] #m #Hc #H destruct
106 /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/
107 | #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct
108 /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/
112 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
113 ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
114 ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2
116 #h #n #p #I #G #L #V1 #T1 #X2 * #c #Hc #H
117 elim (cpg_inv_bind1 … H) -H *
118 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
119 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
120 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
121 /3 width=5 by ex3_2_intro, ex2_intro/
122 | #cT #T2 #_ #_ #_ #_ #H destruct
123 elim (ist_inv_plus_10_dx … H)
127 lemma cpt_inv_appl_sn (h) (n) (G) (L) (V1) (T1):
128 ∀X2. ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] X2 →
129 ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓐV2.T2.
130 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_appl1 … H) -H *
131 [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct
132 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
133 elim (ist_inv_shift … HcV) -HcV #HcV #H destruct
134 /3 width=5 by ex3_2_intro, ex2_intro/
135 | #cV #cW #cU #p #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #H destruct
136 elim (ist_inv_plus_10_dx … H)
137 | #cV #cW #cU #p #V #V2 #W1 #W2 #U1 #U2 #_ #_ #_ #_ #_ #_ #H destruct
138 elim (ist_inv_plus_10_dx … H)
142 lemma cpt_inv_cast_sn (h) (n) (G) (L) (V1) (T1):
143 ∀X2. ⦃G,L⦄ ⊢ ⓝV1.T1 ⬆[h,n] X2 →
144 ∨∨ ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,n] V2 & ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 & X2 = ⓝV2.T2
145 | ∃∃m. ⦃G,L⦄ ⊢ V1 ⬆[h,m] X2 & n = ↑m.
146 #h #n #G #L #V1 #T1 #X2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
147 [ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
148 elim (ist_inv_max … H2) -H2 #nV #nT #HcV #HcT #H destruct
150 /4 width=5 by or_introl, ex3_2_intro, ex2_intro/
152 elim (ist_inv_plus_10_dx … H)
153 | #cV #H12 #H destruct
154 elim (ist_inv_plus_SO_dx … H) -H [| // ] #m #Hm #H destruct
155 /4 width=3 by ex2_intro, or_intror/