From 583c59b229ba770c9694c703b381542ff2e67f4e Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 3 Mar 2013 18:52:14 +0000 Subject: [PATCH] - lambdadelta: we removed focalized reduction from snv preservation - matitadep: bug fix in loop detection --- .../binaries/matitadep/matitadep.ml | 29 +++--- .../basic_2/computation/cprs_cprs.ma | 27 ++++- .../basic_2/computation/dxprs_dxprs.ma | 2 +- .../lambdadelta/basic_2/dynamic/snv.ma | 15 +++ .../lambdadelta/basic_2/dynamic/snv_aaa.ma | 8 +- .../lambdadelta/basic_2/dynamic/snv_cpcs.ma | 98 ++++++++++++++----- .../lambdadelta/basic_2/dynamic/snv_ltpr.ma | 18 ++-- .../lambdadelta/basic_2/dynamic/snv_ssta.ma | 31 ++---- .../{snv_ltpr_ssta.ma => snv_ssta_ltpr.ma} | 41 ++++---- .../lambdadelta/basic_2/dynamic/snv_sstas.ma | 26 +++++ .../basic_2/equivalence/cpcs_cpcs.ma | 29 ++++-- .../basic_2/reducibility/cpr_lift.ma | 10 +- .../lambdadelta/basic_2/unwind/sstas.ma | 3 + .../lambdadelta/basic_2/unwind/sstas_lift.ma | 10 ++ 14 files changed, 237 insertions(+), 110 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/dynamic/{snv_ltpr_ssta.ma => snv_ssta_ltpr.ma} (82%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma diff --git a/matita/components/binaries/matitadep/matitadep.ml b/matita/components/binaries/matitadep/matitadep.ml index fdf5e980f..da82b9fc1 100644 --- a/matita/components/binaries/matitadep/matitadep.ml +++ b/matita/components/binaries/matitadep/matitadep.ml @@ -7,6 +7,10 @@ type file = { let graph = Hashtbl.create 503 +let rec purge dname bdeps = match bdeps with + | [] -> bdeps + | hd :: tl -> if hd = dname then bdeps else purge dname tl + let add fname = if Hashtbl.mem graph fname then () else Hashtbl.add graph fname {ddeps = []; rdeps = None} @@ -18,25 +22,28 @@ let add_ddep fname dname = let init fname dname = add fname; add dname; add_ddep fname dname -let rec compute fname file = match file.rdeps with +let rec compute bdeps fname file = match file.rdeps with | Some rdeps -> rdeps | None -> - let rdeps = List.fold_left (iter fname) StringSet.empty file.ddeps in + let bdeps = fname :: bdeps in + let rdeps = List.fold_left (iter fname bdeps) StringSet.empty file.ddeps in Hashtbl.replace graph fname {file with rdeps = Some rdeps}; rdeps -and iter fname rdeps dname = - if StringSet.mem dname rdeps then - begin Printf.printf "%s: redundant %s\n" fname dname; rdeps end - else +and iter fname bdeps rdeps dname = + if StringSet.mem dname rdeps then begin + Printf.printf "%s: redundant %s\n" fname dname; + rdeps + end else if List.mem dname bdeps then begin + let loop = purge dname (List.rev bdeps) in + Printf.printf "circular: %s\n" (String.concat " " loop); + StringSet.add dname rdeps + end else let file = Hashtbl.find graph dname in - StringSet.add dname (StringSet.union (compute dname file) rdeps) + StringSet.add dname (StringSet.union (compute bdeps dname file) rdeps) let check () = - let iter fname file = - if StringSet.mem fname (compute fname file) then - Printf.printf "%s: circular\n" fname - in + let iter fname file = ignore (compute [] fname file) in Hashtbl.iter iter graph let rec read ich = diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma index 8f94b0fa7..3326b8b46 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_cprs.ma @@ -21,8 +21,8 @@ include "basic_2/computation/cprs_lfpr.ma". (* Advanced properties ******************************************************) -lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. - L.ⓛV ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2. +lemma cprs_abst_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. #L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HT12) -T2 [ /3 width=2/ | /3 width=6 by cprs_strap1, cpr_abst/ (**) (* /3 width=6/ is too slow *) @@ -96,9 +96,9 @@ lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. -lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. - L.ⓛV ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓛ{a}V1. T1 ➡* ⓛ{a}V2. T2. -#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a @(cprs_ind … HV12) -V2 +lemma cprs_abst: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀V,T1,T2. L.ⓛV ⊢ T1 ➡* T2 → + ∀a,I. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 #V #T1 #T2 #HT12 #a #I @(cprs_ind … HV12) -V2 [ lapply (cprs_lsubs_trans … HT12 (L.ⓛV1) ?) -HT12 /2 width=2/ | #V0 #V2 #_ #HV02 #IHV01 @(cprs_trans … IHV01) -V1 /2 width=2/ @@ -112,6 +112,11 @@ lemma cprs_abbr1: ∀L,V1,T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡ @(cprs_trans … IHV1) -IHV1 /2 width=1/ qed. +lemma cprs_bind1: ∀I,L,V1,T1,T2. L. ⓑ{I}V1 ⊢ T1 ➡* T2 → ∀V2. L ⊢ V1 ➡* V2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +* /2 width=1/ /2 width=2/ +qed. + lemma cprs_abbr2_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡* T2 → ∀a. L ⊢ ⓓ{a}V1. T1 ➡* ⓓ{a}V2. T2. #L #V1 #V2 #HV12 #T1 #T2 #HT12 #a @(cprs_ind_dx … HT12) -T1 @@ -130,6 +135,11 @@ lapply (IHV1 T1 T1 ? a) -IHV1 // #HV1 @(cprs_trans … HV1) -HV1 /2 width=1/ qed. +lemma cprs_bind2: ∀L,V1,V2. L ⊢ V1 ➡* V2 → ∀I,T1,T2. L. ⓑ{I}V2 ⊢ T1 ➡* T2 → + ∀a. L ⊢ ⓑ{a,I}V1. T1 ➡* ⓑ{a,I}V2. T2. +#L #V1 #V2 #HV12 * /2 width=1/ /2 width=2/ +qed. + lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → ∀a.L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2. @@ -141,6 +151,13 @@ lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2. ] qed. +lemma ltpr_cprs_trans: ∀L1,L2. L1 ➡ L2 → + ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. +#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 // +#T #T2 #_ #HT2 #IHT2 +@(cprs_trans … IHT2) /2 width=3/ +qed. + (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *) lemma lcpr_cprs_trans: ∀L1,L2. ⦃L1⦄ ➡ ⦃L2⦄ → ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2. 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 772cbd94a..c0aff4efb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_dxprs.ma @@ -21,7 +21,7 @@ include "basic_2/computation/dxprs.ma". (* Advanced properties ******************************************************) lemma dxprs_cprs_trans: ∀h,g,L,T1,T,T2. - ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. + ⦃h, L⦄ ⊢ T1 •*➡*[g] T → L ⊢ T ➡* T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2. #h #g #L #T1 #T #T2 * #T0 #HT10 #HT0 #HT2 lapply (cprs_trans … HT0 … HT2) -T /2 width=3/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma index e39a5764a..982d7edaf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma @@ -111,3 +111,18 @@ 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. /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. +#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 + [ elim (lift_total W 0 (i+1)) /3 width=8/ + | elim (lift_total V 0 (i+1)) /3 width=8/ + ] +| #a #I #L #V #T #_ #_ #_ * /3 width=3/ +| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ +| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma index 010a1ad7d..f492c019b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma @@ -19,9 +19,9 @@ include "basic_2/dynamic/snv.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) -(* Properties on atomic arity assignment for terms **************************) +(* Forward lemmas on atomic arity assignment for terms **********************) -lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. +lemma snv_fwd_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. #h #g #L #T #H elim H -L -T [ /2 width=2/ | #I #L #K #V #i #HLK #_ * /3 width=6/ @@ -36,6 +36,6 @@ lemma snv_aaa: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃A. L ⊢ T ⁝ A. ] qed-. -lemma snv_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T. -#h #g #L #T #H elim (snv_aaa … H) -H /2 width=2/ +lemma snv_fwd_csn: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → L ⊢ ⬊* T. +#h #g #L #T #H elim (snv_fwd_aaa … H) -H /2 width=2/ 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 b1430bd59..7078c9f3e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma @@ -14,43 +14,22 @@ include "basic_2/static/ssta_ssta.ma". include "basic_2/computation/ygt.ma". -include "basic_2/equivalence/fpcs_cpcs.ma". include "basic_2/dynamic/snv_ltpss_dx.ma". +include "basic_2/dynamic/snv_sstas.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) (* Inductive premises for the preservation results **************************) (* -definition IH_ssta_cprs: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. - definition IH_snv_dxprs: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → ∀L2. L1 ➡ L2 → ∀T2. ⦃h, L2⦄ ⊢ T1 •*➡*[g] T2 → ⦃h, L2⦄ ⊩ T2 :[g]. - -fact ssta_cpcs_aux: ∀h,g,L,T1,T2. IH_ssta_cprs h g L T1 → IH_ssta_cprs h g L T2 → - ⦃h, L⦄ ⊩ T1 :[g] → ⦃h, L⦄ ⊩ T2 :[g] → - ∀U1,l1. ⦃h, L⦄ ⊢ T1 •[g, l1] U1 → - ∀U2,l2. ⦃h, L⦄ ⊢ T2 •[g, l2] U2 → - L ⊢ T1 ⬌* T2 → - l1 = l2 ∧ L ⊢ U1 ⬌* U2. -#h #g #L #T1 #T2 #IH1 #IH2 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #H -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (IH1 … HT1 … HTU1 … H1) -T1 // #W1 #H1 #HUW1 -elim (IH2 … HT2 … HTU2 … H2) -T2 // #W2 #H2 #HUW2 -elim (ssta_mono … H1 … H2) -T #H1 #H2 destruct -lapply (fpcs_canc_dx … HUW1 … HUW2) -W2 #HU12 -lapply (fpcs_inv_cpcs … HU12) -HU12 /2 width=1/ -qed-. *) 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 → ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ λh,g,L1,T1. ⦃h, L1⦄ ⊩ T1 :[g] → @@ -64,11 +43,12 @@ 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 → ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & ⦃L1, U1⦄ ⬌* ⦃L2, U2⦄. + ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 & L1 ⊢ U1 ⬌* U2. #h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2 -elim (IH … HTU1 … HL12 … HT1T) // -HL12 -T1 #U #HTU #HU1 +elim (IH … HTU1 … HL12 … HT1T) // -T1 #U #HTU #HU1 elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2 -lapply (fpcs_fpr_strap1 … HU1 L2 U2 ?) -HU1 /2 width=3/ /3 width=3/ +lapply (ltpr_cpr_trans … HL12 U U2 ?) -HL12 /2 width=3/ -HU2 #HU2 +lapply (cpcs_cprs_strap1 … HU1 … HU2) -U /2 width=3/ qed-. fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 → @@ -101,7 +81,6 @@ elim (ssta_ltpr_cpr_aux … HTU … HTT2) // [2: /3 width=7 by snv_cprs_aux, ygt_cprs_trans/ |3: /3 width=3 by ygt_cprs_trans/ ] -L0 -T0 -T1 -T #U2 #HTU2 #HU2 -lapply (fpcs_inv_cpcs … HU2) -HU2 #HU2 lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ qed-. @@ -121,3 +100,68 @@ elim (ssta_cprs_aux … HLT02 HT2 … HTU2 … H2) -T2 /2 width=1/ #W2 #H2 #HUW2 elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/ qed-. + +fact snv_sstas_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊩ T1 :[g] → + ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊩ U1 :[g]. +#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H +@(sstas_ind … H) -U1 // -HT1 /3 width=5 by ygt_sstas_trans/ +qed-. + +fact sstas_cprs_aux: ∀h,g,L0,T0. + (∀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. 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] → + ∀T2. L1 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #T2 #HT12 #U1 #H +@(sstas_ind … H) -U1 [ /3 width=3/ ] +#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12 +lapply (snv_cprs_aux … IH2 … HT1 … HT12) // #HT2 +elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2 +elim (ssta_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 +[2,3: /3 width=7 by snv_sstas_aux, ygt_cprs_trans/ +|4,5: /3 width=3 by ygt_sstas_trans, ygt_cprs_trans/ +] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/ +qed-. + +fact dxprs_cprs_aux: ∀h,g,L0,T0. + (∀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. 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] → + ∀T2. L1 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •*➡*[g] U2 & L1 ⊢ U1 ➡* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #T2 #HT12 #U1 * #W1 #HTW1 #HWU1 +elim (sstas_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12 +lapply (cpcs_cprs_conf … HWU1 … HW12) -W1 #H +elim (cpcs_inv_cprs … H) -H /3 width=3/ +qed-. + +fact sstas_ltpr_aux: ∀h,g,L0,T0. + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → + (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → + ∀L1,T. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T⦄ → ⦃h, L1⦄ ⊩ T :[g] → + ∀L2. L1 ➡ L2 → ∀U1. ⦃h, L1⦄ ⊢ T •*[g] U1 → + ∃∃U2. ⦃h, L2⦄ ⊢ T •*[g] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH2 #IH1 #L1 #T #H01 #HT #L2 #HL12 #U1 #H +@(sstas_ind … H) -U1 [ /4 width=3/ ] +#W1 #U1 #l1 #HTW1 #HWU1 * #W2 #HTW2 #HW12 +lapply (snv_sstas_aux … IH2 … HTW1) // -IH2 -HT #HW1 + +(* +elim (IH1 … HWU1 … HL12 W1) // -IH1 -HW1 -HWU1 -HL12 +[2: /2 width=3 by ygt_sstas_trans/ ] #U2 +*) +(* +fact sstas_dxprs_aux: ∀h,g,L0,T0. + (∀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. 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. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → + ∃∃U2. ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U1 ⬌* U2. +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #HTU1 #T2 * #T #HT1T #HTT2 +*) \ No newline at end of file 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 4bcfa9889..04f7dcb4c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/snv_ltpr_ssta.ma". +include "basic_2/dynamic/snv_cpcs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -20,21 +20,22 @@ include "basic_2/dynamic/snv_ltpr_ssta.ma". fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. (∀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 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH2 -IH1 -L1 +#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [||||*] +[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH3 -IH2 -IH1 -L1 >(tpr_inv_atom1 … H2) -X // -| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH2 +| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -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 -IH2 -IH1 +| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH2 +| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -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,8 +53,9 @@ fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. [ #V2 #T2 #HV12 #HT12 #H destruct lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 - elim (IH2 … HVW1 … HL12 … HV12) -IH2 -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 - lapply (fpcs_canc_sn L1 L1 … W10 W1 … HW12) -HW12 /3 width=1/ -W10 #HW12 + elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 + lapply (cpcs_cprs_conf … HW10 … HW12) -W10 #HW12 + elim (dxprs_cprs_aux … IH2 IH1 IH3 … T2 … HTU1) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #U2 #HTU2 #HU12 @(snv_appl … HV2 HT2 HVW2) (* lapply (IH1 … HT1 … HTU1) -IH1 // #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma index ea04940d8..2bee82488 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma @@ -12,33 +12,20 @@ (* *) (**************************************************************************) -include "basic_2/dynamic/snv.ma". +include "basic_2/dynamic/snv_cpcs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) (* Properties on stratified static type assignment for terms ****************) -lemma snv_ssta: ∀h,g,L,T. ⦃h, L⦄ ⊩ T :[g] → ∃∃U,l. ⦃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 - [ elim (lift_total W 0 (i+1)) /3 width=8/ - | elim (lift_total V 0 (i+1)) /3 width=8/ - ] -| #a #I #L #V #T #_ #_ #_ * /3 width=3/ -| #a #L #V #W #W1 #T0 #T1 #l #_ #_ #_ #_ #_ #_ * /3 width=3/ -| #L #W #T #U #l #_ #_ #HTU #_ #_ #_ /3 width=3/ (**) (* auto fails without the last #_ *) -] -qed-. - -fact snv_ssta_conf_aux: ∀h,g,L,T. ( - ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → - ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → - ♯{L0, T0} < ♯{L, T} → ⦃h, L0⦄ ⊩ U0 :[g] - ) → - ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → - ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → - L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g]. +fact snv_ssta_aux: ∀h,g,L,T. ( + ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → + ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → + ♯{L0, T0} < ♯{L, T} → ⦃h, L0⦄ ⊩ U0 :[g] + ) → + ∀L0,T0. ⦃h, L0⦄ ⊩ T0 :[g] → + ∀U0,l. ⦃h, L0⦄ ⊢ T0 •[g, l + 1] U0 → + L0 = L → T0 = T → ⦃h, L0⦄ ⊩ U0 :[g]. #h #g #L #T #IH1 #L0 #T0 * -L0 -T0 [ | diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma similarity index 82% rename from matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma rename to matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma index cabeceb25..5ee41883b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ltpr_ssta.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_ltpr.ma @@ -12,10 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/static/ssta_ltpss_sn.ma". +include "basic_2/equivalence/cpcs_ltpr.ma". include "basic_2/equivalence/lsubse_ssta.ma". -include "basic_2/equivalence/lfpcs_fpcs.ma". -include "basic_2/dynamic/snv_ssta.ma". include "basic_2/dynamic/snv_cpcs.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) @@ -42,9 +40,8 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0. elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #HW12 lapply (ldrop_fwd_ldrop2 … HLK1) -V1 #H1 - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (fpcs_lift … HW12 … H1 H2 … HWU1 … HWU2) -H1 -H2 -W1 [ /3 width=1/ ] /3 width=6/ + lapply (cpcs_lift … H1 … HWU1 … HWU2 HW12) -H1 -W1 /3 width=6/ | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct lapply (ldrop_mono … H … HLK1) -H #H destruct lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 @@ -63,49 +60,51 @@ fact ssta_ltpr_tpr_aux: ∀h,g,L0,T0. [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1 - [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 -HV12 #U2 #HTU2 #HU12 - lapply (fpcs_fwd_shift … HU12 a) -HU12 /3 width=3/ + [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12 + lapply (cpcs_bind1 … HU12 … V2 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ | #T2 #HT12 #HT2 #H1 #H2 destruct elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12 - lapply (fpcs_fwd_shift … HU12 true) -HU12 #HU12 + lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12 elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 - lapply (fpcs_fpr_strap1 … HU12 L2 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ + lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ ] | #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct elim (tpr_inv_appl1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 - elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 /3 width=5/ + elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12 + lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW #HT2 elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct lapply (cprs_div … HW10 … HW0) -W0 #HW1W elim (ssta_fwd_correct … HVW1)