From: Ferruccio Guidi Date: Thu, 7 Aug 2014 17:34:13 +0000 (+0000) Subject: - bugfixed "aacr" allows to remove historical eta-conversions X-Git-Tag: make_still_working~858 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=795ac6cc4ef54b4470b5e2fba287acca440c9c18;p=helm.git - bugfixed "aacr" allows to remove historical eta-conversions in the apparatus for strong normalization - minor bugfixes in annotations - xhtbl tables updated for the bugfixed stylesheets --- diff --git a/matita/matita/contribs/BTM/web/chc_45.tbl b/matita/matita/contribs/BTM/web/chc_45.tbl index a822c986f..187b82e7a 100644 --- a/matita/matita/contribs/BTM/web/chc_45.tbl +++ b/matita/matita/contribs/BTM/web/chc_45.tbl @@ -14,8 +14,6 @@ table { } -class "component" { 0 } +class "capitalize italic" { 0 } -class "text" { 1 } - -class "number" { 2 * } +class "right italic" { 2 * } diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 5dc025fc3..e985b7e59 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -200,30 +200,30 @@ define SUMMARY_TEMPLATE $$(SUM_$(1)): $$(MAS_$(1)) $(1)/$(1)_probe.txt $(1)/$(1)_mac.txt @printf ' SUMMARY $(1)\n' - @printf 'name "$$(basename $$(@F))"\n\n' > $$@ - @printf 'table {\n' >> $$@ - @printf ' class "gray" [ "category"\n' >> $$@ - @printf ' [ "objects" * ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "cyan" [ "sizes"\n' >> $$@ - @printf ' [ "files" "$$(S4)" ]\n' >> $$@ - @printf ' [ "characters" "$$(word 1, $$(S1))" ]\n' >> $$@ - @printf ' [ "nodes" "$$(word 3, $$(S0))" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "green" [ "propositions"\n' >> $$@ - @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ - @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ - @printf ' [ "total" "$$(P3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf ' class "yellow" [ "concepts"\n' >> $$@ - @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ - @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ - @printf ' [ "total" "$$(C3)" ]\n' >> $$@ - @printf ' ]\n' >> $$@ - @printf '}\n\n' >> $$@ - @printf 'class "component" { 0 }\n\n' >> $$@ - @printf 'class "plane" { 1 } { 3 } { 5 }\n\n' >> $$@ - @printf 'class "number" { 2 } { 4 } { 6 }\n' >> $$@ + @printf 'name "$$(basename $$(@F))"\n\n' > $$@ + @printf 'table {\n' >> $$@ + @printf ' class "gray" [ "category"\n' >> $$@ + @printf ' [ "objects" * ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "cyan" [ "sizes"\n' >> $$@ + @printf ' [ "files" "$$(S4)" ]\n' >> $$@ + @printf ' [ "characters" "$$(word 1, $$(S1))" ]\n' >> $$@ + @printf ' [ "nodes" "$$(word 3, $$(S0))" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ + @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ + @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ + @printf ' [ "total" "$$(P3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "yellow" [ "concepts"\n' >> $$@ + @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ + @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ + @printf ' [ "total" "$$(C3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf '}\n\n' >> $$@ + @printf 'class "capitalize italic" { 0 }\n\n' >> $$@ + @printf 'class "italic" { 1 } { 3 } { 5 }\n\n' >> $$@ + @printf 'class "right italic" { 2 } { 4 } { 6 }\n' >> $$@ .PHONY: $$(SUM_$(1)) endef diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index f854d14ea..29d687e7f 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -33,8 +33,8 @@ table { ] } -class "component" { 0 } +class "top" { * } -class "plane" { 1 } +class "capitalize italic" { 0 } -class "file" { 2 * } +class "italic" { 1 } diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma index 0d054da39..6bcbfe4c7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma @@ -17,6 +17,8 @@ include "basic_2/multiple/drops.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) +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. @@ -29,11 +31,11 @@ definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term. definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term. ∀G,L. ∃k. NF … (RR G L) RS (⋆k). -definition CP2 ≝ λRP:relation3 genv lenv term. +definition CP2 ≝ λRP:candidate. ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T. (* requirements for abstract computation properties *) -record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:relation3 genv lenv term) : Prop ≝ +record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝ { cp0: CP0 RR RS; cp1: CP1 RR RS; cp2: CP2 RP diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma index b95885d7f..be5351c2b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma @@ -24,7 +24,7 @@ include "basic_2/computation/lsubc_drops.ma". (* Basic_1: was: sc3_arity_csubc *) theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → + acp RR RS RP → acr RR RS RP RP → ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 → ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 → ⦃G, L2, T0⦄ ϵ[RP] 〚A〛. @@ -81,11 +81,11 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP. qed. (* Basic_1: was: sc3_arity *) -lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → +lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr 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, aacr_aaa_csubc_lifts/ qed. -lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → +lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr 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 (aacr_acr … H1RP H2RP A) #HA diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma index f5b3f6a05..1537d175c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma @@ -21,43 +21,43 @@ include "basic_2/computation/acp.ma". (* ABSTRACT COMPUTATION PROPERTIES ******************************************) -definition S0 ≝ λC:relation3 genv lenv term. ∀G,L2,L1,T1,d,e. +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:relation3 genv lenv term. +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:relation3 genv lenv term. +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:relation3 genv lenv term. +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:relation3 genv lenv term. +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:relation3 genv lenv term. +definition S4 ≝ λRP,C:candidate. ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k). -definition S5 ≝ λC:relation3 genv lenv term. ∀I,G,L,K,Vs,V1,V2,i. +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:relation3 genv lenv term. +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:relation3 genv lenv term. +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). (* properties of the abstract candidate of reducibility *) -record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3 genv lenv term) : Prop ≝ +record acr (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; @@ -68,13 +68,16 @@ record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:relation3 s7: S7 C }. -(* the abstract candidate of reducibility associated to an atomic arity *) -let rec aacr (RP:relation3 genv lenv term) (A:aarity) (G:genv) (L:lenv) on A: predicate term ≝ -λT. match A with -[ AAtom ⇒ RP G L T -| APair B A ⇒ ∀L0,V0,T0,des. - aacr RP B G L0 V0 → ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] T ≡ T0 → - aacr RP A G L0 (ⓐV0.T0) +(* 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). + +(* the candidate associated to an atomic arity *) +let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝ +match A with +[ AAtom ⇒ RP +| APair B A ⇒ cfun (aacr RP B) (aacr RP A) ]. interpretation @@ -92,7 +95,7 @@ lemma acr_lifts: ∀C. S0 C → S0s C. ] qed. -lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → +lemma rp_lifts: ∀RR,RS,RP. acr 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 @@ -101,7 +104,7 @@ lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → qed. (* Basic_1: was only: sns3_lifts1 *) -lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λG,L,T. RP G L T) → +lemma rp_liftsv_all: ∀RR,RS,RP. acr 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 // @@ -111,7 +114,7 @@ qed. (* Basic_1: was: sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift *) -lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → +lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP → ∀A. acr RR RS RP (aacr RP A). #RR #RS #RP #H1RP #H2RP #A elim A -A normalize // #B #A #IHB #IHA @mk_acr normalize @@ -119,26 +122,26 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) | #G #L #T #H elim (cp1 … H1RP G L) #k #HK lapply (H ? (⋆k) ? (⟠) ? ? ?) -H - [1,3: // |2,4: skip + [3,5: // |2,4: skip | @(s2 … IHB … (◊)) // | #H @(cp2 … H1RP … k) @(s1 … IHA) // ] -| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H +| #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, acp_lifts, cp0, lifts_simple_dx, conj/ -| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HB #HL0 #H +| #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 #HB #HL0 #H +| #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 #HB #HL0 #H +| #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 @@ -148,32 +151,32 @@ lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) 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 #HB #HL0 #H +| #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/ - [ @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/ - | @lifts_applv // + [ @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 #HB #HL0 #H +| #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 aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → +lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr 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 → + ∀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 #HB #HL0 #H +#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB lapply (aacr_acr … H1RP H2RP A) #HCA lapply (aacr_acr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma index a8eb52ab5..e4c5460d0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma @@ -140,5 +140,5 @@ qed-. pr1_head_1 pr1_head_2 pr1_comp clear_pr3_trans pr3_cflat pr3_gen_bind pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12 - pr3_iso_appl_bind pr3_iso_applv_appl_bind pr3_iso_applv_bind + pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index bb225f6c7..becbd624d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -20,7 +20,7 @@ include "basic_2/computation/cpxs_tstc.ma". (* Vector form of forward lemmas involving same top term constructor ********) -(* Basic_1: was just: nf2_iso_applv_lref *) +(* Basic_1: was just: nf2_iso_appls_lref *) lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U. #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *) @@ -60,7 +60,7 @@ elim (cpxs_inv_appl1 … H) -H * qed-. -(* Basic_1: was just: pr3_iso_applv_beta *) +(* Basic_1: was just: pr3_iso_appls_beta *) lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U → ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U. #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/ @@ -109,7 +109,7 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. -(* Basic_1: was just: pr3_iso_applv_abbr *) +(* Basic_1: was just: pr3_iso_appls_abbr *) lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U → ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U. @@ -158,7 +158,7 @@ elim (cpxs_inv_appl1 … H) -H * ] qed-. -(* Basic_1: was just: pr3_iso_applv_cast *) +(* Basic_1: was just: pr3_iso_appls_cast *) lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U → ∨∨ ⒶVs. ⓝW. T ≂ U | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma index 426ae47fa..cd28a524b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx.ma @@ -129,5 +129,5 @@ lemma csx_fwd_flat: ∀h,g,I,G,L,V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓕ{I}V.T → sn3_cdelta sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr - sn3_appl_applv sn3_bind sn3_appl_bind sn3_applv_bind + sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma index 736b21f3b..9573d288b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma @@ -21,7 +21,7 @@ include "basic_2/computation/csx_vector.ma". (* Advanced properties ******************************************************) -(* Basic_1: was just: sn3_applv_lref *) +(* Basic_1: was just: sn3_appls_lref *) lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T. #h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *) @@ -48,7 +48,7 @@ elim (cpxs_fwd_sort_vector … H) -H #H ] qed. -(* Basic_1: was just: sn3_applv_beta *) +(* Basic_1: was just: sn3_appls_beta *) lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T. #h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/ @@ -80,7 +80,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 → ] qed. -(* Basic_1: was just: sn3_applv_abbr *) +(* Basic_1: was just: sn3_appls_abbr *) lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s → ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T. @@ -99,7 +99,7 @@ elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ - ] qed. -(* Basic_1: was just: sn3_applv_cast *) +(* Basic_1: was just: sn3_appls_cast *) lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T. #h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/ @@ -116,7 +116,7 @@ elim (cpxs_fwd_cast_vector … H) -H #H ] qed. -theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (λG,L,T. ⦃G, L⦄ ⊢ ⬊*[h, g] T). +theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g). #h #g @mk_acr // [ /2 width=8 by csx_lift/ | /3 width=1 by csx_applv_cnx/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma index f45319f67..7c0a785ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma @@ -50,8 +50,8 @@ fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = 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/ -| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K1 #V #H destruct /3 width=10/ +| #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-. @@ -82,8 +82,8 @@ fact lsubc_inv_pair2_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K2,W. L2 = 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/ -| #L1 #L2 #V1 #W2 #A #HV1 #H1W2 #H2W2 #HL12 #I #K2 #W #H destruct /3 width=8/ +| #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-. @@ -99,7 +99,7 @@ lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W → (* 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/ +#RP #G #L elim L -L /2 width=1 by lsubc_pair/ qed. (* Basic_1: removed theorems 3: 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 5f75a2d9b..9b46f01f0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drop.ma @@ -42,7 +42,7 @@ qed-. (* Basic_1: was: csubc_drop_conf_rev *) lemma drop_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → + acp RR RS RP → acr RR RS RP 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 #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e 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 90a7aa041..5685fd1ef 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_drops.ma @@ -20,7 +20,7 @@ include "basic_2/computation/lsubc_drop.ma". (* Basic_1: was: csubc_drop1_conf_rev *) lemma drops_lsubc_trans: ∀RR,RS,RP. - acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → + acp RR RS RP → acr RR RS RP RP → ∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 → ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2. #RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma index 06666965b..d8dcf0e8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma @@ -19,8 +19,8 @@ include "basic_2/computation/acp_aaa.ma". (* properties concerning lenv refinement for atomic arity assignment ********) -lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λG,L,T. RP G L T) → +lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr 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/ -#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4/ +#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 aacr_aaa, lsubc_beta/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index 328d64e87..583105a8d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -52,13 +52,14 @@ n: native type annotation NAMING CONVENTIONS FOR TRANSFORMATIONS AND RELATED FORMS -- first letter +- prefix and first letter b: bi contex-sensitive for local environments c: contex-sensitive for terms f: context-freee for closures l: sn contex-sensitive for local environments r: dx contex-sensitive for local environments +s: stratified (prefix) t: context-free for terms - second letter diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl index 7d5f0649b..cbcbb5066 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl @@ -47,6 +47,6 @@ table { } ] } -class "text" { 0 } { 2 * } +class "top" { * } -class "plane" { 1 } +class "italic" { 1 } 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 55e58114b..81cd8e41d 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 @@ -101,7 +101,7 @@ table { [ { "\"big tree\" parallel computation" * } { [ "fpbg ( ⦃?,?,?⦄ >≡[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbg" * ] [ "fpbc ( ⦃?,?,?⦄ ≻≡[?,?] ⦃?,?,?⦄ )" "fpbc_fleq" + "fpbc_fpbs" * ] - [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" "fpbu_fleq" * ] + [ "fpbu ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpbu_lift" + "fpbu_lleq" + "fpbu_fleq" * ] [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fleq" + "fpbs_aaa" + "fpbs_fpbs" + "fpbs_ext" * ] } ] @@ -140,7 +140,7 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" "lpx_lleq" + "lpx_aaa" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_drop" + "lpx_frees" + "lpx_lleq" + "lpx_aaa" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_llpx_sn" + "cpx_lleq" + "cpx_cix" * ] } ] @@ -321,8 +321,8 @@ table { ] } -class "component" { 0 } +class "top" { * } -class "plane" { 1 } +class "capitalize italic" { 0 } -class "file" { 2 * } +class "italic" { 1 } diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index c5e65b0b5..6d8d7435c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -26,6 +26,6 @@ table { ] } -class "plane" { 0 } +class "top" { * } -class "file" { 1 * } +class "italic" { 0 }