]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_fsle.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / rpx_fsle.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "static_2/static/fsle_drops.ma".
16 include "static_2/static/rex_fsle.ma".
17 include "basic_2/rt_transition/rpx_length.ma".
18 include "basic_2/rt_transition/rpx_drops.ma".
19 include "basic_2/rt_transition/rpx_fqup.ma".
20
21 (* UNBOUND PARALLEL RT-TRANSITION FOR REFERRED LOCAL ENVIRONMENTS ***********)
22
23 (* Forward lemmas with free variables inclusion for restricted closures *****)
24
25 (* Note: "❪L2, T1❫ ⊆ ❪L2, T0❫" does not hold *)
26 (* Note: Take L0 = K0.ⓓ(ⓝW.V), L2 = K0.ⓓW, T0 = #0, T1 = ⇧[1]V *)
27 (* Note: This invalidates rpxs_cpx_conf: "∀G. s_r_confluent1 … (cpx G) (rpxs G)" *)
28 lemma rpx_cpx_conf_fsge (G):
29       ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
30       ∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T0❫.
31 #G0 #L0 #T0 @(fqup_wf_ind_eq (Ⓣ) … G0 L0 T0) -G0 -L0 -T0
32 #G #L #T #IH #G0 #L0 * *
33 [ #s0 #HG #HL #HT #X #HX #Y #HY destruct -IH
34   elim (cpx_inv_sort1 … HX) -HX #s1 #H destruct
35   lapply (rpx_fwd_length … HY) -HY #H0
36   /2 width=1 by fsle_sort_bi/
37 | * [| #i ] #HG #HL #HT #X #HX #Y #HY destruct
38   [ elim (cpx_inv_zero1 … HX) -HX
39     [ #H destruct
40       elim (rpx_inv_zero_length … HY) -HY *
41       [ #H1 #H2 destruct -IH //
42       | #I #K0 #K2 #V0 #V2 #HK02 #HV02 #H1 #H2 destruct
43         lapply (rpx_fwd_length … HK02) #H0
44         /4 width=4 by fsle_pair_bi, fqu_fqup, fqu_lref_O/
45       | #I #K0 #K2 #HK02 #H1 #H2 destruct -IH
46         /2 width=1 by fsle_unit_bi/
47       ]
48     | * #I0 #K0 #V0 #V1 #HV01 #HV1X #H destruct
49       elim (rpx_inv_zero_pair_sn … HY) -HY #K2 #V2 #HK02 #HV02 #H destruct
50       lapply (rpx_fwd_length … HK02) #H0
51       /4 width=4 by fsle_lifts_SO_sn, fqu_fqup, fqu_lref_O/
52     ]
53   | elim (cpx_inv_lref1 … HX) -HX
54     [ #H destruct
55       elim (rpx_inv_lref … HY) -HY *
56       [ #H0 #H1 destruct //
57       | #I0 #I2 #K0 #K2 #HK02 #H1 #H2 destruct
58         lapply (rpx_fwd_length … HK02) #H0
59         /4 width=5 by fsle_lifts_SO, fqu_fqup/
60       ]
61     | * #I0 #K0 #V1 #HV1 #HV1X #H0 destruct
62       elim (rpx_inv_lref_bind_sn … HY) -HY #I2 #K2 #HK02 #H destruct
63       lapply (rpx_fwd_length … HK02) #H0
64       /4 width=5 by fsle_lifts_SO, fqu_fqup/
65     ]
66   ]
67 | #l #HG #HL #HT #X #HX #Y #HY destruct -IH
68   >(cpx_inv_gref1 … HX) -X
69   lapply (rpx_fwd_length … HY) -HY #H0
70   /2 width=1 by fsle_gref_bi/
71 | #p #I #V0 #T0 #HG #HL #HT #X #HX #Y #HY destruct
72   elim (rpx_inv_bind … V0 ? HY) -HY #HV0 #HT0
73   elim (cpx_inv_bind1 … HX) -HX *
74   [ #V1 #T1 #HV01 #HT01 #H destruct
75     lapply (rpx_fwd_length … HV0) #H0
76     /4 width=6 by fsle_bind_eq, fsle_fwd_pair_sn/
77   | #T #H2T0 #HTX #H1 #H2 destruct
78     lapply (rpx_inv_lifts_bi … HT0 (Ⓣ) … H2T0) -HT0 [6:|*: /3 width=2 by drops_refl, drops_drop/ ] #HT
79     lapply (rpx_fwd_length … HV0) #H0
80     /5 width=6 by fsle_bind_dx_dx, fsle_lifts_dx, fqup_zeta/
81   ]
82 | #I #V0 #X0 #HG #HL #HT #X #HX #Y #HY destruct
83   elim (rex_inv_flat … HY) -HY #HV0 #HX0
84   elim (cpx_inv_flat1 … HX) -HX *
85   [ #V1 #T1 #HV01 #HT01 #H destruct
86     /3 width=4 by fsle_flat/
87   | #HX #H destruct
88     /4 width=4 by fsle_flat_dx_dx/
89   | #HX #H destruct
90     /4 width=4 by fsle_flat_dx_sn/
91   | #p #V1 #W0 #W1 #T0 #T1 #HV01 #HW01 #HT01 #H1 #H2 #H3 destruct
92     elim (rpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
93     lapply (rpx_fwd_length … HV0) #H0
94     lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
95     lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
96     lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
97     lapply (fsle_fwd_pair_sn … HT) -HT #HT
98     @fsle_bind_sn_ge //
99     [ /4 width=1 by fsle_flat_sn, fsle_flat_dx_dx, fsle_flat_dx_sn, fsle_bind_dx_sn/
100     | /3 width=1 by fsle_flat_dx_dx, fsle_shift/
101     ]
102   | #p #V1 #X1 #W0 #W1 #T0 #T1 #HV01 #HVX1 #HW01 #HT01 #H1 #H2 #H3 destruct
103     elim (rpx_inv_bind … W0 ? HX0) -HX0 #HW0 #HT0
104     lapply (rpx_fwd_length … HV0) #H0
105     lapply (IH … HV01 … HV0) -HV01 -HV0 // #HV
106     lapply (IH … HW01 … HW0) -HW01 -HW0 // #HW
107     lapply (IH … HT01 … HT0) -HT01 -HT0 -IH // #HT
108     lapply (fsle_fwd_pair_sn … HT) -HT #HT
109     @fsle_bind_sn_ge //
110     [ /3 width=1 by fsle_flat_dx_dx, fsle_bind_dx_sn/
111     | /4 width=3 by fsle_flat_sn, fsle_flat_dx_sn, fsle_flat_dx_dx, fsle_shift, fsle_lifts_sn/
112     ]
113   ]
114 ]
115 qed-.
116
117 lemma rpx_fsge_comp (G): rex_fsge_compatible (cpx G).
118 /2 width=4 by rpx_cpx_conf_fsge/ qed-.
119
120 (**) (* this section concerns cpx *)
121 (* Properties with generic extension on referred entries ********************)
122
123 (* Basic_2A1: uses: cpx_frees_trans *)
124 lemma cpx_fsge_comp (G): R_fsge_compatible (cpx G).
125 /2 width=4 by rpx_cpx_conf_fsge/ qed-.
126
127 (* Note: lemma 1000 *)
128 (* Basic_2A1: uses: cpx_llpx_sn_conf *)
129 lemma cpx_rex_conf_sn (R) (G): s_r_confluent1 … (cpx G) (rex R).
130 /3 width=3 by fsge_rex_trans, cpx_fsge_comp/ qed-.
131
132 (* Advanced properties ******************************************************)
133
134 lemma rpx_cpx_conf_sn (G): s_r_confluent1 … (cpx G) (rpx G).
135 /2 width=5 by cpx_rex_conf_sn/ qed-.
136
137 lemma rpx_cpx_conf_fsge_dx (G):
138       ∀L0,T0,T1. ❪G,L0❫ ⊢ T0 ⬈ T1 →
139       ∀L2. ❪G,L0❫ ⊢⬈[T0] L2 → ❪L2,T1❫ ⊆ ❪L0,T1❫.
140 /3 width=5 by rpx_cpx_conf_sn, rpx_fsge_comp/ qed-.