]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / cpxs_drops.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/relocation/drops_ctc.ma".
16 include "basic_2/rt_transition/cpx_drops.ma".
17 include "basic_2/rt_computation/cpxs.ma".
18
19 (* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
20
21 (* Advanced properties ******************************************************)
22
23 lemma cpxs_delta (G) (K):
24       ∀I,V1,V2. ❪G,K❫ ⊢ V1 ⬈* V2 →
25       ∀W2. ⇧[1] V2 ≘ W2 → ❪G,K.ⓑ[I]V1❫ ⊢ #0 ⬈* W2.
26 #G #K #I #V1 #V2 #H @(cpxs_ind … H) -V2
27 [ /3 width=3 by cpx_cpxs, cpx_delta/
28 | #V #V2 #_ #HV2 #IH #W2 #HVW2
29   elim (lifts_total V (𝐔❨1❩))
30   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
31 ]
32 qed.
33
34 lemma cpxs_lref (G) (K):
35       ∀I,T,i. ❪G,K❫ ⊢ #i ⬈* T →
36       ∀U. ⇧[1] T ≘ U → ❪G,K.ⓘ[I]❫ ⊢ #↑i ⬈* U.
37 #G #K #I #T #i #H @(cpxs_ind … H) -T
38 [ /3 width=3 by cpx_cpxs, cpx_lref/
39 | #T0 #T #_ #HT2 #IH #U #HTU
40   elim (lifts_total T0 (𝐔❨1❩))
41   /5 width=11 by cpxs_strap1, cpx_lifts_bi, drops_refl, drops_drop/
42 ]
43 qed.
44
45 (* Basic_2A1: was: cpxs_delta *)
46 lemma cpxs_delta_drops (G) (L):
47       ∀I,K,V1,V2,i. ⇩[i] L ≘ K.ⓑ[I]V1 → ❪G,K❫ ⊢ V1 ⬈* V2 →
48       ∀W2. ⇧[↑i] V2 ≘ W2 → ❪G,L❫ ⊢ #i ⬈* W2.
49 #G #L #I #K #V1 #V2 #i #HLK #H @(cpxs_ind … H) -V2
50 [ /3 width=7 by cpx_cpxs, cpx_delta_drops/
51 | #V #V2 #_ #HV2 #IH #W2 #HVW2
52   elim (lifts_total V (𝐔❨↑i❩))
53   /4 width=11 by cpxs_strap1, cpx_lifts_bi, drops_isuni_fwd_drop2/
54 ]
55 qed.
56
57 (* Advanced inversion lemmas ************************************************)
58
59 lemma cpxs_inv_zero1 (G) (L):
60       ∀T2. ❪G,L❫ ⊢ #0 ⬈* T2 →
61       ∨∨ T2 = #0
62        | ∃∃I,K,V1,V2. ❪G,K❫ ⊢ V1 ⬈* V2 & ⇧[1] V2 ≘ T2 & L = K.ⓑ[I]V1.
63 #G #L #T2 #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
64 #T #T2 #_ #HT2 *
65 [ #H destruct
66   elim (cpx_inv_zero1 … HT2) -HT2 /2 width=1 by or_introl/
67   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
68 | * #I #K #V1 #T1 #HVT1 #HT1 #H destruct
69   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
70   /4 width=7 by cpxs_strap1, drops_refl, drops_drop, ex3_4_intro, or_intror/
71 ]
72 qed-.
73
74 lemma cpxs_inv_lref1 (G) (L):
75       ∀T2,i. ❪G,L❫ ⊢ #↑i ⬈* T2 →
76       ∨∨ T2 = #(↑i)
77        | ∃∃I,K,T. ❪G,K❫ ⊢ #i ⬈* T & ⇧[1] T ≘ T2 & L = K.ⓘ[I].
78 #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
79 #T #T2 #_ #HT2 *
80 [ #H destruct
81   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
82   * /4 width=6 by cpx_cpxs, ex3_3_intro, or_intror/
83 | * #I #K #T1 #Hi #HT1 #H destruct
84   elim (cpx_inv_lifts_sn … HT2 (Ⓣ) … K … HT1) -T
85   /4 width=6 by cpxs_strap1, drops_refl, drops_drop, ex3_3_intro, or_intror/
86 ]
87 qed-.
88
89 (* Basic_2A1: was: cpxs_inv_lref1 *)
90 lemma cpxs_inv_lref1_drops (G) (L):
91       ∀T2,i. ❪G,L❫ ⊢ #i ⬈* T2 →
92       ∨∨ T2 = #i
93        | ∃∃I,K,V1,T1. ⇩[i] L ≘ K.ⓑ[I]V1 & ❪G,K❫ ⊢ V1 ⬈* T1 & ⇧[↑i] T1 ≘ T2.
94 #G #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1 by or_introl/
95 #T #T2 #_ #HT2 *
96 [ #H destruct
97   elim (cpx_inv_lref1_drops … HT2) -HT2 /2 width=1 by or_introl/
98   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
99 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
100   lapply (drops_isuni_fwd_drop2 … HLK) // #H0LK
101   elim (cpx_inv_lifts_sn … HT2 … H0LK … HT1) -H0LK -T
102   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
103 ]
104 qed-.
105
106 (* Properties with generic relocation ***************************************)
107
108 (* Basic_2A1: includes: cpxs_lift *)
109 lemma cpxs_lifts_sn (G):
110       d_liftable2_sn … lifts (cpxs G).
111 /3 width=10 by cpx_lifts_sn, cpxs_strap1, d2_liftable_sn_CTC/ qed-.
112
113 lemma cpxs_lifts_bi (G):
114       d_liftable2_bi … lifts (cpxs G).
115 /3 width=12 by cpxs_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
116
117 (* Inversion lemmas with generic relocation *********************************)
118
119 (* Basic_2A1: includes: cpxs_inv_lift1 *)
120 lemma cpxs_inv_lifts_sn (G):
121       d_deliftable2_sn … lifts (cpxs G).
122 /3 width=6 by d2_deliftable_sn_CTC, cpx_inv_lifts_sn/ qed-.
123
124 lemma cpxs_inv_lifts_bi (G):
125       d_deliftable2_bi … lifts (cpxs G).
126 /3 width=12 by cpxs_inv_lifts_sn, d_deliftable2_sn_bi, lifts_inj/ qed-.