]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma
update in ground and delayed updating
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / gcp_aaa.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/aaa_aaa.ma".
16 include "static_2/static/lsubc_drops.ma".
17
18 (* GENERIC COMPUTATION PROPERTIES *******************************************)
19
20 (* Main properties **********************************************************)
21
22 (* Basic_1: was: sc3_arity_csubc *)
23 theorem acr_aaa_lsubc_lifts (RR) (RS) (RP):
24         gcp RR RS RP → gcr RR RS RP RP →
25         ∀G,L1,T,A. ❨G,L1❩ ⊢ T ⁝ A → ∀b,f,L0. ⇩*[b,f] L0 ≘ L1 →
26         ∀T0. ⇧*[f] T ≘ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
27         ❨G,L2,T0❩ ϵ ⟦A⟧[RP].
28 #RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq (Ⓣ) … G L1 T) -G -L1 -T
29 #Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
30 [ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
31   lapply (aaa_inv_sort … HA) -HA #H destruct
32   >(lifts_inv_sort1 … H0) -H0
33   lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
34   lapply (s2 … HAtom G L2 (ⓔ)) /3 width=7 by cp1, simple_atom/
35 | #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
36   elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
37   elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
38   lapply (acr_gcr … H1RP H2RP A) #HA
39   lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
40   elim (drops_split_trans … H) -H [ |*: /2 width=6 by pr_after_nat_uni/ ] #Y #HLK0 #HY
41   lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
42   elim (drops_inv_skip2 … HY) -HY #Z #K0 #HK01 #HZ #H destruct
43   elim (liftsb_inv_pair_sn … HZ) -HZ #V0 #HV10 #H destruct
44   elim (lifts_total V0 (𝐔❨↑j❩)) #V #HV0
45   elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
46   elim (lsubc_inv_bind2 … H) -H *
47   [ #K2 #HK20 #H destruct
48     lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
49     lapply (s5 … HA ? G ? ? (ⓔ) … HV0 ?) -HA
50     /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
51   | #K2 #V2 #W2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
52     lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
53     lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
54     lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
55     elim (lifts_total V2 (𝐔❨↑j❩)) #V3 #HV23
56     lapply (s5 … HA … G … (ⓔ) … (ⓝW2.V2) (ⓝV.V3) ????)
57     [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
58     lapply (s7 … HA G L2 (ⓔ)) -HA /3 width=7 by acr_lifts/
59   ]
60 | #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
61   elim (aaa_inv_gref … HA)
62 | #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
63   elim (aaa_inv_abbr … HA) -HA #B #HV #HT
64   elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
65   lapply (acr_gcr … H1RP H2RP A) #HA
66   lapply (acr_gcr … H1RP H2RP B) #HB
67   lapply (s1 … HB) -HB #HB
68   lapply (s6 … HA G L2 (ⓔ) (ⓔ)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/
69 | #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
70   elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
71   elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
72   @(acr_abst  … H1RP H2RP) /2 width=10 by/
73   #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B
74   elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20
75   lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
76   [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
77   @(IH … ((⫯f3)∘⫯f) … (L2. ⓛW3)) -IH
78   /4 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans, ext2_pair/
79 | #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
80   elim (aaa_inv_appl … HA) -HA #B #HV #HT
81   elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
82   lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0
83   /3 width=10 by drops_refl, lifts_refl/
84 | #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
85   elim (aaa_inv_cast … HA) -HA #HW #HT
86   elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
87   lapply (acr_gcr … H1RP H2RP A) #HA
88   lapply (s7 … HA G L2 (ⓔ)) /3 width=10 by/
89 ]
90 qed.
91
92 (* Basic_1: was: sc3_arity *)
93 lemma acr_aaa (RR) (RS) (RP):
94       gcp RR RS RP → gcr RR RS RP RP →
95       ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ❨G,L,T❩ ϵ ⟦A⟧[RP].
96 /3 width=9 by drops_refl, lifts_refl, acr_aaa_lsubc_lifts/ qed.
97
98 lemma gcr_aaa (RR) (RS) (RP):
99       gcp RR RS RP → gcr RR RS RP RP →
100       ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → RP G L T.
101 #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
102 lapply (acr_gcr … H1RP H2RP A) #HA
103 @(s1 … HA) /2 width=4 by acr_aaa/
104 qed.