From: Ferruccio Guidi Date: Sun, 19 Feb 2017 18:56:35 +0000 (+0000) Subject: - advances on cnx X-Git-Tag: make_still_working~499 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=38571b4c3881f2b59b7a2cdd016c83b161d3d755 - advances on cnx - generic reducibility moved to the "static" component --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index d35fb52a2..7a4ad7662 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -42,6 +42,10 @@ definition d_liftable1: predicate (relation2 lenv term) ≝ λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K → ∀U. ⬆*[f] T ≡ U → R L U. +definition d_deliftable1: predicate (relation2 lenv term) ≝ + λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K → + ∀T. ⬆*[f] T ≡ U → R K T. + definition d_liftable2: predicate (lenv → relation term) ≝ λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K → ∀U1. ⬆*[f] T1 ≡ U1 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma deleted file mode 100644 index e0e3c54e9..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma +++ /dev/null @@ -1,52 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/syntax/genv.ma". -include "basic_2/relocation/drops_vector.ma". - -(* GENERIC COMPUTATION PROPERTIES *******************************************) - -definition nf ≝ λRR:relation4 genv lenv term term. λRS:relation term. - λG,L,T. NF … (RR G L) RS T. - -definition candidate: Type[0] ≝ relation3 genv lenv term. - -definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G. d_liftable1 (nf RR RS G). - -definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L. ∃s. NF … (RR G L) RS (⋆s). - -definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G). - -definition CP3 ≝ λRP:candidate. - ∀G,L,T,s. RP G L (ⓐ⋆s.T) → RP G L T. - -(* requirements for generic computation properties *) -(* Basic_1: includes: nf2_lift1 *) -(* Basic_2A1: includes: gcp0_lifts *) -(* Basic_2A1: includes: gcp2_lifts *) -record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ -{ cp0: CP0 RR RS; - cp1: CP1 RR RS; - cp2: CP2 RP; - cp3: CP3 RP -}. - -(* Basic properties *********************************************************) - -(* Basic_1: was only: sns3_lifts1 *) -(* Basic_2A1: was: gcp2_lifts_all *) -lemma gcp2_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftable1_all (RP G). -/3 width=7 by cp2, d1_liftable_liftable_all/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma deleted file mode 100644 index 111d967e5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma +++ /dev/null @@ -1,101 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/aaa_aaa.ma". -include "basic_2/rt_computation/lsubc_drops.ma". - -(* GENERIC COMPUTATION PROPERTIES *******************************************) - -(* Main properties **********************************************************) - -(* Basic_1: was: sc3_arity_csubc *) -theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. - gcp RR RS RP → gcr RR RS RP RP → - ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 → - ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → - ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. -#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T -#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ] -[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH - lapply (aaa_inv_sort … HA) -HA #H destruct - >(lifts_inv_sort1 … H0) -H0 - lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom - lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/ -| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct - elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1 - elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct - lapply (acr_gcr … H1RP H2RP A) #HA - lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H - elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY - lapply (drops_tls_at … Hf … HY) -Hf -HY #HY - elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct - elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0 - elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H - elim (lsubc_inv_pair2 … H) -H * - [ #K2 #HK20 #H destruct - lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b - lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA - /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/ - | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1 - lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b - lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A - lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A - elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23 - lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????) - [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2 - lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/ - ] -| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH - elim (aaa_inv_gref … HA) -| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct - elim (aaa_inv_abbr … HA) -HA #B #HV #HT - elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct - lapply (acr_gcr … H1RP H2RP A) #HA - lapply (acr_gcr … H1RP H2RP B) #HB - lapply (s1 … HB) -HB #HB - lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/ -| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct - elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct - elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct - @(acr_abst … H1RP H2RP) /2 width=10 by/ - #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B - elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW - [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3 - @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH - /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ -| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct - elim (aaa_inv_appl … HA) -HA #B #HV #HT - elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct - lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0 - /3 width=10 by drops_refl, lifts_refl/ -| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct - elim (aaa_inv_cast … HA) -HA #HW #HT - elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct - lapply (acr_gcr … H1RP H2RP A) #HA - lapply (s7 … HA G L2 (◊)) /3 width=10 by/ -] -qed. - -(* Basic_1: was: sc3_arity *) -lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. -/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed. - -lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → - ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. -#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT -lapply (acr_gcr … H1RP H2RP A) #HA -@(s1 … HA) /2 width=4 by acr_aaa/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma deleted file mode 100644 index 4493ae7af..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma +++ /dev/null @@ -1,176 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/ineint_5.ma". -include "basic_2/syntax/aarity.ma". -include "basic_2/relocation/lifts_simple.ma". -include "basic_2/relocation/lifts_lifts_vector.ma". -include "basic_2/relocation/drops_drops.ma". -include "basic_2/rt_computation/gcp.ma". - -(* GENERIC COMPUTATION PROPERTIES *******************************************) - -(* Note: this is Girard's CR1 *) -definition S1 ≝ λRP,C:candidate. - ∀G,L,T. C G L T → RP G L T. - -(* Note: this is Tait's iii, or Girard's CR4 *) -definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate. - ∀G,L,Vs. all … (RP G L) Vs → - ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T). - -(* Note: this generalizes Tait's ii *) -definition S3 ≝ λC:candidate. - ∀a,G,L,Vs,V,T,W. - C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T). - -definition S4 ≝ λRP,C:candidate. - ∀G,L,Vs. all … (RP G L) Vs → ∀s. C G L (ⒶVs.⋆s). - -definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. - C G L (ⒶVs.V2) → ⬆*[⫯i] V1 ≡ V2 → - ⬇*[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). - -definition S6 ≝ λRP,C:candidate. - ∀G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b → - ∀a,V,T. C G (L.ⓓV) (ⒶV2b.T) → RP G L V → C G L (ⒶV1b.ⓓ{a}V.T). - -definition S7 ≝ λC:candidate. - ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). - -(* requirements for the generic reducibility candidate *) -record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ -{ s1: S1 RP C; - s2: S2 RR RS RP C; - s3: S3 C; - s4: S4 RP C; - s5: S5 C; - s6: S6 RP C; - s7: S7 C -}. - -(* the functional construction for candidates *) -definition cfun: candidate → candidate → candidate ≝ - λC1,C2,G,K,T. ∀f,L,W,U. - ⬇*[Ⓕ, f] L ≡ K → ⬆*[f] T ≡ U → C1 G L W → C2 G L (ⓐW.U). - -(* the reducibility candidate associated to an atomic arity *) -rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝ -match A with -[ AAtom ⇒ RP -| APair B A ⇒ cfun (acr RP B) (acr RP A) -]. - -interpretation - "reducibility candidate of an atomic arity (abstract)" - 'InEInt RP G L T A = (acr RP A G L T). - -(* Basic properties *********************************************************) - -(* Note: this requires Ⓕ-slicing in cfun since b is unknown in d_liftable_1 *) -(* Note: this requires multiple relocation *) -(* Basic 1: includes: sc3_lift *) -(* Basic 2A1: includes: gcr_lift *) -(* Basic 2A1: note: gcr_lift should be acr_lift *) -(* Basic_1: was: sc3_lift1 *) -(* Basic 2A1: was: gcr_lifts *) -(* Basic 2A1: note: gcr_lifts should be acr_lifts *) -lemma acr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G). -#RR #RS #RP #H #A #G elim A -A -[ /2 width=7 by cp2/ -| #B #A #HB #HA #K #T #HKT #b #f #L #HLK #U #HTU #f0 #L0 #W #U0 #HL0 #HU0 #HW - lapply (drops_trans … HL0 … HLK ??) [3:|*: // ] -L #HL0K - lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -U #HTU0 - /2 width=3 by/ (**) (* full auto fails *) -] -qed-. - -(* Basic_1: was: - sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast -*) -lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → - ∀A. gcr RR RS RP (acr RP A). -#RR #RS #RP #H1RP #H2RP #A elim A -A // -#B #A #IHB #IHA @mk_gcr -[ #G #L #T #H - elim (cp1 … H1RP G L) #s #HK - lapply (s2 … IHB G L (◊) … HK) // #HB - lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H - /3 width=6 by s1, cp3, drops_refl, lifts_refl/ -| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct - lapply (s1 … IHB … HB) #HV0 - @(s2 … IHA … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/ -| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct - elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct - @(s3 … IHA … (V0@V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ -| #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - >(lifts_inv_sort1 … HY) -Y - lapply (s1 … IHB … HB) #HV0 - @(s4 … IHA … (V0@V0s)) /3 width=7 by gcp2_all, conj/ -| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - elim (lifts_inv_lref1 … HY) -HY #j #Hf #H destruct - lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H - elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY - lapply (drops_tls_at … Hf … HY) -HY #HY - elim (drops_inv_skip2 … HY) -HY #K0 #W1 #_ #HVW1 #H destruct - elim (lifts_total W1 (𝐔❴⫯j❵)) #W2 #HW12 - lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H - lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2 - @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/ -| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct - elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct - elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120 - elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s - @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/ - @(HA … (↑f)) /2 width=2 by drops_skip/ - [ @lifts_applv // - lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H - elim (liftsv_split_trans … H (𝐔❴1❵) (↑f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s - >(liftsv_mono … HV12s … HV10s) -V1s // - | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/ - ] -| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB - elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct - elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct - @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/ -] -qed. - -lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → - ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( - ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≡ L → ⬆*[f] W ≡ W0 → ⬆*[↑f] T ≡ T0 → - ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 - ) → - ⦃G, L, ⓛ{p}W.T⦄ ϵ[RP] 〚②B.A〛. -#RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB -lapply (acr_gcr … H1RP H2RP A) #HCA -lapply (acr_gcr … H1RP H2RP B) #HCB -elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct -lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0 -lapply (s3 … HCA … p G L0 (◊)) #H @H -H -lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H -[ @(HA … HL0) // -| lapply (s1 … HCB) -HCB #HCB - lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/ -] -qed. - -(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) -(* Basic_1: removed local theorems 1: sc3_sn3_abst *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma deleted file mode 100644 index 5b994b741..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma +++ /dev/null @@ -1,107 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/lrsubeqc_4.ma". -include "basic_2/static/aaa.ma". -include "basic_2/rt_computation/gcp_cr.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) - -inductive lsubc (RP) (G): relation lenv ≝ -| lsubc_atom: lsubc RP G (⋆) (⋆) -| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A → - lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW) -. - -interpretation - "local environment refinement (generic reducibility)" - 'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2). - -(* Basic inversion lemmas ***************************************************) - -fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 = ⋆ → L2 = ⋆. -#RP #G #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was just: csubc_gen_sort_r *) -lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆. -/2 width=5 by lsubc_inv_atom1_aux/ qed-. - -fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → - (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⫃[RP] K2 & - L2 = K2. ⓛW & X = ⓝW.V & I = Abbr. -#RP #G #L1 #L2 * -L1 -L2 -[ #I #K1 #V #H destruct -| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/ -| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/ -] -qed-. - -(* Basic_1: was: csubc_gen_head_r *) -lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃[RP] L2 → - (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨ - ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⫃[RP] K2 & - L2 = K2.ⓛW & X = ⓝW.V & I = Abbr. -/2 width=3 by lsubc_inv_pair1_aux/ qed-. - -fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L2 = ⋆ → L1 = ⋆. -#RP #G #L1 #L2 * -L1 -L2 -[ // -| #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct -] -qed-. - -(* Basic_1: was just: csubc_gen_sort_l *) -lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⫃[RP] ⋆ → L1 = ⋆. -/2 width=5 by lsubc_inv_atom2_aux/ qed-. - -fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W → - (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⫃[RP] K2 & - L1 = K1.ⓓⓝW.V & I = Abst. -#RP #G #L1 #L2 * -L1 -L2 -[ #I #K2 #W #H destruct -| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/ -| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/ -] -qed-. - -(* Basic_1: was just: csubc_gen_head_l *) -lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W → - (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓑ{I} W) ∨ - ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & - G ⊢ K1 ⫃[RP] K2 & - L1 = K1.ⓓⓝW.V & I = Abst. -/2 width=3 by lsubc_inv_pair2_aux/ qed-. - -(* Basic properties *********************************************************) - -(* Basic_1: was just: csubc_refl *) -lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L. -#RP #G #L elim L -L /2 width=1 by lsubc_pair/ -qed. - -(* Basic_1: removed theorems 3: - csubc_clear_conf csubc_getl_conf csubc_csuba -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma deleted file mode 100644 index 59ba61ad2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma +++ /dev/null @@ -1,69 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/aaa_drops.ma". -include "basic_2/rt_computation/lsubc.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) - -(* Properties with generic slicing ******************************************) - -(* Note: the premise 𝐔⦃f⦄ cannot be removed *) -(* Basic_1: includes: csubc_drop_conf_O *) -(* Basic_2A1: includes: lsubc_drop_O1_trans *) -lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → - ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 → - ∃∃K1. ⬇*[b, f] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2. -#RP #G #L1 #L2 #H elim H -L1 -L2 -[ /2 width=3 by ex2_intro/ -| #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H - elim (drops_inv_pair1_isuni … Hf H) -Hf -H * - [ #Hf #H destruct -IH - /3 width=3 by lsubc_pair, drops_refl, ex2_intro/ - | #g #Hg #HLK2 #H destruct -HL12 - elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ - ] -| #L1 #L2 #V #W #A #HV #H1W #H2W #HL12 #IH #b #f #K2 #Hf #H - elim (drops_inv_pair1_isuni … Hf H) -Hf -H * - [ #Hf #H destruct -IH - /3 width=8 by drops_refl, lsubc_beta, ex2_intro/ - | #g #Hg #HLK2 #H destruct -HL12 - elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ - ] -] -qed-. - -(* Basic_1: was: csubc_drop1_conf_rev *) -(* Basic_1: includes: csubc_drop_conf_rev *) -(* Basic_2A1: includes: drop_lsubc_trans *) -lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP → - ∀b,f,G,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → - ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[b, f] L2 ≡ K2. -#RR #RS #RP #HR #b #f #G #L1 #K1 #H elim H -f -L1 -K1 -[ #f #Hf #Y #H lapply (lsubc_inv_atom1 … H) -H - #H destruct /4 width=3 by lsubc_atom, drops_atom, ex2_intro/ -| #f #I #L1 #K1 #V1 #_ #IH #K2 #HK12 elim (IH … HK12) -K1 - /3 width=5 by lsubc_pair, drops_drop, ex2_intro/ -| #f #I #L1 #K1 #V1 #V2 #HLK1 #HV21 #IH #X #H elim (lsubc_inv_pair1 … H) -H * - [ #K2 #HK12 #H destruct -HLK1 - elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/ - | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct - elim (lifts_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct - elim (IH … HK12) -IH -HK12 #K #HL1K #HK2 - lapply (acr_lifts … HR … HV … HLK1 … HV3) -HV - lapply (acr_lifts … HR … H1W2 … HLK1 … HW23) -H1W2 - /4 width=10 by lsubc_beta, aaa_lifts, drops_skip, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma deleted file mode 100644 index 2969b9a52..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma +++ /dev/null @@ -1,26 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsuba.ma". -include "basic_2/rt_computation/gcp_aaa.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) - -(* Properties with lenv refinement for atomic arity assignment **************) - -lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → - ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2. -#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/ -#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma deleted file mode 100644 index 045ad95bd..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma +++ /dev/null @@ -1,24 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/static/lsubr.ma". -include "basic_2/rt_computation/lsubc.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) - -(* Forward lemmas with restricted refinement for local environments *********) - -lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2. -#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index b47d0e449..41a6c9556 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,3 +1 @@ -lsubc.ma lsubc_drops.ma lsubc_lsubr.ma lsubc_lsuba.ma -gcp.ma gcp_cr.ma gcp_aaa.ma cpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma index b4f5e8c3d..1dcbdf2a4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_transition/cnx.ma". @@ -24,6 +25,15 @@ lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇*[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ⬈[h, o #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct qed. +(* Basic_2A1: includes: cnx_lift *) +lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G). +#h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H +elim (cpx_inv_lifts … H … HLK … HTU) -b -L #T0 #HTU0 #HT0 +lapply (HT … HT0) -G -K #HT0 +elim (tdeq_lifts … HT0 … HTU) -T #X #HX #HU +<(lifts_mono … HX … HTU0) -T0 // +qed-. + (* Inversion lemmas with generic slicing ************************************) (* Basic_2A1: was: cnx_inv_delta *) @@ -35,23 +45,11 @@ lapply (H W ?) -H /2 width=7 by cpx_delta_drops/ -HLK /2 width=5 by lifts_inv_lref2_uni_lt/ qed-. -(* -(* Relocation properties ****************************************************) - -lemma cnx_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄ → ⬇[c, l, k] L0 ≡ L → - ⬆[l, k] T ≡ T0 → ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄. -#h #o #G #L0 #L #T #T0 #c #l #k #HLT #HL0 #HT0 #X #H -elim (cpx_inv_lift1 … H … HL0 … HT0) -L0 #T1 #HT10 #HT1 -<(HLT … HT1) in HT0; -L #HT0 ->(lift_mono … HT10 … HT0) -T1 -X // -qed. - -lemma cnx_inv_lift: ∀h,o,G,L0,L,T,T0,c,l,k. ⦃G, L0⦄ ⊢ ➡[h, o] 𝐍⦃T0⦄ → ⬇[c, l, k] L0 ≡ L → - ⬆[l, k] T ≡ T0 → ⦃G, L⦄ ⊢ ➡[h, o] 𝐍⦃T⦄. -#h #o #G #L0 #L #T #T0 #c #l #k #HLT0 #HL0 #HT0 #X #H -elim (lift_total X l k) #X0 #HX0 -lapply (cpx_lift … H … HL0 … HT0 … HX0) -L #HTX0 ->(HLT0 … HTX0) in HX0; -L0 -X0 #H ->(lift_inj … H … HT0) -T0 -X -l -k // +(* Basic_2A1: includes: cnx_inv_lift *) +lemma cnx_inv_lifts: ∀h,o,G. d_deliftable1 … (cnx h o G). +#h #o #G #L #U #HU #b #f #K #HLK #T #HTU #T0 #H +elim (cpx_lifts … H … HLK … HTU) -b -K #U0 #HTU0 #HU0 +lapply (HU … HU0) -G -L #HU0 +elim (tdeq_inv_lifts … HU0 … HTU) -U #X #HX #HT +<(lifts_inj … HX … HTU0) -U0 // qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 9760148c1..9ed6e4104 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,7 +1,7 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma cpx_lfxs.ma cpx_lfdeq.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma -cnx.ma cnx_simple.ma +cnx.ma cnx_simple.ma cnx_drops.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma new file mode 100644 index 000000000..e0e3c54e9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp.ma @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/syntax/genv.ma". +include "basic_2/relocation/drops_vector.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition nf ≝ λRR:relation4 genv lenv term term. λRS:relation term. + λG,L,T. NF … (RR G L) RS T. + +definition candidate: Type[0] ≝ relation3 genv lenv term. + +definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G. d_liftable1 (nf RR RS G). + +definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L. ∃s. NF … (RR G L) RS (⋆s). + +definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G). + +definition CP3 ≝ λRP:candidate. + ∀G,L,T,s. RP G L (ⓐ⋆s.T) → RP G L T. + +(* requirements for generic computation properties *) +(* Basic_1: includes: nf2_lift1 *) +(* Basic_2A1: includes: gcp0_lifts *) +(* Basic_2A1: includes: gcp2_lifts *) +record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ +{ cp0: CP0 RR RS; + cp1: CP1 RR RS; + cp2: CP2 RP; + cp3: CP3 RP +}. + +(* Basic properties *********************************************************) + +(* Basic_1: was only: sns3_lifts1 *) +(* Basic_2A1: was: gcp2_lifts_all *) +lemma gcp2_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftable1_all (RP G). +/3 width=7 by cp2, d1_liftable_liftable_all/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma new file mode 100644 index 000000000..53b415bde --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma @@ -0,0 +1,101 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/aaa_aaa.ma". +include "basic_2/static/lsubc_drops.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: sc3_arity_csubc *) +theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. + gcp RR RS RP → gcr RR RS RP RP → + ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 → + ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → + ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. +#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T +#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ] +[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH + lapply (aaa_inv_sort … HA) -HA #H destruct + >(lifts_inv_sort1 … H0) -H0 + lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom + lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/ +| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct + elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1 + elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct + lapply (acr_gcr … H1RP H2RP A) #HA + lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H + elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY + lapply (drops_tls_at … Hf … HY) -Hf -HY #HY + elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct + elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0 + elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H + elim (lsubc_inv_pair2 … H) -H * + [ #K2 #HK20 #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b + lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA + /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/ + | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1 + lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b + lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A + lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A + elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23 + lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????) + [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2 + lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/ + ] +| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH + elim (aaa_inv_gref … HA) +| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct + elim (aaa_inv_abbr … HA) -HA #B #HV #HT + elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct + lapply (acr_gcr … H1RP H2RP A) #HA + lapply (acr_gcr … H1RP H2RP B) #HB + lapply (s1 … HB) -HB #HB + lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/ +| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct + elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct + elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct + @(acr_abst … H1RP H2RP) /2 width=10 by/ + #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B + elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20 + lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW + [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3 + @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH + /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ +| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct + elim (aaa_inv_appl … HA) -HA #B #HV #HT + elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct + lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0 + /3 width=10 by drops_refl, lifts_refl/ +| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct + elim (aaa_inv_cast … HA) -HA #HW #HT + elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct + lapply (acr_gcr … H1RP H2RP A) #HA + lapply (s7 … HA G L2 (◊)) /3 width=10 by/ +] +qed. + +(* Basic_1: was: sc3_arity *) +lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛. +/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed. + +lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T. +#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT +lapply (acr_gcr … H1RP H2RP A) #HA +@(s1 … HA) /2 width=4 by acr_aaa/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma new file mode 100644 index 000000000..09dd1d346 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma @@ -0,0 +1,176 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/ineint_5.ma". +include "basic_2/syntax/aarity.ma". +include "basic_2/relocation/lifts_simple.ma". +include "basic_2/relocation/lifts_lifts_vector.ma". +include "basic_2/relocation/drops_drops.ma". +include "basic_2/static/gcp.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +(* Note: this is Girard's CR1 *) +definition S1 ≝ λRP,C:candidate. + ∀G,L,T. C G L T → RP G L T. + +(* Note: this is Tait's iii, or Girard's CR4 *) +definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate. + ∀G,L,Vs. all … (RP G L) Vs → + ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T). + +(* Note: this generalizes Tait's ii *) +definition S3 ≝ λC:candidate. + ∀a,G,L,Vs,V,T,W. + C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T). + +definition S4 ≝ λRP,C:candidate. + ∀G,L,Vs. all … (RP G L) Vs → ∀s. C G L (ⒶVs.⋆s). + +definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. + C G L (ⒶVs.V2) → ⬆*[⫯i] V1 ≡ V2 → + ⬇*[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). + +definition S6 ≝ λRP,C:candidate. + ∀G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b → + ∀a,V,T. C G (L.ⓓV) (ⒶV2b.T) → RP G L V → C G L (ⒶV1b.ⓓ{a}V.T). + +definition S7 ≝ λC:candidate. + ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T). + +(* requirements for the generic reducibility candidate *) +record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ +{ s1: S1 RP C; + s2: S2 RR RS RP C; + s3: S3 C; + s4: S4 RP C; + s5: S5 C; + s6: S6 RP C; + s7: S7 C +}. + +(* the functional construction for candidates *) +definition cfun: candidate → candidate → candidate ≝ + λC1,C2,G,K,T. ∀f,L,W,U. + ⬇*[Ⓕ, f] L ≡ K → ⬆*[f] T ≡ U → C1 G L W → C2 G L (ⓐW.U). + +(* the reducibility candidate associated to an atomic arity *) +rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝ +match A with +[ AAtom ⇒ RP +| APair B A ⇒ cfun (acr RP B) (acr RP A) +]. + +interpretation + "reducibility candidate of an atomic arity (abstract)" + 'InEInt RP G L T A = (acr RP A G L T). + +(* Basic properties *********************************************************) + +(* Note: this requires Ⓕ-slicing in cfun since b is unknown in d_liftable_1 *) +(* Note: this requires multiple relocation *) +(* Basic 1: includes: sc3_lift *) +(* Basic 2A1: includes: gcr_lift *) +(* Basic 2A1: note: gcr_lift should be acr_lift *) +(* Basic_1: was: sc3_lift1 *) +(* Basic 2A1: was: gcr_lifts *) +(* Basic 2A1: note: gcr_lifts should be acr_lifts *) +lemma acr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G). +#RR #RS #RP #H #A #G elim A -A +[ /2 width=7 by cp2/ +| #B #A #HB #HA #K #T #HKT #b #f #L #HLK #U #HTU #f0 #L0 #W #U0 #HL0 #HU0 #HW + lapply (drops_trans … HL0 … HLK ??) [3:|*: // ] -L #HL0K + lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -U #HTU0 + /2 width=3 by/ (**) (* full auto fails *) +] +qed-. + +(* Basic_1: was: + sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast +*) +lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀A. gcr RR RS RP (acr RP A). +#RR #RS #RP #H1RP #H2RP #A elim A -A // +#B #A #IHB #IHA @mk_gcr +[ #G #L #T #H + elim (cp1 … H1RP G L) #s #HK + lapply (s2 … IHB G L (◊) … HK) // #HB + lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H + /3 width=6 by s1, cp3, drops_refl, lifts_refl/ +| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct + lapply (s1 … IHB … HB) #HV0 + @(s2 … IHA … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/ +| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct + elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct + @(s3 … IHA … (V0@V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/ +| #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + >(lifts_inv_sort1 … HY) -Y + lapply (s1 … IHB … HB) #HV0 + @(s4 … IHA … (V0@V0s)) /3 width=7 by gcp2_all, conj/ +| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_lref1 … HY) -HY #j #Hf #H destruct + lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H + elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY + lapply (drops_tls_at … Hf … HY) -HY #HY + elim (drops_inv_skip2 … HY) -HY #K0 #W1 #_ #HVW1 #H destruct + elim (lifts_total W1 (𝐔❴⫯j❵)) #W2 #HW12 + lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H + lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2 + @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/ +| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct + elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct + elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120 + elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s + @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/ + @(HA … (↑f)) /2 width=2 by drops_skip/ + [ @lifts_applv // + lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H + elim (liftsv_split_trans … H (𝐔❴1❵) (↑f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s + >(liftsv_mono … HV12s … HV10s) -V1s // + | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/ + ] +| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct + @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/ +] +qed. + +lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( + ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≡ L → ⬆*[f] W ≡ W0 → ⬆*[↑f] T ≡ T0 → + ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 + ) → + ⦃G, L, ⓛ{p}W.T⦄ ϵ[RP] 〚②B.A〛. +#RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB +lapply (acr_gcr … H1RP H2RP A) #HCA +lapply (acr_gcr … H1RP H2RP B) #HCB +elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct +lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0 +lapply (s3 … HCA … p G L0 (◊)) #H @H -H +lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H +[ @(HA … HL0) // +| lapply (s1 … HCB) -HCB #HCB + lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/ +] +qed. + +(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *) +(* Basic_1: removed local theorems 1: sc3_sn3_abst *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma new file mode 100644 index 000000000..7b5315d4f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma @@ -0,0 +1,107 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lrsubeqc_4.ma". +include "basic_2/static/aaa.ma". +include "basic_2/static/gcp_cr.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) + +inductive lsubc (RP) (G): relation lenv ≝ +| lsubc_atom: lsubc RP G (⋆) (⋆) +| lsubc_pair: ∀I,L1,L2,V. lsubc RP G L1 L2 → lsubc RP G (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| lsubc_beta: ∀L1,L2,V,W,A. ⦃G, L1, V⦄ ϵ[RP] 〚A〛 → ⦃G, L1, W⦄ ϵ[RP] 〚A〛 → ⦃G, L2⦄ ⊢ W ⁝ A → + lsubc RP G L1 L2 → lsubc RP G (L1. ⓓⓝW.V) (L2.ⓛW) +. + +interpretation + "local environment refinement (generic reducibility)" + 'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lsubc_inv_atom1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 = ⋆ → L2 = ⋆. +#RP #G #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was just: csubc_gen_sort_r *) +lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆. +/2 width=5 by lsubc_inv_atom1_aux/ qed-. + +fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X → + (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & + G ⊢ K1 ⫃[RP] K2 & + L2 = K2. ⓛW & X = ⓝW.V & I = Abbr. +#RP #G #L1 #L2 * -L1 -L2 +[ #I #K1 #V #H destruct +| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3 by ex2_intro, or_introl/ +| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10 by ex7_4_intro, or_intror/ +] +qed-. + +(* Basic_1: was: csubc_gen_head_r *) +lemma lsubc_inv_pair1: ∀RP,I,G,K1,L2,X. G ⊢ K1.ⓑ{I}X ⫃[RP] L2 → + (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨ + ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & + G ⊢ K1 ⫃[RP] K2 & + L2 = K2.ⓛW & X = ⓝW.V & I = Abbr. +/2 width=3 by lsubc_inv_pair1_aux/ qed-. + +fact lsubc_inv_atom2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L2 = ⋆ → L1 = ⋆. +#RP #G #L1 #L2 * -L1 -L2 +[ // +| #I #L1 #L2 #V #_ #H destruct +| #L1 #L2 #V #W #A #_ #_ #_ #_ #H destruct +] +qed-. + +(* Basic_1: was just: csubc_gen_sort_l *) +lemma lsubc_inv_atom2: ∀RP,G,L1. G ⊢ L1 ⫃[RP] ⋆ → L1 = ⋆. +/2 width=5 by lsubc_inv_atom2_aux/ qed-. + +fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = K2.ⓑ{I} W → + (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1. ⓑ{I} W) ∨ + ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & + G ⊢ K1 ⫃[RP] K2 & + L1 = K1.ⓓⓝW.V & I = Abst. +#RP #G #L1 #L2 * -L1 -L2 +[ #I #K2 #W #H destruct +| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/ +| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8 by ex6_3_intro, or_intror/ +] +qed-. + +(* Basic_1: was just: csubc_gen_head_l *) +lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W → + (∃∃K1. G ⊢ K1 ⫃[RP] K2 & L1 = K1.ⓑ{I} W) ∨ + ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A & + G ⊢ K1 ⫃[RP] K2 & + L1 = K1.ⓓⓝW.V & I = Abst. +/2 width=3 by lsubc_inv_pair2_aux/ qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was just: csubc_refl *) +lemma lsubc_refl: ∀RP,G,L. G ⊢ L ⫃[RP] L. +#RP #G #L elim L -L /2 width=1 by lsubc_pair/ +qed. + +(* Basic_1: removed theorems 3: + csubc_clear_conf csubc_getl_conf csubc_csuba +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma new file mode 100644 index 000000000..d39dd6816 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/aaa_drops.ma". +include "basic_2/static/lsubc.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) + +(* Properties with generic slicing ******************************************) + +(* Note: the premise 𝐔⦃f⦄ cannot be removed *) +(* Basic_1: includes: csubc_drop_conf_O *) +(* Basic_2A1: includes: lsubc_drop_O1_trans *) +lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → + ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 → + ∃∃K1. ⬇*[b, f] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2. +#RP #G #L1 #L2 #H elim H -L1 -L2 +[ /2 width=3 by ex2_intro/ +| #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=3 by lsubc_pair, drops_refl, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +| #L1 #L2 #V #W #A #HV #H1W #H2W #HL12 #IH #b #f #K2 #Hf #H + elim (drops_inv_pair1_isuni … Hf H) -Hf -H * + [ #Hf #H destruct -IH + /3 width=8 by drops_refl, lsubc_beta, ex2_intro/ + | #g #Hg #HLK2 #H destruct -HL12 + elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/ + ] +] +qed-. + +(* Basic_1: was: csubc_drop1_conf_rev *) +(* Basic_1: includes: csubc_drop_conf_rev *) +(* Basic_2A1: includes: drop_lsubc_trans *) +lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP → + ∀b,f,G,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → + ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[b, f] L2 ≡ K2. +#RR #RS #RP #HR #b #f #G #L1 #K1 #H elim H -f -L1 -K1 +[ #f #Hf #Y #H lapply (lsubc_inv_atom1 … H) -H + #H destruct /4 width=3 by lsubc_atom, drops_atom, ex2_intro/ +| #f #I #L1 #K1 #V1 #_ #IH #K2 #HK12 elim (IH … HK12) -K1 + /3 width=5 by lsubc_pair, drops_drop, ex2_intro/ +| #f #I #L1 #K1 #V1 #V2 #HLK1 #HV21 #IH #X #H elim (lsubc_inv_pair1 … H) -H * + [ #K2 #HK12 #H destruct -HLK1 + elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/ + | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct + elim (lifts_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct + elim (IH … HK12) -IH -HK12 #K #HL1K #HK2 + lapply (acr_lifts … HR … HV … HLK1 … HV3) -HV + lapply (acr_lifts … HR … H1W2 … HLK1 … HW23) -H1W2 + /4 width=10 by lsubc_beta, aaa_lifts, drops_skip, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma new file mode 100644 index 000000000..625aed556 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lsuba.ma". +include "basic_2/static/gcp_aaa.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) + +(* Properties with lenv refinement for atomic arity assignment **************) + +lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2. +#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/ +#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma new file mode 100644 index 000000000..ddf571d83 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/static/lsubr.ma". +include "basic_2/static/lsubc.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************) + +(* Forward lemmas with restricted refinement for local environments *********) + +lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2. +#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index a7fc0d856..4a5a696ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -124,12 +124,6 @@ table { [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] } ] - [ { "generic reducibility" * } { - [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] - [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] - [ "gcp" *] - } - ] } ] class "water" @@ -166,6 +160,12 @@ table { ] class "green" [ { "static typing" * } { + [ { "generic reducibility" * } { + [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] + [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] + [ "gcp" *] + } + ] [ { "atomic arity assignment" * } { [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ]