]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma
c2cd35475a0b4562f6bde13ce33bcdaf1952f735
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lsubc_ldrop.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 "basic_2/static/aaa_lift.ma".
16 include "basic_2/computation/lsubc.ma".
17
18 (* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
19
20 (* Properties concerning basic local environment slicing ********************)
21
22 (* Basic_1: was: csubc_drop_conf_O *)
23 (* Note: the constant 0 can not be generalized *)
24 lemma lsubc_ldrop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⊑[RP] L2 → ∀K2,s,e. ⇩[s, 0, e] L2 ≡ K2 →
25                             ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & G ⊢ K1 ⊑[RP] K2.
26 #RP #G #L1 #L2 #H elim H -L1 -L2
27 [ #X #s #e #H elim (ldrop_inv_atom1 … H) -H /4 width=3 by ldrop_atom, ex2_intro/
28 | #I #L1 #L2 #V #_ #IHL12 #X #s #e #H
29   elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
30   [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H
31     /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/
32   | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
33   ]
34 | #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #s #e #H
35   elim (ldrop_inv_O1_pair1 … H) -H * #He #H destruct
36   [ elim (IHL12 L2 s 0) -IHL12 // #X #H <(ldrop_inv_O2 … H) -H
37     /3 width=8 by lsubc_abbr, ldrop_pair, ex2_intro/
38   | elim (IHL12 … H) -L2 /3 width=3 by ldrop_drop_lt, ex2_intro/
39   ]
40 ]
41 qed-.
42
43 (* Basic_1: was: csubc_drop_conf_rev *)
44 lemma ldrop_lsubc_trans: ∀RR,RS,RP.
45                          acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) →
46                          ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⊑[RP] K2 →
47                          ∃∃L2. G ⊢ L1 ⊑[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2.
48 #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
49 [ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H
50   >He /2 width=3 by ex2_intro/
51 | #L1 #I #V1 #X #H
52   elim (lsubc_inv_pair1 … H) -H *
53   [ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, ldrop_pair, ex2_intro/
54   | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct
55     /3 width=4 by lsubc_abbr, ldrop_pair, ex2_intro/
56   ]
57 | #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12
58   elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_drop, ex2_intro/
59 | #I #L1 #K1 #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H
60   elim (lsubc_inv_pair1 … H) -H *
61   [ #K2 #HK12 #H destruct
62     elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, ldrop_skip, ex2_intro/
63   | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
64     elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
65     elim (IHLK1 … HK12) #K #HL1K #HK2
66     lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
67     lapply (s8 … HA … HV2 … HLK1 HV3) -HV2
68     lapply (s8 … HA … H1W2 … HLK1 HW23) -H1W2
69     /4 width=11 by lsubc_abbr, aaa_lift, ldrop_skip, ex2_intro/
70   ]
71 ]
72 qed-.