From 58ede527a29e92f47321820421a3d8d0735daad8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 Jun 2018 22:54:41 +0200 Subject: [PATCH] update in ground_2 and basic_2 + advances on cpms, cprs, lprs + support for decentralized xoa --- .gitignore | 2 - matita/matita/contribs/lambdadelta/Makefile | 7 +- .../lambdadelta/basic_2/etc/scpds/scpds.etc | 17 ++ .../basic_2/rt_computation/cpms_cpms.ma | 158 +++++++----------- .../basic_2/rt_computation/cpms_lpr.ma | 39 +++-- .../basic_2/rt_computation/cprs_ctc.ma | 31 ++++ .../basic_2/rt_computation/cprs_lpr.ma | 31 ++++ .../basic_2/rt_computation/fpbs_lpxs.ma | 2 - .../basic_2/rt_computation/lprs_aaa.ma | 26 ++- .../basic_2/rt_computation/lprs_cprs.ma | 38 +++++ .../basic_2/rt_computation/lprs_ctc.ma | 30 ++++ .../basic_2/rt_computation/lprs_lpr.ma | 12 +- .../basic_2/rt_computation/lprs_lpxs.ma | 26 ++- .../basic_2/rt_computation/lpxs_lpxs.ma | 1 - .../basic_2/rt_computation/partial.txt | 4 +- .../basic_2/rt_computation/rdsx_lpxs.ma | 1 - .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../lambdadelta/ground_2/lib/functions.ma | 17 +- .../lambdadelta/ground_2/lib/ltc_ctc.ma | 42 +++++ .../ground_2/notation/xoa/ex_5_7.ma | 26 +++ .../lambdadelta/ground_2/web/ground_2_src.tbl | 3 +- .../lambdadelta/ground_2/xoa/ex_5_7.ma | 28 ++++ .../lambdadelta/ground_2/xoa2.conf.xml | 5 +- 23 files changed, 402 insertions(+), 148 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/scpds/scpds.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_ctc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/cprs_lpr.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_ctc.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/ltc_ctc.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/xoa/ex_5_7.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_7.ma diff --git a/.gitignore b/.gitignore index b6713e390..a457deb5b 100644 --- a/.gitignore +++ b/.gitignore @@ -71,7 +71,5 @@ matita/matita/contribs/lambdadelta/.depend matita/matita/contribs/lambdadelta/nodes matita/matita/contribs/lambdadelta/token matita/matita/contribs/lambdadelta/2A1 -matita/matita/contribs/lambdadelta/ground_2/xoa/xoa2.ma -matita/matita/contribs/lambdadelta/ground_2/notation/xoa/notation2.ma matita/matita/contribs/lambdadelta/*/*_probe.txt matita/matita/contribs/lambdadelta/*/web/*_sum.tbl diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 13465a4fc..0c03faa0c 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -11,7 +11,6 @@ XOA := xoa.native XOA_OPTS := ../../matita.conf.xml $(XOA_CONF) XOA2_CONF := ground_2/xoa2.conf.xml -XOA2_TARGETS := ground_2/notation/xoa/notation2.ma ground_2/xoa/xoa2.ma XOA2_OPTS := ../../matita.conf.xml $(XOA2_CONF) DEP_INPUT := .depend @@ -74,11 +73,9 @@ $(XOA_TARGETS): $(XOA_CONF) # xoa2 ####################################################################### -xoa2: $(XOA2_TARGETS) - -$(XOA2_TARGETS): $(XOA2_CONF) +xoa2: $(XOA2_CONF) @echo " EXEC $(XOA) $(XOA2_CONF)" - $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(XOA2_OPTS) + $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) -s $(XOA2_OPTS) # elim ####################################################################### diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/scpds/scpds.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/scpds/scpds.etc new file mode 100644 index 000000000..aa136af73 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/scpds/scpds.etc @@ -0,0 +1,17 @@ +(* these are superseded by confluence of cpms *) + +lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → + ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2. +#h #o #G #L #T1 #T2 #d2 * +#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1 +lapply (lstas_mono … HT10 … HT1) #H destruct // +qed-. + +(* Main properties **********************************************************) + +theorem scpds_conf_eq: ∀h,o,G,L,T0,T1,d. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T1 → + ∀T2. ⦃G, L⦄ ⊢ T0 •*➡*[h, o, d] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡* T & ⦃G, L⦄ ⊢ T2 ➡* T. +#h #o #G #L #T0 #T1 #d0 * #U1 #d1 #_ #_ #H1 #HUT1 #T2 * #U2 #d2 #_ #_ #H2 #HUT2 -d1 -d2 +lapply (lstas_mono … H1 … H2) #H destruct -h -d0 /2 width=3 by cprs_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma index 5fe790c89..a9f2d248c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpms_cpms.ma @@ -12,6 +12,8 @@ (* *) (**************************************************************************) +include "ground_2/xoa/ex_5_7.ma". +include "basic_2/rt_transition/cpm_lsubr.ma". include "basic_2/rt_computation/cpms_drops.ma". include "basic_2/rt_computation/cprs.ma". @@ -19,19 +21,6 @@ include "basic_2/rt_computation/cprs.ma". (* Main properties **********************************************************) -(* Basic_2A1: uses: lstas_scpds_trans scpds_strap2 *) -theorem cpms_trans (h) (G) (L): - ∀n1,T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T → - ∀n2,T2. ⦃G, L⦄ ⊢ T ➡*[n2, h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2. -/2 width=3 by ltc_trans/ qed-. - -(* Basic_2A1: uses: scpds_cprs_trans *) -theorem cpms_cprs_trans (n) (h) (G) (L): - ∀T1,T. ⦃G, L⦄ ⊢ T1 ➡*[n, h] T → - ∀T2. ⦃G, L⦄ ⊢ T ➡*[h] T2 → ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2. -#n #h #G #L #T1 #T #HT1 #T2 #HT2 >(plus_n_O … n) -/2 width=3 by cpms_trans/ qed-. - (* Basic_2A1: includes: cprs_bind *) theorem cpms_bind (n) (h) (G) (L): ∀I,V1,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡*[n, h] T2 → @@ -55,28 +44,6 @@ theorem cpms_appl (n) (h) (G) (L): ] qed. -lemma cpms_inv_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T & ⦃G, L⦄ ⊢ T ➡*[n2, h] T2. -#h #G #L #n1 elim n1 -n1 /2 width=3 by ex2_intro/ -#n1 #IH #n2 #T1 #T2 (plus_n_O … n) +/2 width=3 by cpms_trans/ qed-. -lemma scpds_inv_abst1: ∀h,o,a,G,L,V1,T1,U2,d. ⦃G, L⦄ ⊢ ⓛ{a}V1.T1 •*➡*[h, o, d] U2 → - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 •*➡*[h, o, d] T2 & - U2 = ⓛ{a}V2.T2. -#h #o #a #G #L #V1 #T1 #U2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct -elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct -/3 width=6 by ex4_2_intro, ex3_2_intro/ -qed-. +(* Advanced inversion lemmas ************************************************) -lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 → - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true. -#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2 -lapply (da_inv_bind … Hd1) -Hd1 #Hd1 -elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct -elim (cprs_inv_abbr1 … H2) -H2 * -[ #V2 #U2 #HV12 #HU12 #H destruct -| /3 width=6 by ex4_2_intro, ex3_intro/ +lemma cpms_inv_appl_sn (n) (h) (G) (L): + ∀V1,T1,X2. ⦃G, L⦄ ⊢ ⓐV1.T1 ➡*[n, h] X2 → + ∨∨ ∃∃V2,T2. + ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L⦄ ⊢ T1 ➡*[n, h] T2 & + X2 = ⓐV2.T2 + | ∃∃n1,n2,p,W,T. + ⦃G, L⦄ ⊢ T1 ➡*[n1, h] ⓛ{p}W.T & ⦃G, L⦄ ⊢ ⓓ{p}ⓝW.V1.T ➡*[n2, h] X2 & + n1 + n2 = n + | ∃∃n1,n2,p,V0,V2,V,T. + ⦃G, L⦄ ⊢ V1 ➡*[h] V0 & ⬆*[1] V0 ≘ V2 & + ⦃G, L⦄ ⊢ T1 ➡*[n1, h] ⓓ{p}V.T & ⦃G, L⦄ ⊢ ⓓ{p}V.ⓐV2.T ➡*[n2, h] X2 & + n1 + n2 = n. +#n #h #G #L #V1 #T1 #U2 #H +@(cpms_ind_dx … H) -U2 /3 width=5 by or3_intro0, ex3_2_intro/ +#n1 #n2 #U #U2 #_ * * +[ #V0 #T0 #HV10 #HT10 #H #HU2 destruct + elim (cpm_inv_appl1 … HU2) -HU2 * + [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5 by cpms_step_dx, or3_intro0, ex3_2_intro/ + | #p #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct + lapply (cprs_step_dx … HV10 … HV02) -V0 #HV12 + lapply (lsubr_cpm_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2 + /5 width=8 by cprs_flat_dx, cpms_bind, cpm_cpms, lsubr_beta, ex3_5_intro, or3_intro1/ + | #p #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct + /6 width=12 by cprs_step_dx, cpm_cpms, cpm_appl, cpm_bind, ex5_7_intro, or3_intro2/ + ] +| #m1 #m2 #p #W #T #HT1 #HTU #H #HU2 destruct + lapply (cpms_step_dx … HTU … HU2) -U #H + @or3_intro1 @(ex3_5_intro … HT1 H) // (**) (* auto fails *) +| #m1 #m2 #p #V2 #W2 #V #T #HV12 #HVW2 #HT1 #HTU #H #HU2 destruct + lapply (cpms_step_dx … HTU … HU2) -U #H + @or3_intro2 @(ex5_7_intro … HV12 HVW2 HT1 H) // (**) (* auto fails *) ] qed-. -lemma scpds_inv_lstas_eq: ∀h,o,G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d] T2 → - ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d] T → ⦃G, L⦄ ⊢ T ➡* T2. -#h #o #G #L #T1 #T2 #d2 * -#T0 #d1 #_ #_ #HT10 #HT02 #T #HT1 -lapply (lstas_mono … HT10 … HT1) #H destruct // +lemma cpms_inv_plus (h) (G) (L): ∀n1,n2,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n1+n2, h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡*[n1, h] T & ⦃G, L⦄ ⊢ T ➡*[n2, h] T2. +#h #G #L #n1 elim n1 -n1 /2 width=3 by ex2_intro/ +#n1 #IH #n2 #T1 #T2 (Hf i) -Hf /2 width=3 by ltc_dx/ +qed. + +(* Inversion lemmas with contextual transitive closure **********************) + +lemma ltc_inv_CTC (C) (A) (i) (f) (B) (R:relation4 C A B B): + associative … f → annulment_2 … f i → + ∀c. ltc … f … (R c) i ⊆ CTC … (λc. R c i) c. +#C #A #i #f #B #R #H1f #H2f #c #b1 #b2 +@(insert_eq_0 … i) #a #H +@(ltc_ind_dx A f B … H) -a -b2 /2 width=1 by inj/ -H1f +#a1 #a2 #b #b2 #_ #IH #Hb2 #H "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex7 (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.λ${ident x5}.λ${ident x6}.$P4) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , ident x5 , ident x6 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)" + non associative with precedence 20 + for @{ 'Ex7 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P4) }. + 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 c4ca8f6d2..baad25fc2 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 @@ -56,7 +56,8 @@ table { [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] - [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "ltc" * ] + [ "ltc" "ltc_ctc" * ] + [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_7.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_7.ma new file mode 100644 index 000000000..e98221121 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa/ex_5_7.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* This file was generated by xoa.native: do not edit *********************) + +include "basics/pts.ma". + +include "ground_2/notation/xoa/ex_5_7.ma". + +(* multiple existental quantifier (5, 7) *) + +inductive ex5_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ + | ex5_7_intro: ∀x0,x1,x2,x3,x4,x5,x6. P0 x0 x1 x2 x3 x4 x5 x6 → P1 x0 x1 x2 x3 x4 x5 x6 → P2 x0 x1 x2 x3 x4 x5 x6 → P3 x0 x1 x2 x3 x4 x5 x6 → P4 x0 x1 x2 x3 x4 x5 x6 → ex5_7 ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (5, 7)" 'Ex7 P0 P1 P2 P3 P4 = (ex5_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4). + diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml index f51bae446..8adc7626b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa2.conf.xml @@ -2,8 +2,9 @@
. - ground_2/xoa/xoa2 - ground_2/notation/xoa/notation2 + ground_2/xoa + ground_2/notation/xoa basics/pts.ma + 5 7
-- 2.39.2