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/lib/ltc.ma".
16 include "basic_2/notation/relations/ptystar_6.ma".
17 include "basic_2/rt_transition/cpt.ma".
19 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
21 definition cpts (h) (G) (L): relation3 nat term term ≝
22 ltc … plus … (cpt h G L).
25 "t-bound context-sensitive parallel t-computarion (term)"
26 'PTyStar h n G L T1 T2 = (cpts h G L n T1 T2).
28 (* Basic eliminators ********************************************************)
30 lemma cpts_ind_sn (h) (G) (L) (T2) (Q:relation2 …):
32 (∀n1,n2,T1,T. ❨G,L❩ ⊢ T1 ⬆[h,n1] T → ❨G,L❩ ⊢ T ⬆*[h,n2] T2 → Q n2 T → Q (n1+n2) T1) →
33 ∀n,T1. ❨G,L❩ ⊢ T1 ⬆*[h,n] T2 → Q n T1.
34 #h #G #L #T2 #Q @ltc_ind_sn_refl //
37 lemma cpts_ind_dx (h) (G) (L) (T1) (Q:relation2 …):
39 (∀n1,n2,T,T2. ❨G,L❩ ⊢ T1 ⬆*[h,n1] T → Q n1 T → ❨G,L❩ ⊢ T ⬆[h,n2] T2 → Q (n1+n2) T2) →
40 ∀n,T2. ❨G,L❩ ⊢ T1 ⬆*[h,n] T2 → Q n T2.
41 #h #G #L #T1 #Q @ltc_ind_dx_refl //
44 (* Basic properties *********************************************************)
46 lemma cpt_cpts (h) (G) (L):
47 ∀n,T1,T2. ❨G,L❩ ⊢ T1 ⬆[h,n] T2 → ❨G,L❩ ⊢ T1 ⬆*[h,n] T2.
48 /2 width=1 by ltc_rc/ qed.
50 lemma cpts_step_sn (h) (G) (L):
51 ∀n1,T1,T. ❨G,L❩ ⊢ T1 ⬆[h,n1] T →
52 ∀n2,T2. ❨G,L❩ ⊢ T ⬆*[h,n2] T2 → ❨G,L❩ ⊢ T1 ⬆*[h,n1+n2] T2.
53 /2 width=3 by ltc_sn/ qed-.
55 lemma cpts_step_dx (h) (G) (L):
56 ∀n1,T1,T. ❨G,L❩ ⊢ T1 ⬆*[h,n1] T →
57 ∀n2,T2. ❨G,L❩ ⊢ T ⬆[h,n2] T2 → ❨G,L❩ ⊢ T1 ⬆*[h,n1+n2] T2.
58 /2 width=3 by ltc_dx/ qed-.
60 lemma cpts_bind_dx (h) (n) (G) (L):
61 ∀V1,V2. ❨G,L❩ ⊢ V1 ⬆[h,0] V2 →
62 ∀I,T1,T2. ❨G,L.ⓑ[I]V1❩ ⊢ T1 ⬆*[h,n] T2 →
63 ∀p. ❨G,L❩ ⊢ ⓑ[p,I]V1.T1 ⬆*[h,n] ⓑ[p,I]V2.T2.
64 #h #n #G #L #V1 #V2 #HV12 #I #T1 #T2 #H #a @(cpts_ind_sn … H) -T1
65 /3 width=3 by cpts_step_sn, cpt_cpts, cpt_bind/ qed.
67 lemma cpts_appl_dx (h) (n) (G) (L):
68 ∀V1,V2. ❨G,L❩ ⊢ V1 ⬆[h,0] V2 →
69 ∀T1,T2. ❨G,L❩ ⊢ T1 ⬆*[h,n] T2 → ❨G,L❩ ⊢ ⓐV1.T1 ⬆*[h,n] ⓐV2.T2.
70 #h #n #G #L #V1 #V2 #HV12 #T1 #T2 #H @(cpts_ind_sn … H) -T1
71 /3 width=3 by cpts_step_sn, cpt_cpts, cpt_appl/
74 lemma cpts_ee (h) (n) (G) (L):
75 ∀U1,U2. ❨G,L❩ ⊢ U1 ⬆*[h,n] U2 →
76 ∀T. ❨G,L❩ ⊢ ⓝU1.T ⬆*[h,↑n] U2.
77 #h #n #G #L #U1 #U2 #H @(cpts_ind_sn … H) -U1 -n
78 [ /3 width=1 by cpt_cpts, cpt_ee/
79 | #n1 #n2 #U1 #U #HU1 #HU2 #_ #T >plus_S1
80 /3 width=3 by cpts_step_sn, cpt_ee/
84 lemma cpts_refl (h) (G) (L): reflexive … (cpts h G L 0).
85 /2 width=1 by cpt_cpts/ qed.
87 (* Advanced properties ******************************************************)
89 lemma cpts_sort (h) (G) (L) (n):
90 ∀s. ❨G,L❩ ⊢ ⋆s ⬆*[h,n] ⋆((next h)^n s).
91 #h #G #L #n elim n -n [ // ]
93 /3 width=3 by cpts_step_dx, cpt_sort/
96 (* Basic inversion lemmas ***************************************************)
98 lemma cpts_inv_sort_sn (h) (n) (G) (L) (s):
99 ∀X2. ❨G,L❩ ⊢ ⋆s ⬆*[h,n] X2 → X2 = ⋆(((next h)^n) s).
100 #h #n #G #L #s #X2 #H @(cpts_ind_dx … H) -X2 //
101 #n1 #n2 #X #X2 #_ #IH #HX2 destruct
102 elim (cpt_inv_sort_sn … HX2) -HX2 #H #_ destruct //
105 lemma cpts_inv_lref_sn_ctop (h) (n) (G) (i):
106 ∀X2. ❨G,⋆❩ ⊢ #i ⬆*[h,n] X2 → ∧∧ X2 = #i & n = 0.
107 #h #n #G #i #X2 #H @(cpts_ind_dx … H) -X2
108 [ /2 width=1 by conj/
109 | #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
110 elim (cpt_inv_lref_sn_ctop … HX2) -HX2 #H1 #H2 destruct
115 lemma cpts_inv_zero_sn_unit (h) (n) (I) (K) (G):
116 ∀X2. ❨G,K.ⓤ[I]❩ ⊢ #0 ⬆*[h,n] X2 → ∧∧ X2 = #0 & n = 0.
117 #h #n #I #G #K #X2 #H @(cpts_ind_dx … H) -X2
118 [ /2 width=1 by conj/
119 | #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
120 elim (cpt_inv_zero_sn_unit … HX2) -HX2 #H1 #H2 destruct
125 lemma cpts_inv_gref_sn (h) (n) (G) (L) (l):
126 ∀X2. ❨G,L❩ ⊢ §l ⬆*[h,n] X2 → ∧∧ X2 = §l & n = 0.
127 #h #n #G #L #l #X2 #H @(cpts_ind_dx … H) -X2
128 [ /2 width=1 by conj/
129 | #n1 #n2 #X #X2 #_ * #HX #Hn1 #HX2 destruct
130 elim (cpt_inv_gref_sn … HX2) -HX2 #H1 #H2 destruct
135 lemma cpts_inv_cast_sn (h) (n) (G) (L) (U1) (T1):
136 ∀X2. ❨G,L❩ ⊢ ⓝU1.T1 ⬆*[h,n] X2 →
137 ∨∨ ∃∃U2,T2. ❨G,L❩ ⊢ U1 ⬆*[h,n] U2 & ❨G,L❩ ⊢ T1 ⬆*[h,n] T2 & X2 = ⓝU2.T2
138 | ∃∃m. ❨G,L❩ ⊢ U1 ⬆*[h,m] X2 & n = ↑m.
139 #h #n #G #L #U1 #T1 #X2 #H @(cpts_ind_dx … H) -n -X2
140 [ /3 width=5 by or_introl, ex3_2_intro/
141 | #n1 #n2 #X #X2 #_ * *
142 [ #U #T #HU1 #HT1 #H #HX2 destruct
143 elim (cpt_inv_cast_sn … HX2) -HX2 *
144 [ #U2 #T2 #HU2 #HT2 #H destruct
145 /4 width=5 by cpts_step_dx, ex3_2_intro, or_introl/
146 | #m #HX2 #H destruct <plus_n_Sm
147 /4 width=3 by cpts_step_dx, ex2_intro, or_intror/
149 | #m #HX #H #HX2 destruct
150 /4 width=3 by cpts_step_dx, ex2_intro, or_intror/