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/notation/relations/predtysn_4.ma".
16 include "static_2/static/rex.ma".
17 include "basic_2/rt_transition/cpx_ext.ma".
19 (* EXTENDED PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS **********)
21 definition rpx (G): relation3 term lenv lenv ≝
25 "extended parallel rt-transition on referred entries (local environment)"
26 'PRedTySn T G L1 L2 = (rpx G T L1 L2).
28 (* Basic properties ***********************************************************)
31 ∀I. ❨G,⋆❩ ⊢ ⬈[⓪[I]] ⋆.
32 /2 width=1 by rex_atom/ qed.
36 ❨G,L1❩ ⊢ ⬈[⋆s] L2 → ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[⋆s] L2.ⓘ[I2].
37 /2 width=1 by rex_sort/ qed.
41 ❨G,L1❩ ⊢ ⬈[V1] L2 → ❨G,L1❩ ⊢ V1 ⬈ V2 → ❨G,L1.ⓑ[I]V1❩ ⊢ ⬈[#0] L2.ⓑ[I]V2.
42 /2 width=1 by rex_pair/ qed.
46 ❨G,L1❩ ⊢ ⬈[#i] L2 → ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[#↑i] L2.ⓘ[I2].
47 /2 width=1 by rex_lref/ qed.
51 ❨G,L1❩ ⊢ ⬈[§l] L2 → ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[§l] L2.ⓘ[I2].
52 /2 width=1 by rex_gref/ qed.
54 lemma rpx_bind_repl_dx (G):
55 ∀I,I1,L1,L2,T. ❨G,L1.ⓘ[I]❩ ⊢ ⬈[T] L2.ⓘ[I1] →
56 ∀I2. ❨G,L1❩ ⊢ I ⬈ I2 → ❨G,L1.ⓘ[I]❩ ⊢ ⬈[T] L2.ⓘ[I2].
57 /2 width=2 by rex_bind_repl_dx/ qed-.
59 (* Basic inversion lemmas ***************************************************)
61 lemma rpx_inv_atom_sn (G):
62 ∀Y2,T. ❨G,⋆❩ ⊢ ⬈[T] Y2 → Y2 = ⋆.
63 /2 width=3 by rex_inv_atom_sn/ qed-.
65 lemma rpx_inv_atom_dx (G):
66 ∀Y1,T. ❨G,Y1❩ ⊢ ⬈[T] ⋆ → Y1 = ⋆.
67 /2 width=3 by rex_inv_atom_dx/ qed-.
69 lemma rpx_inv_sort (G):
70 ∀Y1,Y2,s. ❨G,Y1❩ ⊢ ⬈[⋆s] Y2 →
72 | ∃∃I1,I2,L1,L2. ❨G,L1❩ ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
73 /2 width=1 by rex_inv_sort/ qed-.
75 lemma rpx_inv_lref (G):
76 ∀Y1,Y2,i. ❨G,Y1❩ ⊢ ⬈[#↑i] Y2 →
78 | ∃∃I1,I2,L1,L2. ❨G,L1❩ ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
79 /2 width=1 by rex_inv_lref/ qed-.
81 lemma rpx_inv_gref (G):
82 ∀Y1,Y2,l. ❨G,Y1❩ ⊢ ⬈[§l] Y2 →
84 | ∃∃I1,I2,L1,L2. ❨G,L1❩ ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1] & Y2 = L2.ⓘ[I2].
85 /2 width=1 by rex_inv_gref/ qed-.
87 lemma rpx_inv_bind (G):
88 ∀p,I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓑ[p,I]V.T] L2 →
89 ∧∧ ❨G,L1❩ ⊢ ⬈[V] L2 & ❨G,L1.ⓑ[I]V❩ ⊢ ⬈[T] L2.ⓑ[I]V.
90 /2 width=2 by rex_inv_bind/ qed-.
92 lemma rpx_inv_flat (G):
93 ∀I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓕ[I]V.T] L2 →
94 ∧∧ ❨G,L1❩ ⊢ ⬈[V] L2 & ❨G,L1❩ ⊢ ⬈[T] L2.
95 /2 width=2 by rex_inv_flat/ qed-.
97 (* Advanced inversion lemmas ************************************************)
99 lemma rpx_inv_sort_bind_sn (G):
100 ∀I1,Y2,L1,s. ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[⋆s] Y2 →
101 ∃∃I2,L2. ❨G,L1❩ ⊢ ⬈[⋆s] L2 & Y2 = L2.ⓘ[I2].
102 /2 width=2 by rex_inv_sort_bind_sn/ qed-.
104 lemma rpx_inv_sort_bind_dx (G):
105 ∀I2,Y1,L2,s. ❨G,Y1❩ ⊢ ⬈[⋆s] L2.ⓘ[I2] →
106 ∃∃I1,L1. ❨G,L1❩ ⊢ ⬈[⋆s] L2 & Y1 = L1.ⓘ[I1].
107 /2 width=2 by rex_inv_sort_bind_dx/ qed-.
109 lemma rpx_inv_zero_pair_sn (G):
110 ∀I,Y2,L1,V1. ❨G,L1.ⓑ[I]V1❩ ⊢ ⬈[#0] Y2 →
111 ∃∃L2,V2. ❨G,L1❩ ⊢ ⬈[V1] L2 & ❨G,L1❩ ⊢ V1 ⬈ V2 & Y2 = L2.ⓑ[I]V2.
112 /2 width=1 by rex_inv_zero_pair_sn/ qed-.
114 lemma rpx_inv_zero_pair_dx (G):
115 ∀I,Y1,L2,V2. ❨G,Y1❩ ⊢ ⬈[#0] L2.ⓑ[I]V2 →
116 ∃∃L1,V1. ❨G,L1❩ ⊢ ⬈[V1] L2 & ❨G,L1❩ ⊢ V1 ⬈ V2 & Y1 = L1.ⓑ[I]V1.
117 /2 width=1 by rex_inv_zero_pair_dx/ qed-.
119 lemma rpx_inv_lref_bind_sn (G):
120 ∀I1,Y2,L1,i. ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[#↑i] Y2 →
121 ∃∃I2,L2. ❨G,L1❩ ⊢ ⬈[#i] L2 & Y2 = L2.ⓘ[I2].
122 /2 width=2 by rex_inv_lref_bind_sn/ qed-.
124 lemma rpx_inv_lref_bind_dx (G):
125 ∀I2,Y1,L2,i. ❨G,Y1❩ ⊢ ⬈[#↑i] L2.ⓘ[I2] →
126 ∃∃I1,L1. ❨G,L1❩ ⊢ ⬈[#i] L2 & Y1 = L1.ⓘ[I1].
127 /2 width=2 by rex_inv_lref_bind_dx/ qed-.
129 lemma rpx_inv_gref_bind_sn (G):
130 ∀I1,Y2,L1,l. ❨G,L1.ⓘ[I1]❩ ⊢ ⬈[§l] Y2 →
131 ∃∃I2,L2. ❨G,L1❩ ⊢ ⬈[§l] L2 & Y2 = L2.ⓘ[I2].
132 /2 width=2 by rex_inv_gref_bind_sn/ qed-.
134 lemma rpx_inv_gref_bind_dx (G):
135 ∀I2,Y1,L2,l. ❨G,Y1❩ ⊢ ⬈[§l] L2.ⓘ[I2] →
136 ∃∃I1,L1. ❨G,L1❩ ⊢ ⬈[§l] L2 & Y1 = L1.ⓘ[I1].
137 /2 width=2 by rex_inv_gref_bind_dx/ qed-.
139 (* Basic forward lemmas *****************************************************)
141 lemma rpx_fwd_pair_sn (G):
142 ∀I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[②[I]V.T] L2 → ❨G,L1❩ ⊢ ⬈[V] L2.
143 /2 width=3 by rex_fwd_pair_sn/ qed-.
145 lemma rpx_fwd_bind_dx (G):
146 ∀p,I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓑ[p,I]V.T] L2 → ❨G,L1.ⓑ[I]V❩ ⊢ ⬈[T] L2.ⓑ[I]V.
147 /2 width=2 by rex_fwd_bind_dx/ qed-.
149 lemma rpx_fwd_flat_dx (G):
150 ∀I,L1,L2,V,T. ❨G,L1❩ ⊢ ⬈[ⓕ[I]V.T] L2 → ❨G,L1❩ ⊢ ⬈[T] L2.
151 /2 width=3 by rex_fwd_flat_dx/ qed-.