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/rt_transition/cpg_drops.ma".
16 include "basic_2/rt_transition/cpm.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
20 (* Advanced properties ******************************************************)
22 (* Basic_1: includes: pr2_delta1 *)
23 (* Basic_2A1: includes: cpr_delta *)
24 lemma cpm_delta_drops: ∀n,h,G,L,K,V,V2,W2,i.
25 ⬇*[i] L ≡ K.ⓓV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
26 ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[n, h] W2.
27 #n #h #G #L #K #V #V2 #W2 #i #HLK *
28 /3 width=8 by cpg_delta_drops, ex2_intro/
31 lemma cpm_ell_drops: ∀n,h,G,L,K,V,V2,W2,i.
32 ⬇*[i] L ≡ K.ⓛV → ⦃G, K⦄ ⊢ V ➡[n, h] V2 →
33 ⬆*[⫯i] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡[⫯n, h] W2.
34 #n #h #G #L #K #V #V2 #W2 #i #HLK *
35 /3 width=8 by cpg_ell_drops, isrt_succ, ex2_intro/
38 (* Advanced inversion lemmas ************************************************)
40 lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 →
42 | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1
43 | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
44 ⬆*[⫯i] V2 ≡ T2 & I = LRef i
45 | ∃∃k,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[k, h] V2 &
46 ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯k.
47 #n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H *
48 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
49 /3 width=1 by or4_intro0, conj/
50 | #s #H1 #H2 #H3 destruct lapply (isrt_inv_01 … Hc) -Hc
51 /4 width=3 by or4_intro1, ex3_intro, sym_eq/ (**) (* sym_eq *)
52 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
53 /4 width=8 by ex4_4_intro, ex2_intro, or4_intro2/
54 | #cV #i #K #V1 #V2 #HLK #HV12 #HVT2 #H1 #H2 destruct
55 elim (isrt_inv_plus_SO_dx … Hc) -Hc
56 /4 width=10 by ex5_5_intro, ex2_intro, or4_intro3/
60 lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 →
62 | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 &
64 | ∃∃k,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[k, h] V2 &
65 ⬆*[⫯i] V2 ≡ T2 & n = ⫯k.
66 #n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H *
67 [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc
68 /3 width=1 by or3_intro0, conj/
69 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
70 /4 width=6 by ex3_3_intro, ex2_intro, or3_intro1/
71 | #cV #K #V1 #V2 #HLK #HV12 #HVT2 #H destruct
72 elim (isrt_inv_plus_SO_dx … Hc) -Hc
73 /4 width=8 by ex4_4_intro, ex2_intro, or3_intro2/
77 (* Properties with generic slicing for local environments *******************)
79 (* Basic_1: includes: pr0_lift pr2_lift *)
80 (* Basic_2A1: includes: cpr_lift *)
81 lemma cpm_lifts: ∀n,h,G. d_liftable2 (cpm n h G).
82 #n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
83 elim (cpg_lifts … HT12 … HLK … HTU1) -K -T1
84 /3 width=5 by ex2_intro/
87 (* Inversion lemmas with generic slicing for local environments *************)
89 (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *)
90 (* Basic_2A1: includes: cpr_inv_lift1 *)
91 lemma cpm_inv_lifts1: ∀n,h,G. d_deliftable2_sn (cpm n h G).
92 #n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
93 elim (cpg_inv_lifts1 … HU12 … HLK … HTU1) -L -U1
94 /3 width=5 by ex2_intro/