From: Ferruccio Guidi Date: Sun, 14 Sep 2014 21:25:04 +0000 (+0000) Subject: slight refactoring in the proof of strong normalization X-Git-Tag: make_still_working~840 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=33f8507cadd3b36dc9afa227d8968dda66fe2034;p=helm.git slight refactoring in the proof of strong normalization --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma index ade57bbd9..d12f16a77 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma @@ -111,8 +111,9 @@ qed-. theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g). #h #g @mk_gcp -[ /3 width=13 by cnx_lift/ +[ normalize /3 width=13 by cnx_lift/ | #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/ +| /2 width=8 by csx_lift/ | /2 width=3 by csx_fwd_flat_dx/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma index 33f847019..96a008b6c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tsts_vector.ma @@ -118,9 +118,8 @@ qed. theorem csx_gcr: ∀h,g. gcr (cpx h g) (eq …) (csx h g) (csx h g). #h #g @mk_gcr // -[ /2 width=8 by csx_lift/ -| /3 width=1 by csx_applv_cnx/ -|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +[ /3 width=1 by csx_applv_cnx/ +|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ | /2 width=7 by csx_applv_delta/ | #G #L #V1s #V2s #HV12s #a #V #T #H #HV @(csx_applv_theta … HV12s) -HV12s diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma index 67dd3f6d6..3cab7cbaf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp.ma @@ -17,38 +17,42 @@ include "basic_2/multiple/drops.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,L0,L,T,T0,s,d,e. NF … (RR G L) RS T → - ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0. - -definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term. - ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L → - ∀T,T0. ⇧*[des] T ≡ T0 → - NF … (RR G L) RS T → NF … (RR G L0) RS T0. + ∀G. l_liftable1 (nf RR RS G) (Ⓕ). definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. ∀G,L. ∃k. NF … (RR G L) RS (⋆k). -definition CP2 ≝ λRP:candidate. +definition CP2 ≝ λRP:candidate. ∀G. l_liftable1 (RP G) (Ⓕ). + +definition CP3 ≝ λRP:candidate. ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. (* requirements for generic computation properties *) 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 + cp2: CP2 RP; + cp3: CP3 RP }. (* Basic properties *********************************************************) (* Basic_1: was: nf2_lift1 *) -lemma gcp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS. -#RR #RS #HRR #G #L1 #L2 #s #des #H elim H -L1 -L2 -des -[ #L #T1 #T2 #H #HT1 - <(lifts_inv_nil … H) -H // -| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=10 by/ -] +lemma gcp0_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀G. l_liftables1 (nf RR RS G) (Ⓕ). +#RR #RS #RP #H #G @l1_liftable_liftables @(cp0 … H) +qed. + +lemma gcp2_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀G. l_liftables1 (RP G) (Ⓕ). +#RR #RS #RP #H #G @l1_liftable_liftables @(cp2 … H) +qed. + +(* Basic_1: was only: sns3_lifts1 *) +lemma gcp2_lifts_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. l_liftables1_all (RP G) (Ⓕ). +#RR #RS #RP #H #G @l1_liftables_liftables_all /2 width=7 by gcp2_lifts/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma index 3522d41ac..3b5f84378 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_aaa.ma @@ -53,8 +53,8 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) [1,3: /2 width=1 by lift_flat/ ] - lapply (s7 … HB G L2 (◊)) #H @H -H [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ] + lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/ + lapply (s7 … HB G L2 (◊)) /3 width=7 by gcr_lift/ ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct @@ -64,9 +64,9 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (s6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct - @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ] + @(acr_abst … H1RP H2RP) /2 width=5 by/ #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B - elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 + elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma index ca6b3df49..a596e246d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/gcp_cr.ma @@ -21,13 +21,6 @@ include "basic_2/computation/gcp.ma". (* GENERIC COMPUTATION PROPERTIES *******************************************) -definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e. - C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. - -definition S0s ≝ λC:candidate. - ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → - ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. - (* Note: this is Girard's CR1 *) definition S1 ≝ λRP,C:candidate. ∀G,L,T. C G L T → RP G L T. @@ -58,8 +51,7 @@ definition S7 ≝ λC:candidate. (* requirements for the generic reducibility candidate *) record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝ -{ s0: S0 C; - s1: S1 RP C; +{ s1: S1 RP C; s2: S2 RR RS RP C; s3: S3 C; s4: S4 RP C; @@ -70,8 +62,8 @@ record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate (* the functional construction for candidates *) definition cfun: candidate → candidate → candidate ≝ - λC1,C2,G,K,T. ∀L,V,U,des. - ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U). + λC1,C2,G,K,T. ∀L,W,U,des. + ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L W → C2 G L (ⓐW.U). (* the reducibility candidate associated to an atomic arity *) let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ @@ -86,50 +78,35 @@ interpretation (* Basic properties *********************************************************) -(* Basic_1: was: sc3_lift1 *) -lemma gcr_lifts: ∀C. S0 C → S0s C. -#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des -[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // -| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 - elim (lifts_inv_cons … H) -H /3 width=10 by/ -] +(* Basic 1: was: sc3_lift *) +lemma gcr_lift: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. l_liftable1 (acr RP A G) (Ⓕ). +#RR #RS #RP #H #A elim A -A +/3 width=8 by cp2, drops_cons, lifts_cons/ qed. -lemma rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP → - ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → - RP G L V → RP G L0 V0. -#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV -@gcr_lifts /width=7 by/ -@(s0 … HRP) -qed. - -(* Basic_1: was only: sns3_lifts1 *) -lemma rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP → - ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → - all … (RP G L) Vs → all … (RP G L0) V0s. -#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // -#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ +(* Basic_1: was: sc3_lift1 *) +lemma gcr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. l_liftables1 (acr RP A G) (Ⓕ). +#RR #RS #RP #H #A #G @l1_liftable_liftables /2 width=7 by gcr_lift/ qed. (* Basic_1: was: - sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift + 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 -[ /3 width=7 by drops_cons, lifts_cons/ -| #G #L #T #H +[ #G #L #T #H elim (cp1 … H1RP G L) #k #HK lapply (H L (⋆k) T (◊) ? ? ?) -H // [ lapply (s2 … IHB G L (◊) … HK) // - | #H @(cp2 … H1RP … k) @(s1 … IHA) // + | /3 width=6 by s1, cp3/ ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #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=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/ + /3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/ | #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #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 @@ -139,7 +116,7 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → 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 rp_liftsv_all, conj/ + @(s4 … IHA … (V0 @ V0s)) /3 width=7 by gcp2_lifts_all, conj/ | #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct @@ -155,12 +132,12 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct elim (lift_total V10 0 1) #V20 #HV120 elim (liftv_total 0 1 V10s) #V20s #HV120s - @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by gcp2_lifts, liftv_cons/ @(HA … (des + 1)) /2 width=2 by drops_skip/ [ @lifts_applv // elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s >(liftv_mono … HV12s … HV10s) -V1s // - | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ + | @(gcr_lift … H1RP … HB … HV120) /2 width=2 by drop_drop/ ] | #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct @@ -179,7 +156,7 @@ lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → 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 (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 +lapply (gcr_lifts … H1RP … HL0 … HW0 HW) -HW #HW0 lapply (s3 … HCA … a G L0 (◊)) #H @H -H lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H [ @(HA … HL0) // diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma index 36f35527c..0e48ce8a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma @@ -41,11 +41,10 @@ lemma lsubc_drop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀K2,s,e. ⇩ qed-. (* Basic_1: was: csubc_drop_conf_rev *) -lemma drop_lsubc_trans: ∀RR,RS,RP. - gcp RR RS RP → gcr RR RS RP RP → +lemma drop_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP → ∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2. -#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e +#RR #RS #RP #Hgcp #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H >He /2 width=3 by ex2_intro/ | #L1 #I #V1 #X #H @@ -63,9 +62,8 @@ lemma drop_lsubc_trans: ∀RR,RS,RP. | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct elim (IHLK1 … HK12) #K #HL1K #HK2 - lapply (acr_gcr … Hgcp Hgcr A) -Hgcp -Hgcr #HA - lapply (s0 … HA … HV2 … HLK1 HV3) -HV2 - lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2 + lapply (gcr_lift … Hgcp … HV2 … HLK1 … HV3) -HV2 + lapply (gcr_lift … Hgcp … H1W2 … HLK1 … HW23) -H1W2 /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma index e1c30a75a..3f53eb54d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma @@ -19,14 +19,13 @@ include "basic_2/computation/lsubc_drop.ma". (* Properties concerning generic local environment slicing ******************) (* Basic_1: was: csubc_drop1_conf_rev *) -lemma drops_lsubc_trans: ∀RR,RS,RP. - gcp RR RS RP → gcr RR RS RP RP → +lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP → ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. -#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #des #H elim H -L1 -K1 -des +#RR #RS #RP #Hgcp #G #L1 #K1 #des #H elim H -L1 -K1 -des [ /2 width=3 by drops_nil, ex2_intro/ | #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12 - elim (drop_lsubc_trans … Hgcp Hgcr … HLK1 … HK12) -Hgcp -Hgcr -K1 #K #HLK #HK2 + elim (drop_lsubc_trans … Hgcp … HLK1 … HK12) -Hgcp -K1 #K #HLK #HK2 elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa.etc new file mode 100644 index 000000000..8f72937c4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rajust_5.ma". +include "basic_2/substitution/drop.ma". + +(* AJUSTMENT ****************************************************************) + +inductive fpa (s:bool): bi_relation lenv term ≝ +| fpa_fwd: ∀L,K,T,U,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → fpa s K T L U +| fpa_bwd: ∀L,K,T,U,d,e. ⇩[s, d, e] L ≡ K → ⇧[d, e] T ≡ U → fpa s L U K T +. + +interpretation + "ajustment (restricted closure)" + 'RAjust L1 T1 s L2 T2 = (fpa s L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma fpa_refl: ∀s. bi_reflexive … (fpa s). +/2 width=4 by fpa_fwd/ qed. + +lemma fpa_sym: ∀s. bi_symmetric … (fpa s). +#s #L1 #L2 #T1 #T2 * /2 width=4 by fpa_fwd, fpa_bwd/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa_fpa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa_fpa.etc new file mode 100644 index 000000000..c62b8bfb9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpa_fpa.etc @@ -0,0 +1,22 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/fpa.ma". + +(* AJUSTMENT ****************************************************************) + +(* Main properties **********************************************************) + +theorem fpa_conf: ∀s. bi_confluent … (fpa s). +/3 width=4 by fpa_sym, ex2_2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas.etc new file mode 100644 index 000000000..6817d8c90 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas.etc @@ -0,0 +1,59 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rajuststar_5.ma". +include "basic_2/substitution/fpa.ma". + +(* MULTIPLE AJUSTMENT *******************************************************) + +definition fpas: bool → bi_relation lenv term ≝ λs. bi_TC … (fpa s). + +interpretation + "multiple ajustment (restricted closure)" + 'RAjustStar L1 T1 s L2 T2 = (fpas s L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma fpas_ind: ∀L1,T1,s. ∀R:relation2 …. R L1 T1 → + (∀L,L2,T,T2. ⦃L1, T1⦄ ⇳*[s] ⦃L, T⦄ → ⦃L, T⦄ ⇳[s] ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ → R L2 T2. +#L1 #T1 #s #R #IH1 #IH2 #L2 #T2 #H +@(bi_TC_star_ind … IH1 IH2 L2 T2 H) // +qed-. + +lemma fpas_ind_dx: ∀L2,T2,s. ∀R:relation2 …. R L2 T2 → + (∀L1,L,T1,T. ⦃L1, T1⦄ ⇳[s] ⦃L, T⦄ → ⦃L, T⦄ ⇳*[s] ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ → R L1 T1. +#L2 #T2 #s #R #IH1 #IH2 #L1 #T1 #H +@(bi_TC_star_ind_dx … IH1 IH2 L1 T1 H) // +qed-. + +(* Basic properties *********************************************************) + +lemma fpas_refl: ∀s. bi_reflexive … (fpas s). +/2 width=1 by bi_inj/ qed. + +lemma fpas_sym: ∀s. bi_symmetric … (fpas s). +/3 width=1 by fpa_sym, bi_TC_symmetric/ qed-. + +lemma fpa_fpas: ∀L1,L2,T1,T2,s. ⦃L1, T1⦄ ⇳[s] ⦃L2, T2⦄ → ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄. +/2 width=1 by bi_inj/ qed. + +lemma fpas_strap1: ∀L1,L,L2,T1,T,T2,s. ⦃L1, T1⦄ ⇳*[s] ⦃L, T⦄ → ⦃L, T⦄ ⇳[s] ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄. +/2 width=4 by bi_step/ qed-. + +lemma fpas_strap2: ∀L1,L,L2,T1,T,T2,s. ⦃L1, T1⦄ ⇳[s] ⦃L, T⦄ → ⦃L, T⦄ ⇳*[s] ⦃L2, T2⦄ → + ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄. +/2 width=4 by bi_TC_strap/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_fpas.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_fpas.etc new file mode 100644 index 000000000..28d648e7b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_fpas.etc @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||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/substitution/fpa_fpa.ma". +include "basic_2/multiple/fpas.ma". + +(* MULTIPLE AJUSTMENT *******************************************************) + +(* Advanced properties ******************************************************) + +lemma fpas_strip: ∀L0,L1,L2,T0,T1,T2,s. ⦃L0, T0⦄ ⇳[s] ⦃L1, T1⦄ → ⦃L0, T0⦄ ⇳*[s] ⦃L2, T2⦄ → + ∃∃L,T. ⦃L1, T1⦄ ⇳*[s] ⦃L, T⦄ & ⦃L2, T2⦄ ⇳[s] ⦃L, T⦄. +/3 width=4 by fpa_conf, bi_TC_strip/ qed-. + +(* Main properties **********************************************************) + +theorem fpas_conf: ∀s. bi_confluent … (fpas s). +/3 width=4 by fpa_conf, bi_TC_confluent/ qed-. + +theorem fpas_trans: ∀s. bi_transitive … (fpas s). +/2 width=4 by bi_TC_transitive/ qed-. + +theorem fpas_canc_sn: ∀L,L1,L2,T,T1,T2,s. + ⦃L, T⦄ ⇳*[s] ⦃L1, T1⦄→ ⦃L, T⦄ ⇳*[s] ⦃L2, T2⦄ → ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄. +/3 width=4 by fpas_trans, fpas_sym/ qed-. + +theorem fpas_canc_dx: ∀L1,L2,L,T1,T2,T,s. + ⦃L1, T1⦄ ⇳*[s] ⦃L, T⦄ → ⦃L2, T2⦄ ⇳*[s] ⦃L, T⦄ → ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄. +/3 width=4 by fpas_trans, fpas_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_vector.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_vector.etc new file mode 100644 index 000000000..65e8190e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/fpas_vector.etc @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/term_vector.ma". +include "basic_2/multiple/fpas.ma". + +(* MULTIPLE VECTOR AJUSTMENT ************************************************) + +inductive fpasv (s:bool): bi_relation lenv (list term) ≝ +| fpasv_nil : ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ → fpasv s L1 (◊) L2 (◊) +| fpasv_cons: ∀L1,L2,T1s,T2s,T1,T2. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ → + fpasv s L1 T1s L2 T2s → + fpasv s L1 (T1 @ T1s) L2 (T2 @ T2s) +. + +interpretation + "multiple vector ajustment (restricted closure)" + 'RAjustStar L1 T1s s L2 T2s = (fpasv s L1 T1s L2 T2s). + +(* Basic inversion lemmas ***************************************************) + + + +(* Basic_1: was just: lifts1_flat (left to right) *) +lemma fpas_inv_applv1: ∀L1,L2,V1s,T1,X,s. ⦃L1, Ⓐ V1s.T1⦄ ⇳*[s] ⦃L2, X⦄ → + ∃∃V2s,T2. ⦃L1, V1s⦄ ⇳*[s] ⦃L2, V2s⦄ & ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ & + X = Ⓐ V2s.T2. +#L1 #L2 #V1s elim V1s -V1s +[ #T1 #X #s #H + @(ex3_2_intro … (◊) X) /2 width=3 by fpasv_nil/ (**) (* explicit constructor *) +| #V1 #V1s #IHV1s #T1 #X #s #H + elim (lifts_inv_flat1 … H) -H #V2 #Y #HV12 #HY #H destruct + elim (IHV1s … HY) -IHV1s -HY #V2s #T2 #HV12s #HT12 #H destruct + @(ex3_2_intro) [4: // |3: /2 width=2 by liftsv_cons/ |1,2: skip | // ] (**) (* explicit constructor *) +] +qed-. + +(* Basic properties *********************************************************) + +(* Basic_1: was just: lifts1_flat (right to left) *) +lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s → + ∀T1,T2. ⇧*[des] T1 ≡ T2 → + ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2. +#V1s #V2s #des #H elim H -V1s -V2s /3 width=1 by lifts_flat/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp.etc new file mode 100644 index 000000000..b9b2db820 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp.etc @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/genv.ma". +include "basic_2/multiple/fpas.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition candidate: Type[0] ≝ relation3 genv lenv term. + +definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L1,L2,T1,T2,s. ⦃L1, T1⦄ ⇳[s] ⦃L2, T2⦄ → + NF … (RR G L1) RS T1 → NF … (RR G L2) RS T2. + +definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L1,L2,T1,T2,s. ⦃L1, T1⦄ ⇳*[s] ⦃L2, T2⦄ → + NF … (RR G L1) RS T1 → NF … (RR G L2) RS T2. + +definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. + ∀G,L. ∃k. NF … (RR G L) RS (⋆k). + +definition CP2 ≝ λRP:candidate. + ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. + +(* requirements for generic computation properties *) +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 +}. + +(* Basic properties *********************************************************) + +(* Basic_1: was just: nf2_lift1 *) +lemma gcp_fpas: ∀RR,RS. CP0 RR RS → CP0s RR RS. +#RR #RS #HRR #G #L1 #L2 #T1 #T2 #s #H @(fpas_ind … H) -L2 -T2 /3 width=5 by/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp_cr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp_cr.etc new file mode 100644 index 000000000..76490987f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/gcp_cr.etc @@ -0,0 +1,185 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/aarity.ma". +include "basic_2/substitution/lift_vector.ma". +include "basic_2/computation/gcp.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition S0 ≝ λC:candidate. ∀G,L1,L2,T1,T2. ⦃L1, T1⦄ ⇳[Ⓕ] ⦃L2, T2⦄ → + C G L1 T1 → C G L2 T2. + +definition S0s ≝ λC:candidate. ∀G,L1,L2,T1,T2. ⦃L1, T1⦄ ⇳*[Ⓕ] ⦃L2, T2⦄ → + C G L1 T1 → C G L2 T2. + +(* 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 → ∀k. C G L (ⒶVs.⋆k). + +definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. + C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 → + ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i). + +definition S6 ≝ λRP,C:candidate. + ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{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 ≝ +{ s0: S0 C; + 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. ∀L,V,U. ⦃K, T⦄ ⇳*[Ⓕ] ⦃L, U⦄ → + C1 G L V → C2 G L (ⓐV.U). + +(* the reducibility candidate associated to an atomic arity *) +let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ +match A with +[ AAtom ⇒ RP +| APair B A ⇒ cfun (acr RP B) (acr RP A) +]. + +interpretation + "candidate of reducibility of an atomic arity (abstract)" + 'InEInt RP G L T A = (acr RP A G L T). + +(* Basic properties *********************************************************) + +(* Basic_1: was just: sc3_lift1 *) +lemma gcr_fpas: ∀C. S0 C → S0s C. +#C #HC #G #L1 #L2 #T1 #T2 #H @(fpas_ind … H) -L2 -T2 /3 width=5 by/ +qed. +(* +lemma rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → + RP G L V → RP G L0 V0. +#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV +@gcr_lifts /width=7 by/ +@(s0 … HRP) +qed. + +(* Basic_1: was only: sns3_lifts1 *) +lemma rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → + all … (RP G L) Vs → all … (RP G L0) V0s. +#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ +qed. +*) +(* Basic_1: was: + sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift +*) +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 +[ /3 width=4 by fpas_strap2/ +| #G #L #T #H + elim (cp1 … H1RP G L) #k #HK + lapply (H L (⋆k) T ? ?) -H // + [ @(s2 … IHB … (◊)) // + | #H @(cp2 … H1RP … k) @(s1 … IHA) // + ] +| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #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=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/ +| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #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 #k #L0 #V0 #X #des #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 rp_liftsv_all, conj/ +| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB + elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct + elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct + elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0 + >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02 + elim (drops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct + elim (lift_total W1 0 (i0 + 1)) #W2 #HW12 + elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2 + >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2 + @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/ +| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #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 (lift_total V10 0 1) #V20 #HV120 + elim (liftv_total 0 1 V10s) #V20s #HV120s + @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/ + @(HA … (des + 1)) /2 width=2 by drops_skip/ + [ @lifts_applv // + elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s + >(liftv_mono … HV12s … HV10s) -V1s // + | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ + ] +| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #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 → + ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( + ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 → + ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛 + ) → + ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. +#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #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 (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 +@(s3 … HCA … (◊)) +@(s6 … HCA … (◊) (◊)) // +[ @(HA … HL0) // +| lapply (s1 … HCB) -HCB #HCB + @(s7 … H2RP … (◊)) /2 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/etc/fpa/rajust_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/rajust_5.etc new file mode 100644 index 000000000..ef0fbc49b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/rajust_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⇳ [ break term 46 s ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'RAjust $L1 $T1 $s $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/rajuststar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/rajuststar_5.etc new file mode 100644 index 000000000..7cf9191d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/fpa/rajuststar_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⇳ * [ break term 46 s ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'RAjustStar $L1 $T1 $s $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/gcp/gcp_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/gcp/gcp_aaa.etc new file mode 100644 index 000000000..0ad8732d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/gcp/gcp_aaa.etc @@ -0,0 +1,85 @@ +(**************************************************************************) +(* ___ *) +(* ||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/multiple/lifts_lifts.ma". +include "basic_2/multiple/drops_drops.ma". +include "basic_2/static/aaa_lifts.ma". +include "basic_2/static/aaa_aaa.ma". +include "basic_2/computation/lsubc_drops.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +(* Main properties **********************************************************) + +(* Basic_1: was: sc3_arity_csubc *) +theorem acr_aaa_csubc: ∀RR,RS,RP. + gcp RR RS RP → gcr RR RS RP RP → + ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → + ∀L2. G ⊢ L2 ⫃[RP] L1 → ⦃G, L2, T⦄ ϵ[RP] 〚A〛. +#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A +[ #G #L1 #k #L2 #HL21 + lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom + lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/ +| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L2 #HL21 + lapply (acr_gcr … H1RP H2RP B) #HB + elim (lsubc_drop_O1_trans … HL21 … HLK1) -L1 #X #HLK2 #H + elim (lsubc_inv_pair2 … H) -H * + [ #K2 #HK21 #H destruct -HKV1B + lapply (drop_fwd_drop2 … HLK2) #H + elim (lift_total V1 0 (i +1)) #V #HV1 + lapply (s5 … HB ? G ? ? (◊) … HV1 HLK2) /3 width=7 by s0/ + | #K2 #V2 #A2 #HVA2 #H1V1A2 #H2V1A2 #_ #H1 #H2 destruct -IHB + lapply (aaa_mono … H2V1A2 … HKV1B) #H destruct -H2V1A2 -HKV1B + lapply (drop_fwd_drop2 … HLK2) #H + elim (lift_total V1 0 (i +1)) #V3 #HV13 + elim (lift_total V2 0 (i +1)) #V #HV2 + lapply (s5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/ -HLK2 + lapply (s7 … HB G L2 (◊)) /3 width=7 by s0/ + ] +| #a #G #L1 #V #T #B #A #_ #_ #IHB #IHA #L2 #HL21 + 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=1 by lsubc_pair/ +| #a #G #L1 #W #T #B #A #HLWB #_ #IHB #IHA #L2 #HL21 + @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ] + #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B + @(gcr_lifts … L2.ⓓⓝW.V3,T … HL32) + elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL21) -L2 #L2 #HL32 #HL21 + lapply (aaa_lifts … L2 W3 … des3 … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B + @(s0 + + @(IHA (L2. ⓛW3) … (des3 + 1)) -IHA + /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ +| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + /3 width=10 by drops_nil, lifts_nil/ +| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20 + elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct + lapply (acr_gcr … H1RP H2RP A) #HA + lapply (s7 … HA G L2 (◊)) /3 width=5 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〛. +/2 width=8 by drops_nil, lifts_nil, 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/etc/gcp/gcp_cr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/gcp/gcp_cr.etc new file mode 100644 index 000000000..d8d3bbc83 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/gcp/gcp_cr.etc @@ -0,0 +1,177 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/aarity.ma". +include "basic_2/multiple/mr2_mr2.ma". +include "basic_2/multiple/lifts_lift_vector.ma". +include "basic_2/multiple/drops_drop.ma". +include "basic_2/computation/gcp.ma". + +(* GENERIC COMPUTATION PROPERTIES *******************************************) + +definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e. + C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2. + +definition S0s ≝ λC:candidate. + ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 → + ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2. + +(* 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 → ∀k. C G L (ⒶVs.⋆k). + +definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i. + ⇩[i] L ≡ K.ⓑ{I}V1 → ⇧[0, i+1] V1 ≡ V2 → + C G L (ⒶVs.V2) → C G L (ⒶVs.#i). + +definition S6 ≝ λRP,C:candidate. + ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → + ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{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 ≝ +{ (* s0: S0 C; *) + 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. ∀V. C1 G K V → C2 G K (ⓐV.T). + +(* the reducibility candidate associated to an atomic arity *) +let rec acr (RP:candidate) (A:aarity) on A: candidate ≝ +match A with +[ AAtom ⇒ RP +| APair B A ⇒ cfun (acr RP B) (acr RP A) +]. + +interpretation + "candidate of reducibility of an atomic arity (abstract)" + 'InEInt RP G L T A = (acr RP A G L T). + +(* Basic properties *********************************************************) +(* +(* Basic_1: was: sc3_lift1 *) +lemma gcr_lifts: ∀C. S0 C → S0s C. +#C #HC #G #L1 #L2 #des #H elim H -L1 -L2 -des +[ #L #T1 #T2 #H #HT1 <(lifts_inv_nil … H) -H // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 + elim (lifts_inv_cons … H) -H /3 width=10 by/ +] +qed. +*) +axiom rp_lift: ∀RP. S0 RP. + + +axiom rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 → + RP G L V → RP G L0 V0. +(* +#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV +@gcr_lifts /width=7 by/ +@(s0 … HRP) +qed. +*) +(* Basic_1: was only: sns3_lifts1 *) +axiom rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP → + ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s → + all … (RP G L) Vs → all … (RP G L0) V0s. +(* +#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize // +#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/ +qed. +*) + +lemma gcr_lift: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀A. S0 (acr RP A). +#RR #RS #RP #H1RP #H2RP #A elim A -A /2 width=7 by rp_lift/ +#B #A #IHB #IHA #G #L2 #L1 #T1 #d #e #IH #T2 #HL21 #HT12 #V #HB +@(IHA … HL21) [3: @(lift_flat … HT12) |1: skip | + +(* Basic_1: was: + sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift +*) +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) #k #HK + lapply (H (⋆k) ?) -H + [ lapply (s2 … IHB G L (◊) … HK) // + | #H @(cp2 … H1RP … k) @(s1 … IHA) // + ] +| #G #L #Vs #HVs #T #H1T #H2T #V #HB + lapply (s1 … IHB … HB) #HV + @(s2 … IHA … (V @ Vs)) + /3 width=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/ +| #a #G #L #Vs #U #T #W #HA #V #HB + @(s3 … IHA … (V @ Vs)) /2 width=1 by/ +| #G #L #Vs #HVs #k #V #HB + lapply (s1 … IHB … HB) #HV + @(s4 … IHA … (V @ Vs)) /3 width=7 by rp_liftsv_all, conj/ +| #I #G #L #K #Vs #V1 #V2 #i #HLK #HV12 #HA #V #HB + @(s5 … IHA … (V @ Vs) … HLK HV12) /2 width=1 by/ +| #G #L #V1s #V2s #HV12s #a #W #T #HA #HW #V1 #HB + elim (lift_total V1 0 1) #V2 #HV12 + @(s6 … IHA … (V1 @ V1s) (V2 @ V2s)) /2 width=1 by liftv_cons/ + @HA @(gcr_lift … H1RP H2RP … HB … HV12) /2 width=2 by drop_drop/ +| #G #L #Vs #T #W #HA #HW #V #HB + @(s7 … IHA … (V @ Vs)) /2 width=1 by/ +] +qed. + +lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → + ∀a,G,L,W,T,B,A. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → ( + ∀V. ⦃G, L, V⦄ ϵ[RP] 〚B〛 → ⦃G, L.ⓓⓝW.V, T⦄ ϵ[RP] 〚A〛 + ) → + ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛. +#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #B #A #HW #HA #L0 #V0 #X #des #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 (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0 +lapply (s3 … HCA … a 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/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma index 4508cf6a3..bb357cd21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/drops.ma @@ -16,7 +16,7 @@ include "basic_2/notation/relations/rdropstar_3.ma". include "basic_2/notation/relations/rdropstar_4.ma". include "basic_2/substitution/drop.ma". include "basic_2/multiple/mr2_minus.ma". -include "basic_2/multiple/lifts.ma". +include "basic_2/multiple/lifts_vector.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) @@ -33,6 +33,19 @@ interpretation "iterated slicing (local environment) general" 'RDropStar des T1 T2 = (drops true des T1 T2). *) +definition l_liftable1: relation2 lenv term → predicate bool ≝ + λR,s. ∀K,T. R K T → ∀L,d,e. ⇩[s, d, e] L ≡ K → + ∀U. ⇧[d, e] T ≡ U → R L U. + +definition l_liftables1: relation2 lenv term → predicate bool ≝ + λR,s. ∀L,K,des. ⇩*[s, des] L ≡ K → + ∀T,U. ⇧*[des] T ≡ U → R K T → R L U. + +definition l_liftables1_all: relation2 lenv term → predicate bool ≝ + λR,s. ∀L,K,des. ⇩*[s, des] L ≡ K → + ∀Ts,Us. ⇧*[des] Ts ≡ Us → + all … (R K) Ts → all … (R L) Us. + (* Basic inversion lemmas ***************************************************) fact drops_inv_nil_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → des = ◊ → L1 = L2. @@ -93,4 +106,17 @@ lemma drops_skip: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] ]. qed. +lemma l1_liftable_liftables: ∀R,s. l_liftable1 R s → l_liftables1 R s. +#R #s #HR #L #K #des #H elim H -L -K -des +[ #L #T #U #H #HT <(lifts_inv_nil … H) -H // +| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2 + elim (lifts_inv_cons … H) -H /3 width=10 by/ +] +qed. + +lemma l1_liftables_liftables_all: ∀R,s. l_liftables1 R s → l_liftables1_all R s. +#R #s #HR #L #K #des #HLK #Ts #Us #H elim H -Ts -Us normalize // +#Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/ +qed. + (* Basic_1: removed theorems 1: drop1_getl_trans *) diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 643f7c5ef..91b69fc6c 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1517,6 +1517,7 @@ let predefined_classes = [ ["^"; "↑"; ] ; ["⇑"; "⇧"; "⬆"; ] ; ["⇓"; "⇩"; "⬇"; "⬊"; "➷"; ] ; + ["⇕"; "⇳"; "⬍"; ]; ["↔"; "⇔"; "⬄"; "⬌"; ] ; ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ]; ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];