From 037b48dbbc0b4373ad1e43d837ac9158787486ef Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 9 Mar 2013 17:14:31 +0000 Subject: [PATCH] - lenv refinement for stratified native validity redefined - contrib specufic web pages moved here --- matita/matita/contribs/lambdadelta/Makefile | 2 +- .../lambdadelta/apps_2/web/apps_2.ldw.xml | 52 ++++ .../lambdadelta/apps_2/web/apps_2_src.tbl | 38 +++ .../lsubsv/lsubsv.etc => dynamic/lsubsv.ma} | 32 +- .../lsubsv_ldrop.ma} | 8 +- .../lsubsv_snv.etc => dynamic/lsubsv_snv.ma} | 7 +- .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 13 + .../lambdadelta/basic_2/web/basic_2.ldw.xml | 78 +++++ .../lambdadelta/basic_2/web/basic_2_blk.tbl | 52 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 293 ++++++++++++++++++ .../lambdadelta/ground_2/xoa.conf.xml | 1 + .../contribs/lambdadelta/ground_2/xoa.ma | 8 + .../lambdadelta/ground_2/xoa_notation.ma | 10 + 13 files changed, 572 insertions(+), 22 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml create mode 100644 matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsubsv/lsubsv.etc => dynamic/lsubsv.ma} (71%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsubsv/lsubsv_ldrop.etc => dynamic/lsubsv_ldrop.ma} (91%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsubsv/lsubsv_snv.etc => dynamic/lsubsv_snv.ma} (99%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml create mode 100644 matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl create mode 100644 matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index f13eb7e21..8b6f8e6ed 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -115,7 +115,7 @@ stats: $(STTS) # summary #################################################################### define SUMMARY_TEMPLATE - TBL_$(1) := $(1)/$(1)_sum.tbl + TBL_$(1) := $(1)/web/$(1)_sum.tbl TBLS += $$(TBL_$(1)) $$(TBL_$(1)): S1 := $$(shell ls $$(MAS_$(1)) | wc -l) diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml new file mode 100644 index 000000000..394568e00 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml @@ -0,0 +1,52 @@ + + + +
Contents of the Specification
+ This specification comprises a collection of checked + applications of λδ version 2. + In particular it contains the components below. + + + Martin-Löf's Type Theory with one universe + using λδ as theory of expressions. + + + The validation algorithm for λδ as implemented in + Helena 0.8. + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + + + + The Applications directory is started. + + + The Functional component is started + inside the specification of λδ version 2. + + + The MLTT1 component is started. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + Each component contains its own notation file. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ 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 new file mode 100644 index 000000000..d5508e3d6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -0,0 +1,38 @@ +name "apps_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] + class "orange" + [ { "MLTT1" * } { + [ { "" * } { + [ "genv_primitive" "judgement" * ] + } + ] + } + ] + class "red" + [ { "functional" * } { + [ { "reduction and type machine" * } { + [ "rtm" "rtm_step ( ? ⇨ ? )" * ] + } + ] + [ { "unfold" * } { + [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * } diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma similarity index 71% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 25122262a..92ed705fe 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -21,8 +21,8 @@ inductive lsubsv (h:sh) (g:sd h): relation lenv ≝ | lsubsv_atom: lsubsv h g (⋆) (⋆) | lsubsv_pair: ∀I,L1,L2,V. lsubsv h g L1 L2 → lsubsv h g (L1. ⓑ{I} V) (L2. ⓑ{I} V) -| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → L1 ⊢ W2 ⬌* W1 → - ⦃h, L1⦄ ⊢ V1 •[g, l + 1] W1 → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 → +| lsubsv_abbr: ∀L1,L2,V1,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 → + L1 ⊢ W2 ⬌* W1 → ⦃h, L2⦄ ⊩ W2 :[g] → lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2) . @@ -36,7 +36,7 @@ fact lsubsv_inv_atom1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 = ⋆ → #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct ] qed-. @@ -46,26 +46,28 @@ lemma lsubsv_inv_atom1: ∀h,g,L2. h ⊢ ⋆ ⊩:⊑[g] L2 → L2 = ⋆. fact lsubsv_inv_pair1_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & - K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. + ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] & + h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. #h #g #L1 #L2 * -L1 -L2 [ #J #K1 #U1 #H destruct | #I #L1 #L2 #V #HL12 #J #K1 #U1 #H destruct /3 width=3/ -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=10/ +| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #HL12 #J #K1 #U1 #H destruct /3 width=9/ ] qed-. lemma lsubsv_inv_pair1: ∀h,g,I,K1,L2,V1. h ⊢ K1. ⓑ{I} V1 ⊩:⊑[g] L2 → (∃∃K2. h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓑ{I} V1) ∨ - ∃∃K2,W1,W2,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & - K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. + ∃∃K2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] & + h ⊢ K1 ⊩:⊑[g] K2 & L2 = K2. ⓛW2 & I = Abbr. /2 width=3 by lsubsv_inv_pair1_aux/ qed-. fact lsubsv_inv_atom2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L2 = ⋆ → L1 = ⋆. #h #g #L1 #L2 * -L1 -L2 [ // | #I #L1 #L2 #V #_ #H destruct -| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +| #L1 #L2 #V1 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct ] qed-. @@ -75,19 +77,21 @@ lemma lsubsv_inv_atom2: ∀h,g,L1. h ⊢ L1 ⊩:⊑[g] ⋆ → L1 = ⋆. fact lsubsv_inv_pair2_aux: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ∀I,K2,W2. L2 = K2. ⓑ{I} W2 → (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & - K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. + ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] & + h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. #h #g #L1 #L2 * -L1 -L2 [ #J #K2 #U2 #H destruct | #I #L1 #L2 #V #HL12 #J #K2 #U2 #H destruct /3 width=3/ -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=11/ +| #L1 #L2 #V1 #W1 #W2 #l #HV #HVW1 #HW21 #HW2 #HL12 #J #K2 #U2 #H destruct /3 width=9/ ] qed-. lemma lsubsv_inv_pair2: ∀h,g,I,L1,K2,W2. h ⊢ L1 ⊩:⊑[g] K2. ⓑ{I} W2 → (∃∃K1. h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓑ{I} W2) ∨ - ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & - K1 ⊢ W2 ⬌* W1 & h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. + ∃∃K1,W1,V1,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W2 ⬌* W1 & ⦃h, K2⦄ ⊩ W2 :[g] & + h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. (* Basic_forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma index 2c3381f86..55e72c775 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_ldrop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma @@ -31,11 +31,11 @@ lemma lsubsv_ldrop_O1_conf: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ | elim (IHL12 … HLK1) -L1 /3 width=3/ ] -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HW21 #HVW1 #HWV2 #_ #IHL12 #K1 #e #H +| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K1 #e #H elim (ldrop_inv_O1 … H) -H * #He #HLK1 [ destruct elim (IHL12 L1 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=6/ + <(ldrop_inv_refl … H) in HL12; -H /3 width=4/ | elim (IHL12 … HLK1) -L1 /3 width=3/ ] ] @@ -54,11 +54,11 @@ lemma lsubsv_ldrop_O1_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → <(ldrop_inv_refl … H) in HL12; -H /3 width=3/ | elim (IHL12 … HLK2) -L2 /3 width=3/ ] -| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HW21 #HVW1 #HWV2 #_ #IHL12 #K2 #e #H +| #L1 #L2 #V1 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K2 #e #H elim (ldrop_inv_O1 … H) -H * #He #HLK2 [ destruct elim (IHL12 L2 0 ?) -IHL12 // #X #HL12 #H - <(ldrop_inv_refl … H) in HL12; -H /3 width=6/ + <(ldrop_inv_refl … H) in HL12; -H /3 width=4/ | elim (IHL12 … HLK2) -L2 /3 width=3/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index e5bd9951e..f085cc3b5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubsv/lsubsv_snv.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -13,16 +13,17 @@ (**************************************************************************) include "basic_2/dynamic/lsubsv_ldrop.ma". +(* include "basic_2/dynamic/lsubsv_ssta.ma". include "basic_2/dynamic/lsubsv_cpcs.ma". - +*) (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) (* Properties concerning stratified native validity *************************) - +(* axiom lsubsv_xprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ∀T1,T2. ⦃h, L2⦄ ⊢ T1 •➡*[g] T2 → ⦃h, L1⦄ ⊢ T1 •➡*[g] T2. -(* + /3 width=3 by lsubsv_fwd_lsubss, lsubss_xprs_trans/ qed-. *) axiom lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] → diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma index 5b4df6be5..c17f7e071 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -14,6 +14,7 @@ include "basic_2/computation/dxprs_dxprs.ma". include "basic_2/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/lsubsv_snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -62,3 +63,15 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 /2 width=8/ + | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct + elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 + elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 + lapply (cprs_div … HW230 … HW10) -W30 #HW210 + lapply (ltpr_cpcs_conf … HL12 … HW210) -HW210 #HW210 + lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2 + lapply (IH1 … HW20 … HL12 W20 ?) // [ /2 width=1/ ] -HW20 #HW20 + lapply (IH1 … HT20 … (L2.ⓛW20) … HT202) [1,2: /2 width=1/ ] -IH1 -HT20 -HT202 #HT2 + elim (IH3 … HVW1 … HL12 … HV12) // [2: /2 width=1/ ] -HV1 -HVW1 -HV12 #W200 #HVW200 #H + lapply (cpcs_trans … HW210 … H) -W10 #HW200 + lapply (lsubsv_snv_trans … HT2 (L2.ⓓV2) ?) -L1 -HT2 /2 width=1/ /2 width=4/ + | \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml new file mode 100644 index 000000000..c20aa4b10 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -0,0 +1,78 @@ + + + +
System's Syntax and Behavior
+ This is a summary of the "block structure" + of the System's syntactic items and reductions. + +
+ * In terms only. + ** In terms and local environments only. + *** In global environments only. + **** Sort level k in terms only. + + +
Summary of the Specification
+ Here is a numerical acount of the specification's contents + and its timeline. + +
+ + Context-sensitive subject equivalence + for native type assignment. + + + Closure of extended context-sensitive computation + for native validity. + + + Extended context-sensitive strong normalization + for simply typed terms. + + + Confluence for context-free parallel reduction on closures. + + + Term binders polarized to control ζ reduction. + + + Context-sensitive subject equivalence + for atomic arity assignment + (anniversary milestone). + + + Context-sensitive strong normalization + for simply typed terms. + + + Support for abstract candidates of reducibility. + + + Confluence for context-sensitive parallel reduction on terms. + + + Confluence for context-free parallel reduction on terms. + + + Specification starts. + + +
Logical Structure of the Specification
+ The source files are grouped in planes and components + according to the following table. + A notation file covering the whole specification is provided. + The notation for the relations or functions introduced in each file + is shown in parentheses (? are placeholders). + +
+ +
Physical Structure of the Specification
+ The source files are grouped in directories, + one for each component. + +
+ 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 new file mode 100644 index 000000000..ed50adf79 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl @@ -0,0 +1,52 @@ +name "basic_2_blk" + +table { + class "grey" [ { "domain" * } { + [ + [ "block" ] [ "leader" ] + [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] + ] + } ] + [ { "{X | Γ ⊢ X : W}" * } { + class "wine" [ + [ "local typed abstraction *" ] [ "Γ ⊢ +λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "magenta" [ + [ "local typed declaration **" ] [ "Γ ⊢ -λW" ] + [ "ⓐV" ] [ "→β" ] [ "no" ] [ "#i" ] + ] + class "prune" [ + [ "global typed declaration ***" ] [ "Γ ⊢ pλW" ] + [ "no" ] [ "no" ] [ "no" ] [ "$p" ] + ] + class "blue" [ + [ "native type annotation *" ] [ "Γ ⊢ ⓝW" ] + [ "no" ] [ "no" ] [ "yes" ] [ "no" ] + ] + } ] + [ { "{X | Γ ⊢ X = V}" * } { + class "sky" [ + [ "local abbreviation *" ] [ "Γ ⊢ +δV" ] + [ "no" ] [ "local →δ" ] [ "yes" ] [ "#i" ] + ] + class "cyan" [ + [ "local definition **" ] [ "Γ ⊢ -δV" ] + [ "no" ] [ "local →δ" ] [ "no" ] [ "#i" ] + ] + class "water" [ + [ "global definition ***" ] [ "Γ ⊢ pδV" ] + [ "no" ] [ "global →δ" ] [ "no" ] [ "$p" ] + ] + } ] + [ { "no" * } { + class "green" [ + [ "sort ****" ] [ "Γ ⊢ ⋆k" ] + [ "no" ] [ "no" ] [ "no" ] [ "no" ] + ] + } ] +} + +class "text" { 0 } { 2 * } + +class "plane" { 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 new file mode 100644 index 000000000..1f49b9cd4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -0,0 +1,293 @@ +name "basic_2_src" + +table { + class "grey" + [ { "component" * } { + [ { "plane" * } { + [ "files" * ] + } + ] + } + ] +(* + class "wine" + [ { "examples" * } { + [ { "" * } { + [ "" * ] + } + ] + } + ] + class "magenta" + [ { "higher order dynamic typing" * } { + [ { "higher order native type assignment" * } { + [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + } + ] + } + ] +*) + class "prune" + [ { "dynamic typing" * } { +(* + [ { "local env. ref. for native type assignment" * } { + [ "lsubn ( ? ⊢ ? :⊑ ? )" "lsubn_ldrop" "lsubn_cpcs" "lsubn_nta" * ] + } + ] + [ { "native type assignment" * } { + [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ] + } + ] +*) + [ { "local env. ref. for stratified native validity" * } { + [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" "lsubsv_snv" * ] + } + ] + [ { "stratified native validity" * } { + [ "snv ( ⦃?,?⦄ ⊩ ? :[?] )" "snv_lift" + "snv_ltpss_dx" + "snv_ltpss_sn" + "snv_aaa" + "snv_ssta" + "snv_sstas" + "snv_ssta_ltpr" + "snv_ltpr" + "snv_cpcs" * ] + } + ] + } + ] + class "blue" + [ { "equivalence" * } { + [ { "focalized equivalence" * } { + [ "lfpcs ( ⦃?⦄ ⬌* ⦃?⦄ )" "lfpcs_aaa" + "lfpcs_fpcs" + "lfpcs_lfprs" + "lfpcs_lfpcs" * ] + [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ] + } + ] + [ { "local env. ref. for context-sensitive equivalence" * } { + [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ] + } + ] + [ { "context-sensitive equivalence" * } { + [ "cpcs ( ? ⊢ ? ⬌* ? )" "cpcs_ltpss_dx" + "cpcs_ltpss_sn" + "cpcs_delift" + "cpcs_aaa" + "cpcs_ltpr" + "cpcs_cprs" + "cpcs_cpcs" * ] + } + ] + } + ] + class "sky" + [ { "conversion" * } { + [ { "focalized conversion" * } { + [ "lfpc ( ⦃?⦄ ⬌ ⦃?⦄ )" "lfpc_lfpc" * ] + [ "fpc ( ⦃?,?⦄ ⬌ ⦃?,?⦄ )" "fpc_fpc" * ] + } + ] + [ { "context-sensitive conversion" * } { + [ "cpc ( ? ⊢ ? ⬌ ? )" "cpc_cpc" * ] + } + ] + } + ] + class "cyan" + [ { "computation" * } { + [ { "focalized computation" * } { + [ "lfprs ( ⦃?⦄ ➡* ⦃?⦄ )" "lfprs_aaa" + "lfprs_ltprs" + "lfprs_cprs" + "lfprs_fprs" + "lfprs_lfprs" * ] + [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] + } + ] + [ { "\"big tree\" order" * } { + [ "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ] + } + ] + [ { "decomposed extended computation" * } { + [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ] + } + ] + [ { "weakly normalizing computation" * } { + [ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ] + } + ] + [ { "strongly normalizing computation" * } { + [ "csn_vector ( ? ⊢ ⬊* ? )" "csn_cpr_vector" + "csn_tstc_vector" + "csn_aaa" * ] + [ "csn ( ? ⊢ ⬊* ? )" "csn_alt ( ? ⊢ ⬊⬊* ? )" "csn_lift" + "csn_cpr" + "csn_lfpr" * ] + } + ] + [ { "context-sensitive computation" * } { + [ "cprs (? ⊢ ? ➡* ?)" "cprs_lift" + "cprs_tpss" + "cprs_ltpss_dx" + "cprs_ltpss_sn" + "cprs_delift" + "cprs_aaa" + "cprs_ltpr" + "cprs_lfpr" + "cprs_cprs" + "cprs_lfprs" + "cprs_tstc" + "cprs_tstc_vector" * ] + } + ] + [ { "context-free computation" * } { + [ "ltprs ( ? ➡* ? )" "ltprs_alt ( ? ➡➡* ? )" "ltprs_ldrop" + "ltprs_ltprs" * ] + [ "tprs ( ? ➡* ?)" "tprs_lift" + "tprs_tprs" * ] + } + ] + [ { "local env. ref. for abstract candidates of reducibility" * } { + [ "lsubc ( ? ⊑[?] ? )" "lsubc_ldrop" + "lsubc_ldrops" + "lsubc_lsuba" * ] + } + ] + [ { "support for abstract computation properties" * } { + [ "acp" "acp_cr ( ⦃?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ] + } + ] + } + ] + class "water" + [ { "reducibility" * } { + [ { "context-sensitive focalized reduction" * } { + [ "cfpr ( ? ⊢ ⦃?,?⦄ ➡ ⦃?,?⦄ )" "cnfpr_ltpss" + "cfpr_aaa" + "cfpr_cpr" + "cfpr_cfpr" * ] + } + ] + [ { "context-free focalized reduction" * } { + [ "lfpr ( ⦃?⦄ ➡ ⦃?⦄ )" "lfpr_alt ( ⦃?⦄ ➡➡ ⦃?⦄ )" "lfpr_aaa" + "lfpr_cpr" + "lfpr_fpr" + "lfpr_lfpr" * ] + [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ] + } + ] + [ { "\"big tree\" successor" * } { + [ "ysucc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ] + } + ] + [ { "context-sensitive normal forms" * } { + [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] + } + ] + [ { "context-sensitive reduction" * } { + [ "cpr ( ? ⊢ ? ➡ ? )" "cpr_lift" + "cpr_tpss" + "cpr_ltpss_dx" + "cpr_ltpss_sn" + "cpr_delift" + "cpr_aaa" + "cpr_ltpr" + "cpr_cpr" * ] + } + ] + [ { "context-sensitive reducible forms" * } { + [ "crf ( ? ⊢ 𝐑⦃?⦄ )" "crf_append" "cif ( ? ⊢ 𝐈⦃?⦄ )" "cif_append" * ] + } + ] + [ { "context-free normal forms" * } { + [ "thnf ( 𝐇𝐍⦃?⦄ )" * ] + } + ] + [ { "context-free reduction" * } { + [ "ltpr ( ? ➡ ? )" "ltpr_ldrop" + "ltpr_tps" + "ltpr_ltpss_dx" + "ltpr_ltpss_sn" + "ltpr_aaa" + "ltpr_ltpr" * ] + [ "tpr ( ? ➡ ? )" "tpr_lift" + "tpr_tps" + "tpr_tpss" + "tpr_delift" + "tpr_tpr" * ] + } + ] + } + ] + class "green" + [ { "unwind" * } { + [ { "iterated stratified static type assignment" * } { + [ "sstas ( ⦃?,?⦄ ⊢ ? •*[?] ? )" "sstas_lift" + "sstas_ltpss_dx" + "sstas_ltpss_sn" + "sstas_aaa" + "sstas_lsubss" + "sstas_sstas" * ] + } + ] + } + ] + class "grass" + [ { "static typing" * } { + [ { "local env. ref. for stratified static type assignment" * } { + [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_lsubss" * ] + } + ] + [ { "stratified static type assignment" * } { + [ "ssta ( ⦃?,?⦄ ⊢ ? •[?,?] ? )" "ssta_lift" + "ssta_ltpss_dx" + "ssta_ltpss_sn" + "ssta_aaa" + "ssta_ssta" * ] + } + ] + [ { "local env. ref. for atomic arity assignment" * } { + [ "lsuba ( ? ⁝⊑ ? )" "lsuba_ldrop" + "lsuba_aaa" + "lsuba_lsuba" * ] + } + ] + [ { "atomic arity assignment" * } { + [ "aaa ( ? ⊢ ? ⁝ ? )" "aaa_lift" + "aaa_lifts" + "aaa_ltpss_dx" + "aaa_ltpss_sn" + "aaa_aaa" * ] + } + ] + [ { "parameters" * } { + [ "sh" "sd" * ] + } + ] + } + ] + class "yellow" + [ { "unfold" * } { + [ { "basic local env. thinning" * } { + [ "thin ( ? ▼*[?,?] ≡ ? )" "thin_ldrop" + "thin_delift" * ] + } + ] + [ { "inverse basic term relocation" * } { + [ "delift ( ? ⊢ ? ▼*[?,?] ≡ ? )" "delift_alt ( ? ⊢ ? ▼▼*[?,?] ≡ ? )" "delift_lift" + "delift_tpss" + "delift_ltpss" + "delift_delift" * ] + } + ] + [ { "partial unfold" * } { + [ "ltpss_sn ( ? ⊢ ▶*[?,?] ? )" "ltpss_sn_alt ( ? ⊢ ▶▶*[?,?] ? )" "ltpss_sn_ldrop" + "ltpss_sn_tps" + "ltpss_sn_tpss" + "ltpss_sn_ltpss_sn" * ] + [ "ltpss_dx ( ? ▶*[?,?] ? )" "ltpss_dx_ldrop" + "ltpss_dx_tps" + "ltpss_dx_tpss" + "ltpss_dx_ltpss_dx" * ] + [ "tpss ( ? ⊢ ? ▶*[?,?] ? )" "tpss_alt ( ? ⊢ ? ▶▶*[?,?] ? )" "tpss_lift" "tpss_tpss" * ] + } + ] + [ { "generic local env. slicing" * } { + [ "ldrops ( ⇩*[?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ] + } + ] + [ { "iterated restricted structural predecessor for closures" * } { + [ "frsups ( ⦃?,?⦄ ⧁* ⦃?,?⦄ )" "frsups_frsups" * ] + [ "frsupp ( ⦃?,?⦄ ⧁+ ⦃?,?⦄ )" "frsupp_frsupp" * ] + } + ] + [ { "generic term relocation" * } { + [ "lifts_vector ( ⇧*[?] ? ≡ ? )" "lifts_lift_vector" * ] + [ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ] + } + ] + [ { "support for generic relocation" * } { + [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ] + } + ] + } + ] + class "orange" + [ { "substitution" * } { + [ { "parallel substitution" * } { + [ "tps ( ? ⊢ ? ▶[?,?] ? )" "tps_lift" + "tps_tps" * ] + } + ] + [ { "global env. slicing" * } { + [ "gdrop ( ⇩[?] ? ≡ ? )" "gdrop_gdrop" * ] + } + ] + [ { "basic local env. slicing" * } { + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx" + "ldrop_sfr" + "ldrop_ldrop" * ] + } + ] + [ { "local env. ref. for substitution" * } { + [ "lsubs ( ? ≼[?,?] ? )" "(lsubs_lsubs)" "lsubs_sfr ( ≽[?,?] ? )" * ] + } + ] + [ { "restricted structural predecessor for closures" * } { + [ "frsup ( ⦃?,?⦄ ⧁ ⦃?,?⦄ )" * ] + } + ] + [ { "basic term relocation" * } { + [ "lift_vector ( ⇧[?,?] ? ≡ ? )" "lift_lift_vector" * ] + [ "lift ( ⇧[?,?] ? ≡ ? )" "lift_lift" * ] + } + ] + } + ] + class "red" + [ { "grammar" * } { + [ { "same head term form" * } { + [ "tshf ( ? ≈ ? )" "(tshf_tshf)" * ] + } + ] + [ { "same top term constructor" * } { + [ "tstc ( ? ≃ ? )" "tstc_tstc" + "tstc_vector" * ] + } + ] + [ { "closures" * } { + [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?} )" * ] + } + ] + [ { "internal syntax" * } { + [ "genv" * ] + [ "lenv" "lenv_weight ( ♯{?} )" "lenv_length ( |?| )" "lenv_append ( ? @@ ? )" "lenv_px" + "lenv_px_bi" * ] + [ "term" "term_weight ( ♯{?} )" "term_simple ( 𝐒⦃?⦄ )" "term_vector" * ] + [ "item" * ] + } + ] + [ { "external syntax" * } { + [ "aarity" * ] + } + ] + } + ] +} + +class "component" { 0 } + +class "plane" { 1 } + +class "file" { 2 * } diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index ddc63af0e..662b9e516 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -35,6 +35,7 @@ 6 5 6 6 6 7 + 7 4 7 7 3 4 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma index 06bbcb29c..8bb95ec6e 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma @@ -184,6 +184,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5). +(* multiple existental quantifier (7, 4) *) + +inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝ + | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6). + (* multiple existental quantifier (7, 7) *) inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma index 890f52739..22a565d44 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma @@ -224,6 +224,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 , non associative with precedence 20 for @{ 'Ex (λ${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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P5) }. +(* multiple existental quantifier (7, 4) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P6) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P6) }. + (* multiple existental quantifier (7, 7) *) 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 break & term 19 P5 break & term 19 P6)" -- 2.39.2