From b4283c079ed7069016b8d924bbc7e08872440829 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 15 Jul 2019 19:40:22 +0200 Subject: [PATCH] =?utf8?q?additions=20and=20corrections=20for=20the=20arti?= =?utf8?q?cle=20on=20=CE=BB=CE=B4-2B?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + candidates: condition S4 removed + arity assignment: decidability proved + minor additions --- .../basic_2/rt_computation/cpxs_cnx.ma | 10 ++- .../basic_2/rt_computation/csx_cnx_vector.ma | 1 + .../basic_2/rt_computation/csx_gcp.ma | 2 +- .../basic_2/rt_computation/csx_gcr.ma | 13 +-- .../lambdadelta/static_2/static/aaa_aaa.ma | 19 +++++ .../lambdadelta/static_2/static/aaa_dec.ma | 80 +++++++++++++++++++ .../lambdadelta/static_2/static/aaa_drops.ma | 7 ++ .../lambdadelta/static_2/static/gcp.ma | 15 ++-- .../lambdadelta/static_2/static/gcp_aaa.ma | 2 +- .../lambdadelta/static_2/static/gcp_cr.ma | 15 +--- .../lambdadelta/static_2/syntax/aarity.ma | 8 ++ .../lambdadelta/static_2/web/static_2_src.tbl | 2 +- 12 files changed, 143 insertions(+), 31 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma index 6dd802001..453c91e45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_cnx.ma @@ -17,10 +17,16 @@ include "basic_2/rt_computation/cpxs.ma". (* UNBOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************) +(* Properties with normal forms *********************************************) + +lemma cpxs_cnx (h) (G) (L) (T1): + (∀T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → T1 ≛ T2) → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄. +/3 width=1 by cpx_cpxs/ qed. + (* Inversion lemmas with normal terms ***************************************) -lemma cpxs_inv_cnx1: ∀h,G,L,T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ → - T1 ≛ T2. +lemma cpxs_inv_cnx1 (h) (G) (L): + ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬈*[h] T2 → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T1⦄ → T1 ≛ T2. #h #G #L #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /5 width=9 by cnx_tdeq_trans, tdeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma index 91a7f2925..fbaee7c73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cnx_vector.ma @@ -38,5 +38,6 @@ qed. (* Advanced properties ******************************************************) +(* Note: strong normalization does not depend on this any more *) lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄. /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma index ead714a32..716032c85 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcp.ma @@ -23,7 +23,7 @@ include "basic_2/rt_computation/csx_drops.ma". theorem csx_gcp: ∀h. gcp (cpx h) tdeq (csx h). #h @mk_gcp [ normalize /3 width=13 by cnx_lifts/ -| /3 width=5 by O, cnx_sort, ex_intro/ +| /2 width=4 by cnx_sort/ | /2 width=8 by csx_lifts/ | /2 width=3 by csx_fwd_flat_dx/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma index b95725eec..a757a9374 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_gcr.ma @@ -21,12 +21,13 @@ include "basic_2/rt_computation/csx_csx_vector.ma". (* Main properties with generic candidates of reducibility ******************) theorem csx_gcr: ∀h. gcr (cpx h) tdeq (csx h) (csx h). -#h @mk_gcr // -[ /3 width=1 by csx_applv_cnx/ -|2,3,6: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/ +#h @mk_gcr +[ // +| #G #L #Vs #Hvs #T #HT #H + @(csx_applv_cnx … H) -H // (**) (* auto fails *) +| /2 width=1 by csx_applv_beta/ | /2 width=7 by csx_applv_delta/ -| #G #L #V1b #V2b #HV12b #a #V #T #H #HV - @(csx_applv_theta … HV12b) -HV12b - @csx_abbr // +| /3 width=3 by csx_applv_theta, csx_abbr/ +| /2 width=1 by csx_applv_cast/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma index bd1eb91a2..968112846 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_aaa.ma @@ -36,3 +36,22 @@ theorem aaa_mono: ∀G,L,T,A1. ⦃G,L⦄ ⊢ T ⁝ A1 → ∀A2. ⦃G,L⦄ ⊢ T elim (aaa_inv_cast … H) -H /2 width=1 by/ ] qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma aaa_aaa_inv_appl (G) (L) (V) (T) (B) (X): + ∀A. ⦃G,L⦄ ⊢ ⓐV.T ⁝ A → ⦃G,L⦄ ⊢ V ⁝ B → ⦃G,L⦄⊢ T ⁝ X → ②B.A = X. +#G #L #V #T #B #X #A #H #H1V #H1T +elim (aaa_inv_appl … H) -H #B0 #H2V #H2T +lapply (aaa_mono … H2V … H1V) -V #H destruct +lapply (aaa_mono … H2T … H1T) -G -L -T // +qed-. + +lemma aaa_aaa_inv_cast (G) (L) (U) (T) (B) (A): + ∀X. ⦃G,L⦄ ⊢ ⓝU.T ⁝ X → ⦃G,L⦄ ⊢ U ⁝ B → ⦃G,L⦄⊢ T ⁝ A → ∧∧ B = X & A = X. +#G #L #U #T #B #A #X #H #H1U #H1T +elim (aaa_inv_cast … H) -H #H2U #H2T +lapply (aaa_mono … H1U … H2U) -U #HB +lapply (aaa_mono … H1T … H2T) -G -L -T #HA +/2 width=1 by conj/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma new file mode 100644 index 000000000..045657326 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_dec.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "static_2/static/aaa_drops.ma". +include "static_2/static/aaa_aaa.ma". + +(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************) + +(* Main properties **********************************************************) + +theorem aaa_dec (G) (L) (T): Decidable (∃A. ⦃G,L⦄ ⊢ T ⁝ A). +#G #L #T @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T +#G0 #L0 #T0 #IH #G #L * * [||| #p * | * ] +[ #s #HG #HL #HT destruct -IH + /3 width=2 by aaa_sort, ex_intro, or_introl/ +| #i #HG #HL #HT destruct + elim (drops_F_uni L i) [| * * #I [| #V ] #K ] #HLK + [1,2: -IH + @or_intror * #A #H + elim (aaa_inv_lref_drops … H) -H #J #Y #X #HLY #_ -G -A + lapply (drops_mono … HLY … HLK) -L -i #H destruct + | elim (IH G K V) -IH [3: /2 width=2 by fqup_lref/ ] + [ * /4 width=6 by aaa_lref_drops, ex_intro, or_introl/ + | #H0 @or_intror * #A #H + lapply (aaa_pair_inv_lref … H … HLK) -I -L -i + /3 width=2 by ex_intro/ + ] + ] +| #l #HG #HL #HT destruct -IH + @or_intror * #A #H + @(aaa_inv_gref … H) +| #V #T #HG #HL #HT destruct + elim (IH G L V) [ * #B #HB | #HnB | // ] + [ elim (IH G (L.ⓓV) T) [ * #A #HA | #HnA | // ] ] -IH + [ /4 width=2 by aaa_abbr, ex_intro, or_introl/ ] + @or_intror * #A #H + elim (aaa_inv_abbr … H) -H #B0 #HB0 #HA0 + /3 width=2 by ex_intro/ +| #W #T #HG #HL #HT destruct + elim (IH G L W) [ * #B #HB | #HnB | // ] + [ elim (IH G (L.ⓛW) T) [ * #A #HA | #HnA | // ] ] -IH + [ /4 width=2 by aaa_abst, ex_intro, or_introl/ ] + @or_intror * #A #H + elim (aaa_inv_abst … H) -H #B0 #A0 #HB0 #HA0 #H destruct + /3 width=2 by ex_intro/ +| #V #T #HG #HL #HT destruct + elim (IH G L V) [ * #B #HB | #HnB | // ] + [ elim (IH G L T) [ * #X #HX | #HnX | // ] ] -IH + [ elim (is_apear_dec B X) [ * #A #H destruct | #HnX ] + [ /4 width=4 by aaa_appl, ex_intro, or_introl/ ] + ] + @or_intror * #A #H + [ lapply (aaa_aaa_inv_appl … H HB HX) -G -L -V -T + |*: elim (aaa_inv_appl … H) -H #B0 #HB0 #HA0 + ] + /3 width=2 by ex_intro/ +| #U #T #HG #HL #HT destruct + elim (IH G L U) [ * #B #HB | #HnB | // ] + [ elim (IH G L T) [ * #A #HA | #HnA | // ] ] -IH + [ elim (eq_aarity_dec B A) [ #H destruct | #HnA ] + [ /4 width=3 by aaa_cast, ex_intro, or_introl/ ] + ] + @or_intror * #X #H + [ elim (aaa_aaa_inv_cast … H HB HA) -G -L -U -T + |*: elim (aaa_inv_cast … H) -H #HU #HT + ] + /3 width=2 by ex_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma index b006c2d21..b04f0c05f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa_drops.ma @@ -43,6 +43,13 @@ lemma aaa_inv_lref_drops: ∀G,A,i,L. ⦃G,L⦄ ⊢ #i ⁝ A → ] qed-. +lemma aaa_pair_inv_lref (G) (L) (i): + ∀A. ⦃G,L⦄ ⊢ #i ⁝ A → ∀I,K,V. ⬇*[i] L ≘ K.ⓑ{I}V → ⦃G,K⦄ ⊢ V ⁝ A. +#G #L #i #A #H #I #K #V #HLK +elim (aaa_inv_lref_drops … H) -H #J #Y #X #HLY #HX +lapply (drops_mono … HLY … HLK) -L -i #H destruct // +qed-. + (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: aaa_lift *) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma index 569152d1e..73cfc105e 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp.ma @@ -17,21 +17,18 @@ include "static_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 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 CP0 (RR) (RS) ≝ ∀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 CP1 (RR) (RS) ≝ ∀G,L,s. nf RR RS G L (⋆s). -definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G). +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. +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 *) diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma index d1dc57ece..7fa84f9fb 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma @@ -31,7 +31,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. 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/ + lapply (s2 … HAtom G L2 (Ⓔ)) /3 width=7 by cp1, simple_atom/ | #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 diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma index 10d8fa4b1..d13387c3f 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma @@ -28,16 +28,13 @@ definition S1 ≝ λRP,C:candidate. (* 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). + ∀T. 𝐒⦃T⦄ → nf RR RS G L 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). @@ -54,7 +51,6 @@ record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate { 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 @@ -99,12 +95,14 @@ qed-. (* Basic_1: was: sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast *) +(* Note: one sort must exist *) 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 + letin s ≝ 0 (* one sort must exist *) + lapply (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/ @@ -117,11 +115,6 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → elim (lifts_inv_flat1 … H0) -H0 #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 #X0 #HV0s #H0 #H destruct - >(lifts_inv_sort1 … H0) -X0 - 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 #X0 #HV0s #H0 #H destruct elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma index 89199fabb..db3820964 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma @@ -72,3 +72,11 @@ lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2). ] ] qed-. + +lemma is_apear_dec (B) (X): Decidable (∃A. ②B.A = X). +#B * [| #X #A ] +[| elim (eq_aarity_dec X B) #HX ] +[| /3 width=2 by ex_intro, or_introl/ ] +@or_intror * #A #H destruct +/2 width=1 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl index 723104f7b..2df44f0d2 100644 --- a/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/static_2/web/static_2_src.tbl @@ -27,7 +27,7 @@ table { ] [ { "atomic arity assignment" * } { [ [ "restricted refinement for lenvs" ] "lsuba" + "( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_rdeq" + "aaa_fdeq" + "aaa_aaa" * ] + [ [ "for terms" ] "aaa" + "( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_rdeq" + "aaa_fdeq" + "aaa_aaa" + "aaa_dec" * ] } ] [ { "degree-based equivalence" * } { -- 2.39.2