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_computation/cpms_drops.ma".
16 include "basic_2/dynamic/cnv.ma".
18 (* CONTEXT_SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
20 (* Advanced dproperties *****************************************************)
22 (* Basic_2A1: uses: snv_lref *)
23 lemma cnv_lref_drops (a) (h) (G): ∀I,K,V,i,L. ⦃G, K⦄ ⊢ V ![a, h] →
24 ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, L⦄ ⊢ #i ![a, h].
25 #a #h #G #I #K #V #i elim i -i
27 lapply (drops_fwd_isid … H ?) -H // #H destruct
28 /2 width=1 by cnv_zero/
30 elim (drops_inv_succ … H) -H #J0 #K0 #HK0 #H destruct
31 /3 width=1 by cnv_lref/
35 (* Advanced inversion lemmas ************************************************)
37 (* Basic_2A1: uses: snv_inv_lref *)
38 lemma cnv_inv_lref_drops (a) (h) (G):
39 ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] →
40 ∃∃I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ![a, h].
43 elim (cnv_inv_zero … H) -H #I #K #V #HV #H destruct
44 /3 width=5 by drops_refl, ex2_3_intro/
46 elim (cnv_inv_lref … H) -H #I #L #HL #H destruct
47 elim (IH … HL) -IH -HL #J #K #V #HLK #HV
48 /3 width=5 by drops_drop, ex2_3_intro/
52 (* Advanced forward lemmas **************************************************)
54 lemma cnv_lref_fwd_drops (a) (h) (G):
55 ∀i,L. ⦃G, L⦄ ⊢ #i ![a, h] →
56 ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ![a, h].
57 #a #h #o #i #L #H #I #K #V #HLK
58 elim (cnv_inv_lref_drops … H) -H #Z #Y #X #HLY #HX
59 lapply (drops_mono … HLY … HLK) -L #H destruct //
62 (* Properties with generic slicing for local environments *******************)
64 (* Basic_2A1: uses: snv_lift *)
65 lemma cnv_lifts (a) (h): ∀G. d_liftable1 (cnv a h G).
67 @(fqup_wf_ind_eq (Ⓣ) … G K T) -G -K -T #G0 #K0 #T0 #IH #G #K * * [|||| * ]
68 [ #s #HG #HK #HT #_ #b #f #L #_ #X #H2 destruct
69 >(lifts_inv_sort1 … H2) -X -K -f //
70 | #i #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
71 elim (cnv_inv_lref_drops … H1) -H1 #I0 #K0 #V #HK0 #HV
72 elim (lifts_inv_lref1 … H2) -H2 #j #Hf #H destruct
73 (**) (* this should be a lemma *)
74 lapply (drops_trans … HLK … HK0 ??) -HLK [3,6: |*: // ] #H
75 elim (drops_split_trans … H) -H [1,6: |*: /2 width=6 by after_uni_dx/ ] #Y #HL #HY
76 lapply (drops_tls_at … Hf … HY) -HY #HY
77 elim (drops_inv_skip2 … HY) -HY #Z #L0 #HLK0 #HZ #H destruct
78 elim (liftsb_inv_pair_sn … HZ) -HZ #W #HVW #H destruct
79 (**) (* end of the lemma *)
80 /4 width=8 by cnv_lref_drops, fqup_lref, drops_inv_gen/
81 | #l #HG #HK #HT #H1 #b #f #L #_ #X #_ destruct
82 elim (cnv_inv_gref … H1)
83 | #p #I #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
84 elim (cnv_inv_bind … H1) -H1 #HV #HT
85 elim (lifts_inv_bind1 … H2) -H2 #W #U #HVW #HTU #H destruct
86 /5 width=8 by cnv_bind, drops_skip, ext2_pair/
87 | #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
88 elim (cnv_inv_appl … H1) #n #p #W0 #U0 #Ha #HV #HT #HVW0 #HTW0
89 elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
90 elim (lifts_total W0 f)
91 elim (lifts_total U0 (⫯f))
92 /4 width=17 by cnv_appl, cpms_lifts_bi, lifts_bind/
93 | #V #T #HG #HK #HT #H1 #b #f #L #HLK #X #H2 destruct
94 elim (cnv_inv_cast … H1) #U0 #HV #HT #HVU0 #HTU0
95 elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
96 elim (lifts_total U0 f)
97 /3 width=12 by cnv_cast, cpms_lifts_bi/
101 (* Inversion lemmas with generic slicing for local environments *************)
103 (* Basic_2A1: uses: snv_inv_lift *)
104 lemma cnv_inv_lifts (a) (h): ∀G. d_deliftable1 (cnv a h G).
106 @(fqup_wf_ind_eq (Ⓣ) … G L U) -G -L -U #G0 #L0 #U0 #IH #G #L * * [|||| * ]
107 [ #s #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
108 >(lifts_inv_sort2 … H2) -X -L -f //
109 | #j #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
110 elim (cnv_inv_lref_drops … H1) -H1 #I0 #L0 #W #HL0 #HW
111 elim (lifts_inv_lref2 … H2) -H2 #i #Hf #H destruct
112 (**) (* this should be a lemma *)
113 lapply (drops_split_div … HLK (𝐔❴i❵) ???) -HLK [4,8: * |*: // ] #Y0 #HK #HLY0
114 lapply (drops_conf … HL0 … HLY0 ??) -HLY0 [3,6: |*: /2 width=6 by after_uni_dx/ ] #HLY0
115 lapply (drops_tls_at … Hf … HLY0) -HLY0 #HLY0
116 elim (drops_inv_skip1 … HLY0) -HLY0 #Z #K0 #HLK0 #HZ #H destruct
117 elim (liftsb_inv_pair_dx … HZ) -HZ #V #HVW #H destruct
118 (**) (* end of the lemma *)
119 /4 width=8 by cnv_lref_drops, fqup_lref, drops_inv_F/
120 | #l #HG #HL #HU #H1 #b #f #K #_ #X #_ destruct
121 elim (cnv_inv_gref … H1)
122 | #p #I #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
123 elim (cnv_inv_bind … H1) -H1 #HW #HU
124 elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
125 /5 width=8 by cnv_bind, drops_skip, ext2_pair/
126 | #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
127 elim (cnv_inv_appl … H1) #n #p #W0 #U0 #Ha #HW #HU #HW0 #HU0
128 elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
129 elim (cpms_inv_lifts_sn … HW0 … HLK … HVW) -HW0 #V0 #HVW0 #HV0
130 elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X0 #H #HT0
131 elim (lifts_inv_bind2 … H) -H #X #T0 #HX #HTU0 #H destruct
132 lapply (lifts_inj … HX … HVW0) -HX #H destruct
133 /3 width=8 by cnv_appl/
134 | #W #U #HG #HL #HU #H1 #b #f #K #HLK #X #H2 destruct
135 elim (cnv_inv_cast … H1) #U0 #HW #HU #HWU0 #HU0
136 elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
137 elim (cpms_inv_lifts_sn … HWU0 … HLK … HVW) -HWU0 #V0 #HVU0 #HV0
138 elim (cpms_inv_lifts_sn … HU0 … HLK … HTU) -HU0 #X #HX #HTV0
139 lapply (lifts_inj … HX … HVU0) -HX #H destruct
140 /3 width=8 by cnv_cast/