From 8ff4315142253a1a0478b67c07dddf70c36f50cd Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 16 Mar 2013 22:24:19 +0000 Subject: [PATCH] - lambdadelta: last recursive part of preservation finally proved! some notational changes - BTM: one file was missing - probe: now sources and objects not having a .ma file are deleted --- matita/components/binaries/probe/engine.ml | 5 - .../components/binaries/probe/matitaList.ml | 8 +- .../components/binaries/probe/matitaRemove.ml | 31 ++++++ .../binaries/probe/matitaRemove.mli | 12 ++ matita/components/binaries/probe/options.ml | 6 +- matita/components/binaries/probe/options.mli | 2 + matita/components/binaries/probe/probe.ml | 9 +- matita/matita/contribs/BTM/web/BTM.ldw.xml | 15 +++ .../lambdadelta/basic_2/computation/dxprs.ma | 2 +- .../basic_2/computation/dxprs_dxprs.ma | 14 ++- .../basic_2/computation/dxprs_lift.ma | 2 +- .../lambdadelta/basic_2/dynamic/lsubsv.ma | 30 ++--- .../basic_2/dynamic/lsubsv_dxprs.ma | 2 +- .../basic_2/dynamic/lsubsv_ssta.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv.ma | 16 +-- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 24 ++-- .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 40 ++++++- .../basic_2/dynamic/snv_ssta_ltpr.ma | 6 +- .../lambdadelta/basic_2/dynamic/snv_sstas.ma | 2 +- .../lambdadelta/basic_2/dynamic/ypr.ma | 2 +- .../lambdadelta/basic_2/dynamic/ysc.ma | 2 +- .../basic_2/equivalence/lsubse_ldrop.ma | 65 ----------- .../equivalence/{lsubse.ma => lsubss.ma} | 78 ++++++------- .../{lsubse_cpcs.ma => lsubss_cpcs.ma} | 8 +- .../lsubss_ldrop.ma} | 14 +-- .../{lsubse_ssta.ma => lsubss_ssta.ma} | 20 ++-- .../basic_2/etc/lsubss/dxprs_lsubss.etc | 26 ----- .../lambdadelta/basic_2/etc/lsubss/lsubss.etc | 105 ------------------ .../basic_2/etc/lsubss/lsubss_lsubss.etc | 36 ------ .../basic_2/etc/lsubss/lsubss_ssta.etc | 69 ------------ .../basic_2/etc/lsubss/sstas_lsubss.etc | 30 ----- .../contribs/lambdadelta/basic_2/notation.ma | 16 +-- .../lambdadelta/basic_2/static/ssta.ma | 56 +++++----- .../lambdadelta/basic_2/static/ssta_aaa.ma | 2 +- .../lambdadelta/basic_2/static/ssta_lift.ma | 12 +- .../basic_2/static/ssta_ltpss_dx.ma | 20 ++-- .../basic_2/static/ssta_ltpss_sn.ma | 12 +- .../lambdadelta/basic_2/static/ssta_ssta.ma | 4 +- .../lambdadelta/basic_2/unwind/sstas.ma | 10 +- .../lambdadelta/basic_2/unwind/sstas_lift.ma | 4 +- .../lambdadelta/basic_2/unwind/sstas_sstas.ma | 4 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 4 + .../lambdadelta/basic_2/web/basic_2_src.tbl | 10 +- .../lambdadelta/ground_2/xoa.conf.xml | 3 - 44 files changed, 311 insertions(+), 535 deletions(-) create mode 100644 matita/components/binaries/probe/matitaRemove.ml create mode 100644 matita/components/binaries/probe/matitaRemove.mli create mode 100644 matita/matita/contribs/BTM/web/BTM.ldw.xml delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/equivalence/lsubse_ldrop.ma rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{lsubse.ma => lsubss.ma} (54%) rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{lsubse_cpcs.ma => lsubss_cpcs.ma} (83%) rename matita/matita/contribs/lambdadelta/basic_2/{etc/lsubss/lsubss_ldrop.etc => equivalence/lsubss_ldrop.ma} (89%) rename matita/matita/contribs/lambdadelta/basic_2/equivalence/{lsubse_ssta.ma => lsubss_ssta.ma} (77%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/dxprs_lsubss.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_lsubss.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc diff --git a/matita/components/binaries/probe/engine.ml b/matita/components/binaries/probe/engine.ml index 55936e542..5117f57fc 100644 --- a/matita/components/binaries/probe/engine.ml +++ b/matita/components/binaries/probe/engine.ml @@ -55,8 +55,3 @@ let get_uri str = aux (F.dirname bdir) (F.concat (F.basename bdir) file) in aux dir file -(* - - let bpath = F.dirname str ^ "/" in - bpath, buri -*) diff --git a/matita/components/binaries/probe/matitaList.ml b/matita/components/binaries/probe/matitaList.ml index 7af98d59c..9f66bb6d6 100644 --- a/matita/components/binaries/probe/matitaList.ml +++ b/matita/components/binaries/probe/matitaList.ml @@ -38,11 +38,17 @@ let add_src devel path = let str = F.concat "cic:" path ^ "/" in O.srcs := US.add (U.uri_of_string str) !O.srcs +let add_remove base path = + O.remove := F.concat base path :: !O.remove + let rec scan_entry base devel path = if F.check_suffix path ".con.ng" then add_obj path else if F.check_suffix path ".ind.ng" then add_obj path else if F.check_suffix path ".var.ng" then add_obj path else - if F.check_suffix path ".ng" then add_src devel path else + if F.check_suffix path ".ng" then + if src_exists (F.chop_extension devel ^ ".ma") + then add_src devel path else add_remove base path + else if src_exists devel || src_exists (devel ^ ".ma") then let files = Y.readdir (F.concat base path) in let map base file = scan_entry base (F.concat devel file) (F.concat path file) in diff --git a/matita/components/binaries/probe/matitaRemove.ml b/matita/components/binaries/probe/matitaRemove.ml new file mode 100644 index 000000000..1ef87a5ca --- /dev/null +++ b/matita/components/binaries/probe/matitaRemove.ml @@ -0,0 +1,31 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +module A = Array +module F = Filename +module Y = Sys +module U = Unix + +module O = Options + +let remove_dir dir = + if Y.file_exists dir then begin + let map name = Y.remove (F.concat dir name) in + A.iter map (Y.readdir dir); + U.rmdir dir (* Sys.remove does not seem to remove empty directories *) + end + +let objects () = + let map name = + Y.remove name; + remove_dir (F.chop_extension name) + in + List.iter map !O.remove diff --git a/matita/components/binaries/probe/matitaRemove.mli b/matita/components/binaries/probe/matitaRemove.mli new file mode 100644 index 000000000..7e45d9082 --- /dev/null +++ b/matita/components/binaries/probe/matitaRemove.mli @@ -0,0 +1,12 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +val objects: unit -> unit diff --git a/matita/components/binaries/probe/options.ml b/matita/components/binaries/probe/options.ml index 23f208d53..4c3c51d12 100644 --- a/matita/components/binaries/probe/options.ml +++ b/matita/components/binaries/probe/options.ml @@ -16,6 +16,8 @@ let default_objs = US.empty let default_srcs = US.empty +let default_remove = [] + let default_exclude = [] let default_net = 0 @@ -28,6 +30,8 @@ let objs = ref default_objs let srcs = ref default_srcs +let remove = ref default_remove + let exclude = ref default_exclude let net = ref default_net @@ -38,6 +42,6 @@ let no_init = ref default_no_init let clear () = R.clear (); - objs := default_objs; srcs := default_srcs; + objs := default_objs; srcs := default_srcs; remove := default_remove; 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 2db004edc..3e9789c76 100644 --- a/matita/components/binaries/probe/options.mli +++ b/matita/components/binaries/probe/options.mli @@ -13,6 +13,8 @@ val objs: NUri.UriSet.t ref val srcs: NUri.UriSet.t ref +val remove: string list ref + val exclude: NCic.generated list ref val net: int ref diff --git a/matita/components/binaries/probe/probe.ml b/matita/components/binaries/probe/probe.ml index 8900bbebf..55b942cc1 100644 --- a/matita/components/binaries/probe/probe.ml +++ b/matita/components/binaries/probe/probe.ml @@ -19,6 +19,7 @@ module H = HLog module O = Options module M = MatitaList +module D = MatitaRemove module S = NCicScan module E = Engine @@ -62,6 +63,9 @@ let process s = else if E.is_registry s then init s else scan_from s +let clear () = + D.objects (); O.clear () + let _ = let help = "Usage: probe [ -X | | -gp | HELM (base)uri | -i | -on | os | -sn | -ss ]*" in let help_X = " Clear configuration, options and counters" in @@ -73,7 +77,7 @@ let _ = let help_sn = " Print the number of sources" in let help_ss = " Print the list of sources" in A.parse [ - "-X" , A.Unit O.clear, help_X; + "-X" , A.Unit clear, help_X; "-g" , A.Unit set_g, help_g; "-i" , A.Unit out_i, help_i; "-on", A.Unit out_on, help_on; @@ -81,4 +85,5 @@ let _ = "-p" , A.Unit set_p, help_p; "-sn", A.Unit out_sn, help_sn; "-ss", A.Unit out_ss, help_ss; - ] process help + ] process help; + D.objects () diff --git a/matita/matita/contribs/BTM/web/BTM.ldw.xml b/matita/matita/contribs/BTM/web/BTM.ldw.xml new file mode 100644 index 000000000..32ee158a1 --- /dev/null +++ b/matita/matita/contribs/BTM/web/BTM.ldw.xml @@ -0,0 +1,15 @@ + + + +
Character classes
+ This table shows how the first 45 positive integers + are distributed in the four classes. + + + +
+ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma index 90663d932..4656a1595 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma @@ -40,6 +40,6 @@ lemma dxprs_strap1: ∀h,g,L,T1,T,T2. qed. lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l. - ⦃h, L⦄ ⊢ T1 •[g, l+1] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. + ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. #h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma index c0aff4efb..9d051adaa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/unwind/sstas_sstas.ma". -include "basic_2/computation/cprs_cprs.ma". +include "basic_2/computation/cprs_lfprs.ma". include "basic_2/computation/dxprs.ma". (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************) @@ -31,3 +31,15 @@ lemma sstas_dxprs_trans: ∀h,g,L,T1,T,T2. #h #g #L #T1 #T #T2 #HT1 * #T0 #HT0 #HT02 lapply (sstas_trans … HT1 … HT0) -T /2 width=3/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma dxprs_inv_abbr_abst: ∀h,g,a1,a2,L,V1,W2,T1,T2. ⦃h, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[g] ⓛ{a2}W2.T2 → + ∃∃T. ⦃h, L.ⓓV1⦄ ⊢ T1 •*➡*[g] T & ⇧[0, 1] ⓛ{a2}W2.T2 ≡ T & a1 = true. +#h #g #a1 #a2 #L #V1 #W2 #T1 #T2 * #X #H1 #H2 +elim (sstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct +elim (cprs_inv_abbr1 … H2) -H2 * +[ #V2 #U2 #HV12 #HU12 #H destruct +| /3 width=3/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma index 628563cf4..eaa73f345 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_lift.ma @@ -30,7 +30,7 @@ qed-. (* Advanced properties ******************************************************) -lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] T → +lemma ssta_cprs_dxprs: ∀h,g,L,T1,T,T2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma index fcd0deb29..7958de918 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/equivalence/lsubse.ma". +include "basic_2/equivalence/lsubss.ma". include "basic_2/dynamic/snv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) @@ -22,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,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_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) . @@ -47,8 +47,8 @@ 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,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 & + ∃∃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 @@ -59,8 +59,8 @@ 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,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 & + ∃∃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-. @@ -78,8 +78,8 @@ 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 & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + ∃∃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 @@ -90,23 +90,23 @@ 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 & - K1 ⊢ W1 ⬌* W2 & ⦃h, K2⦄ ⊩ W2 :[g] & ⦃h, K2⦄ ⊢ W2 •[g,l] V2 & + ∃∃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. +lemma lsubsv_fwd_lsubss: ∀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. -/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs1/ +/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs1/ qed-. lemma lsubsv_fwd_lsubs2: ∀h,g,L1,L2. h ⊢ L1 ⊩:⊑[g] L2 → L1 ≼[0, |L2|] L2. -/3 width=3 by lsubsv_fwd_lsubse, lsubse_fwd_lsubs2/ +/3 width=3 by lsubsv_fwd_lsubss, lsubss_fwd_lsubs2/ qed-. (* Basic properties *********************************************************) @@ -117,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_lsubse, lsubse_cprs_trans/ +/3 width=5 by lsubsv_fwd_lsubss, lsubss_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 index e742fe63a..f77bc41eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_dxprs.ma @@ -33,7 +33,7 @@ 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 (snv_fwd_ssta … HU1) #l1 #W1 #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 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 94db2292b..b85b4a8fa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma @@ -12,15 +12,15 @@ (* *) (**************************************************************************) -include "basic_2/equivalence/lsubse_ssta.ma". +include "basic_2/equivalence/lsubss_ssta.ma". include "basic_2/dynamic/lsubsv.ma". (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE VALIDITY **************) (* Properties on stratified static type assignment **************************) -lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g,l] U2 → +lemma lsubsv_ssta_trans: ∀h,g,L2,T,U2,l. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ → ∀L1. h ⊢ L1 ⊩:⊑[g] L2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T •[g,l] U1 & L1 ⊢ U1 ⬌* U2. -/3 width=3 by lsubsv_fwd_lsubse, lsubse_ssta_trans/ + ∃∃U1. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ & L1 ⊢ U1 ⬌* U2. +/3 width=3 by lsubsv_fwd_lsubss, lsubss_ssta_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index 538de0334..4eb644013 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -22,10 +22,10 @@ inductive snv (h:sh) (g:sd h): lenv → predicate term ≝ | snv_lref: ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → snv h g K V → snv h g L (#i) | snv_bind: ∀a,I,L,V,T. snv h g L V → snv h g (L.ⓑ{I}V) T → snv h g L (ⓑ{a,I}V.T) | snv_appl: ∀a,L,V,W,W0,T,U,l. snv h g L V → snv h g L T → - ⦃h, L⦄ ⊢ V •[g, l + 1] W → L ⊢ W ➡* W0 → + ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ → L ⊢ W ➡* W0 → ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U → snv h g L (ⓐV.T) | snv_cast: ∀L,W,T,U,l. snv h g L W → snv h g L T → - ⦃h, L⦄ ⊢ T •[g, l + 1] U → L ⊢ U ⬌* W → snv h g L (ⓝW.T) + ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → L ⊢ U ⬌* W → snv h g L (ⓝW.T) . interpretation "stratified native validity (term)" @@ -78,7 +78,7 @@ lemma snv_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊩ ⓑ{a,I}V.T :[g] → fact snv_inv_appl_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀V,T. X = ⓐV.T → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & - ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & + ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 & ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. #h #g #L #X * -L -X [ #L #k #V #T #H destruct @@ -91,13 +91,13 @@ qed. lemma snv_inv_appl: ∀h,g,L,V,T. ⦃h, L⦄ ⊩ ⓐV.T :[g] → ∃∃a,W,W0,U,l. ⦃h, L⦄ ⊩ V :[g] & ⦃h, L⦄ ⊩ T :[g] & - ⦃h, L⦄ ⊢ V •[g, l + 1] W & L ⊢ W ➡* W0 & + ⦃h, L⦄ ⊢ V •[g] ⦃l+1, W⦄ & L ⊢ W ➡* W0 & ⦃h, L⦄ ⊢ T •*➡*[g] ⓛ{a}W0.U. /2 width=3/ qed-. fact snv_inv_cast_aux: ∀h,g,L,X. ⦃h, L⦄ ⊩ X :[g] → ∀W,T. X = ⓝW.T → ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & - ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W. + ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W. #h #g #L #X * -L -X [ #L #k #W #T #H destruct | #I #L #K #V #i #_ #_ #W #T #H destruct @@ -109,15 +109,15 @@ qed. lemma snv_inv_cast: ∀h,g,L,W,T. ⦃h, L⦄ ⊩ ⓝW.T :[g] → ∃∃U,l. ⦃h, L⦄ ⊩ W :[g] & ⦃h, L⦄ ⊩ T :[g] & - ⦃h, L⦄ ⊢ T •[g, l + 1] U & L ⊢ U ⬌* W. + ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ & L ⊢ U ⬌* W. /2 width=3/ qed-. (* Basic forward lemmas *****************************************************) -lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃h, L⦄ ⊢ T •[g, l] U. +lemma snv_fwd_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃l,U. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄. #h #g #L #T #H elim H -L -T [ #L #k elim (deg_total h g k) /3 width=3/ -| * #L #K #V #i #HLK #_ * #W #l0 #HVW +| * #L #K #V #i #HLK #_ * #l0 #W #HVW [ elim (lift_total W 0 (i+1)) /3 width=8/ | elim (lift_total V 0 (i+1)) /3 width=8/ ] 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 12c2bf8f5..c80e11c79 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -28,20 +28,20 @@ definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. 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 **********************************) + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊩ U1 :[g]. 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]. +(* Properties for the preservation results **********************************) + 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]. @@ -52,9 +52,9 @@ qed-. fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. #h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2 elim (IH … HTU1 … HL12 … HT1T) // -L1 -T1 #U #HTU #HU1 elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2 @@ -74,9 +74,9 @@ fact ssta_ltpr_cprs_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⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → + ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L2 ⊢ U1 ⬌* U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H @(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ] #T #T2 #HT1T #HTT2 * #U #HTU #HU1 @@ -92,8 +92,8 @@ fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0. (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → ⦃h, L2⦄ ⊩ T2 :[g] → - ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g, l1] U1 → - ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g, l2] U2 → + ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → + ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 → l1 = l2 ∧ L2 ⊢ U1 ⬌* U2. #h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H @@ -151,7 +151,7 @@ fact ssta_dxprs_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⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → - ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g, l+1] U1 → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → + ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2. #h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ] 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 2afaa8e06..79ca41081 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -62,12 +62,12 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 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/ + lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /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 … HW10 … HW230) -W30 #HW120 - elim (snv_fwd_ssta … HW20) #U20 #l0 #HWU20 + elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 elim (ssta_fwd_correct … HVW1) (lsubss_inv_atom1 … H) -H // -| #I #L1 #L #W #HL1 #IHL1 #X #H - elim (lsubss_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=1/ - | #V #l #H1WV #H2WV #HL2 #H1 #H2 destruct /3 width=3/ - ] -| #L1 #L #V1 #W1 #l #H1VW1 #H2VW1 #HL1 #IHL1 #X #H - elim (lsubss_inv_pair1 … H) -H * #L2 - [ #HL2 #H destruct /3 width=5/ - | #V #l0 #_ #_ #_ #_ #H destruct - ] -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc deleted file mode 100644 index f9c628921..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/lsubss_ssta.etc +++ /dev/null @@ -1,69 +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_lift.ma". -include "basic_2/static/ssta_ssta.ma". -include "basic_2/static/lsubss_ldrop.ma". - -(* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED STATIC TYPE ASSIGNMENT *******) - -(* Properties concerning stratified native type assignment ******************) - -lemma lsubss_ssta_trans: ∀h,g,L2,T,U,l. ⦃h, L2⦄ ⊢ T •[g,l] U → - ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •[g,l] U. -#h #g #L2 #T #U #l #H elim H -L2 -T -U -l -[ /2 width=1/ -| #L2 #K2 #V2 #W2 #U2 #i #l #HLK2 #_ #HWU2 #IHVW2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ | -HWU2 -IHVW2 -HLK1 ] - [ #HK12 #H destruct /3 width=6/ - | #V1 #l0 #_ #_ #_ #_ #H destruct - ] -| #L2 #K2 #W2 #V2 #U2 #i #l #HLK2 #HWV2 #HWU2 #IHWV2 #L1 #HL12 - elim (lsubss_ldrop_O1_trans … HL12 … HLK2) -L2 #X #H #HLK1 - elim (lsubss_inv_pair2 … H) -H * #K1 [ -HWV2 | -IHWV2 ] - [ #HK12 #H destruct /3 width=6/ - | #V1 #l0 #H1 #H2 #_ #H #_ destruct - elim (ssta_fwd_correct … H2) -H2 #V #H - elim (ssta_mono … HWV2 … H) -HWV2 -H /2 width=6/ - ] -| /4 width=1/ -| /3 width=1/ -| /3 width=1/ -] -qed. - -lemma lsubss_ssta_conf: ∀h,g,L1,T,U,l. ⦃h, L1⦄ ⊢ T •[g,l] U → - ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •[g,l] U. -#h #g #L1 #T #U #l #H elim H -L1 -T -U -l -[ /2 width=1/ -| #L1 #K1 #V1 #W1 #U1 #i #l #HLK1 #HVW1 #HWU1 #IHVW1 #L2 #HL12 - elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 - elim (lsubss_inv_pair1 … H) -H * #K2 [ -HVW1 | -IHVW1 ] - [ #HK12 #H destruct /3 width=6/ - | #V2 #l0 #H1 #H2 #_ #H #_ destruct - elim (ssta_mono … HVW1 … H1) -HVW1 -H1 #H1 #H2 destruct - elim (ssta_fwd_correct … H2) -H2 /2 width=6/ - ] -| #L1 #K1 #W1 #V1 #U1 #i #l #HLK1 #_ #HWU1 #IHWV1 #L2 #HL12 - elim (lsubss_ldrop_O1_conf … HL12 … HLK1) -L1 #X #H #HLK2 - elim (lsubss_inv_pair1 … H) -H * #K2 [ | -HWU1 -IHWV1 -HLK2 ] - [ #HK12 #H destruct /3 width=6/ - | #V2 #l0 #_ #_ #_ #_ #H destruct - ] -| /4 width=1/ -| /3 width=1/ -| /3 width=1/ -] -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc deleted file mode 100644 index 5ec33634f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lsubss/sstas_lsubss.etc +++ /dev/null @@ -1,30 +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/lsubss_ssta.ma". -include "basic_2/unwind/sstas.ma". - -(* ITERATED STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS *********************) - -(* Properties on lenv ref for stratified type assignment ********************) - -lemma lsubss_sstas_trans: ∀h,g,L2,T,U. ⦃h, L2⦄ ⊢ T •*[g] U → - ∀L1. h ⊢ L1 •⊑[g] L2 → ⦃h, L1⦄ ⊢ T •*[g] U. -#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/ -qed. - -lemma lsubss_sstas_conf: ∀h,g,L1,T,U. ⦃h, L1⦄ ⊢ T •*[g] U → - ∀L2. h ⊢ L1 •⊑[g] L2 → ⦃h, L2⦄ ⊢ T •*[g] U. -#h #g #L2 #T #U #H @(sstas_ind_dx … H) -T // /3 width=5/ -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation.ma index c17f8bc2d..54b47600c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation.ma @@ -254,13 +254,9 @@ notation "hvbox( h ⊢ break term 46 L1 ÷ ⊑ break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqB $h $L1 $L2 }. -notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g , break term 46 l ] break term 46 T2 )" +notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 • break [ term 46 g ] break ⦃ term 46 l , break term 46 T2 ⦄ )" non associative with precedence 45 - for @{ 'StaticType $h $g $l $L $T1 $T2 }. - -notation "hvbox( h ⊢ break term 46 L1 • ⊑ [ term 46 g ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'CrSubEqS $h $g $L1 $L2 }. + for @{ 'StaticType $h $g $L $T1 $T2 $l }. (* Unwind *******************************************************************) @@ -430,9 +426,9 @@ notation "hvbox( L ⊢ break term 46 T1 ⬌* break term 46 T2 )" non associative with precedence 45 for @{ 'PConvStar $L $T1 $T2 }. -notation "hvbox( h ⊢ break term 46 L1 ⊢ • ⊑ [ term 46 g ] break term 46 L2 )" +notation "hvbox( h ⊢ break term 46 L1 • ⊑ break [ term 46 g ] break term 46 L2 )" non associative with precedence 45 - for @{ 'CrSubEqSE $h $g $L1 $L2 }. + for @{ 'CrSubEqS $h $g $L1 $L2 }. notation "hvbox( ⦃ term 46 L1 ⦄ ⬌ * break ⦃ term 46 L2 ⦄ )" non associative with precedence 45 @@ -456,7 +452,7 @@ notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊩ break term 46 T : break non associative with precedence 45 for @{ 'NativeValid $h $g $L $T }. -notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ [ term 46 g ] break term 46 L2 )" +notation "hvbox( h ⊢ break term 46 L1 ⊩ : ⊑ break [ term 46 g ] break term 46 L2 )" non associative with precedence 45 for @{ 'CrSubEqV $h $g $L1 $L2 }. @@ -468,7 +464,7 @@ notation "hvbox( h ⊢ break ⦃ term 46 L1, break term 46 T1 ⦄ ≻ break [ te 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 ⦄ )" +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 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma index ee7a26e22..d7a32e928 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma @@ -32,14 +32,14 @@ inductive ssta (h:sh) (g:sd h): nat → lenv → relation term ≝ . interpretation "stratified static type assignment (term)" - 'StaticType h g l L T U = (ssta h g l L T U). + 'StaticType h g L T U l = (ssta h g l L T U). definition ssta_step: ∀h. sd h → lenv → relation term ≝ λh,g,L,T,U. - ∃l. ⦃h, L⦄ ⊢ T •[g, l+1] U. + ∃l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄. (* Basic inversion lemmas ************************************************) -fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. T = ⋆k0 → +fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀k0. T = ⋆k0 → deg h g k0 l ∧ U = ⋆(next h k0). #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #Hkl #k0 #H destruct /2 width=1/ @@ -51,15 +51,15 @@ fact ssta_inv_sort1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀k0. qed. (* Basic_1: was just: sty0_gen_sort *) -lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k •[g, l] U → +lemma ssta_inv_sort1: ∀h,g,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k •[g] ⦃l, U⦄ → deg h g k l ∧ U = ⋆(next h k). /2 width=4/ qed-. -fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀j. T = #j → - (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W & +fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀j. T = #j → + (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g] ⦃l, W⦄ & ⇧[0, j + 1] W ≡ U ) ∨ - (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V & + (∃∃K,W,V,l0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g] ⦃l0, V⦄ & ⇧[0, j + 1] W ≡ U & l = l0 + 1 ). #h #g #L #T #U #l * -L -T -U -l @@ -73,16 +73,16 @@ fact ssta_inv_lref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀j. qed. (* Basic_1: was just: sty0_gen_lref *) -lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g, l] U → - (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g, l] W & +lemma ssta_inv_lref1: ∀h,g,L,U,i,l. ⦃h, L⦄ ⊢ #i •[g] ⦃l, U⦄ → + (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V •[g] ⦃l, W⦄ & ⇧[0, i + 1] W ≡ U ) ∨ - (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g, l0] V & + (∃∃K,W,V,l0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W •[g] ⦃l0, V⦄ & ⇧[0, i + 1] W ≡ U & l = l0 + 1 ). /2 width=3/ qed-. -fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. T = §p0 → ⊥. +fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀p0. T = §p0 → ⊥. #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #_ #p0 #H destruct | #L #K #V #W #U #i #l #_ #_ #_ #p0 #H destruct @@ -92,12 +92,12 @@ fact ssta_inv_gref1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀p0. | #L #W #T #U #l #_ #p0 #H destruct qed. -lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g, l] U → ⊥. +lemma ssta_inv_gref1: ∀h,g,L,U,p,l. ⦃h, L⦄ ⊢ §p •[g] ⦃l, U⦄ → ⊥. /2 width=9/ qed-. -fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → +fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀a,I,X,Y. T = ⓑ{a,I}Y.X → - ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z. + ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z. #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #_ #a #I #X #Y #H destruct | #L #K #V #W #U #i #l #_ #_ #_ #a #I #X #Y #H destruct @@ -109,12 +109,12 @@ fact ssta_inv_bind1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → qed. (* Basic_1: was just: sty0_gen_bind *) -lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •[g, l] U → - ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g, l] Z & U = ⓑ{a,I}Y.Z. +lemma ssta_inv_bind1: ∀h,g,a,I,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{a,I}Y.X •[g] ⦃l, U⦄ → + ∃∃Z. ⦃h, L.ⓑ{I}Y⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓑ{a,I}Y.Z. /2 width=3/ qed-. -fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y. T = ⓐY.X → - ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z. +fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ∀X,Y. T = ⓐY.X → + ∃∃Z. ⦃h, L⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓐY.Z. #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #_ #X #Y #H destruct | #L #K #V #W #U #i #l #_ #_ #_ #X #Y #H destruct @@ -126,12 +126,12 @@ fact ssta_inv_appl1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ∀X,Y qed. (* Basic_1: was just: sty0_gen_appl *) -lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g, l] U → - ∃∃Z. ⦃h, L⦄ ⊢ X •[g, l] Z & U = ⓐY.Z. +lemma ssta_inv_appl1: ∀h,g,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓐY.X •[g] ⦃l, U⦄ → + ∃∃Z. ⦃h, L⦄ ⊢ X •[g] ⦃l, Z⦄ & U = ⓐY.Z. /2 width=3/ qed-. -fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → - ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X •[g, l] U. +fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → + ∀X,Y. T = ⓝY.X → ⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄. #h #g #L #T #U #l * -L -T -U -l [ #L #k #l #_ #X #Y #H destruct | #L #K #V #W #U #l #i #_ #_ #_ #X #Y #H destruct @@ -143,13 +143,13 @@ fact ssta_inv_cast1_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → qed. (* Basic_1: was just: sty0_gen_cast *) -lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g, l] U → - ⦃h, L⦄ ⊢ X •[g, l] U. +lemma ssta_inv_cast1: ∀h,g,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X •[g] ⦃l, U⦄ → + ⦃h, L⦄ ⊢ X •[g] ⦃l, U⦄. /2 width=4/ qed-. (* Advanced inversion lemmas ************************************************) -lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥. +lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁+ ⦃L, T⦄ → ⊥. #h #g #L #T #U #l #H elim H -L -T -U -l [ #L #k #l #_ #H elim (frsupp_inv_atom1_frsups … H) @@ -173,7 +173,7 @@ lemma ssta_inv_frsupp: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U ] qed-. -fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → T = U → ⊥. +fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → T = U → ⊥. #h #g #L #T #U #l #H elim H -L -T -U -l [ #L #k #l #_ #H lapply (next_lt h k) destruct -H -e0 (**) (* destruct: these premises are not erased *) @@ -189,10 +189,10 @@ fact ssta_inv_refl_aux: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → T = U ] qed-. -lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g, l] T → ⊥. +lemma ssta_inv_refl: ∀h,g,T,L,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, T⦄ → ⊥. /2 width=8 by ssta_inv_refl_aux/ qed-. -lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥. +lemma ssta_inv_frsups: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → ⦃L, U⦄ ⧁* ⦃L, T⦄ → ⊥. #h #g #L #T #U #L #HTU #H elim (frsups_inv_all … H) -H [ * #_ #H destruct /2 width=6 by ssta_inv_refl/ | /2 width=8 by ssta_inv_frsupp/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma index 01841483c..eafec7430 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma @@ -19,7 +19,7 @@ include "basic_2/static/ssta.ma". (* Properties on atomic arity assignment for terms **************************) -lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g, l] U → L ⊢ U ⁝ A. +lemma ssta_aaa: ∀h,g,L,T,A. L ⊢ T ⁝ A → ∀U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → L ⊢ U ⁝ A. #h #g #L #T #A #H elim H -L -T -A [ #L #k #U #l #H elim (ssta_inv_sort1 … H) -H #_ #H destruct // diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma index e4f78acd6..c0a6b2b97 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma @@ -20,9 +20,9 @@ include "basic_2/static/ssta.ma". (* Properties on relocation *************************************************) (* Basic_1: was just: sty0_lift *) -lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 → ∀T2. ⇧[d, e] T1 ≡ T2 → - ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[g, l] U2. + ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄. #h #g #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l [ #L1 #k #l #Hkl #L2 #d #e #HL21 #X1 #H1 #X2 #H2 >(lift_inv_sort1 … H1) -X1 @@ -60,9 +60,9 @@ lemma ssta_lift: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → qed. (* Note: apparently this was missing in basic_1 *) -lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 → +lemma ssta_inv_lift1: ∀h,g,L2,T2,U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 → ∀T1. ⇧[d, e] T1 ≡ T2 → - ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 & ⇧[d, e] U1 ≡ U2. + ∃∃U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ & ⇧[d, e] U1 ≡ U2. #h #g #L2 #T2 #U2 #l #H elim H -L2 -T2 -U2 -l [ #L2 #k #l #Hkl #L1 #d #e #_ #X #H >(lift_inv_sort2 … H) -X /3 width=3/ @@ -105,8 +105,8 @@ qed. (* Advanced forvard lemmas **************************************************) (* Basic_1: was just: sty0_correct *) -lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l] U → - ∃T0. ⦃h, L⦄ ⊢ U •[g, l - 1] T0. +lemma ssta_fwd_correct: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l, U⦄ → + ∃T0. ⦃h, L⦄ ⊢ U •[g] ⦃l-1, T0⦄. #h #g #L #T #U #l #H elim H -L -T -U -l [ /4 width=2/ | #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma index 48ac6a400..72eff7850 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_dx.ma @@ -21,10 +21,10 @@ include "basic_2/static/ssta_lift.ma". (* Properties about dx parallel unfold **************************************) (* Note: apparently this was missing in basic_1 *) -lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ▶* [d, e] U2. #h #g #L1 #T1 #U #l #H elim H -L1 -T1 -U -l [ #L1 #k1 #l1 #Hkl1 #L2 #d #e #_ #T2 #H @@ -102,24 +102,24 @@ lemma ssta_ltpss_dx_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U ] qed. -lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_ltpss_dx_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ▶* [d, e] U2. /3 width=5/ qed. -lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 → +lemma ssta_ltpss_dx_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ▶* [d, e] L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L2 ⊢ U1 ▶* [d, e] U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L2 ⊢ U1 ▶* [d, e] U2. /2 width=5/ qed. -lemma ssta_tpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_tpss_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀T2,d,e. L ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2. + ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L ⊢ U1 ▶* [d, e] U2. /2 width=5/ qed. -lemma ssta_tps_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_tps_conf: ∀h,g,L,T1,U1,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀T2,d,e. L ⊢ T1 ▶ [d, e] T2 → - ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g, l] U2 & L ⊢ U1 ▶* [d, e] U2. + ∃∃U2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L ⊢ U1 ▶* [d, e] U2. /2 width=5/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma index 342a839d5..d554f1fe4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma @@ -19,9 +19,9 @@ include "basic_2/static/ssta_ltpss_dx.ma". (* Properties about sn parallel unfold **************************************) -lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 → +lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L1 ⊢ U1 ▶* [d, e] U2. + ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* [d, e] U2. #h #g #L1 #T #U1 #l #HTU1 #L2 #d #e #HL12 lapply (ltpss_sn_ltpssa … HL12) -HL12 #HL12 @(ltpssa_ind … HL12) -L2 [ /2 width=3/ ] -HTU1 @@ -33,10 +33,10 @@ lapply (ltpss_sn_tpss_trans_eq … HU2 … HL1) -HU2 -HL1 #HU2 lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ qed. -lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶* [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* [d, e] U2. #h #g #L1 #T1 #U1 #l #HTU1 #L2 #d #e #HL12 #T2 #HT12 elim (ssta_ltpss_sn_conf … HTU1 … HL12) -HTU1 #U #HT1U #HU1 @@ -45,9 +45,9 @@ lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2 lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/ qed. -lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → +lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 → ∀T2. L2 ⊢ T1 ▶ [d, e] T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* [d, e] U2. /3 width=3/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma index b20e4366a..adaf999ee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma @@ -20,8 +20,8 @@ include "basic_2/static/ssta.ma". (* Main properties **********************************************************) (* Note: apparently this was missing in basic_1 *) -theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g, l1] U1 → - ∀U2,l2. ⦃h, L⦄ ⊢ T •[g, l2] U2 → l1 = l2 ∧ U1 = U2. +theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g] ⦃l1, U1⦄ → + ∀U2,l2. ⦃h, L⦄ ⊢ T •[g] ⦃l2, U2⦄ → l1 = l2 ∧ U1 = U2. #h #g #L #T #U1 #l1 #H elim H -L -T -U1 -l1 [ #L #k #l #Hkl #X #l2 #H elim (ssta_inv_sort1 … H) -H #Hkl2 #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma index 93fe0a7e0..5ff1bae0f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas.ma @@ -27,7 +27,7 @@ interpretation "iterated stratified static type assignment (term)" lemma sstas_ind: ∀h,g,L,T. ∀R:predicate term. R T → ( - ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g, l + 1] U2 → + ∀U1,U2,l. ⦃h, L⦄ ⊢ T •* [g] U1 → ⦃h, L⦄ ⊢ U1 •[g] ⦃l+1, U2⦄ → R U1 → R U2 ) → ∀U. ⦃h, L⦄ ⊢ T •*[g] U → R U. @@ -37,7 +37,7 @@ qed-. lemma sstas_ind_dx: ∀h,g,L,U2. ∀R:predicate term. R U2 → ( - ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g, l + 1] U1 → ⦃h, L⦄ ⊢ U1 •* [g] U2 → + ∀T,U1,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •* [g] U2 → R U1 → R T ) → ∀T. ⦃h, L⦄ ⊢ T •*[g] U2 → R T. @@ -50,15 +50,15 @@ qed-. lemma sstas_refl: ∀h,g,L. reflexive … (sstas h g L). // qed. -lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g, l+1] U → ⦃h, L⦄ ⊢ T •*[g] U. +lemma ssta_sstas: ∀h,g,L,T,U,l. ⦃h, L⦄ ⊢ T •[g] ⦃l+1, U⦄ → ⦃h, L⦄ ⊢ T •*[g] U. /3 width=2 by R_to_star, ex_intro/ qed. (**) (* auto fails without trace *) -lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g,l+1] U2 → +lemma sstas_strap1: ∀h,g,L,T1,T2,U2,l. ⦃h, L⦄ ⊢ T1 •*[g] T2 → ⦃h, L⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ → ⦃h, L⦄ ⊢ T1 •*[g] U2. /3 width=4 by sstep, ex_intro/ (**) (* auto fails without trace *) qed. -lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g, l+1] U1 → ⦃h, L⦄ ⊢ U1 •*[g] U2 → +lemma sstas_strap2: ∀h,g,L,T1,U1,U2,l. ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L⦄ ⊢ U1 •*[g] U2 → ⦃h, L⦄ ⊢ T1 •*[g] U2. /3 width=3 by star_compl, ex_intro/ (**) (* auto fails without trace *) qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma index e8ba22729..d8d253e12 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_lift.ma @@ -19,9 +19,9 @@ include "basic_2/unwind/sstas.ma". (* Advanced forward lemmas **************************************************) -lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → +lemma sstas_fwd_correct: ∀h,g,L,T1,U1,l1. ⦃h, L⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → ∀T2. ⦃h, L⦄ ⊢ T1 •*[g] T2 → - ∃∃U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2. + ∃∃U2,l2. ⦃h, L⦄ ⊢ T2 •[g] ⦃l2, U2⦄. #h #g #L #T1 #U1 #l1 #HTU1 #T2 #H @(sstas_ind … H) -T2 [ /2 width=3/ ] -HTU1 #T #T2 #l #_ #HT2 * #U #l0 #_ -l0 elim (ssta_fwd_correct … HT2) -T /2 width=3/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma index 84b941232..eef812b56 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/unwind/sstas_sstas.ma @@ -20,7 +20,7 @@ include "basic_2/unwind/sstas.ma". (* Advanced inversion lemmas ************************************************) lemma sstas_inv_O: ∀h,g,L,T,U. ⦃h, L⦄ ⊢ T •*[g] U → - ∀T0. ⦃h, L⦄ ⊢ T •[g , 0] T0 → U = T. + ∀T0. ⦃h, L⦄ ⊢ T •[g] ⦃0, T0⦄ → U = T. #h #g #L #T #U #H @(sstas_ind_dx … H) -T // #T0 #U0 #l0 #HTU0 #_ #_ #T1 #HT01 elim (ssta_mono … HTU0 … HT01) + + Mutual recursive preservation of stratified native validity + for hyper computation on closures. + Confluence for context-free parallel reduction on closures. 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 8a80df07e..c4c962070 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 @@ -64,8 +64,8 @@ table { [ "fpcs ( ⦃?,?⦄ ⬌* ⦃?,?⦄ )" "fpcs_aaa" + "fpcs_cpcs" + "fpcs_fprs" + "fpcs_fpcs" * ] } ] - [ { "local env. ref. for context-sensitive equivalence" * } { - [ "lsubse ( ? ⊢•⊑[?] ? )" "lsubse_ldrop" + "lsubse_ssta" + "lsubse_cpcs" * ] + [ { "local env. ref. for stratified static type assignment" * } { + [ "lsubss ( ? •⊑[?] ? )" "lsubss_ldrop" + "lsubss_ssta" + "lsubss_cpcs" * ] } ] [ { "context-sensitive equivalence" * } { @@ -170,12 +170,6 @@ table { ] 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" * ] } diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml index ac5237562..43ef2780b 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml +++ b/matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml @@ -1,8 +1,5 @@ -
- $(MATITA_RT_BASE_DIR) -
contribs/lambdadelta/ground_2/ xoa -- 2.39.2