From: Ferruccio Guidi Date: Wed, 13 Mar 2013 22:11:34 +0000 (+0000) Subject: - lambdadelta: third recursive part of preservation finally proved! X-Git-Tag: make_still_working~1218 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=603c8b3cdab901c26f63b5fed2c65e49693cc9a3 - lambdadelta: third recursive part of preservation finally proved! Makefile: xoa.conf passed to probe for future use - xoa, probe: now can *really* take several configuration files --- diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index 246088727..23f208d53 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -9,6 +9,7 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) +module R = Helm_registry module US = NUri.UriSet let default_objs = US.empty @@ -19,6 +20,10 @@ let default_exclude = [] let default_net = 0 +let default_no_devel = true + +let default_no_init = true + let objs = ref default_objs let srcs = ref default_srcs @@ -27,8 +32,12 @@ let exclude = ref default_exclude let net = ref default_net -let no_devel = ref true +let no_devel = ref default_no_devel + +let no_init = ref default_no_init let clear () = + R.clear (); objs := default_objs; srcs := default_srcs; - exclude := default_exclude; net := default_net + exclude := default_exclude; net := default_net; + no_devel := default_no_devel; no_init := default_no_init diff --git a/matita/components/binaries/probe/options.mli b/matita/components/binaries/probe/options.mli index 31b22307a..2db004edc 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -17,6 +17,8 @@ val exclude: NCic.generated list ref val net: int ref -val clear: unit -> unit - val no_devel: bool ref + +val no_init: bool ref + +val clear: unit -> unit diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index fb7b4eab9..8900bbebf 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -28,9 +28,12 @@ let no_log _ _ = () let init registry = R.load_from registry; - B.init (); - C.set_trust trusted; - H.set_log_callback no_log + if !O.no_init then begin + B.init (); + C.set_trust trusted; + H.set_log_callback no_log; + O.no_init := false; + end let scan_uri devel str = M.from_string (R.get "matita.basedir") devel str; @@ -61,7 +64,7 @@ let process s = let _ = let help = "Usage: probe [ -X | | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in - let help_X = " Reset options and counters" in + let help_X = " Clear configuration, options and counters" in let help_g = " Exclude generated objects" in let help_i = " Print the total intrinsic size" in let help_p = " Exclude provided objects" in diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index de451f814..ae5bd03ab 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -9,7 +9,9 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module R = Helm_registry +module G = Arg + +module R = Helm_registry module L = Lib module A = Ast @@ -26,14 +28,19 @@ let unm_and s = let process conf = let preamble = L.get_preamble conf in - let ooch = L.open_out preamble (R.get_string "xoa.objects") in - let noch = L.open_out preamble (R.get_string "xoa.notations") in - List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); - List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex"); - List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or"); - List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and"); - close_out noch; close_out ooch + if R.has "xoa.objects" && R.has "xoa.notations" then begin + let ooch = L.open_out preamble (R.get_string "xoa.objects") in + let noch = L.open_out preamble (R.get_string "xoa.notations") in + List.iter (L.out_include ooch) (R.get_list R.string "xoa.include"); + List.iter (E.generate ooch noch) (R.get_list unm_ex "xoa.ex"); + List.iter (E.generate ooch noch) (R.get_list unm_or "xoa.or"); + List.iter (E.generate ooch noch) (R.get_list unm_and "xoa.and"); + close_out noch; close_out ooch + end let _ = - let help = "Usage: xoa [ ]*\n" in - Arg.parse [] process help + let help = "Usage: xoa [ -X | ]*\n" in + let help_X = " Clear configuration" in + Arg.parse [ + "-X" , G.Unit R.clear, help_X; + ] process help diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e96fc9b04..3e5b74eaf 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -3,24 +3,25 @@ H := @ TRIM := sed "s/ \\+$$//" -XOA_DIR := ../../../components/binaries/xoa -XOA := xoa.native -DEP_DIR := ../../../components/binaries/matitadep -DEP := matitadep.native -MAC_DIR := ../../../components/binaries/mac -MAC := mac.native -PRB_DIR := ../../../components/binaries/probe -PRB := probe.native -PRB_OPTS := ../../matita.conf.xml -g - +XOA_DIR := ../../../components/binaries/xoa +XOA := xoa.native XOA_CONF := ground_2/xoa.conf.xml XOA_TARGETS := ground_2/xoa_notation.ma ground_2/xoa.ma -ORIG := . ./orig.sh +DEP_DIR := ../../../components/binaries/matitadep +DEP := matitadep.native + +MAC_DIR := ../../../components/binaries/mac +MAC := mac.native + +PRB_DIR := ../../../components/binaries/probe +PRB := probe.native +PRB_OPTS := ../../matita.conf.xml $(XOA_CONF) -g -ORIGS := basic_2/basic_1.orig +ORIG := . ./orig.sh +ORIGS := basic_2/basic_1.orig -TAGS := all xoa orig deps stats tbls trim +TAGS := all xoa orig deps stats tbls trim PACKAGES := ground_2 basic_2 apps_2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma deleted file mode 100644 index 708c1a8c7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt.ma +++ /dev/null @@ -1,95 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reducibility/ysc.ma". -include "basic_2/computation/yprs.ma". - -(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) - -inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝ -| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ → - ygt h g L1 T1 L2 T2 -| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T -. - -interpretation "'big tree' proper parallel computation (closure)" - 'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2). - -(* Basic forvard lemmas *****************************************************) - -lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2 -/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/ -qed-. - -(* Basic properties *********************************************************) - -lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -/3 width=4/ qed. - -lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 -lapply (ygt_fwd_yprs … H1) #H0 -elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/ -qed-. - -lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2 -[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ] -qed-. - -lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 // -/2 width=4 by ygt_strap1/ -qed-. - -lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → - ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T // -/3 width=4 by ygt_strap2/ -qed-. - -lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. -/3 width=1/ qed. - -lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → - h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 -[ #H elim H // -| #T #T2 #_ #HT2 #IHT1 #HT12 - elim (term_eq_dec T1 T) #H destruct - [ -IHT1 /4 width=1/ - | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 - @(ygt_strap1 … HT1) -HT1 /2 width=1/ - ] -] -qed. - -lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → ⊥) → - h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 -[ #H elim H // -| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12 - elim (term_eq_dec T1 T) #H destruct - [ -IHT1 /3 width=2/ - | lapply (IHT1 … H) -IHT1 -H #HT1 - @(ygt_strap1 … HT1) -HT1 /2 width=2/ - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma deleted file mode 100644 index 31ab7a917..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/ygt_ygt.ma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/computation/ygt.ma". - -(* "BIG TREE" ORDER FOR CLOSURES ********************************************) - -(* Main properties **********************************************************) - -theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g). -/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma deleted file mode 100644 index 8b7e4cc98..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs.ma +++ /dev/null @@ -1,77 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/unwind/sstas.ma". -include "basic_2/reducibility/ypr.ma". -include "basic_2/computation/ltprs.ma". -include "basic_2/computation/cprs.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -definition yprs: ∀h. sd h → bi_relation lenv term ≝ - λh,g. bi_TC … (ypr h g). - -interpretation "'big tree' parallel computation (closure)" - 'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). - -(* Basic eliminators ********************************************************) - -lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → - (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → R L T → R L2 T2) → - ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L2 T2. -/3 width=7 by bi_TC_star_ind/ qed-. - -lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → - (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → R L T → R L1 T1) → - ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L1 T1. -/3 width=7 by bi_TC_star_ind_dx/ qed-. - -(* Basic properties *********************************************************) - -lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). -/2 width=1/ qed. - -lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/2 width=1/ qed. - -lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/2 width=4/ qed-. - -lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → - h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/2 width=4/ qed-. - -lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → - h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/3 width=1/ qed. - -lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/ -qed. - -lemma ltprs_yprs: ∀h,g,L1,L2,T. L1 ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄. -#h #g #L1 #L2 #T #H @(ltprs_ind … H) -L2 // /3 width=4 by ypr_ltpr, yprs_strap1/ -qed. - -lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → - h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄. -#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/ -qed. - -lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → - h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. -/3 width=4 by yprs_strap2, ypr_ltpr, cprs_yprs/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma deleted file mode 100644 index 4fd2d2a60..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/yprs_yprs.ma +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/computation/yprs.ma". - -(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) - -theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). -/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index 9979efb4e..fcd0deb29 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/equivalence/lsubse.ma". include "basic_2/dynamic/snv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) @@ -21,8 +22,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,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 → - L1 ⊢ W2 ⬌* W1 → ⦃h, L2⦄ ⊩ W2 :[g] → +| lsubsv_abbr: ∀L1,L2,V1,V2,W1,W2,l. ⦃h, L1⦄ ⊩ V1 :[g] → ⦃h, L1⦄ ⊢ V1 •[g, l+1] W1 → + L1 ⊢ W1 ⬌* W2 → ⦃h, L2⦄ ⊩ W2 :[g] → ⦃h, L2⦄ ⊢ W2 •[g, l] V2 → lsubsv h g L1 L2 → lsubsv h g (L1. ⓓV1) (L2. ⓛW2) . @@ -36,7 +37,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 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #_ #H destruct ] qed-. @@ -46,28 +47,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,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. + ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + 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 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #HL12 #J #K1 #U1 #H destruct /3 width=9/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #HL12 #J #K1 #U1 #H destruct /3 width=11/ ] 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,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. + ∃∃K2,V2,W1,W2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + 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 #W1 #W2 #l #_ #_ #_ #_ #_ #H destruct +| #L1 #L2 #V1 #V2 #W1 #W2 #l #_ #_ #_ #_ #_ #_ #H destruct ] qed-. @@ -77,31 +78,35 @@ 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,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. + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + 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 #W1 #W2 #l #HV #HVW1 #HW21 #HW2 #HL12 #J #K2 #U2 #H destruct /3 width=9/ +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV #HVW1 #HW12 #HW2 #HWV2 #HL12 #J #K2 #U2 #H destruct /3 width=11/ ] 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,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. + ∃∃K1,W1,V1,V2,l. ⦃h, K1⦄ ⊩ V1 :[g] & ⦃h, K1⦄ ⊢ V1 •[g,l+1] W1 & + K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + h ⊢ K1 ⊩:⊑[g] K2 & L1 = K1. ⓓV1 & I = Abst. /2 width=3 by lsubsv_inv_pair2_aux/ qed-. (* Basic_forward lemmas *****************************************************) +lemma lsubsv_fwd_lsubse: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → h ⊢ L1 ⊢•⊑[g] L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ /2 width=6/ +qed-. + lemma lsubsv_fwd_lsubs1: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L1|] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs1/ qed-. lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2. -#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs2/ qed-. (* Basic properties *********************************************************) @@ -112,5 +117,5 @@ qed. lemma lsubsv_cprs_trans: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. -/3 width=5 by lsubsv_fwd_lsubs2, cprs_lsubs_trans/ +/3 width=5 by lsubsv_fwd_lsubse, lsubse_cprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma new file mode 100644 index 000000000..e742fe63a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma @@ -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/dynamic/snv_cpcs.ma". +include "basic_2/dynamic/lsubsv_ssta.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties for the preservation results **********************************) + +fact sstas_lsubsv_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → + ∀L2,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T⦄ → ⦃h, L2⦄ ⊩ T :[g] → + ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀U2. ⦃h, L2⦄ ⊢ T •*[g] U2 → + ∃∃U1. ⦃h, L1⦄ ⊢ T •*[g] U1 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T #HLT0 #HT #L1 #HL12 #U2 #H @(sstas_ind … H) -U2 [ /2 width=3/ ] +#U2 #W #l #HTU2 #HU2W * #U1 #HTU1 #HU12 +lapply (IH1 … HT … HL12) // #H +lapply (snv_sstas_aux … IH2 … HTU1) // /3 width=4 by ygt_yprs_trans, lsubsv_yprs/ -H #HU1 +lapply (snv_sstas_aux … IH2 … HTU2) // #H +lapply (IH1 … H … HL12) [ /3 width=4 by ygt_yprs_trans, sstas_yprs/ ] -H #HU2 +elim (snv_fwd_ssta … HU1) #W1 #l1 #HUW1 +elim (lsubsv_ssta_trans … HU2W … HL12) -HU2W #W2 #HUW2 #HW2 +elim (ssta_ltpr_cpcs_aux … IH4 IH3 … HU1 HU2 … HUW1 … HUW2 … HU12) -HU1 -HU2 -HUW2 -HU12 // +[2,3: /4 width=4 by ygt_yprs_trans, sstas_yprs, lsubsv_yprs/ ] -L2 -L0 -T0 -U2 #H #HW12 destruct +lapply (cpcs_trans … HW12 … HW2) -W2 /3 width=4/ +qed-. + +fact dxprs_lsubsv_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → + ∀L2,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T1⦄ → ⦃h, L2⦄ ⊩ T1 :[g] → + ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → + ∃∃T. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T & L1 ⊢ T2 ➡* T. +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 #T1 #HLT0 #HT1 #L1 #HL12 #T2 * #T #HT1T #HTT2 +lapply (lsubsv_cprs_trans … HL12 … HTT2) -HTT2 #HTT2 +elim (sstas_lsubsv_aux … IH4 IH3 IH2 IH1 … HLT0 … HL12 … HT1T) // -L2 -L0 -T0 #T0 #HT10 #HT0 +lapply (cpcs_cprs_strap1 … HT0 … HTT2) -T #HT02 +elim (cpcs_inv_cprs … HT02) -HT02 /3 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma index 55e72c775..bf109cdc0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma +++ 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 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K1 #e #H +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #_ #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=4/ + <(ldrop_inv_refl … H) in HL12; -H /3 width=6/ | 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 #W1 #W2 #l #HV1 #HVW1 #HW21 #HW2 #_ #IHL12 #K2 #e #H +| #L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #HWV2 #_ #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=4/ + <(ldrop_inv_refl … H) in HL12; -H /3 width=6/ | elim (IHL12 … HLK2) -L2 /3 width=3/ ] ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma new file mode 100644 index 000000000..7928373cf --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/snv_aaa.ma". +include "basic_2/dynamic/lsubsv.ma". + +(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) + +(* Properties on local environment refinement for atomic arity assignment ***) + +lemma lsubsv_fwd_lsuba: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ⁝⊑ L2. +#h #g #L1 #L2 #H elim H -L1 -L2 // /2 width=1/ +#L1 #L2 #V1 #V2 #W1 #W2 #l #HV1 #HVW1 #HW12 #HW2 #_ #_ #HL12 +elim (snv_fwd_aaa … HV1) -HV1 #A #HV1 +elim (snv_fwd_aaa … HW2) -HW2 #B #HW2 +lapply (ssta_aaa … HV1 … HVW1) -HVW1 #H1 +lapply (lsuba_aaa_trans … HW2 … HL12) #H2 +lapply (aaa_cpcs_mono … HW12 … H1 … H2) -W1 -H2 #H destruct /2 width=3/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma index 18ca504d4..1482dd986 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma @@ -12,45 +12,49 @@ (* *) (**************************************************************************) +include "basic_2/computation/dxprs_dxprs.ma". include "basic_2/dynamic/lsubsv_ldrop.ma". +include "basic_2/dynamic/lsubsv_dxprs.ma". include "basic_2/dynamic/lsubsv_cpcs.ma". -(* -include "basic_2/dynamic/lsubsv_ssta.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-. -*) -lemma lsubsv_snv_trans: ∀h,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] → - ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g]. -#h #g #L2 #T #H elim H -L2 -T // -[ #I2 #L2 #K2 #W2 #i #HLK2 #_ #IHW2 #L1 #HL12 - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -IHW2 ] - [ #HK12 #H destruct /3 width=5/ - | #W1 #V1 #l #HV1 #_ #_ #_ #_ #H #_ destruct /2 width=5/ +fact snv_lsubsv_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → + ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_lsubsv h g L1 T1. +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L2 * * [||||*] // +[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2 + elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1 + lapply (ldrop_pair2_fwd_fw … HLK2 (#i)) -HLK2 #HLK2 + elim (lsubsv_inv_pair2 … H) -H * #K1 + [ #HK12 #H destruct /4 width=8 by snv_lref, fw_ygt/ (**) (* auto too slow without trace *) + | #W1 #V1 #V2 #l #HV1 #_ #_ #_ #_ #_ #H #_ destruct /2 width=5/ ] -| #a #I #L2 #V #T #_ #_ #IHV #IHT #L1 #HL12 /4 width=1/ -| #a #L2 #V #W #W0 #T #U #l #_ #_ #HVW #HW0 #HTU #IHV #IHT #L1 #HL12 - lapply (IHV … HL12) -IHV #HV - lapply (IHT … HL12) -IHT #HT +| #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1 + elim (snv_inv_gref … H) +| #a #I #V #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_bind … H) -H /4 width=4/ +| #V #T #HL0 #HT0 #H #L1 #HL12 destruct + elim (snv_inv_appl … H) -H #a #W #W0 #U #l #HV #HT #HVW #HW0 #HTU lapply (lsubsv_cprs_trans … HL12 … HW0) -HW0 #HW0 -(* - lapply (lsubsv_ssta_trans … HVW … HL12) -HVW #HVW - lapply (lsubsv_xprs_trans … HL12 … HTU) -HL12 -HTU /2 width=8/ -*) -| #L2 #W #T #U #l #_ #_ #HTU #HUW #IHW #IHT #L1 #HL12 - lapply (IHW … HL12) -IHW #HW - lapply (IHT … HL12) -IHT #HT + elim (lsubsv_ssta_trans … HVW … HL12) -HVW #W1 #HVW1 #HW1 + lapply (cpcs_cprs_strap1 … HW1 … HW0) -W #HW10 + elim (dxprs_lsubsv_aux … IH4 IH3 IH2 IH1 … HL12 … HTU) -IH4 -IH3 -IH2 -HTU // /2 width=1/ #X #HTU #H + elim (cprs_inv_abst1 Abst W0 … H) -H #W #U2 #HW0 #HU2 #H destruct + lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H + elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0 + lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0 + /4 width=8 by snv_appl, fw_ygt/ (**) (* auto too slow without trace *) +| #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 + elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW -(* - lapply (lsubsv_ssta_trans … HTU … HL12) -HTU #HTU --HL12 -HWU /2 width=4/ + elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0 + lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fw_ygt/ (**) (* auto too slow without trace *) ] qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma index f6ef16c40..94db2292b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma @@ -12,39 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/equivalence/cpcs_cpcs.ma". -include "basic_2/dynamic/lsubsv_ldrop.ma". +include "basic_2/equivalence/lsubse_ssta.ma". +include "basic_2/dynamic/lsubsv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) -(* Properties on stratified native type assignment **************************) +(* Properties on stratified static type assignment **************************) lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 → ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → - ∃∃U1. L1 ⊢ U2 ⬌* U1 & ⦃h, L1⦄ ⊢ T •[g,l] U1. -#h #g #L2 #T #U2 #l #H elim H -L2 -T -U2 -l -[ #L2 #k #l #Hkl #L1 #_ /3 width=3/ -| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * - [ #K1 #HK12 #H destruct - elim (IHVW2 … HK12) -K2 #W1 #HW21 #H - elim (lift_total W1 0 (i+1)) #U1 #HWU1 - lapply (ldrop_fwd_ldrop2 … HLK1) /3 width=9/ - | #K1 #V1 #W1 #l0 #_ #_ #_ #_ #_ #_ #H destruct - ] -| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #_ #HWU2 #IHWV2 #L1 #HL12 - elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubsv_inv_pair2 … H) -H * - [ #K1 #HK12 #H destruct - elim (IHWV2 … HK12) -K2 #V1 #_ #H -V2 /3 width=6/ - | #K1 #W1 #V1 #l0 #HV1 #HVW1 #HW21 #HW2 #HK12 #H #_ destruct - elim (IHWV2 … HK12) -K2 #V #_ #H - elim (lift_total W1 0 (i+1)) #U1 #HWU1 - lapply (ldrop_fwd_ldrop2 … HLK1) #HLK - @(ex2_intro … U1) - [ @(cpcs_lift … HLK … HWU2 … HWU1 HW21) - | @(ssta_ldef … HLK1 … HWU1) - (* - /3 width=9/ - *) \ No newline at end of file + ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2. +/3 width=3 by lsubsv_fwd_lsubse, lsubse_ssta_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma index 1d5f93c49..12c2bf8f5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -13,10 +13,10 @@ (**************************************************************************) include "basic_2/unwind/sstas_sstas.ma". -include "basic_2/computation/ygt.ma". include "basic_2/equivalence/cpcs_ltpr.ma". include "basic_2/dynamic/snv_ltpss_dx.ma". include "basic_2/dynamic/snv_sstas.ma". +include "basic_2/dynamic/ygt.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -36,6 +36,12 @@ definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] U1 → ⦃h, L1⦄ ⊩ U1 :[g]. +(* Properties for the preservation results **********************************) + +definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝ + λh,g,L2,T. ⦃h, L2⦄ ⊩ T :[g] → + ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → ⦃h, L1⦄ ⊩ T :[g]. + fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 → ⦃h, L1⦄ ⊩ T1 :[g] → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊩ T2 :[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 74732eab2..f3238fbd9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -14,30 +14,30 @@ 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 *************************************) (* Properties on context-free parallel reduction for local environments *****) fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH3 -IH2 -IH1 -L1 +#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] +[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1 >(tpr_inv_atom1 … H2) -X // -| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2 +| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 >(tpr_inv_atom1 … H2) -X elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1 lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/ -| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2 -IH1 +| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2 +| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #HV1 #HT1 elim (tpr_inv_bind1 … H2) -H2 * [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct @@ -52,7 +52,7 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. | #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 elim (tpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct + [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 @@ -73,7 +73,8 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. 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 + lapply (IH4 … HT2 (L2.ⓓV2) ?) -HT2 + [ (* /2 width=4/ *) + | + | /2 width=1/ + ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma new file mode 100644 index 000000000..85419d1ea --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma @@ -0,0 +1,99 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/ysc.ma". +include "basic_2/dynamic/yprs.ma". + +(* "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **********************) + +inductive ygt (h) (g) (L1) (T1): relation2 lenv term ≝ +| ygt_inj : ∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≻[g] ⦃L2, T2⦄ → + ygt h g L1 T1 L2 T2 +| ygt_step: ∀L,L2,T. ygt h g L1 T1 L T → L ➡ L2 → ygt h g L1 T1 L2 T +. + +interpretation "'big tree' proper parallel computation (closure)" + 'BTPRedStarProper h g L1 T1 L2 T2 = (ygt h g L1 T1 L2 T2). + +(* Basic forvard lemmas *****************************************************) + +lemma ygt_fwd_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 #H elim H -L2 -T2 +/3 width=4 by yprs_strap1, ysc_ypr, ypr_ltpr/ +qed-. + +(* Basic properties *********************************************************) + +lemma ysc_ygt: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +/3 width=4/ qed. + +lemma ygt_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 +lapply (ygt_fwd_yprs … H1) #H0 +elim (ypr_inv_ysc … H2) -H2 [| * #HL2 #H destruct ] /2 width=4/ +qed-. + +lemma ygt_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L1 #L #L2 #T1 #T #T2 #H1 #H2 elim H2 -L2 -T2 +[ /3 width=4 by ygt_inj, yprs_strap2/ | /2 width=3/ ] +qed-. + +lemma ygt_yprs_trans: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ >[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L1 #L #L2 #T1 #T #T2 #HT1 #HT2 @(yprs_ind … HT2) -L2 -T2 // +/2 width=4 by ygt_strap1/ +qed-. + +lemma yprs_ygt_trans: ∀h,g,L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → + ∀L2,T2. h ⊢ ⦃L, T⦄ >[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +#h #g #L1 #L #T1 #T #HT1 @(yprs_ind … HT1) -L -T // +/3 width=4 by ygt_strap2/ +qed-. + +lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) → + h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 +[ #H elim H // +| #T #T2 #_ #HT2 #IHT1 #HT12 + elim (term_eq_dec T1 T) #H destruct + [ -IHT1 /4 width=1/ + | lapply (IHT1 … H) -IHT1 -H -HT12 #HT1 + @(ygt_strap1 … HT1) -HT1 /2 width=1/ + ] +] +qed. + +lemma sstas_ygt: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → (T1 = T2 → ⊥) → + h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 +[ #H elim H // +| #T #T2 #l #_ #HT2 #IHT1 #HT12 -HT12 + elim (term_eq_dec T1 T) #H destruct + [ -IHT1 /3 width=2/ + | lapply (IHT1 … H) -IHT1 -H #HT1 + @(ygt_strap1 … HT1) -HT1 /2 width=2/ + ] +] +qed. + +lemma lsubsv_ygt: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → + h ⊢ ⦃L1, T⦄ >[g] ⦃L2, T⦄. +/4 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma new file mode 100644 index 000000000..99deeefb1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_ygt.ma @@ -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/dynamic/ygt.ma". + +(* "BIG TREE" ORDER FOR CLOSURES ********************************************) + +(* Main properties **********************************************************) + +theorem ygt_trans: ∀h,g. bi_transitive … (ygt h g). +/3 width=4 by ygt_fwd_yprs, ygt_yprs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma new file mode 100644 index 000000000..ea20e0283 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reducibility/ltpr.ma". +include "basic_2/dynamic/lsubsv.ma". + +(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) + +inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ +| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2 +| ypr_ltpr : ∀L2. L1 ➡ L2 → ypr h g L1 T1 L2 T1 +| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 +| ypr_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2 +| ypr_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → ypr h g L1 T1 L2 T1 +. + +interpretation + "'big tree' parallel reduction (closure)" + 'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). +/2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma new file mode 100644 index 000000000..30c90c43e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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/computation/ltprs.ma". +include "basic_2/dynamic/ypr.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +definition yprs: ∀h. sd h → bi_relation lenv term ≝ + λh,g. bi_TC … (ypr h g). + +interpretation "'big tree' parallel computation (closure)" + 'BTPRedStar h g L1 T1 L2 T2 = (yprs h g L1 T1 L2 T2). + +(* Basic eliminators ********************************************************) + +lemma yprs_ind: ∀h,g,L1,T1. ∀R:relation2 lenv term. R L1 T1 → + (∀L,L2,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → R L T → R L2 T2) → + ∀L2,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L2 T2. +/3 width=7 by bi_TC_star_ind/ qed-. + +lemma yprs_ind_dx: ∀h,g,L2,T2. ∀R:relation2 lenv term. R L2 T2 → + (∀L1,L,T1,T. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → R L T → R L1 T1) → + ∀L1,T1. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄ → R L1 T1. +/3 width=7 by bi_TC_star_ind_dx/ qed-. + +(* Basic properties *********************************************************) + +lemma yprs_refl: ∀h,g. bi_reflexive … (yprs h g). +/2 width=1/ qed. + +lemma ypr_yprs: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +/2 width=1/ qed. + +lemma yprs_strap1: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ ≽[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +/2 width=4/ qed-. + +lemma yprs_strap2: ∀h,g,L1,L,L2,T1,T,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L, T⦄ → + h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +/2 width=4/ qed-. + +lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → + h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +/3 width=1/ qed. + +lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/ +qed. + +lemma ltprs_yprs: ∀h,g,L1,L2,T. L1 ➡* L2 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄. +#h #g #L1 #L2 #T #H @(ltprs_ind … H) -L2 // /3 width=4 by ypr_ltpr, yprs_strap1/ +qed. + +lemma sstas_yprs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → + h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄. +#h #g #L #T1 #T2 #H @(sstas_ind … H) -T2 // /3 width=4 by ypr_ssta, yprs_strap1/ +qed. + +lemma lsubsv_yprs: ∀h,g,L1,L2,T. h ⊢ L2 ⊩:⊑[g] L1 → h ⊢ ⦃L1, T⦄ ≥[g] ⦃L2, T⦄. +/3 width=1/ qed. + +lemma ltpr_cprs_yprs: ∀h,g,L1,L2,T1,T2. L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → + h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄. +/3 width=4 by yprs_strap2, ypr_ltpr, cprs_yprs/ +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma new file mode 100644 index 000000000..96354706d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/yprs.ma". + +(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************) + +theorem yprs_trans: ∀h,g. bi_transitive … (yprs h g). +/2 width=4/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma new file mode 100644 index 000000000..d63fd745c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dynamic/ypr.ma". + +(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) + +inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ +| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2 +| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2 +| ysc_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ysc h g L1 T1 L1 T2 +| ysc_lsubsv: ∀L2. h ⊢ L2 ⊩:⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1 +. + +interpretation + "'big tree' proper parallel reduction (closure)" + 'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2). + +(* Basic properties *********************************************************) + +lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄. +#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/ +qed. + +(* Inversion lemmas on "big tree" parallel reduction for closures ***********) + +lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ → + h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ ∨ (L1 ➡ L2 ∧ T1 = T2). +#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/ +[ #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/ +| #L2 #HL21 elim (lenv_eq_dec L1 L2) #H destruct /3 width=1/ /4 width=1/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma index 9988b3d4c..58a82cd25 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma @@ -37,6 +37,10 @@ interpretation "abbreviation (local environment)" interpretation "abstraction (local environment)" 'DxAbst L T = (LPair L Abst T). +(* Basic properties *********************************************************) + +axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2). + (* Basic inversion lemmas ***************************************************) lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index 7b34b1e5b..c17f8bc2d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -340,14 +340,6 @@ notation "hvbox( ⦃ term 46 L1 ⦄ ➡ ➡ break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPRedAlt $L1 $L2 }. -notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }. - -notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }. - (* Computation **************************************************************) notation "hvbox( T1 ➡ * break term 46 T2 )" @@ -410,14 +402,6 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ • * ⬊ * break [ ter non associative with precedence 45 for @{ 'DecomposedXSN $h $g $L $T }. -notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }. - -notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }. - (* Conversion ***************************************************************) notation "hvbox( L ⊢ break term 46 T1 ⬌ break term 46 T2 )" @@ -476,6 +460,22 @@ notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ term 46 g ] break term 46 L2 non associative with precedence 45 for @{ 'CrSubEqV $h $g $L1 $L2 }. +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRed $h $g $L1 $T1 $L2 $T2 }. + +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedProper $h $g $L1 $T1 $L2 $T2 }. + +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedStar $h $g $L1 $T1 $L2 $T2 }. + +notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ > break [ term 46 g ] break ⦃ term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTPRedStarProper $h $g $L1 $T1 $L2 $T2 }. + notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )" non associative with precedence 45 for @{ 'NativeType $h $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ypr.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ypr.ma deleted file mode 100644 index 4b4122549..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ypr.ma +++ /dev/null @@ -1,35 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/static/ssta.ma". -include "basic_2/reducibility/ltpr.ma". -include "basic_2/reducibility/cpr.ma". - -(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************) - -inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝ -| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2 -| ypr_ltpr: ∀L2. L1 ➡ L2 → ypr h g L1 T1 L2 T1 -| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2 -| ypr_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ypr h g L1 T1 L1 T2 -. - -interpretation - "'big tree' parallel reduction (closure)" - 'BTPRed h g L1 T1 L2 T2 = (ypr h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ypr_refl: ∀h,g. bi_reflexive … (ypr h g). -/2 width=1/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma b/matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma deleted file mode 100644 index e0aa31061..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reducibility/ysc.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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/reducibility/ypr.ma". - -(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************) - -inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝ -| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2 -| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2 -| ysc_ssta: ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g, l + 1] T2 → ysc h g L1 T1 L1 T2 -. - -interpretation - "'big tree' proper parallel reduction (closure)" - 'BTPRedProper h g L1 T1 L2 T2 = (ysc h g L1 T1 L2 T2). - -(* Basic properties *********************************************************) - -lemma ysc_ypr: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄. -#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /2 width=1/ /2 width=2/ -qed. - -(* Inversion lemmas on "big tree" parallel reduction for closures ***********) - -lemma ypr_inv_ysc: ∀h,g,L1,L2,T1,T2. h ⊢ ⦃L1, T1⦄ ≽[g] ⦃L2, T2⦄ → - h ⊢ ⦃L1, T1⦄ ≻[g] ⦃L2, T2⦄ ∨ (L1 ➡ L2 ∧ T1 = T2). -#h #g #L1 #L2 #T1 #T2 * -L2 -T2 /3 width=1/ /3 width=2/ -#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct /3 width=1/ /4 width=1/ -qed-. 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 82f61e68c..ea981eaa5 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 @@ -39,8 +39,16 @@ table { } ] *) + [ { "\"big tree\" parallel computation" * } { + [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ] + } + ] + [ { "\"big tree\" parallel reduction" * } { + [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ] + } + ] [ { "local env. ref. for stratified native validity" * } { - [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_ssta" + "lsubsv_cpcs" + "lsubsv_snv" * ] + [ "lsubsv ( ? ⊢ ? ⊩:⊑[?] ? )" "lsubsv_ldrop" + "lsubsv_lsuba" + "lsubsv_ssta" + "lsubsv_dxprs" + "lsubsv_cpcs" + "lsubsv_snv" * ] } ] [ { "stratified native validity" * } { @@ -86,10 +94,6 @@ table { [ "fprs ( ⦃?,?⦄ ➡* ⦃?,?⦄ )" "fprs_aaa" + "fprs_fprs" * ] } ] - [ { "\"big tree\" parallel computation" * } { - [ "yprs ( ? ⊢ ⦃?,?⦄ ≥[g] ⦃?,?⦄ )" "yprs_yprs" "ygt ( ? ⊢ ⦃?,?⦄ >[g] ⦃?,?⦄ )" "ygt_ygt" * ] - } - ] [ { "decomposed extended computation" * } { [ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_ltpss_dx" + "dxprs_ltpss_sn" + "dxprs_aaa" + "dxpr_lsubss" + "dxprs_dxprs" * ] } @@ -133,10 +137,6 @@ table { [ "fpr ( ⦃?,?⦄ ➡ ⦃?,?⦄ )" "fpr_cpr" + "fpr_fpr" * ] } ] - [ { "\"big tree\" parallel reduction" * } { - [ "ypr ( ? ⊢ ⦃?,?⦄ ≽[g] ⦃?,?⦄ )" "ysc ( ? ⊢ ⦃?,?⦄ ≻[g] ⦃?,?⦄ )" * ] - } - ] [ { "context-sensitive normal forms" * } { [ "cnf ( ? ⊢ 𝐍⦃?⦄ )" "cnf_lift" + "cnf_cif" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index 662b9e516..ac5237562 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -2,12 +2,6 @@
$(MATITA_RT_BASE_DIR) -
contribs/lambdadelta/ground_2/ @@ -35,8 +29,8 @@ 6 5 6 6 6 7 - 7 4 7 7 + 8 5 3 4 3 diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma index 8bb95ec6e..f1dcd2830 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.ma @@ -184,14 +184,6 @@ 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 ≝ @@ -200,6 +192,14 @@ inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A interpretation "multiple existental quantifier (7, 7)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6). +(* multiple existental quantifier (8, 5) *) + +inductive ex8_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7:A0→A1→A2→A3→A4→Prop) : Prop ≝ + | ex8_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → P5 x0 x1 x2 x3 x4 → P6 x0 x1 x2 x3 x4 → P7 x0 x1 x2 x3 x4 → ex8_5 ? ? ? ? ? ? ? ? ? ? ? ? ? +. + +interpretation "multiple existental quantifier (8, 5)" 'Ex P0 P1 P2 P3 P4 P5 P6 P7 = (ex8_5 ? ? ? ? ? P0 P1 P2 P3 P4 P5 P6 P7). + (* multiple disjunction connective (3) *) inductive or3 (P0,P1,P2: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 22a565d44..02bb27542 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma @@ -224,16 +224,6 @@ 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)" @@ -244,6 +234,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) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.λ${ident x5}:$T5.λ${ident x6}:$T6.$P6) }. +(* multiple existental quantifier (8, 5) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 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 break & term 19 P7)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P7) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 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 break & term 19 P7)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P7) }. + (* multiple disjunction connective (3) *) notation "hvbox(∨∨ term 29 P0 break | term 29 P1 break | term 29 P2)"