From cafb43926d8553c5b7f8dafcb5d734783c19bbfb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 20 Nov 2017 19:36:51 +0000 Subject: [PATCH] - ground_2: rtmap: disjointness relation - lib: some additions - basic_2: first version of tc_lfxs_inv_lex_lfeq some improvements new explanatory column in basic_2_src.tbl --- .../basic_2/i_static/tc_lfxs_fqup.ma | 13 +- .../basic_2/i_static/tc_lfxs_lfeq.ma | 73 ++---- .../lambdadelta/basic_2/relocation/lex.ma | 12 +- .../lambdadelta/basic_2/relocation/lexs.ma | 44 +++- .../lambdadelta/basic_2/relocation/lexs_tc.ma | 18 +- .../lambdadelta/basic_2/static/lfdeq_fqup.ma | 1 - .../lambdadelta/basic_2/static/lfeq_fqup.ma | 24 ++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 230 +++++++++--------- ...{partial_compile.sh => compile_partial.sh} | 0 .../contribs/lambdadelta/compile_static.sh | 1 + .../lambdadelta/ground_2/lib/relations.ma | 30 ++- .../ground_2/notation/relations/parallel_2.ma | 19 ++ .../ground_2/relocation/rtmap_sdj.ma | 146 +++++++++++ .../ground_2/relocation/rtmap_sle.ma | 4 +- .../lambdadelta/ground_2/web/ground_2_src.tbl | 6 +- matita/matita/contribs/lambdadelta/static.txt | 7 + 16 files changed, 427 insertions(+), 201 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma rename matita/matita/contribs/lambdadelta/{partial_compile.sh => compile_partial.sh} (100%) create mode 100644 matita/matita/contribs/lambdadelta/compile_static.sh create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/relations/parallel_2.ma create mode 100644 matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma create mode 100644 matita/matita/contribs/lambdadelta/static.txt diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma index c92a4ad7b..bc7061ba7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma @@ -19,11 +19,12 @@ include "basic_2/i_static/tc_lfxs.ma". (* Advanced properties ******************************************************) -lemma tc_lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀T. reflexive … (tc_lfxs R T). +lemma tc_lfxs_refl: ∀R. c_reflexive … R → + ∀T. reflexive … (tc_lfxs R T). /3 width=1 by lfxs_refl, inj/ qed. (* Basic_2A1: uses: TC_lpx_sn_pair TC_lpx_sn_pair_refl *) -lemma tc_lfxs_pair_refl: ∀R. (∀L. reflexive … (R L)) → +lemma tc_lfxs_pair_refl: ∀R. c_reflexive … R → ∀L,V1,V2. LTC … R L V1 V2 → ∀I,T. L.ⓑ{I}V1 ⪤**[R, T] L.ⓑ{I}V2. #R #HR #L #V1 #V2 #H elim H -V2 /3 width=3 by tc_lfxs_step_dx, lfxs_pair_refl, inj/ @@ -31,7 +32,7 @@ qed. (* Advanced eliminators *****************************************************) -lemma tc_lfxs_ind_sn: ∀R. (∀L. reflexive … (R L)) → +lemma tc_lfxs_ind_sn: ∀R. c_reflexive … R → ∀L1,T. ∀R0:predicate …. R0 L1 → (∀L,L2. L1 ⪤**[R, T] L → L ⪤*[R, T] L2 → R0 L → R0 L2) → ∀L2. L1 ⪤**[R, T] L2 → R0 L2. @@ -39,7 +40,7 @@ lemma tc_lfxs_ind_sn: ∀R. (∀L. reflexive … (R L)) → @(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/ qed-. -lemma tc_lfxs_ind_dx: ∀R. (∀L. reflexive … (R L)) → +lemma tc_lfxs_ind_dx: ∀R. c_reflexive … R → ∀L2,T. ∀R0:predicate …. R0 L2 → (∀L1,L. L1 ⪤*[R, T] L → L ⪤**[R, T] L2 → R0 L → R0 L1) → ∀L1. L1 ⪤**[R, T] L2 → R0 L1. @@ -49,7 +50,7 @@ qed-. (* Advanced inversion lemmas ************************************************) -lemma tc_lfxs_inv_bind_void: ∀R. (∀L. reflexive … (R L)) → +lemma tc_lfxs_inv_bind_void: ∀R. c_reflexive … R → ∀p,I,L1,L2,V,T. L1 ⪤**[R, ⓑ{p,I}V.T] L2 → L1 ⪤**[R, V] L2 ∧ L1.ⓧ ⪤**[R, T] L2.ⓧ. #R #HR #p #I #L1 #L2 #V #T #H @(tc_lfxs_ind_sn … HR … H) -L2 @@ -60,7 +61,7 @@ qed-. (* Advanced forward lemmas **************************************************) -lemma tc_lfxs_fwd_bind_dx_void: ∀R. (∀L. reflexive … (R L)) → +lemma tc_lfxs_fwd_bind_dx_void: ∀R. c_reflexive … R → ∀p,I,L1,L2,V,T. L1 ⪤**[R, ⓑ{p,I}V.T] L2 → L1.ⓧ ⪤**[R, T] L2.ⓧ. #R #HR #p #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_bind_void … H) -H // diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma index 53782a58d..64e38fc48 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lfeq.ma @@ -12,56 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/static/lfeq.ma". +include "basic_2/syntax/ext2_tc.ma". +include "basic_2/relocation/lexs_tc.ma". +include "basic_2/relocation/lex.ma". +include "basic_2/static/lfeq_fqup.ma". include "basic_2/static/lfxs_lfxs.ma". include "basic_2/i_static/tc_lfxs_fqup.ma". -(* -axiom cext2_inv_LTC: ∀R,L,I1,I2. cext2 (LTC … R) L I1 I2 → LTC … (cext2 R) L I1 I2. - -#R #L #I1 #I2 * -I1 -I2 -[ /2 width=1 by ext2_unit, inj/ -| #I #V1 #V2 #HV12 -*) - - -(* -lemma pippo: ∀RN,RP. (∀L. reflexive … (RP L)) → - ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → - TC … (lexs RN RP f) L1 L2. -#RN #RP #HRP #f #L1 #L2 #H elim H -f -L1 -L2 -[ /2 width=1 by lexs_atom, inj/ ] -#f #I1 #I2 #L1 #L2 #HL12 #HI12 #IH -[ @step [3: -*) - -(* -axiom lexs_frees_confluent_LTC_sn: ∀RN,RP. lexs_frees_confluent RN RP → - lexs_frees_confluent (LTC … RN) RP. - -#RN #RP #HR #f1 #L1 #T #Hf1 #L2 #H -*) (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) -lemma pippo: ∀R. (∀L. reflexive … (R L)) → - (lexs_frees_confluent (cext2 R) cfull) → - ∀L1,L2,T. L1 ⪤**[R, T] L2 → - ∃∃L. L1 ⪤*[LTC … R, T] L & L ≡[T] L2. -#R #H1R #H2R #L1 #L2 #T #H +lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → + (lexs_frees_confluent (cext2 R) cfull) → + (∀f. 𝐈⦃f⦄ → s_rs_transitive … (cext2 R) (λ_.lexs cfull (cext2 R) f)) → + ∀L1,L2,T. L1 ⪤**[R, T] L2 → + ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2. +#R #H1R #H2R #H3R #L1 #L2 #T #H @(tc_lfxs_ind_sn … H1R … H) -H -L2 -[ /4 width=5 by lfxs_refl, inj, ex2_intro/ -| #L0 #L2 #_ #HL02 * #L * #f1 #Hf1 #HL1 #HL0 - lapply (lexs_co ??? cfull … (cext2_inv_LTC R) … HL1) -HL1 // #HL1 - lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 #HL2 - elim (lexs_frees_confluent_LTC_sn … H2R … Hf1 … HL1) #f2 #Hf2 #Hf21 - lapply (lfxs_inv_frees … HL2 … Hf2) -HL2 #HL2 - elim (lexs_sle_split … ceq_ext … HL2 … Hf21) -HL2 - [ #L0 #HL0 #HL02 - |*: /2 width=1 by ext2_refl/ - ] - lapply (sle_lexs_trans … HL0 … Hf21) -Hf21 // #H - elim (H2R … Hf2 … H) -H #f0 #Hf0 #Hf02 - lapply (sle_lexs_trans … HL02 … Hf02) -f2 // #HL02 - @(ex2_intro … L0) - [ @(ex2_intro … Hf1) - | @(ex2_intro … HL02) // +[ /4 width=3 by lfeq_refl, lex_refl, inj, ex2_intro/ +| #L0 #L2 #_ #HL02 * #L * #f0 #Hf0 #HL1 #HL0 + lapply (lfeq_lfxs_trans … HL0 … HL02) -L0 * #f1 #Hf1 #HL2 + elim (lexs_sdj_split … ceq_ext … HL2 f0 ?) -HL2 + [ #L0 #HL0 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] + lapply (lexs_sdj … HL0 f1 ?) /2 width=1 by sdj_isid_sn/ #H + elim (H2R … Hf1 … H) -H #f2 #Hf2 #Hf21 + lapply (sle_lexs_trans … HL02 … Hf21) -f1 // #HL02 + lapply (lexs_co ?? cfull (LTC … (cext2 R)) … HL1) -HL1 /2 width=1 by ext2_inv_tc/ #HL1 + lapply (lexs_inv_tc_dx … HL1) -HL1 /2 width=1 by ext2_refl/ #HL1 + lapply (step ????? HL1 … HL0) -L #HL10 + lapply (lexs_tc_dx … H3R … HL10) -HL10 // #HL10 + lapply (lexs_co … cfull (cext2 (LTC … R)) … HL10) -HL10 /2 width=1 by ext2_tc/ #HL10 + /3 width=5 by ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma index 72260e801..5c8b23e55 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex.ma @@ -12,14 +12,22 @@ (* *) (**************************************************************************) +include "ground_2/relocation/rtmap_uni.ma". include "basic_2/notation/relations/relation_3.ma". +include "basic_2/syntax/cext2.ma". include "basic_2/relocation/lexs.ma". (* GENERIC EXTENSION OF A CONTEXT-SENSITIVE REALTION ON TERMS ***************) (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) -definition lex: (lenv → relation bind) → relation lenv ≝ - λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, R, f] L2. +definition lex: (lenv → relation term) → relation lenv ≝ + λR,L1,L2. ∃∃f. 𝐈⦃f⦄ & L1 ⪤*[cfull, cext2 R, f] L2. interpretation "generic extension (local environment)" 'Relation R L1 L2 = (lex R L1 L2). + +(* Basic properties *********************************************************) + +(* Basic_2A1: was: lpx_sn_refl *) +lemma lex_refl: ∀R. c_reflexive … R → reflexive … (lex R). +/4 width=3 by lexs_refl, ext2_refl, ex2_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index bd0a3af6b..a58966696 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -13,6 +13,7 @@ (**************************************************************************) include "ground_2/relocation/rtmap_sle.ma". +include "ground_2/relocation/rtmap_sdj.ma". include "basic_2/notation/relations/relationstar_5.ma". include "basic_2/syntax/lenv.ma". @@ -170,10 +171,7 @@ lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⪤*[RN, RP, f] #RN #RP #L1 #L2 @eq_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) qed-. -(* Basic_2A1: uses: lpx_sn_refl *) -lemma lexs_refl: ∀RN,RP. - (∀L. reflexive … (RN L)) → - (∀L. reflexive … (RP L)) → +lemma lexs_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f.reflexive … (lexs RN RP f). #RN #RP #HRN #HRP #f #L generalize in match f; -f elim L -L // #L #I #IH #f elim (pn_split f) * @@ -194,16 +192,13 @@ lemma lexs_pair_repl: ∀RN,RP,f,I1,I2,L1,L2. L1.ⓘ{J1} ⪤*[RN, RP, f] L2.ⓘ{J2}. /3 width=3 by lexs_inv_tl, lexs_fwd_bind/ qed-. -lemma lexs_co: ∀RN1,RP1,RN2,RP2. - (∀L1,I1,I2. RN1 L1 I1 I2 → RN2 L1 I1 I2) → - (∀L1,I1,I2. RP1 L1 I1 I2 → RP2 L1 I1 I2) → +lemma lexs_co: ∀RN1,RP1,RN2,RP2. RN1 ⊆ RN2 → RP1 ⊆ RP2 → ∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → L1 ⪤*[RN2, RP2, f] L2. #RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 /3 width=1 by lexs_atom, lexs_next, lexs_push/ qed-. -lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. - (∀L1,I1,I2. RP1 L1 I1 I2 → RP2 L1 I1 I2) → +lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. RP1 ⊆ RP2 → ∀f,L1,L2. L1 ⪤*[RN1, RP1, f] L2 → 𝐈⦃f⦄ → L1 ⪤*[RN2, RP2, f] L2. #RN1 #RP1 #RN2 #RP2 #HR #f #L1 #L2 #H elim H -f -L1 -L2 // @@ -213,7 +208,19 @@ lemma lexs_co_isid: ∀RN1,RP1,RN2,RP2. ] qed-. -lemma sle_lexs_trans: ∀RN,RP. (∀L,I1,I2. RN L I1 I2 → RP L I1 I2) → +lemma lexs_sdj: ∀RN,RP. RP ⊆ RN → + ∀f1,L1,L2. L1 ⪤*[RN, RP, f1] L2 → + ∀f2. f1 ∥ f2 → L1 ⪤*[RP, RN, f2] L2. +#RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // +#f1 #I1 #I2 #L1 #L2 #_ #HI12 #IH #f2 #H12 +[ elim (sdj_inv_nx … H12) -H12 [2,3: // ] + #g2 #H #H2 destruct /3 width=1 by lexs_push/ +| elim (sdj_inv_px … H12) -H12 [2,4: // ] * + #g2 #H #H2 destruct /3 width=1 by lexs_next, lexs_push/ +] +qed-. + +lemma sle_lexs_trans: ∀RN,RP. RN ⊆ RP → ∀f2,L1,L2. L1 ⪤*[RN, RP, f2] L2 → ∀f1. f1 ⊆ f2 → L1 ⪤*[RN, RP, f1] L2. #RN #RP #HR #f2 #L1 #L2 #H elim H -f2 -L1 -L2 // @@ -226,7 +233,7 @@ lemma sle_lexs_trans: ∀RN,RP. (∀L,I1,I2. RN L I1 I2 → RP L I1 I2) → ] qed-. -lemma sle_lexs_conf: ∀RN,RP. (∀L,I1,I2. RP L I1 I2 → RN L I1 I2) → +lemma sle_lexs_conf: ∀RN,RP. RP ⊆ RN → ∀f1,L1,L2. L1 ⪤*[RN, RP, f1] L2 → ∀f2. f1 ⊆ f2 → L1 ⪤*[RN, RP, f2] L2. #RN #RP #HR #f1 #L1 #L2 #H elim H -f1 -L1 -L2 // @@ -239,7 +246,7 @@ lemma sle_lexs_conf: ∀RN,RP. (∀L,I1,I2. RP L I1 I2 → RN L I1 I2) → ] qed-. -lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. reflexive … (R2 L)) → +lemma lexs_sle_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → ∀f,L1,L2. L1 ⪤*[R1, RP, f] L2 → ∀g. f ⊆ g → ∃∃L. L1 ⪤*[R1, RP, g] L & L ⪤*[R2, cfull, f] L2. #R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 @@ -252,6 +259,19 @@ lemma lexs_sle_split: ∀R1,R2,RP. (∀L. reflexive … (R1 L)) → (∀L. refle ] qed-. +lemma lexs_sdj_split: ∀R1,R2,RP. c_reflexive … R1 → c_reflexive … R2 → + ∀f,L1,L2. L1 ⪤*[R1, RP, f] L2 → ∀g. f ∥ g → + ∃∃L. L1 ⪤*[RP, R1, g] L & L ⪤*[R2, cfull, f] L2. +#R1 #R2 #RP #HR1 #HR2 #f #L1 #L2 #H elim H -f -L1 -L2 +[ /2 width=3 by lexs_atom, ex2_intro/ ] +#f #I1 #I2 #L1 #L2 #_ #HI12 #IH #y #H +[ elim (sdj_inv_nx … H ??) -H [ |*: // ] #g #Hfg #H destruct + elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/ +| elim (sdj_inv_px … H ??) -H [1,3: * |*: // ] #g #Hfg #H destruct + elim (IH … Hfg) -IH -Hfg /3 width=5 by lexs_next, lexs_push, ex2_intro/ +] +qed-. + lemma lexs_dec: ∀RN,RP. (∀L,I1,I2. Decidable (RN L I1 I2)) → (∀L,I1,I2. Decidable (RP L I1 I2)) → diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma index e68f1109d..46a31fe94 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_tc.ma @@ -19,32 +19,32 @@ include "basic_2/relocation/lexs.ma". (* Properties with transitive closure ***************************************) -lemma lexs_tc_refl: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +lemma lexs_tc_refl: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f. reflexive … (TC … (lexs RN RP f)). /3 width=1 by lexs_refl, TC_reflexive/ qed. -lemma lexs_tc_next_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → +lemma lexs_tc_next_sn: ∀RN,RP. c_reflexive … RN → ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RN L1 I1 I2 → TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRN #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 /3 width=3 by lexs_next, TC_strap, inj/ qed. -lemma lexs_tc_next_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +lemma lexs_tc_next_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 → TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 /4 width=5 by lexs_refl, lexs_next, step, inj/ qed. -lemma lexs_tc_push_sn: ∀RN,RP. (∀L. reflexive … (RP L)) → +lemma lexs_tc_push_sn: ∀RN,RP. c_reflexive … RP → ∀f,I2,L1,L2. TC … (lexs RN RP f) L1 L2 → ∀I1. RP L1 I1 I2 → TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRP #f #I2 #L1 #L2 #H @(TC_ind_dx ??????? H) -L1 /3 width=3 by lexs_push, TC_strap, inj/ qed. -lemma lexs_tc_push_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +lemma lexs_tc_push_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. L1 ⪤*[RN, RP, f] L2 → TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 @@ -63,14 +63,14 @@ qed. (* Main properties with transitive closure **********************************) -theorem lexs_tc_next: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +theorem lexs_tc_next: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,I1,I2,L1. (LTC … RN) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 → TC … (lexs RN RP (⫯f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 /4 width=5 by lexs_tc_next_sn, lexs_tc_refl, trans_TC/ qed. -theorem lexs_tc_push: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +theorem lexs_tc_push: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,I1,I2,L1. (LTC … RP) L1 I1 I2 → ∀L2. TC … (lexs RN RP f) L1 L2 → TC … (lexs RN RP (↑f)) (L1.ⓘ{I1}) (L2.ⓘ{I2}). #RN #RP #HRN #HRP #f #I1 #I2 #L1 #H elim H -I2 @@ -104,14 +104,14 @@ qed. (* Advanced inversion lemmas ************************************************) -lemma lexs_inv_tc_sn: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +lemma lexs_inv_tc_sn: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,L1,L2. L1 ⪤*[LTC … RN, RP, f] L2 → TC … (lexs RN RP f) L1 L2. #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by lexs_tc_next, lexs_tc_push_sn, lexs_atom, inj/ qed-. (* Basic_2A1: uses: lpx_sn_LTC_TC_lpx_sn *) -lemma lexs_inv_tc_dx: ∀RN,RP. (∀L. reflexive … (RN L)) → (∀L. reflexive … (RP L)) → +lemma lexs_inv_tc_dx: ∀RN,RP. c_reflexive … RN → c_reflexive … RP → ∀f,L1,L2. L1 ⪤*[RN, LTC … RP, f] L2 → TC … (lexs RN RP f) L1 L2. #RN #RP #HRN #HRP #f #L1 #L2 #H elim H -f -L1 -L2 /2 width=1 by lexs_tc_push, lexs_tc_next_sn, lexs_atom, inj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma index 78320e1b1..c39dd5bbc 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma @@ -19,7 +19,6 @@ include "basic_2/static/lfdeq.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: uses: lleq_refl *) lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T). /2 width=1 by lfxs_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma new file mode 100644 index 000000000..92479a038 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fqup.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfxs_fqup.ma". +include "basic_2/static/lfeq.ma". + +(* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was: lleq_refl *) +lemma lfeq_refl: ∀T. reflexive … (lfeq T). +/2 width=1 by lfxs_refl/ 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 7d4282e13..7737099cc 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 @@ -3,8 +3,8 @@ name "basic_2_src" table { class "gray" [ { "component" * } { - [ { "plane" * } { - [ "files" * ] + [ { "section" * } { + [ [ "plane" ] "files" * ] } ] } @@ -13,7 +13,7 @@ table { class "wine" [ { "" * } { [ { "" * } { - [ "" * ] + [ [ "" ] "" * ] } ] } @@ -21,7 +21,7 @@ table { (* [ { "higher order dynamic typing" * } { [ { "higher order native type assignment" * } { - [ "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] + [ [ "" ] "ntas ( ⦃?,?⦄ ⊢ ? :* ? )" "nta_lift" * ] } ] } @@ -31,21 +31,21 @@ table { [ { "dynamic typing" * } { (* [ { "local env. ref. for native type assignment" * } { - [ "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ] + [ [ "" ] "lsubn ( ? ⊢ ? :⫃ ? )" "lsubn_drop" "lsubn_cpcs" "lsubn_nta" * ] } ] [ { "native type assignment" * } { - [ "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ] + [ [ "" ] "nta ( ⦃?,?⦄ ⊢ ? : ? )" "nta_alt ( ⦃?,?⦄ ⊢ ? :: ? )" "nta_lift" "nta_ltpss" "nta_thin" "nta_aaa" "nta_sta" "nta_ltpr" "nta_nta" * ] } ] *) [ { "local env. ref. for stratified native validity" * } { - [ "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] + [ [ "" ] "lsubsv ( ? ⊢ ? ⫃¡[?,?] ? )" "lsubsv_lsuba" + "lsubsv_lsubd" + "lsubsv_lstas" + "lsubsv_scpds" + "lsubsv_cpcs" + "lsubsv_snv" * ] } ] [ { "stratified native validity" * } { - [ "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] - [ "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ] + [ [ "" ] "shnv ( ⦃?,?⦄ ⊢ ? ¡[?,?,?] )" * ] + [ [ "" ] "snv ( ⦃?,?⦄ ⊢ ? ¡[?,?] )" "snv_lift" + "snv_aaa" + "snv_da_lpr" + "snv_lstas" + "snv_lstas_lpr" + "snv_lpr" + "snv_fsb" + "snv_scpes" + "snv_preserve" * ] } ] } @@ -53,11 +53,11 @@ table { class "prune" [ { "equivalence" * } { [ { "decomposed rt-equivalence" * } { - [ "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] + [ [ "" ] "scpes ( ⦃?,?⦄ ⊢ ? •*⬌*[?,?,?,?] ? )" "scpes_aaa" + "scpes_cpcs" + "scpes_scpes" * ] } ] [ { "context-sensitive equivalence" * } { - [ "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ] + [ [ "" ] "cpcs ( ⦃?,?⦄ ⊢ ? ⬌* ? )" "cpcs_aaa" + "cpcs_cprs" + "cpcs_cpcs" * ] } ] } @@ -65,8 +65,8 @@ table { *) class "blue" [ { "rt-conversion" * } { - [ { "context-sensitive r-conversion" * } { - [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] + [ { "context-sensitive parallel r-conversion" * } { + [ [ "for terms" ] "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] } ] } @@ -75,71 +75,74 @@ table { [ { "rt-computation" * } { (* [ { "evaluation for context-sensitive rt-reduction" * } { - [ "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] + [ [ "" ] "cpxe ( ⦃?,?⦄ ⊢ ➡*[?,?] 𝐍⦃?⦄ )" * ] } ] [ { "evaluation for context-sensitive reduction" * } { - [ "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] + [ [ "" ] "cpre ( ⦃?,?⦄ ⊢ ➡* 𝐍⦃?⦄ )" "cpre_cpre" * ] } ] [ { "strongly normalizing qrst-computation" * } { - [ "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ] + [ [ "" ] "fsb ( ⦥[?,?] ⦃?,?,?⦄ )" "fsb_alt ( ⦥⦥[?,?] ⦃?,?,?⦄ )" "fsb_aaa" + "fsb_csx" * ] } ] [ { "strongly normalizing rt-computation" * } { - [ "llsx_csx" * ] - [ "csx_fpbs" * ] + [ [ "" ] "llsx_csx" * ] + [ [ "" ] "csx_fpbs" * ] } ] [ { "parallel qrst-computation" * } { - [ "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] - [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ] + [ [ "" ] "fpbg ( ⦃?,?,?⦄ >≛[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fleq" + "fpbg_fpbs" + "fpbg_fpbg" * ] + [ [ "" ] "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_aaa" + "fpbs_fpb" + "fpbs_fpbs" * ] } ] [ { "decomposed rt-computation" * } { - [ "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ] + [ [ "" ] "scpds ( ⦃?,?⦄ ⊢ ? •*➡*[?,?,?] ? )" "scpds_lift" + "scpds_aaa" + "scpds_scpds" * ] } ] [ { "context-sensitive computation" * } { - [ "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ] - [ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] + [ [ "" ] "lprs ( ⦃?,?⦄ ⊢ ➡* ? )" "lprs_drop" + "lprs_cprs" + "lprs_lprs" * ] + [ [ "" ] "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ] } ] *) - [ { "uncounted context-sensitive rt-computation" * } { - [ "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] - [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] - [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] - [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] - [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] + [ { "uncounted context-sensitive parallel rt-computation" * } { + [ [ "refinement for lenvs" ] "lsubsx ( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] + [ [ "strongly normalizing on referred entries for lenvs" ] "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] + [ [ "strongly normalizing for term vectors" ] "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] + [ [ "strongly normalizing for terms" ] "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] + [ [ "on referred entries for lenvs" ] "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] + [ [ "for terms" ] "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] } ] class "cyan" [ { "rt-transition" * } { - [ { "uncounted rst-transition" * } { - [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] + [ { "uncounted parallel rst-transition" * } { + [ [ "for closures" ] "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] + [ [ "proper for closures" ] "fpb ( ⦃?,?,?⦄ ≻[?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] - [ { "t-bound context-sensitive rt-transition" * } { - [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] - [ "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] - [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] - [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] + [ { "context-sensitive parallel r-transition" * } { + [ [ "for lenvs on referred entries" ] "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ [ "for binders" ] "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] + [ [ "for terms" ] "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] } ] - [ { "uncounted context-sensitive rt-transition" * } { - [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] - [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] + [ { "t-bound context-sensitive parallel rt-transition" * } { + [ [ "for terms" ] "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] } ] - [ { "counted context-sensitive rt-transition" * } { - [ "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] + [ { "uncounted context-sensitive parallel rt-transition" * } { + [ [ "normal form for terms" ] "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] + [ [ "for lenvs on referred entries" ] "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] + [ [ "for binders" ] "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] + [ [ "for terms" ] "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] + } + ] + [ { "counted context-sensitive parallel rt-transition" * } { + [ [ "for terms" ] "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] } ] } @@ -147,7 +150,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated extension on referred entries" * } { - [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] + [ [ "" ] "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_drops" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] } @@ -155,35 +158,36 @@ table { class "green" [ { "static typing" * } { [ { "generic reducibility" * } { - [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] - [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] - [ "gcp" *] + [ [ "" ] "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ] + [ [ "" ] "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ] + [ [ "" ] "gcp" *] } ] [ { "atomic arity assignment" * } { - [ "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] - [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] + [ [ "" ] "lsuba ( ? ⊢ ? ⫃⁝ ? )" "lsuba_drops" + "lsuba_lsubr" + "lsuba_aaa" + "lsuba_lsuba" * ] + [ [ "" ] "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfdeq" + "aaa_aaa" * ] } ] [ { "degree-based equivalence on referred entries" * } { - [ "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] - [ "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] + [ [ "" ] "ffdeq ( ⦃?,?,?⦄ ≛[?,?] ⦃?,?,?⦄ )" "ffdeq_fqup" + "ffdeq_ffdeq" * ] + [ [ "" ] "lfdeq ( ? ≛[?,?,?] ? )" "lfdeq_length" + "lfdeq_drops" + "lfdeq_fqup" + "lfdeq_fqus" + "lfdeq_lfdeq" * ] } ] [ { "syntactic equivalence on referred entries" * } { - [ "lfeq ( ? ≡[?] ? )" * ] + [ [ "" ] "lfeq ( ? ≡[?] ? )" "lfeq_fqup" * ] } + ] [ { "generic extension on referred entries" * } { - [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] + [ [ "" ] "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ] } ] [ { "context-sensitive free variables" * } { - [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] - [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] + [ [ "" ] "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_lsubr" + "lsubf_frees" + "lsubf_lsubf" * ] + [ [ "" ] "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_drops" + "frees_fqup" + "frees_frees" * ] } ] [ { "restricted ref. for local env." * } { - [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] + [ [ "" ] "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ] } ] } @@ -191,8 +195,8 @@ table { class "grass" [ { "s-computation" * } { [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] - [ "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] + [ [ "" ] "fqus ( ⦃?,?,?⦄ ⊐*[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐* ⦃?,?,?⦄ )" "fqus_weight" + "fqus_drops" + "fqus_fqup" + "fqus_fqus" * ] + [ [ "" ] "fqup ( ⦃?,?,?⦄ ⊐+[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐+ ⦃?,?,?⦄ )" "fqup_weight" + "fqup_drops" + "fqup_fqup" * ] } ] } @@ -200,8 +204,8 @@ table { class "yellow" [ { "s-transition" * } { [ { "structural successor for closures" * } { - [ "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] - [ "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] + [ [ "" ] "fquq ( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ] + [ [ "" ] "fqu ( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ ) ( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ] } ] } @@ -209,23 +213,23 @@ table { class "orange" [ { "relocation" * } { [ { "generic slicing for local environments" * } { - [ "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ] - [ "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] + [ [ "" ] "drops_vector ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" * ] + [ [ "" ] "drops ( ⬇*[?,?] ? ≡ ? ) ( ⬇*[?] ? ≡ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" * ] } ] [ { "generic relocation" * } { - [ "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] - [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] - [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] + [ [ "" ] "lifts_bind ( ⬆*[?] ? ≡ ? )" "lifts_weight_bind" + "lifts_lifts_bind" * ] + [ [ "" ] "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] + [ [ "" ] "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] } ] [ { "ranged equivalence for local environments" * } { - [ "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] + [ [ "" ] "lreq ( ? ≡[?] ? )" "lreq_length" + "lreq_lreq" * ] } ] [ { "generic entrywise extension" * } { - [ "lex ( ? ⦻[?] ? )" * ] - [ "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] + [ [ "" ] "lex ( ? ⦻[?] ? )" * ] + [ [ "" ] "lexs ( ? ⦻*[?,?,?] ? )" "lexs_tc" + "lexs_length" + "lexs_lexs" * ] } ] } @@ -233,55 +237,55 @@ table { class "red" [ { "syntax" * } { [ { "append for local environments" * } { - [ "append ( ? @@ ? )" "append_length" * ] + [ [ "" ] "append ( ? @@ ? )" "append_length" * ] } ] [ { "head equivalence for terms" * } { - [ "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] + [ [ "" ] "theq ( ? ⩳[?,?] ? )" "theq_simple" + "theq_tdeq" + "theq_theq" + "theq_simple_vector" * ] } ] [ { "degree-based equivalence" * } { - [ "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ] - [ "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ] + [ [ "" ] "tdeq_ext ( ? ≛[?,?] ? ) ( ? ⊢ ? ≛[?,?] ? )" * ] + [ [ "" ] "tdeq ( ? ≛[?,?] ? )" "tdeq_tdeq" * ] } ] [ { "closures" * } { - [ "cl_weight ( ♯{?,?,?} )" * ] - [ "cl_restricted_weight ( ♯{?,?} )" * ] + [ [ "" ] "cl_weight ( ♯{?,?,?} )" * ] + [ [ "" ] "cl_restricted_weight ( ♯{?,?} )" * ] } ] [ { "global environments" * } { - [ "genv" * ] + [ [ "" ] "genv" * ] } ] [ { "local environments" * } { - [ "ceq_ext" "ceq_ext_ceq_ext" * ] - [ "cext2" * ] - [ "lenv_length ( |?| )" * ] - [ "lenv_weight ( ♯{?} )" * ] - [ "lenv" * ] + [ [ "" ] "ceq_ext" "ceq_ext_ceq_ext" * ] + [ [ "" ] "cext2" * ] + [ [ "" ] "lenv_length ( |?| )" * ] + [ [ "" ] "lenv_weight ( ♯{?} )" * ] + [ [ "" ] "lenv" * ] } ] [ { "binders for local environments" * } { - [ "ext2" "ext2_tc" + "ext2_ext2" * ] - [ "bind" "bind_weight" * ] + [ [ "" ] "ext2" "ext2_tc" + "ext2_ext2" * ] + [ [ "" ] "bind" "bind_weight" * ] } ] [ { "terms" * } { - [ "term_vector ( Ⓐ?.? )" * ] - [ "term_simple ( 𝐒⦃?⦄ )" * ] - [ "term_weight ( ♯{?} )" * ] - [ "term" * ] + [ [ "" ] "term_vector ( Ⓐ?.? )" * ] + [ [ "" ] "term_simple ( 𝐒⦃?⦄ )" * ] + [ [ "" ] "term_weight ( ♯{?} )" * ] + [ [ "" ] "term" * ] } ] [ { "items" * } { - [ "item_sd" * ] - [ "item_sh" * ] - [ "item" * ] + [ [ "" ] "item_sd" * ] + [ [ "" ] "item_sh" * ] + [ [ "" ] "item" * ] } ] [ { "atomic arities" * } { - [ "aarity" * ] + [ [ "" ] "aarity" * ] } ] } @@ -290,78 +294,78 @@ table { class "top" { * } -class "capitalize italic" { 0 } +class "capitalize italic" { 0 1 } -class "italic" { 1 } +class "italic" { 2 } (* [ { "normal forms for context-sensitive rt-reduction" * } { - [ "cnx_crx" + "cnx_cix" * ] + [ [ "" ] "cnx_crx" + "cnx_cix" * ] } ] [ { "irreducible forms for context-sensitive rt-reduction" * } { - [ "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ] + [ [ "" ] "cix ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐈⦃?⦄ )" "cix_lift" * ] } ] [ { "reducible forms for context-sensitive rt-reduction" * } { - [ "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ] + [ [ "" ] "crx ( ⦃?,?⦄ ⊢ ➡[?,?] 𝐑⦃?⦄ )" "crx_lift" * ] } ] [ { "normal forms for context-sensitive reduction" * } { - [ "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] + [ [ "" ] "cnr ( ⦃?,?⦄ ⊢ ➡ 𝐍⦃?⦄ )" "cnr_lift" + "cnr_crr" + "cnr_cir" * ] } ] [ { "irreducible forms for context-sensitive reduction" * } { - [ "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ] + [ [ "" ] "cir ( ⦃?,?⦄ ⊢ ➡ 𝐈⦃?⦄ )" "cir_lift" * ] } ] [ { "reducible forms for context-sensitive reduction" * } { - [ "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ] + [ [ "" ] "crr ( ⦃?,?⦄ ⊢ ➡ 𝐑⦃?⦄ )" "crr_lift" * ] } ] [ { "unfold" * } { - [ "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ] + [ [ "" ] "unfold ( ⦃?,?⦄ ⊢ ? ⧫* ? )" * ] } ] [ { "iterated static type assignment" * } { - [ "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ] + [ [ "" ] "lstas ( ⦃?,?⦄ ⊢ ? •*[?,?] ? )" "lstas_lift" + "lstas_llpx_sn.ma" + "lstas_aaa" + "lstas_da" + "lstas_lstas" * ] } ] [ { "local env. ref. for degree assignment" * } { - [ "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ] + [ [ "" ] "lsubd ( ? ⊢ ? ⫃▪[?,?] ? )" "lsubd_da" + "lsubd_lsubd" * ] } ] [ { "degree assignment" * } { - [ "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ] + [ [ "" ] "da ( ⦃?,?⦄ ⊢ ? ▪[?,?] ? )" "da_lift" + "da_aaa" + "da_da" * ] } ] [ { "context-sensitive multiple rt-substitution" * } { - [ "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] + [ [ "" ] "cpys ( ⦃?,?⦄ ⊢ ? ▶*[?,?] ? )" "cpys_alt ( ⦃?,?⦄ ⊢ ? ▶▶*[?,?] ? )" "cpys_lift" + "cpys_cpys" * ] } ] [ { "pointwise union for local environments" * } { - [ "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ] + [ [ "" ] "llor ( ? ⋓[?,?] ? ≡ ? )" "llor_alt" + "llor_drop" * ] } ] [ { "lazy pointwise extension of a relation" * } { - [ "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ] + [ [ "" ] "llpx_sn" "llpx_sn_alt" + "llpx_sn_alt_rec" + "llpx_sn_tc" + "llpx_sn_lreq" + "llpx_sn_drop" + "llpx_sn_lpx_sn" + "llpx_sn_frees" + "llpx_sn_llor" * ] } ] [ { "global env. slicing" * } { - [ "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ] + [ [ "" ] "gget ( ⬇[?] ? ≡ ? )" "gget_gget" * ] } ] [ { "context-sensitive ordinary rt-substitution" * } { - [ "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ] + [ [ "" ] "cpy ( ⦃?,?⦄ ⊢ ? ▶[?,?] ? )" "cpy_lift" + "cpy_nlift" + "cpy_cpy" * ] } ] [ { "local env. ref. for rt-substitution" * } { - [ "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] + [ [ "" ] "lsuby ( ? ⊆[?,?] ? )" "lsuby_lsuby" * ] } ] [ { "pointwise extension of a relation" * } { - [ "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] + [ [ "" ] "lpx_sn" "lpx_sn_alt" + "lpx_sn_drop" + "lpx_sn_lpx_sn" * ] } ] - [ "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ] - [ "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] + [ [ "" ] "cpx_lreq" + "cpr_cir" + "fpb_lift" + "fpbq_lift" ] + [ [ "" ] "lleq ( ? ≡[?,?] ? )" "lleq_alt" + "lleq_alt_rec" + "lleq_lreq" + "lleq_drop" + "lleq_fqus" + "lleq_llor" + "lleq_lleq" * ] *) diff --git a/matita/matita/contribs/lambdadelta/partial_compile.sh b/matita/matita/contribs/lambdadelta/compile_partial.sh similarity index 100% rename from matita/matita/contribs/lambdadelta/partial_compile.sh rename to matita/matita/contribs/lambdadelta/compile_partial.sh diff --git a/matita/matita/contribs/lambdadelta/compile_static.sh b/matita/matita/contribs/lambdadelta/compile_static.sh new file mode 100644 index 000000000..827c52e18 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/compile_static.sh @@ -0,0 +1 @@ +../../matitac.opt `cat static.txt` diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma index e62b1fcda..86be38640 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma @@ -17,14 +17,32 @@ include "ground_2/xoa/xoa_props.ma". (* GENERIC RELATIONS ********************************************************) -(* PROPERTIES OF RELATIONS **************************************************) +(* Inclusion ****************************************************************) -definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝ + λR1,R2. (∀a1,a2. R1 a1 a2 → R2 a1 a2). + +interpretation "2-relation inclusion" + 'subseteq R1 R2 = (subR2 ?? R1 R2). + +definition subR3 (S1) (S2) (S3): relation (relation3 S1 S2 S3) ≝ + λR1,R2. (∀a1,a2,a3. R1 a1 a2 a3 → R2 a1 a2 a3). + +interpretation "3-relation inclusion" + 'subseteq R1 R2 = (subR3 ??? R1 R2). + +(* Properties of relations **************************************************) + +definition relation5: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ λA,B,C,D,E.A→B→C→D→E→Prop. -definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +definition relation6: Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] ≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. +(**) (* we dont use "∀a. reflexive … (R a)" since auto seems to dislike repeatd δ-expansion *) +definition c_reflexive (A) (B): predicate (relation3 A B B) ≝ + λR. ∀a,b. R a b b. + definition Decidable: Prop → Prop ≝ λR. R ∨ (R → ⊥). definition Transitive: ∀A. ∀R: relation A. Prop ≝ λA,R. @@ -47,9 +65,9 @@ definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & R1 a a2. -definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. - ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → - ∃∃a,b. R a1 b1 a b & R a2 b2 a b. +definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. + ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → + ∃∃a,b. R a1 b1 a b & R a2 b2 a b. definition lsub_trans: ∀A,B. relation2 (A→relation B) (relation A) ≝ λA,B,R1,R2. ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 L1 L2 → R1 L1 T1 T2. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/relations/parallel_2.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/parallel_2.ma new file mode 100644 index 000000000..dbbc88185 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/relations/parallel_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation "hvbox( f1 ∥ break term 46 f2 )" + non associative with precedence 45 + for @{ 'Parallel $f1 $f2 }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma new file mode 100644 index 000000000..99c6915db --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sdj.ma @@ -0,0 +1,146 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.tcs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/notation/relations/parallel_2.ma". +include "ground_2/relocation/rtmap_isid.ma". + +(* RELOCATION MAP ***********************************************************) + +coinductive sdj: relation rtmap ≝ +| sdj_pp: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ↑f2 = g2 → sdj g1 g2 +| sdj_np: ∀f1,f2,g1,g2. sdj f1 f2 → ⫯f1 = g1 → ↑f2 = g2 → sdj g1 g2 +| sdj_pn: ∀f1,f2,g1,g2. sdj f1 f2 → ↑f1 = g1 → ⫯f2 = g2 → sdj g1 g2 +. + +interpretation "disjointness (rtmap)" + 'Parallel f1 f2 = (sdj f1 f2). + +(* Basic properties *********************************************************) + +axiom sdj_eq_repl_back1: ∀f2. eq_repl_back … (λf1. f1 ∥ f2). + +lemma sdj_eq_repl_fwd1: ∀f2. eq_repl_fwd … (λf1. f1 ∥ f2). +#f2 @eq_repl_sym /2 width=3 by sdj_eq_repl_back1/ +qed-. + +axiom sdj_eq_repl_back2: ∀f1. eq_repl_back … (λf2. f1 ∥ f2). + +lemma sdj_eq_repl_fwd2: ∀f1. eq_repl_fwd … (λf2. f1 ∥ f2). +#f1 @eq_repl_sym /2 width=3 by sdj_eq_repl_back2/ +qed-. + +corec lemma sdj_sym: symmetric … sdj. +#f1 #f2 * -f1 -f2 +#f1 #f2 #g1 #g2 #Hf #H1 #H2 +[ @(sdj_pp … H2 H1) | @(sdj_pn … H2 H1) | @(sdj_np … H2 H1) ] -g2 -g1 +/2 width=1 by/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma sdj_inv_pp: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 → f1 ∥ f2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct +[ lapply (injective_push … Hx1) -Hx1 + lapply (injective_push … Hx2) -Hx2 // +| elim (discr_push_next … Hx1) +| elim (discr_push_next … Hx2) +] +qed-. + +lemma sdj_inv_np: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ↑f2 = g2 → f1 ∥ f2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct +[ elim (discr_next_push … Hx1) +| lapply (injective_next … Hx1) -Hx1 + lapply (injective_push … Hx2) -Hx2 // +| elim (discr_push_next … Hx2) +] +qed-. + +lemma sdj_inv_pn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 → f1 ∥ f2. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct +[ elim (discr_next_push … Hx2) +| elim (discr_push_next … Hx1) +| lapply (injective_push … Hx1) -Hx1 + lapply (injective_next … Hx2) -Hx2 // +] +qed-. + +lemma sdj_inv_nn: ∀g1,g2. g1 ∥ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → ⊥. +#g1 #g2 * -g1 -g2 +#f1 #f2 #g1 #g2 #H #H1 #H2 #x1 #x2 #Hx1 #Hx2 destruct +[ elim (discr_next_push … Hx1) +| elim (discr_next_push … Hx2) +| elim (discr_next_push … Hx1) +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma sdj_inv_nx: ∀g1,g2. g1 ∥ g2 → ∀f1. ⫯f1 = g1 → + ∃∃f2. f1 ∥ f2 & ↑f2 = g2. +#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1 +[ lapply (sdj_inv_np … H … H1 H2) -H /2 width=3 by ex2_intro/ +| elim (sdj_inv_nn … H … H1 H2) +] +qed-. + +lemma sdj_inv_xn: ∀g1,g2. g1 ∥ g2 → ∀f2. ⫯f2 = g2 → + ∃∃f1. f1 ∥ f2 & ↑f1 = g1. +#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2 +[ lapply (sdj_inv_pn … H … H1 H2) -H /2 width=3 by ex2_intro/ +| elim (sdj_inv_nn … H … H1 H2) +] +qed-. + +lemma sdj_inv_xp: ∀g1,g2. g1 ∥ g2 → ∀f2. ↑f2 = g2 → + ∨∨ ∃∃f1. f1 ∥ f2 & ↑f1 = g1 + | ∃∃f1. f1 ∥ f2 & ⫯f1 = g1. +#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2 +[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_np … H … H1 H2) ] -H -H2 +/3 width=3 by ex2_intro, or_introl, or_intror/ +qed-. + +lemma sdj_inv_px: ∀g1,g2. g1 ∥ g2 → ∀f1. ↑f1 = g1 → + ∨∨ ∃∃f2. f1 ∥ f2 & ↑f2 = g2 + | ∃∃f2. f1 ∥ f2 & ⫯f2 = g2. +#g1 #g2 elim (pn_split g2) * #f2 #H2 #H #f1 #H1 +[ lapply (sdj_inv_pp … H … H1 H2) | lapply (sdj_inv_pn … H … H1 H2) ] -H -H1 +/3 width=3 by ex2_intro, or_introl, or_intror/ +qed-. + +(* Properties with isid *****************************************************) + +corec lemma sdj_isid_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ∥ f2. +#f2 * -f2 +#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * +/3 width=5 by sdj_np, sdj_pp/ +qed. + +corec lemma sdj_isid_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ∥ f2. +#f1 * -f1 +#f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * +/3 width=5 by sdj_pn, sdj_pp/ +qed. + +(* Inversion lemmas with isid ***********************************************) + +corec lemma sdj_inv_refl: ∀f. f ∥ f → 𝐈⦃f⦄. +#f cases (pn_split f) * #g #Hg #H +[ lapply (sdj_inv_pp … H … Hg Hg) -H /3 width=3 by isid_push/ +| elim (sdj_inv_nn … H … Hg Hg) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma index 120902ce5..c357babf9 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma @@ -24,7 +24,7 @@ coinductive sle: relation rtmap ≝ . interpretation "inclusion (rtmap)" - 'subseteq t1 t2 = (sle t1 t2). + 'subseteq f1 f2 = (sle f1 f2). (* Basic properties *********************************************************) @@ -83,7 +83,7 @@ lemma sle_inv_pp: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 #x1 #H #Hx1 destruct lapply (injective_push … Hx1) -Hx1 // qed-. -lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2. +lemma sle_inv_nn: ∀g1,g2. g1 ⊆ g2 → ∀f1,f2. ⫯f1 = g1 → ⫯f2 = g2 → f1 ⊆ f2. #g1 #g2 #H #f1 #f2 #H1 #H2 elim (sle_inv_nx … H … H1) -g1 #x2 #H #Hx2 destruct lapply (injective_next … Hx2) -Hx2 // qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index a90603dd0..b42fb82e4 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -23,11 +23,11 @@ table { [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_pushs ( ↑*[?]? )" "rtmap_nexts ( ⫯*[?]? )" "rtmap_tl ( ⫱? )" "rtmap_tls ( ⫱*[?]? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_isdiv ( 𝛀⦃?⦄ )" "rtmap_fcla ( 𝐂⦃?⦄ ≡ ? )" "rtmap_isfin ( 𝐅⦃?⦄ )" "rtmap_isuni ( 𝐔⦃?⦄ )" "rtmap_uni ( 𝐔❴?❵ )" - "rtmap_sle ( ? ⊆ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" + "rtmap_sle ( ? ⊆ ? )" "rtmap_sdj ( ? ∥ ? )" "rtmap_sand ( ? ⋒ ? ≡ ? )" "rtmap_sor ( ? ⋓ ? ≡ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" "rtmap_coafter ( ? ~⊚ ? ≡ ? )" * ] [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "" "" "" "" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "" - "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" + "" "" "" "" "" "" "" "nstream_sor" "" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )" * ] (* [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" @@ -55,7 +55,7 @@ table { [ "stream ( ? @ ? )" "stream_eq ( ? ≐ ? )" "stream_hdtl ( ↓? )" "stream_tls ( ↓*[?]? )" * ] [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ⫯? ) ( ⫰? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] - [ "relations" "star" "lstar" * ] + [ "relations ( ? ⊆ ? )" "star" "lstar" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/static.txt b/matita/matita/contribs/lambdadelta/static.txt new file mode 100644 index 000000000..7596031ba --- /dev/null +++ b/matita/matita/contribs/lambdadelta/static.txt @@ -0,0 +1,7 @@ +ground_2 +basic_2/syntax +basic_2/relocation +basic_2/s_transition +basic_2/s_computation +basic_2/static +basic_2/i_static -- 2.39.2